awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have A : List.map toMatrix L = listTransvecCol M
Tactic: have A : L.map toMatrix = listTransvecCol M := by simp [L, listTransvecCol, Function.comp_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have B : List.map toMatrix L' = listTransvecRow M
Tactic: have B : L'.map toMatrix = listTransvecRow M := by simp [L', listTransvecRow, Function.comp_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
B : List.map toMatrix L' = listTransvecRow M
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have rw : ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal
Tactic: rw [A, B]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have pos : ∀ (H : M.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: by_cases H : IsTwoBlockDiagonal M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
pos :
  ∀ (H : M.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
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have neg : ∀ (H : ¬M.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: by_cases H : IsTwoBlockDiagonal M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.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
have pos : ∀ (hM : M (inr ()) (inr ()) = 0),
  ∃ (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: by_cases hM : M (inr unit) (inr unit) = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
pos :
  ∀ (hM : M (inr ()) (inr ()) = 0),
    ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
      ((List.map toMatrix L).prod * M * (List.map toMatrix 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
have neg : ∀ (hM : ¬M (inr ()) (inr ()) = 0),
  ∃ (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: by_cases hM : M (inr unit) (inr unit) = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : M (inr ()) (inr ()) = 0
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have 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 : 𝕜)
Tactic: simp only [not_and_or, IsTwoBlockDiagonal, toBlocks₁₂, toBlocks₂₁, ← Matrix.ext_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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), M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
have inl : ∀
  (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 : Fin r), M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 (Sum.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) (Sum.inl j)) i
              j :
            𝕜)
          (0 i j : 𝕜)
inl :
  ∀
    (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 (Sum.inl i) (inr j))
                i j :
              𝕜)
            (0 i j : 𝕜)),
    ∃ (i : Fin r), M (Sum.inl i) (inr ()) ≠ 0 ∨ M (inr ()) (Sum.inl i) ≠ 0
⊢ ∃ (i : Fin r), M (Sum.inl i) (inr ()) ≠ 0 ∨ M (inr ()) (Sum.inl i) ≠ 0
have inr : ∀
  (H :
    ¬∀ (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) (Sum.inl j)) i
              j :
            𝕜)
          (0 i j : 𝕜)),
  ∃ (i : Fin r), M (Sum.inl i) (inr ()) ≠ 0 ∨ M (inr ()) (Sum.inl i) ≠ 0
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : Fin r), M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
have inl : ∀ (H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0) (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 : 𝕜)
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  ¬∀ (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), M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
have inr : ∀ (H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0) (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 : 𝕜)
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
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 : 𝕜)
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have this : ∃ (i : Fin r), M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
Tactic: have : ∃ i : Fin r, M (inl i) (inr unit) ≠ 0 ∨ M (inr unit) (inl i) ≠ 0 := by
    rcases H with H | H
    · contrapose! H
      rintro i ⟨⟩
      exact (H i).1
    · contrapose! H
      rintro ⟨⟩ j
      exact (H j).2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : 𝕜)
this : ∃ (i : Fin r), M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have pos : ∀ (i : Fin r) (h : M (inl i) (inr ()) ≠ 0),
  ∃ (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: rcases this with ⟨i, h | h⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : 𝕜)
this : ∃ (i : Fin r), M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
pos :
  ∀ (i : Fin r) (h : M (inl i) (inr ()) ≠ 0),
    ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
      ((List.map toMatrix L).prod * M * (List.map toMatrix 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
have pos₁ : ∀ (i : Fin r) (h : M (inr ()) (inl i) ≠ 0),
  ∃ (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: rcases this with ⟨i, h | h⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
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 (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have hM' : M' (inr ()) (inr ()) ≠ 0
Tactic: have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [M', hM]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
hM' : M' (inr ()) (inr ()) ≠ 0
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have pos : ∀ (L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜))
  (hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix 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: rcases exists_isTwoBlockDiagonal_of_ne_zero M' hM' with ⟨L, L', hLL'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
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 (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
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
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have hLL'₁ : ((List.map toMatrix L).prod * (M' * (List.map toMatrix L').prod)).IsTwoBlockDiagonal
Tactic: rw [Matrix.mul_assoc] at hLL'
Cleared hypotheses: hLL'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
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
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have pos : ((List.map toMatrix (L ++ [{ i := inr (), j := inl i, hij := sorry, c := 1 : TransvectionStruct (Fin r ⊕ Unit) 𝕜 }])).prod *
      M *
    (List.map toMatrix L').prod).IsTwoBlockDiagonal
Tactic: refine ⟨L ++ [⟨inr unit, inl i, by simp, 1⟩], L', ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
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
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have hM' : M' (inr ()) (inr ()) ≠ 0
Tactic: have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [M', hM]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have pos : ∀ (L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜))
  (hLL' : ((List.map toMatrix L).prod * M' * (List.map toMatrix 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: rcases exists_isTwoBlockDiagonal_of_ne_zero M' hM' with ⟨L, L', hLL'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have pos : ((List.map toMatrix L).prod * M *
    (List.map toMatrix
        ({ i := inl i, j := inr (), hij := sorry, c := 1 : TransvectionStruct (Fin r ⊕ Unit) 𝕜 } ::
          L')).prod).IsTwoBlockDiagonal
Tactic: refine ⟨L, ⟨inl i, inr unit, by simp, 1⟩::L', ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
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 *
      (List.map toMatrix
          ({ i := inl i, j := inr (), hij := ⋯, c := 1 : TransvectionStruct (Fin r ⊕ Unit) 𝕜 } ::
            L')).prod).IsTwoBlockDiagonal
have pos : ((List.map toMatrix L).prod * M * transvection (inl i) (inr ()) 1 * (List.map toMatrix L').prod).IsTwoBlockDiagonal
Tactic: simp only [← Matrix.mul_assoc, toMatrix_mk, List.prod_cons, List.map]