[Merged by Bors] - chore(LinearAlgebra): golf `of_mem_specialOrthogonalGroup_fin_two_iff` using `grind` #30516

euprunin · 2025-10-13T18:01:03Z

Show trace profiling of of_mem_specialOrthogonalGroup_fin_two_iff: 544 ms before, 246 ms after 🎉

Trace profiling of `of_mem_specialOrthogonalGroup_fin_two_iff` before PR 30516

diff --git a/Mathlib/LinearAlgebra/UnitaryGroup.lean b/Mathlib/LinearAlgebra/UnitaryGroup.lean
index 3a082442ee..52e8d7c6fb 100644
--- a/Mathlib/LinearAlgebra/UnitaryGroup.lean
+++ b/Mathlib/LinearAlgebra/UnitaryGroup.lean
@@ -276,6 +276,7 @@ theorem mem_specialOrthogonalGroup_iff :
     A ∈ specialOrthogonalGroup n R ↔ A ∈ orthogonalGroup n R ∧ A.det = 1 :=
   Iff.rfl
 
+set_option trace.profiler true in
 @[simp]
 lemma of_mem_specialOrthogonalGroup_fin_two_iff {a b c d : R} :
     !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔

ℹ [1583/1583] Built Mathlib.LinearAlgebra.UnitaryGroup (7.2s)
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:280:0: [Elab.command] [0.029996] @[simp]
    theorem of_mem_specialOrthogonalGroup_fin_two_iff {a b c d : R} :
        !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1 :=
      by
      trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
      ·
        simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
          Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
      refine ⟨?_, ?_⟩
      · rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
        refine ⟨?_, ?_, ?_⟩
        · linear_combination -a * h₂ + c * h₁ + d * h₃
        · linear_combination -c * h₀ + a * h₁ - b * h₃
        · linear_combination h₀
      · rintro ⟨rfl, rfl, H⟩
        ring_nf at H ⊢
        tauto
  [Elab.definition.header] [0.026545] Matrix.of_mem_specialOrthogonalGroup_fin_two_iff
    [Elab.step] [0.023993] expected type: Prop, term
        !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1
      [Elab.step] [0.023984] expected type: Prop, term
          Iff✝ (!![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R) (a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1)
        [Elab.step] [0.016843] expected type: Prop, term
            !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R
          [Elab.step] [0.016834] expected type: Prop, term
              Membership.mem✝ (Matrix.specialOrthogonalGroup (Fin 2) R) !![a, b; c, d]
            [Elab.step] [0.013772] expected type: Matrix (Fin 2) (Fin 2) R, term
                !![a, b; c, d]
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:280:0: [Elab.command] [0.030286] @[simp]
    lemma of_mem_specialOrthogonalGroup_fin_two_iff {a b c d : R} :
        !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1 :=
      by
      trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
      ·
        simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
          Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
      refine ⟨?_, ?_⟩
      · rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
        refine ⟨?_, ?_, ?_⟩
        · linear_combination -a * h₂ + c * h₁ + d * h₃
        · linear_combination -c * h₀ + a * h₁ - b * h₃
        · linear_combination h₀
      · rintro ⟨rfl, rfl, H⟩
        ring_nf at H ⊢
        tauto
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:280:0: [Elab.async] [0.555585] elaborating proof of Matrix.of_mem_specialOrthogonalGroup_fin_two_iff
  [Elab.definition.value] [0.543691] Matrix.of_mem_specialOrthogonalGroup_fin_two_iff
    [Elab.step] [0.536332] 
          trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
          ·
            simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
              Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
          refine ⟨?_, ?_⟩
          · rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
            refine ⟨?_, ?_, ?_⟩
            · linear_combination -a * h₂ + c * h₁ + d * h₃
            · linear_combination -c * h₀ + a * h₁ - b * h₃
            · linear_combination h₀
          · rintro ⟨rfl, rfl, H⟩
            ring_nf at H ⊢
            tauto
      [Elab.step] [0.536316] 
            trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
            ·
              simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
                Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
            refine ⟨?_, ?_⟩
            · rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
              refine ⟨?_, ?_, ?_⟩
              · linear_combination -a * h₂ + c * h₁ + d * h₃
              · linear_combination -c * h₀ + a * h₁ - b * h₃
              · linear_combination h₀
            · rintro ⟨rfl, rfl, H⟩
              ring_nf at H ⊢
              tauto
        [Elab.step] [0.039138] trans
              ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
          [Elab.step] [0.034711] expected type: Prop, term
              ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
            [Elab.step] [0.034703] expected type: Prop, term
                And✝ ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1)
                  (a * d - b * c = 1)
              [Elab.step] [0.024486] expected type: Prop, term
                  ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1)
                [Elab.step] [0.024473] expected type: Prop, term
                    (a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1
                  [Elab.step] [0.024464] expected type: Prop, term
                      And✝ (a * a + b * b = 1 ∧ a * c + b * d = 0) (c * a + d * b = 0 ∧ c * c + d * d = 1)
                    [Elab.step] [0.013813] expected type: Prop, term
                        (a * a + b * b = 1 ∧ a * c + b * d = 0)
                      [Elab.step] [0.013807] expected type: Prop, term
                          a * a + b * b = 1 ∧ a * c + b * d = 0
                        [Elab.step] [0.013802] expected type: Prop, term
                            And✝ (a * a + b * b = 1) (a * c + b * d = 0)
                          [Elab.step] [0.010148] expected type: Prop, term
                              a * a + b * b = 1
                            [Elab.step] [0.010141] expected type: Prop, term
                                binrel% Eq✝ (a * a + b * b) 1
                    [Elab.step] [0.010560] expected type: Prop, term
                        c * a + d * b = 0 ∧ c * c + d * d = 1
                      [Elab.step] [0.010504] expected type: Prop, term
                          And✝ (c * a + d * b = 0) (c * c + d * d = 1)
              [Elab.step] [0.010150] expected type: Prop, term
                  a * d - b * c = 1
                [Elab.step] [0.010131] expected type: Prop, term
                    binrel% Eq✝ (a * d - b * c) 1
        [Elab.step] [0.256621] ·
              simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
                Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
          [Elab.step] [0.256546] simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
                  ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
            [Elab.step] [0.256541] simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
                    ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
              [Elab.step] [0.256531] simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
                    ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
                [Meta.synthInstance] [0.043407] ❌️ OneHomClass ((Fin 2 → Fin 2 → R) ≃ Matrix (Fin 2) (Fin 2) R)
                      (Fin 2 → Fin 2 → R) (Matrix (Fin 2) (Fin 2) R)
                [Meta.Tactic.simp.discharge] [0.024283] one_apply_ne discharge ✅️
                      0 ≠ Fin.succ 0
                  [Meta.isDefEq] [0.010857] ✅️ 0 = 1 =?= 0 = 1
        [Elab.step] [0.106235] ·
              rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
              refine ⟨?_, ?_, ?_⟩
              · linear_combination -a * h₂ + c * h₁ + d * h₃
              · linear_combination -c * h₀ + a * h₁ - b * h₃
              · linear_combination h₀
          [Elab.step] [0.106116] 
                rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
                refine ⟨?_, ?_, ?_⟩
                · linear_combination -a * h₂ + c * h₁ + d * h₃
                · linear_combination -c * h₀ + a * h₁ - b * h₃
                · linear_combination h₀
            [Elab.step] [0.106109] 
                  rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
                  refine ⟨?_, ?_, ?_⟩
                  · linear_combination -a * h₂ + c * h₁ + d * h₃
                  · linear_combination -c * h₀ + a * h₁ - b * h₃
                  · linear_combination h₀
              [Elab.step] [0.068748] · linear_combination -a * h₂ + c * h₁ + d * h₃
                [Elab.step] [0.068730] linear_combination -a * h₂ + c * h₁ + d * h₃
                  [Elab.step] [0.068725] linear_combination -a * h₂ + c * h₁ + d * h₃
                    [Elab.step] [0.068713] linear_combination -a * h₂ + c * h₁ + d * h₃
              [Elab.step] [0.022145] · linear_combination -c * h₀ + a * h₁ - b * h₃
                [Elab.step] [0.022096] linear_combination -c * h₀ + a * h₁ - b * h₃
                  [Elab.step] [0.022090] linear_combination -c * h₀ + a * h₁ - b * h₃
                    [Elab.step] [0.022079] linear_combination -c * h₀ + a * h₁ - b * h₃
              [Elab.step] [0.014071] · linear_combination h₀
                [Elab.step] [0.014037] linear_combination h₀
                  [Elab.step] [0.014031] linear_combination h₀
                    [Elab.step] [0.014021] linear_combination h₀
        [Elab.step] [0.134040] ·
              rintro ⟨rfl, rfl, H⟩
              ring_nf at H ⊢
              tauto
          [Elab.step] [0.132278] 
                rintro ⟨rfl, rfl, H⟩
                ring_nf at H ⊢
                tauto
            [Elab.step] [0.132271] 
                  rintro ⟨rfl, rfl, H⟩
                  ring_nf at H ⊢
                  tauto
              [Elab.step] [0.114315] ring_nf at H ⊢
              [Elab.step] [0.017045] tauto
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:281:6: [Elab.async] [0.024704] Lean.addDecl
  [Kernel] [0.024673] ✅️ typechecking declarations [Matrix.of_mem_specialOrthogonalGroup_fin_two_iff]
Build completed successfully (1583 jobs).

Trace profiling of `of_mem_specialOrthogonalGroup_fin_two_iff` after PR 30516

diff --git a/Mathlib/LinearAlgebra/UnitaryGroup.lean b/Mathlib/LinearAlgebra/UnitaryGroup.lean
index 3a082442ee..ec636bbe67 100644
--- a/Mathlib/LinearAlgebra/UnitaryGroup.lean
+++ b/Mathlib/LinearAlgebra/UnitaryGroup.lean
@@ -276,6 +276,7 @@ theorem mem_specialOrthogonalGroup_iff :
     A ∈ specialOrthogonalGroup n R ↔ A ∈ orthogonalGroup n R ∧ A.det = 1 :=
   Iff.rfl
 
+set_option trace.profiler true in
 @[simp]
 lemma of_mem_specialOrthogonalGroup_fin_two_iff {a b c d : R} :
     !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔
@@ -284,15 +285,7 @@ lemma of_mem_specialOrthogonalGroup_fin_two_iff {a b c d : R} :
     c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
   · simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
       ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
-  refine ⟨?_, ?_⟩
-  · rintro ⟨⟨⟨h₀, h₁⟩, -, h₂⟩, h₃⟩
-    refine ⟨?_, ?_, ?_⟩
-    · linear_combination - a * h₂ + c * h₁ + d * h₃
-    · linear_combination - c * h₀ + a * h₁ - b * h₃
-    · linear_combination h₀
-  · rintro ⟨rfl, rfl, H⟩
-    ring_nf at H ⊢
-    tauto
+  grind
 
 lemma mem_specialOrthogonalGroup_fin_two_iff {M : Matrix (Fin 2) (Fin 2) R} :
     M ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔

ℹ [1583/1583] Built Mathlib.LinearAlgebra.UnitaryGroup (3.6s)
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:280:0: [Elab.command] [0.018905] @[simp]
    theorem of_mem_specialOrthogonalGroup_fin_two_iff {a b c d : R} :
        !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1 :=
      by
      trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
      ·
        simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
          Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
      grind
  [Elab.definition.header] [0.014189] Matrix.of_mem_specialOrthogonalGroup_fin_two_iff
    [Elab.step] [0.010692] expected type: Prop, term
        !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1
      [Elab.step] [0.010683] expected type: Prop, term
          Iff✝ (!![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R) (a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1)
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:280:0: [Elab.command] [0.023283] @[simp]
    lemma of_mem_specialOrthogonalGroup_fin_two_iff {a b c d : R} :
        !![a, b; c, d] ∈ Matrix.specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1 :=
      by
      trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
      ·
        simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
          Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
      grind
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:280:0: [Elab.async] [0.249360] elaborating proof of Matrix.of_mem_specialOrthogonalGroup_fin_two_iff
  [Elab.definition.value] [0.246201] Matrix.of_mem_specialOrthogonalGroup_fin_two_iff
    [Elab.step] [0.245570] 
          trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
          ·
            simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
              Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
          grind
      [Elab.step] [0.245558] 
            trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
            ·
              simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
                Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
            grind
        [Elab.step] [0.015840] trans
              ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
          [Elab.step] [0.014607] expected type: Prop, term
              ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
            [Elab.step] [0.014600] expected type: Prop, term
                And✝ ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1)
                  (a * d - b * c = 1)
              [Elab.step] [0.011593] expected type: Prop, term
                  ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1)
                [Elab.step] [0.011586] expected type: Prop, term
                    (a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1
                  [Elab.step] [0.011580] expected type: Prop, term
                      And✝ (a * a + b * b = 1 ∧ a * c + b * d = 0) (c * a + d * b = 0 ∧ c * c + d * d = 1)
        [Elab.step] [0.187635] ·
              simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff, ← Matrix.ext_iff,
                Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
          [Elab.step] [0.187554] simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
                  ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
            [Elab.step] [0.187548] simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
                    ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
              [Elab.step] [0.187537] simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
                    ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]
                [Meta.synthInstance] [0.034536] ❌️ OneHomClass ((Fin 2 → Fin 2 → R) ≃ Matrix (Fin 2) (Fin 2) R)
                      (Fin 2 → Fin 2 → R) (Matrix (Fin 2) (Fin 2) R)
                [Meta.Tactic.simp.discharge] [0.012761] one_apply_ne discharge ✅️
                      0 ≠ Fin.succ 0
        [Elab.step] [0.042044] grind
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:288:2: [Elab.async] [0.046294] Lean.addDecl
  [Kernel] [0.046259] ✅️ typechecking declarations [Matrix.of_mem_specialOrthogonalGroup_fin_two_iff._proof_1_5]
info: Mathlib/LinearAlgebra/UnitaryGroup.lean:281:6: [Elab.async] [0.033020] Lean.addDecl
  [Kernel] [0.032990] ✅️ typechecking declarations [Matrix.of_mem_specialOrthogonalGroup_fin_two_iff]
Build completed successfully (1583 jobs).

…` using `grind`

github-actions · 2025-10-13T18:02:09Z

PR summary 7a9e177031

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg

Thanks! What does local profiling say? I'll maintainer merge if that's positive or neutral.

euprunin · 2025-10-14T15:44:57Z

@grunweg Thanks a lot for reviewing. Local profiling says: 544 ms before, 246 ms after 🎉

I've added trace profiling results to the PR description.

grunweg · 2025-10-14T18:06:39Z

Thanks!
maintainer merge

github-actions · 2025-10-14T18:06:57Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

riccardobrasca · 2025-10-14T19:27:10Z

Thanks!

bors merge

…` using `grind` (#30516)

mathlib-bors · 2025-10-14T19:58:13Z

Pull request successfully merged into master.

Build succeeded:

chore(LinearAlgebra): golf `of_mem_specialOrthogonalGroup_fin_two_iff…

e477d92

…` using `grind`

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 13, 2025

grunweg reviewed Oct 14, 2025

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 14, 2025

euprunin removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 14, 2025

leanprover-community-mathlib4-bot added the maintainer-merge label Oct 14, 2025

leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge labels Oct 14, 2025

mathlib-bors bot pushed a commit that referenced this pull request Oct 14, 2025

chore(LinearAlgebra): golf `of_mem_specialOrthogonalGroup_fin_two_iff…

1af1826

…` using `grind` (#30516)

mathlib-bors bot changed the title ~~chore(LinearAlgebra): golf of_mem_specialOrthogonalGroup_fin_two_iff using grind~~ [Merged by Bors] - chore(LinearAlgebra): golf of_mem_specialOrthogonalGroup_fin_two_iff using grind Oct 14, 2025

mathlib-bors bot closed this Oct 14, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Merged by Bors] - chore(LinearAlgebra): golf `of_mem_specialOrthogonalGroup_fin_two_iff` using `grind` #30516

[Merged by Bors] - chore(LinearAlgebra): golf `of_mem_specialOrthogonalGroup_fin_two_iff` using `grind` #30516

Uh oh!

euprunin commented Oct 13, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Oct 13, 2025

Uh oh!

grunweg left a comment

Uh oh!

euprunin commented Oct 14, 2025 •

edited

Loading

Uh oh!

grunweg commented Oct 14, 2025

Uh oh!

github-actions bot commented Oct 14, 2025

Uh oh!

riccardobrasca commented Oct 14, 2025

Uh oh!

mathlib-bors bot commented Oct 14, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

[Merged by Bors] - chore(LinearAlgebra): golf of_mem_specialOrthogonalGroup_fin_two_iff using grind #30516

[Merged by Bors] - chore(LinearAlgebra): golf of_mem_specialOrthogonalGroup_fin_two_iff using grind #30516

Uh oh!

Conversation

euprunin commented Oct 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Trace profiling of of_mem_specialOrthogonalGroup_fin_two_iff before PR 30516

Trace profiling of of_mem_specialOrthogonalGroup_fin_two_iff after PR 30516

Uh oh!

github-actions bot commented Oct 13, 2025

PR summary 7a9e177031

Import changes for modified files

Declarations diff

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

euprunin commented Oct 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg commented Oct 14, 2025

Uh oh!

github-actions bot commented Oct 14, 2025

Uh oh!

riccardobrasca commented Oct 14, 2025

Uh oh!

mathlib-bors bot commented Oct 14, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

[Merged by Bors] - chore(LinearAlgebra): golf `of_mem_specialOrthogonalGroup_fin_two_iff` using `grind` #30516

[Merged by Bors] - chore(LinearAlgebra): golf `of_mem_specialOrthogonalGroup_fin_two_iff` using `grind` #30516

euprunin commented Oct 13, 2025 •

edited

Loading

Trace profiling of `of_mem_specialOrthogonalGroup_fin_two_iff` before PR 30516

Trace profiling of `of_mem_specialOrthogonalGroup_fin_two_iff` after PR 30516

euprunin commented Oct 14, 2025 •

edited

Loading