awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Fintype p
inst_3 : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
rw : (C * (A * B)).trace = (C * A * B).trace
⊢ (A * B * C).trace = (C * A * B).trace
have rw₁ : (C * (A * B)).trace = (C * (A * B)).trace
Tactic: rw [trace_mul_comm, Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Fintype p
inst_3 : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * (B * C)).trace = (C * (A * B)).trace
have rw : (A * B * C).trace = (C * (A * B)).trace
Tactic: rw [← Matrix.mul_assoc, trace_mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Fintype p
inst_3 : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
rw : (A * B * C).trace = (C * (A * B)).trace
⊢ (A * (B * C)).trace = (C * (A * B)).trace
have rw₁ : (C * (A * B)).trace = (C * (A * B)).trace
Tactic: rw [← Matrix.mul_assoc, trace_mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
ι : Type u_8
inst_1 : Unique ι
inst_2 : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (replicateCol ι a * replicateRow ι b).trace = a ⬝ᵥ b
have apply : ∀ (x : n), Membership.mem (γ := Finset n) Finset.univ x → (replicateCol ι a * replicateRow ι b).diag x = a x * b x
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (vecMulVec a b).trace = a ⬝ᵥ b
have rw : (replicateCol Unit a * replicateRow Unit b).trace = a ⬝ᵥ b
Tactic: rw [vecMulVec_eq Unit, trace_replicateCol_mul_replicateRow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring R
a b : n → R
rw : (replicateCol Unit a * replicateRow Unit b).trace = a ⬝ᵥ b
⊢ (vecMulVec a b).trace = a ⬝ᵥ b
have rw₁ : a ⬝ᵥ b = a ⬝ᵥ b
Tactic: rw [vecMulVec_eq Unit, trace_replicateCol_mul_replicateRow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
R : Type u_6
n : ℕ
inst : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace
have delta : M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Fin n.succ, M.diag i
Tactic: delta trace
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
R : Type u_6
n : ℕ
inst : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Fin n.succ, M.diag i
have rw : M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i =
  ∑ i : Option (Fin n), M.diag (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) i)
Tactic: rw [← (finSuccEquiv n).symm.sum_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
R : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ ((↑M : Matrix m m R) * N * (↑M⁻¹ : Matrix m m R)).trace = N.trace
have rw : ((↑M⁻¹ : Matrix m m R) * (↑M : Matrix m m R) * N).trace = N.trace
Tactic: rw [trace_mul_cycle, Units.inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
R : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
rw : ((↑M⁻¹ : Matrix m m R) * (↑M : Matrix m m R) * N).trace = N.trace
⊢ ((↑M : Matrix m m R) * N * (↑M⁻¹ : Matrix m m R)).trace = N.trace
have rw₁ : (1 * N).trace = N.trace
Tactic: rw [trace_mul_cycle, Units.inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
R : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
rw : ((↑M⁻¹ : Matrix m m R) * (↑M : Matrix m m R) * N).trace = N.trace
rw₁ : (1 * N).trace = N.trace
⊢ ((↑M : Matrix m m R) * N * (↑M⁻¹ : Matrix m m R)).trace = N.trace
have rw₂ : N.trace = N.trace
Tactic: rw [trace_mul_cycle, Units.inv_mul, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
R : Type u_6
inst : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + A 1 1 + A 2 2
have rw : A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))
Tactic: rw [← add_zero (A 2 2), add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : Nonempty n
r : R
⊢ ∃ (a : Matrix n n R), a.trace = r
have inhabit : ∀ (inhabited_h : Inhabited n), ∃ (a : Matrix n n R), a.trace = r
Tactic: inhabit n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : Nonempty n
r : R
⊢ ∃ (a : Matrix n n R), a.trace = r
have inhabit : ∀ (inhabited_h : Inhabited n), ∃ (a : Matrix n n R), a.trace = r
Tactic: classical
  inhabit n
  exact ⟨single default default r, trace_single_eq_same default r⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
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
have refine : ∀ (h : ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace), A = B
Tactic: refine ⟨fun h x => h ▸ rfl, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
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 = B
have a : ∀ (i : m) (j : n), A i j = B i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
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
have refine : ∀ (h : ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace), A = B
Tactic: refine ⟨fun h x => h ▸ rfl, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
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 = B
have a : ∀ (i : m) (j : n), A i j = B i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
i j : n
inst_2 : Finite n
c : R
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) = transvection i j c
have intro : ∀ (val : Fintype n), updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) = transvection i j c
Tactic: cases nonempty_fintype n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) = transvection i j c
have intro : ∀ (a b : n), updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
have pos : ∀ (ha : i = a), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
have neg : ∀ (ha : ¬i = a), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
have pos : ∀ (hb : j = 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j)) a b = transvection i j c a b
have neg : ∀ (hb : ¬j = 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ (transvection i j c).det = 1
have rw : (updateRow 1 i (1 i + HSMul.hSMul (β := n → R) c (1 j))).det = 1
Tactic: rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ (transvection i j c).det = 1
have rw₁ : Eq.{u₂ + 1} (α := R) (det.{u₂, u_1} (n := n) 1) 1
Tactic: rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ (transvection i j c).det = 1
have rw₂ : Eq.{u₂ + 1} (α := R) 1 1
Tactic: rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ Nonempty (TransvectionStruct n R)
have choose : ∀ (x y : n) (hxy : x ≠ y), Nonempty (TransvectionStruct n R)
Tactic: choose x y hxy using exists_pair_ne n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
L : List (TransvectionStruct n R)
⊢ (List.map toMatrix L).prod.det = 1
have nil : Eq.{u₂ + 1} (α := R) (det.{u₂, u_1} (n := n) (List.prod (List.map toMatrix []))) 1
Tactic: induction L with
  | nil => simp
  | cons _ _ IH => simp [IH]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ (List.map toMatrix L).prod.det = 1
have 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
Tactic: induction L with
  | nil => simp
  | cons _ _ IH => simp [IH]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
t : TransvectionStruct n R
⊢ t.inv.toMatrix * t.toMatrix = 1
have 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
Tactic: rcases t with ⟨_, _, t_hij⟩
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 * t.inv.toMatrix = 1
have 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
Tactic: rcases t with ⟨_, _, t_hij⟩
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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) (t :: L).reverse).prod * (List.map toMatrix (t :: L)).prod = 1
have cons : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (t.inv.toMatrix * t.toMatrix) *
    (List.map toMatrix 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
L : List (TransvectionStruct n R)
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
have nil : HMul.hMul (α := Matrix n n R) (List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse [])))
    (List.prod (List.map toMatrix [])) =
  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
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
have 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
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
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ (List.map toMatrix (t :: L)).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod = 1
have cons : t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
    t.inv.toMatrix =
  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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1
have cons : t.toMatrix * 1 * t.inv.toMatrix = 1
Tactic: simp_rw [IH, Matrix.mul_one, t.mul_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1
have cons₁ : t.toMatrix * t.inv.toMatrix = 1
Tactic: simp_rw [IH, Matrix.mul_one, t.mul_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
R : Type u₂
inst : DecidableEq n
inst_1 : CommRing R
inst_2 : Fintype n
L : List (TransvectionStruct n R)
⊢ (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
have nil : HMul.hMul (α := Matrix n n R) (List.prod (List.map toMatrix []))
    (List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse []))) =
  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]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
have 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
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]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
have refine : Pairwise fun (i j : n) ↦ Commute (single i j 1) M
Tactic: refine mem_range_scalar_of_commute_single ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
have 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
Tactic: refine ⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ Commute t.toMatrix M
have rw : ∀ (h : ∀ (i j : n), i ≠ j → Commute (single i j 1) M) (t : TransvectionStruct n R), Commute t.toMatrix M
Tactic: rw [mem_range_scalar_iff_commute_single] at h
Cleared hypotheses: h, t
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ Commute t.toMatrix M
have refine : Commute (single t.i t.j t.c) M
Tactic: refine (Commute.one_left M).add_left ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ Commute (single t.i t.j t.c) M
have h₁ : single t.i t.j t.c = HSMul.hSMul (β := Matrix n n R) t.c (single t.i t.j 1)
Tactic: convert! (h _ _ t.hij).smul_left t.c using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
⊢ single t.i t.j t.c = HSMul.hSMul (β := Matrix n n R) t.c (single t.i t.j 1)
have h₁ : single t.i t.j t.c = single t.i t.j (HSMul.hSMul (β := R) t.c 1)
Tactic: rw [smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
h₁ : single t.i t.j t.c = single t.i t.j (HSMul.hSMul (β := R) t.c 1)
⊢ single t.i t.j t.c = HSMul.hSMul (β := Matrix n n R) t.c (single t.i t.j 1)
have h₂ : single t.i t.j t.c = single t.i t.j (t.c * 1)
Tactic: rw [smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : ∀ (i j : n), i ≠ j → Commute (single i j 1) M
t : TransvectionStruct n R
h₁ : single t.i t.j t.c = single t.i t.j (HSMul.hSMul (β := R) t.c 1)
h₂ : single t.i t.j t.c = single t.i t.j (t.c * 1)
⊢ single t.i t.j t.c = HSMul.hSMul (β := Matrix n n R) t.c (single t.i t.j 1)
have h₃ : single t.i t.j t.c = single t.i t.j t.c
Tactic: rw [smul_single, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
t : TransvectionStruct n R
⊢ (sumInl p t).toMatrix = fromBlocks t.toMatrix 0 0 1
have mk : ∀ (i j : n) (hij : i ≠ j) (c : R),
  (sumInl p { i := i, j := j, hij := hij, c := c : TransvectionStruct n R }).toMatrix =
    fromBlocks { i := i, j := j, hij := hij, c := c }.toMatrix 0 0 1
Tactic: cases t
Cleared hypotheses: t