awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ (L₀ : List (TransvectionStruct (Fin r) 𝕜)) (L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜),
      (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D :
    Fin r ⊕ Unit → 𝕜), (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have rcases : ∀ (L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜))
  (hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal),
  ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D :
    Fin r ⊕ Unit → 𝕜), (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
Tactic: rcases exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec M with ⟨L₁, L₁', hM⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ (L₀ : List (TransvectionStruct (Fin r) 𝕜)) (L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜),
      (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D :
    Fin r ⊕ Unit → 𝕜), (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have rcases : ∀ (L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜)
  (h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀),
  ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D :
    Fin r ⊕ Unit → 𝕜), (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
Tactic: rcases IH M'' with ⟨L₀, L₀', D₀, h₀⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ (L₀ : List (TransvectionStruct (Fin r) 𝕜)) (L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜),
      (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D :
    Fin r ⊕ Unit → 𝕜), (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have L₁'₁ : (List.map toMatrix (List.map (sumInl Unit) L₀ ++ L₁)).prod * M *
    (List.map toMatrix (L₁' ++ List.map (sumInl Unit) L₀')).prod =
  diagonal (Sum.elim D₀ fun (x : Unit) ↦ M' (inr ()) (inr ()))
Tactic: refine
    ⟨L₀.map (sumInl Unit) ++ L₁, L₁' ++ L₀'.map (sumInl Unit),
      Sum.elim D₀ fun _ => M' (inr unit) (inr unit), ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ (L₀ : List (TransvectionStruct (Fin r) 𝕜)) (L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜),
      (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
⊢ (List.map toMatrix (List.map (sumInl Unit) L₀ ++ L₁)).prod * M *
      (List.map toMatrix (L₁' ++ List.map (sumInl Unit) L₀')).prod =
    diagonal (Sum.elim D₀ fun (x : Unit) ↦ M' (inr ()) (inr ()))
have suffices : (List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
  diagonal (Sum.elim D₀ fun (x : Unit) ↦ c)
Tactic: suffices (L₀.map (toMatrix ∘ sumInl Unit)).prod * M' * (L₀'.map (toMatrix ∘ sumInl Unit)).prod =
      diagonal (Sum.elim D₀ fun _ => c) by
    simpa [M', c, Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ (L₀ : List (TransvectionStruct (Fin r) 𝕜)) (L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜),
      (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
⊢ M' = fromBlocks M'' 0 0 (diagonal fun (x : Unit) ↦ c)
have rw : fromBlocks M'.toBlocks₁₁ 0 0 M'.toBlocks₂₂ = fromBlocks M'' 0 0 (diagonal fun (x : Unit) ↦ c)
Tactic: rw [← fromBlocks_toBlocks M', hM.1, hM.2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ (L₀ : List (TransvectionStruct (Fin r) 𝕜)) (L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜),
      (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
⊢ (List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
    diagonal (Sum.elim D₀ fun (x : Unit) ↦ c)
have this : M' = fromBlocks M'' 0 0 (diagonal fun (x : Unit) ↦ c)
Tactic: have : M' = fromBlocks M'' 0 0 (diagonal fun _ => c) := by
    rw [← fromBlocks_toBlocks M', hM.1, hM.2]
    rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ (L₀ : List (TransvectionStruct (Fin r) 𝕜)) (L₀' : List (TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜),
      (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
this : M' = fromBlocks M'' 0 0 (diagonal fun (x : Unit) ↦ c)
⊢ (List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
    diagonal (Sum.elim D₀ fun (x : Unit) ↦ c)
have rw : (List.map (toMatrix ∘ sumInl Unit) L₀).prod * fromBlocks M'' 0 0 (diagonal fun (x : Unit) ↦ c) *
    (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
  diagonal (Sum.elim D₀ fun (x : Unit) ↦ c)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
H :
  ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L).prod
          ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
        (List.map toMatrix L').prod =
      diagonal D
⊢ ∃ (L : List (TransvectionStruct p 𝕜)) (L' : List (TransvectionStruct p 𝕜)) (D : p → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have rcases : ∀ (L₀ L₀' : List (TransvectionStruct n 𝕜)) (D₀ : n → 𝕜)
  (h₀ :
    HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
          ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
        (List.map toMatrix L₀').prod =
      diagonal D₀),
  ∃ (L : List (TransvectionStruct p 𝕜)) (L' : List (TransvectionStruct p 𝕜)) (D : p → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
Tactic: rcases H with ⟨L₀, L₀', D₀, h₀⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
⊢ ∃ (L : List (TransvectionStruct p 𝕜)) (L' : List (TransvectionStruct p 𝕜)) (D : p → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have refine : (List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod * M *
    (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod =
  diagonal (D₀ ∘ (⇑e : (a : p) → n))
Tactic: refine ⟨L₀.map (reindexEquiv e.symm), L₀'.map (reindexEquiv e.symm), D₀ ∘ e, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
⊢ (List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod * M *
      (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))
have this : M =
  (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
    ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)
Tactic: have : M = reindexAlgEquiv 𝕜 _ e.symm (reindexAlgEquiv 𝕜 _ e M) := by
    simp only [Equiv.symm_symm, submatrix_submatrix, reindex_apply, submatrix_id_id,
      Equiv.symm_comp_self, reindexAlgEquiv_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
this :
  M =
    (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
      ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)
⊢ (List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod * M *
      (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))
have rw : HMul.hMul (β := Matrix p p 𝕜) (List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod
      ((reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
          ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M) :
        Matrix p p 𝕜) *
    (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod =
  diagonal (D₀ ∘ (⇑e : (a : p) → n))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
this :
  M =
    (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
      ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)
⊢ HMul.hMul (β := Matrix p p 𝕜) (List.map toMatrix (List.map (reindexEquiv e.symm) L₀)).prod
        ((reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
            ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M) :
          Matrix p p 𝕜) *
      (List.map toMatrix (List.map (reindexEquiv e.symm) L₀')).prod =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))
have simp : HMul.hMul (β := Matrix p p 𝕜)
    (HMul.hMul (α := Matrix p p 𝕜) (β := Matrix p p 𝕜)
      ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (List.map toMatrix L₀).prod : Matrix p p 𝕜)
      ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
          ((reindex e e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M) :
        Matrix p p 𝕜))
    ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (List.map toMatrix L₀').prod : Matrix p p 𝕜) =
  diagonal (D₀ ∘ (⇑e : (a : p) → n))
Tactic: simp only [toMatrix_reindexEquiv_prod, List.map_map, reindexAlgEquiv_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : DecidableEq p
inst_3 : Fintype n
inst_4 : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ :
  HMul.hMul (β := Matrix n n 𝕜) (List.map toMatrix L₀).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M : Matrix n n 𝕜) *
      (List.map toMatrix L₀').prod =
    diagonal D₀
this :
  M =
    (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
      ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)
⊢ HMul.hMul (β := Matrix p p 𝕜)
      (HMul.hMul (α := Matrix p p 𝕜) (β := Matrix p p 𝕜)
        ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (List.map toMatrix L₀).prod : Matrix p p 𝕜)
        ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
            ((reindex e e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M) :
          Matrix p p 𝕜))
      ((reindex e.symm e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (List.map toMatrix L₀').prod : Matrix p p 𝕜) =
    diagonal (D₀ ∘ (⇑e : (a : p) → n))
have simp : Eq (α := Matrix p p 𝕜) ((reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜) (diagonal D₀) : Matrix p p 𝕜)
  (diagonal (D₀ ∘ (⇑e : (a : p) → n)) : Matrix p p 𝕜)
Tactic: simp only [← reindexAlgEquiv_apply 𝕜, ← reindexAlgEquiv_mul, h₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have suffices : ∀ (cn : ℕ),
  Fintype.card n = cn →
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
Tactic: suffices ∀ cn, Fintype.card n = cn →
      ∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D by exact this _ rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have zero : List.prod (List.map toMatrix []) * M * List.prod (List.map toMatrix []) = diagonal fun (x : n) ↦ 1
Tactic: refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
⊢ List.prod (List.map toMatrix []) * M * List.prod (List.map toMatrix []) = diagonal fun (x : n) ↦ 1
have zero : ∀ (i j : n),
  HMul.hMul (β := Matrix n n 𝕜) (List.prod (List.map toMatrix []) * M) (List.prod (List.map toMatrix [])) i j =
    diagonal (fun (x : n) ↦ 1) i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
i j : n
⊢ HMul.hMul (β := Matrix n n 𝕜) (List.prod (List.map toMatrix []) * M) (List.prod (List.map toMatrix [])) i j =
    diagonal (fun (x : n) ↦ 1) i j
have zero : ∀ (hn : IsEmpty n) (i j : n),
  HMul.hMul (β := Matrix n n 𝕜) (List.prod (List.map toMatrix []) * M) (List.prod (List.map toMatrix [])) i j =
    diagonal (fun (x : n) ↦ 1) i j
Tactic: rw [Fintype.card_eq_zero_iff] at hn
Cleared hypotheses: hn, i, j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ n ≃ Fin r ⊕ Unit
have refine : Fintype.card n = Fintype.card (Fin r ⊕ Unit)
Tactic: refine Fintype.equivOfCardEq ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ Fintype.card n = Fintype.card (Fin r ⊕ Unit)
have rw : r + 1 = Fintype.card (Fin r ⊕ Unit)
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ r + 1 = Fintype.card (Fin r ⊕ Unit)
have rw : r + 1 = Fintype.card (Fin r) + Fintype.card Unit
Tactic: rw [@Fintype.card_sum (Fin r) Unit _ _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have succ : ∀ (e : n ≃ Fin r ⊕ Unit),
  ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
Tactic: have e : n ≃ Fin r ⊕ Unit := by
      refine Fintype.equivOfCardEq ?_
      rw [hn]
      rw [@Fintype.card_sum (Fin r) Unit _ _]
      simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = r),
    ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
e : n ≃ Fin r ⊕ Unit
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have succ : ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D :
  Fin r ⊕ Unit → 𝕜),
  HMul.hMul (β := Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (List.map toMatrix L).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix n n 𝕜) → Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) M :
          Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) *
      (List.map toMatrix L').prod =
    diagonal D
Tactic: apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
n : Type
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n 𝕜
cn : ℕ
hn : Fintype.card n = cn
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
have zero : ∀ (n : Type) [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n 𝕜) (hn : Fintype.card n = 0),
  ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
Tactic: induction cn generalizing n M with
  | zero =>
    refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩
    ext i j
    rw [Fintype.card_eq_zero_iff] at hn
    exact hn.elim' i
  | succ r IH =>
    have e : n ≃ Fin r ⊕ Unit := by
      refine Fintype.equivOfCardEq ?_
      rw [hn]
      rw [@Fintype.card_sum (Fin r) Unit _ _]
      simp
    apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e
    apply
      exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction fun N =>
        IH (Fin r) N (by simp)
Cleared hypotheses: n, inst_1, inst_2, M, cn, hn