awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
⊢ A = B ↔ ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace

Tactic:
⟨fun h x => h ▸ rfl, fun h => ?_⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
refine : ∀ (h : ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace), A = B
⊢ A = B ↔ ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace

Tactic:
refine ⟨fun h x => h ▸ rfl, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
h : ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace
a : ∀ (i : m) (j : n), A i j = B i j
⊢ A = B

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
h : ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace
i : m
j : n
⊢ A i j = B i j

Tactic:
simpa [trace_single_mul] using h (single j i (1 : R))

Premises used: Matrix.trace_single_mul, OfNat.ofNat, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
h : ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace
i : m
j : n
⊢ A i j = B i j

Tactic:
classical
  simpa [trace_single_mul] using h (single j i (1 : R))

Premises used: Matrix.trace_single_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
⊢ A = B ↔ ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace

Tactic:
⟨fun h x => h ▸ rfl, fun h => ?_⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
refine : ∀ (h : ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace), A = B
⊢ A = B ↔ ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace

Tactic:
refine ⟨fun h x => h ▸ rfl, fun h => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
h : ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace
a : ∀ (i : m) (j : n), A i j = B i j
⊢ A = B

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
h : ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace
i : m
j : n
⊢ A i j = B i j

Tactic:
simpa [trace_mul_single] using h (single j i (1 : R))

Premises used: Matrix.trace_mul_single, OfNat.ofNat, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : NonAssocSemiring R
A B : Matrix m n R
h : ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace
i : m
j : n
⊢ A i j = B i j

Tactic:
classical
  simpa [trace_mul_single] using h (single j i (1 : R))

Premises used: Matrix.trace_mul_single
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
⊢ Eq (α := Matrix n n R) (transvection i j 0) 1

Tactic:
simp [transvection]

Premises used: Matrix.transvection
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Finite n
c : R
intro : ∀ (val : Fintype n), updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) = transvection i j c
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) = transvection i j c

Tactic:
cases nonempty_fintype n

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Finite n
c : R
val : Fintype n
intro : ∀ (a b : n), updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) = transvection i j c

Tactic:
ext a b
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Finite n
c : R
val : Fintype n
a b : n
pos : ∀ (ha : i = a), updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
neg : ∀ (ha : ¬i = a), updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b

Tactic:
by_cases ha : i = a
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Finite n
c : R
val : Fintype n
a b : n
ha : i = a
pos : ∀ (hb : j = b), updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
neg : ∀ (hb : ¬j = b), updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b

Tactic:
by_cases hb : j = b
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Finite n
c : R
val : Fintype n
a b : n
ha : i = a
hb : j = b
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b

Tactic:
simp only [ha, updateRow_self, Pi.add_apply, one_apply, Pi.smul_apply, hb, ↓reduceIte,
        smul_eq_mul, mul_one, transvection, add_apply, single_apply_same]

Premises used: Matrix.one_apply, Matrix.add_apply, Matrix.transvection, Pi.add_apply, Matrix.single_apply_same, reduceIte, Matrix.updateRow_self, smul_eq_mul, mul_one, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Finite n
c : R
val : Fintype n
a b : n
ha : i = a
hb : ¬j = b
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b

Tactic:
simp only [ha, updateRow_self, Pi.add_apply, one_apply, Pi.smul_apply, hb, ↓reduceIte,
        smul_eq_mul, mul_zero, add_zero, transvection, add_apply, and_false, not_false_eq_true,
        single_apply_of_ne]

Premises used: Matrix.single_apply_of_ne, Matrix.one_apply, Matrix.add_apply, Matrix.transvection, MulZeroClass.mul_zero, Pi.add_apply, reduceIte, Matrix.updateRow_self, and_false, smul_eq_mul, add_zero, not_false_eq_true, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Finite n
c : R
val : Fintype n
a b : n
ha : ¬i = a
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b

Tactic:
simp only [updateRow_ne, transvection, ha, Ne.symm ha, single_apply_of_ne, add_zero,
      Ne, not_false_iff,
      false_and, add_apply]

Premises used: Matrix.single_apply_of_ne, Matrix.add_apply, false_and, Ne, Ne.symm, Matrix.transvection, Matrix.updateRow_ne, add_zero, not_false_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Fintype n
h : i ≠ j
c d : R
⊢ transvection i j c * transvection i j d = transvection i j (c + d)

Tactic:
simp [transvection, Matrix.add_mul, Matrix.mul_add, h.symm, add_assoc,
    single_add]

Premises used: Matrix.single_add, add_assoc, Ne.symm, Matrix.transvection, Matrix.add_mul, Matrix.mul_add
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Fintype n
b : n
c : R
M : Matrix n n R
⊢ (transvection i j c * M) i b = M i b + c * M j b

Tactic:
simp [transvection, Matrix.add_mul]

Premises used: Matrix.transvection, Matrix.add_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Fintype n
a : n
c : R
M : Matrix n n R
⊢ (M * transvection i j c) a j = M a j + c * M a i

Tactic:
simp [transvection, Matrix.mul_add, mul_comm]

Premises used: Matrix.transvection, Matrix.mul_add, mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Fintype n
a b : n
ha : a ≠ i
c : R
M : Matrix n n R
⊢ (transvection i j c * M) a b = M a b

Tactic:
simp [transvection, Matrix.add_mul, ha]

Premises used: Matrix.transvection, Matrix.add_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Fintype n
a b : n
hb : b ≠ j
c : R
M : Matrix n n R
⊢ (M * transvection i j c) a b = M a b

Tactic:
simp [transvection, Matrix.mul_add, hb]

Premises used: Matrix.transvection, Matrix.mul_add
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Fintype n
h : i ≠ j
c : R
rw : (updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j))).det = 1
rw₁ : Eq.{u₂ + 1} (α := R) (det.{u₂, u_1} (n := n) 1) 1
rw₂ rw₃ : Eq.{u₂ + 1} (α := R) 1 1
⊢ (transvection i j c).det = 1

Tactic:
rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]

Premises used: Matrix.det_updateRow_add_smul_self, Matrix.updateRow_eq_transvection, Matrix.det_one
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : CommRing R
i j : n
inst_4 : Nontrivial n
choose : ∀ (x y : n) (hxy : x ≠ y), Nonempty (TransvectionStruct n R)
⊢ Nonempty (TransvectionStruct n R)

Tactic:
choose x y hxy using exists_pair_ne n

Premises used: exists_pair_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : CommRing R
i j : n
inst_4 : Nontrivial n
x y : n
hxy : x ≠ y
⊢ Nonempty (TransvectionStruct n R)

Tactic:
⟨⟨x, y, hxy, 0⟩⟩

Premises used: Nonempty.intro, Matrix.TransvectionStruct.mk, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : CommRing R
i j : n
inst_4 : Nontrivial n
x y : n
hxy : x ≠ y
⊢ Nonempty (TransvectionStruct n R)

Tactic:
exact ⟨⟨x, y, hxy, 0⟩⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
hij : i ≠ j
c : R
⊢ { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }.toMatrix = transvection i j c

Tactic:
rfl

Premises used: Matrix.TransvectionStruct.toMatrix, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
⊢ t.toMatrix.det = 1

Tactic:
det_transvection_of_ne _ _ t.hij _

Premises used: Matrix.TransvectionStruct.hij, Matrix.TransvectionStruct.toMatrix, Matrix.det_transvection_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
⊢ Eq.{u₂ + 1} (α := R) (det.{u₂, u_1} (n := n) (List.prod (List.map toMatrix []))) 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
head : TransvectionStruct n R
tail : List (TransvectionStruct n R)
IH : (List.map toMatrix tail).prod.det = 1
⊢ (List.map toMatrix (head :: tail)).prod.det = 1

Tactic:
simp [IH]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
L : List (TransvectionStruct n R)
nil : Eq.{u₂ + 1} (α := R) (det.{u₂, u_1} (n := n) (List.prod (List.map toMatrix []))) 1
cons :
  ∀ (head : TransvectionStruct n R) (tail : List (TransvectionStruct n R)) (IH : (List.map toMatrix tail).prod.det = 1),
    (List.map toMatrix (head :: tail)).prod.det = 1
⊢ (List.map toMatrix L).prod.det = 1

Tactic:
induction L with
  | nil => simp
  | cons _ _ IH => simp [IH]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
rcases :
  ∀ (i j : n) (t_hij : i ≠ j) (c : R),
    { i := i, j := j, hij := t_hij, c := c : TransvectionStruct n R }.inv.toMatrix *
        { i := i, j := j, hij := t_hij, c := c : TransvectionStruct n R }.toMatrix =
      1
⊢ t.inv.toMatrix * t.toMatrix = 1

Tactic:
rcases t with ⟨_, _, t_hij⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j : n
t_hij : i ≠ j
c : R
⊢ { i := i, j := j, hij := t_hij, c := c : TransvectionStruct n R }.inv.toMatrix *
      { i := i, j := j, hij := t_hij, c := c : TransvectionStruct n R }.toMatrix =
    1

Tactic:
simp [toMatrix, transvection_mul_transvection_same, t_hij]

Premises used: Matrix.transvection_mul_transvection_same, Matrix.TransvectionStruct.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
rcases :
  ∀ (i j : n) (t_hij : i ≠ j) (c : R),
    { i := i, j := j, hij := t_hij, c := c : TransvectionStruct n R }.toMatrix *
        { i := i, j := j, hij := t_hij, c := c : TransvectionStruct n R }.inv.toMatrix =
      1
⊢ t.toMatrix * t.inv.toMatrix = 1

Tactic:
rcases t with ⟨_, _, t_hij⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
i j : n
t_hij : i ≠ j
c : R
⊢ { i := i, j := j, hij := t_hij, c := c : TransvectionStruct n R }.toMatrix *
      { i := i, j := j, hij := t_hij, c := c : TransvectionStruct n R }.inv.toMatrix =
    1

Tactic:
simp [toMatrix, transvection_mul_transvection_same, t_hij]

Premises used: Matrix.transvection_mul_transvection_same, Matrix.TransvectionStruct.toMatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
⊢ HMul.hMul (α := Matrix n n R) (List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse [])))
      (List.prod (List.map toMatrix [])) =
    1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
this :
  (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (t.inv.toMatrix * t.toMatrix) *
      (List.map toMatrix L).prod =
    1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod * (List.map toMatrix (t :: L)).prod = 1

Tactic:
simpa [Matrix.mul_assoc]

Premises used: Matrix.mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
cons :
  (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (t.inv.toMatrix * t.toMatrix) *
      (List.map toMatrix L).prod =
    1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod * (List.map toMatrix (t :: L)).prod = 1

Tactic:
suffices
      (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (t.inv.toMatrix * t.toMatrix) *
          (L.map toMatrix).prod = 1
      by simpa [Matrix.mul_assoc]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (t.inv.toMatrix * t.toMatrix) *
      (List.map toMatrix L).prod =
    1

Tactic:
simpa [inv_mul] using IH

Premises used: Matrix.TransvectionStruct.inv_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
L : List (TransvectionStruct n R)
nil :
  HMul.hMul (α := Matrix n n R) (List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse [])))
      (List.prod (List.map toMatrix [])) =
    1
cons :
  ∀ (t : TransvectionStruct n R) (L : List (TransvectionStruct n R))
    (IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1),
    (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod * (List.map toMatrix (t :: L)).prod = 1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1

Tactic:
induction L with
  | nil => simp
  | cons t L IH =>
    suffices
      (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (t.inv.toMatrix * t.toMatrix) *
          (L.map toMatrix).prod = 1
      by simpa [Matrix.mul_assoc]
    simpa [inv_mul] using IH

Premises used: Matrix.TransvectionStruct.inv_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
⊢ HMul.hMul (α := Matrix n n R) (List.prod (List.map toMatrix []))
      (List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse []))) =
    1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
this :
  t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1
⊢ (List.map toMatrix (t :: L)).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod = 1

Tactic:
simpa [Matrix.mul_assoc]

Premises used: Matrix.mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
cons :
  t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1
⊢ (List.map toMatrix (t :: L)).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod = 1

Tactic:
suffices
      t.toMatrix *
            ((L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod) *
          t.inv.toMatrix = 1
      by simpa [Matrix.mul_assoc]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
cons : t.toMatrix * 1 * t.inv.toMatrix = 1
cons₁ : t.toMatrix * t.inv.toMatrix = 1
⊢ t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1

Tactic:
simp_rw [IH, Matrix.mul_one, t.mul_inv]

Premises used: Matrix.mul_one, Matrix.TransvectionStruct.mul_inv
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
L : List (TransvectionStruct n R)
nil :
  HMul.hMul (α := Matrix n n R) (List.prod (List.map toMatrix []))
      (List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse []))) =
    1
cons :
  ∀ (t : TransvectionStruct n R) (L : List (TransvectionStruct n R))
    (IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1),
    (List.map toMatrix (t :: L)).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod = 1
⊢ (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1

Tactic:
induction L with
  | nil => simp
  | cons t L IH =>
    suffices
      t.toMatrix *
            ((L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod) *
          t.inv.toMatrix = 1
      by simpa [Matrix.mul_assoc]
    simp_rw [IH, Matrix.mul_one, t.mul_inv]

Premises used: Matrix.mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R)) M

Tactic:
mem_range_scalar_of_commute_single ?_

Premises used: Matrix.mem_range_scalar_of_commute_single
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
refine : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
⊢ Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R)) M

Tactic:
refine mem_range_scalar_of_commute_single ?_

Premises used: Matrix.mem_range_scalar_of_commute_single
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
hM : ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
i j : n
hij : i ≠ j
⊢ Commute (single i j 1) M

Tactic:
simpa [transvection, mul_add, add_mul] using (hM ⟨i, j, hij, 1⟩).eq

Premises used: add_mul, Matrix.transvection, Matrix.TransvectionStruct.mk, mul_add, OfNat.ofNat, Commute.eq
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
⊢ Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R)) M ↔
    ∀ (t : TransvectionStruct n R), Commute t.toMatrix M

Tactic:
⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩

Premises used: Iff.intro, Matrix.mem_range_scalar_of_commute_transvectionStruct
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
refine :
  ∀ (h : Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R)) M)
    (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R)) M ↔
    ∀ (t : TransvectionStruct n R), Commute t.toMatrix M

Tactic:
refine ⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
M : Matrix n n R
h : Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(scalar n) : (a : R) → Matrix n n R)) M
t : TransvectionStruct n R
rw : ∀ (h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M) (t : TransvectionStruct n R), Commute t.toMatrix M
⊢ Commute t.toMatrix M

Tactic:
rw [mem_range_scalar_iff_commute_single] at h

Premises used: Matrix.mem_range_scalar_iff_commute_single