awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Fin r → Unit → 𝕜) → Matrix (Fin r) Unit 𝕜) (fun (i : Fin r) (j : Unit) ↦ M (inl i) (inr j)) i j :
            𝕜)
          (0 i j : 𝕜)) ∨
    ¬∀ (i : Unit) (j : Fin r),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Unit → Fin r → 𝕜) → Matrix Unit (Fin r) 𝕜) (fun (i : Unit) (j : Fin r) ↦ M (inr i) (inl j)) i j :
            𝕜)
          (0 i j : 𝕜)
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix L').prod).IsTwoBlockDiagonal
pos :
  ((List.map toMatrix L).prod * M *
      (List.map toMatrix
          ({ i := inl i, j := inr (), hij := ⋯, c := 1 : TransvectionStruct (Fin r ⊕ Unit) 𝕜 } ::
            L')).prod).IsTwoBlockDiagonal
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
refine ⟨L, ⟨inl i, inr unit, by simp, 1⟩::L', ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Fin r → Unit → 𝕜) → Matrix (Fin r) Unit 𝕜) (fun (i : Fin r) (j : Unit) ↦ M (inl i) (inr j)) i j :
            𝕜)
          (0 i j : 𝕜)) ∨
    ¬∀ (i : Unit) (j : Fin r),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Unit → Fin r → 𝕜) → Matrix Unit (Fin r) 𝕜) (fun (i : Unit) (j : Fin r) ↦ M (inr i) (inl j)) i j :
            𝕜)
          (0 i j : 𝕜)
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix L').prod).IsTwoBlockDiagonal
pos :
  ((List.map toMatrix L).prod * M * transvection (inl i) (inr ()) 1 * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ((List.map toMatrix L).prod * M *
      (List.map toMatrix
          ({ i := inl i, j := inr (), hij := ⋯, c := 1 : TransvectionStruct (Fin r ⊕ Unit) 𝕜 } ::
            L')).prod).IsTwoBlockDiagonal

Tactic:
simp only [← Matrix.mul_assoc, toMatrix_mk, List.prod_cons, List.map]

Premises used: List.map, Matrix.mul_assoc, Matrix.TransvectionStruct.toMatrix_mk, List.prod_cons
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Fin r → Unit → 𝕜) → Matrix (Fin r) Unit 𝕜) (fun (i : Fin r) (j : Unit) ↦ M (inl i) (inr j)) i j :
            𝕜)
          (0 i j : 𝕜)) ∨
    ¬∀ (i : Unit) (j : Fin r),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Unit → Fin r → 𝕜) → Matrix Unit (Fin r) 𝕜) (fun (i : Unit) (j : Fin r) ↦ M (inr i) (inl j)) i j :
            𝕜)
          (0 i j : 𝕜)
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix L').prod).IsTwoBlockDiagonal
pos :
  ((List.map toMatrix L).prod * (M * transvection (inl i) (inr ()) 1) * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ((List.map toMatrix L).prod * M * transvection (inl i) (inr ()) 1 * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
rw [Matrix.mul_assoc (L.map toMatrix).prod]

Premises used: List.map, Matrix.mul_assoc, Matrix.TransvectionStruct.toMatrix, List.prod
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Fin r → Unit → 𝕜) → Matrix (Fin r) Unit 𝕜) (fun (i : Fin r) (j : Unit) ↦ M (inl i) (inr j)) i j :
            𝕜)
          (0 i j : 𝕜)) ∨
    ¬∀ (i : Unit) (j : Fin r),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Unit → Fin r → 𝕜) → Matrix Unit (Fin r) 𝕜) (fun (i : Unit) (j : Fin r) ↦ M (inr i) (inl j)) i j :
            𝕜)
          (0 i j : 𝕜)
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ((List.map toMatrix L).prod * (M * transvection (inl i) (inr ()) 1) * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
hLL'
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Fin r → Unit → 𝕜) → Matrix (Fin r) Unit 𝕜) (fun (i : Fin r) (j : Unit) ↦ M (inl i) (inr j)) i j :
            𝕜)
          (0 i j : 𝕜)) ∨
    ¬∀ (i : Unit) (j : Fin r),
        Eq.{u_3 + 1} (α := 𝕜)
          ((of : (a : Unit → Fin r → 𝕜) → Matrix Unit (Fin r) 𝕜) (fun (i : Unit) (j : Fin r) ↦ M (inr i) (inl j)) i j :
            𝕜)
          (0 i j : 𝕜)
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ((List.map toMatrix L).prod * (M * transvection (inl i) (inr ()) 1) * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
exact hLL'
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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) 𝕜
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
⊢ ∃ (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⟩

Premises used: Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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₁₁
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
⊢ ∃ (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₀⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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

Tactic:
⟨L₀.map (sumInl Unit) ++ L₁, L₁' ++ L₀'.map (sumInl Unit),
      Sum.elim D₀ fun _ => M' (inr unit) (inr unit), ?_⟩

Premises used: Unit.unit, List.map, Matrix.TransvectionStruct.sumInl, Unit, Sum.inr, Exists.intro, HAppend.hAppend, Sum.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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.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 ()))
⊢ ∃ (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:
refine
    ⟨L₀.map (sumInl Unit) ++ L₁, L₁' ++ L₀'.map (sumInl Unit),
      Sum.elim D₀ fun _ => M' (inr unit) (inr unit), ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 :
  (List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
    diagonal (Sum.elim D₀ fun (x : Unit) ↦ c)
⊢ (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:
simpa [M', c, Matrix.mul_assoc]

Premises used: Matrix.mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 ())
suffices :
  (List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
    diagonal (Sum.elim D₀ fun (x : Unit) ↦ c)
⊢ (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:
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]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 ())
rw : fromBlocks M'.toBlocks₁₁ 0 0 M'.toBlocks₂₂ = fromBlocks M'' 0 0 (diagonal fun (x : Unit) ↦ c)
⊢ M' = fromBlocks M'' 0 0 (diagonal fun (x : Unit) ↦ c)

Tactic:
rw [← fromBlocks_toBlocks M', hM.1, hM.2]

Premises used: Matrix.fromBlocks_toBlocks, And.right, And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 ())
⊢ fromBlocks M'.toBlocks₁₁ 0 0 M'.toBlocks₂₂ = fromBlocks M'' 0 0 (diagonal fun (x : Unit) ↦ c)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)

Tactic:
have : M' = fromBlocks M'' 0 0 (diagonal fun _ => c) := by
    rw [← fromBlocks_toBlocks M', hM.1, hM.2]
    rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
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)
⊢ (List.map (toMatrix ∘ sumInl Unit) L₀).prod * M' * (List.map (toMatrix ∘ sumInl Unit) L₀').prod =
    diagonal (Sum.elim D₀ fun (x : Unit) ↦ c)

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 * 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:
simp [h₀]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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
⊢ ∃ (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₀⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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

Tactic:
⟨L₀.map (reindexEquiv e.symm), L₀'.map (reindexEquiv e.symm), D₀ ∘ e, ?_⟩

Premises used: List.map, Function.comp, Exists.intro, Matrix.TransvectionStruct.reindexEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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₀
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))
⊢ ∃ (L : List (TransvectionStruct p 𝕜)) (L' : List (TransvectionStruct p 𝕜)) (D : p → 𝕜),
    (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
refine ⟨L₀.map (reindexEquiv e.symm), L₀'.map (reindexEquiv e.symm), D₀ ∘ e, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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₀
⊢ M =
    (reindexAlgEquiv 𝕜 𝕜 e.symm : (a : Matrix n n 𝕜) → Matrix p p 𝕜)
      ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix p p 𝕜) → Matrix n n 𝕜) M)

Tactic:
simp only [Equiv.symm_symm, submatrix_submatrix, reindex_apply, submatrix_id_id,
      Equiv.symm_comp_self, reindexAlgEquiv_apply]

Premises used: Equiv.symm_comp_self, Matrix.reindex_apply, Equiv.symm_symm, Matrix.submatrix_id_id, Matrix.submatrix_submatrix, Matrix.reindexAlgEquiv_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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₀
⊢ 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]