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) 𝕜
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

Tactic:
exists_isTwoBlockDiagonal_of_ne_zero M hM

Premises used: Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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

Tactic:
exact exists_isTwoBlockDiagonal_of_ne_zero M hM

Premises used: Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : M (inr ()) (inr ()) = 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 : 𝕜)) ∨
    ¬∀ (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

Premises used: Matrix.IsTwoBlockDiagonal, Matrix.toBlocks₁₂, Matrix.toBlocks₂₁, not_and_or, Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (Sum.inr ()) (Sum.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) (Sum.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 (Sum.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) (Sum.inr j)) i j :
              𝕜)
            (0 i j : 𝕜)),
    ∃ (i : Fin r), M (Sum.inl i) (Sum.inr ()) ≠ 0 ∨ M (Sum.inr ()) (Sum.inl i) ≠ 0
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 (Sum.inr i) (Sum.inl j)) i j :
              𝕜)
            (0 i j : 𝕜)),
    ∃ (i : Fin r), M (Sum.inl i) (Sum.inr ()) ≠ 0 ∨ M (Sum.inr ()) (Sum.inl i) ≠ 0
⊢ ∃ (i : Fin r), M (Sum.inl i) (Sum.inr ()) ≠ 0 ∨ M (Sum.inr ()) (Sum.inl i) ≠ 0

Tactic:
rcases H with H | H
-- 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 (Sum.inl i) (inr j)) i
            j :
          𝕜)
        (0 i j : 𝕜)
inl :
  ∀ (H : ∀ (i : Fin r), M (Sum.inl i) (inr ()) = 0 ∧ M (inr ()) (Sum.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 (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

Tactic:
contrapose! H
-- 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), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
i : Fin r
⊢ 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
        PUnit.unit :
      𝕜)
    (0 i PUnit.unit : 𝕜)

Tactic:
(H i).1

Premises used: And.left
-- 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), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
i : Fin r
⊢ 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
        PUnit.unit :
      𝕜)
    (0 i PUnit.unit : 𝕜)

Tactic:
exact (H i).1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (Sum.inr ()) (Sum.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 (Sum.inr i) (inl j)) i
            j :
          𝕜)
        (0 i j : 𝕜)
inr :
  ∀ (H : ∀ (i : Fin r), M (inl i) (Sum.inr ()) = 0 ∧ M (Sum.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 (Sum.inr i) (inl j)) i j :
        𝕜)
      (0 i j : 𝕜)
⊢ ∃ (i : Fin r), M (inl i) (Sum.inr ()) ≠ 0 ∨ M (Sum.inr ()) (inl i) ≠ 0

Tactic:
contrapose! H
-- 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), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
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)) PUnit.unit
        j :
      𝕜)
    (0 PUnit.unit j : 𝕜)

Tactic:
(H j).2

Premises used: And.right
-- 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), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
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)) PUnit.unit
        j :
      𝕜)
    (0 PUnit.unit j : 𝕜)

Tactic:
exact (H j).2

Premises used: And.right
-- 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), 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
-- 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 : 𝕜)
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
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
⊢ ∃ (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⟩

Premises used: Matrix.TransvectionStruct.i
-- 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 (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
⊢ M' (inr ()) (inr ()) ≠ 0

Tactic:
simpa [M', hM]
-- 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 (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
⊢ M' (inr ()) (inr ()) ≠ 0

Tactic:
have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [M', hM]
-- 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 (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
hM' : M' (inr ()) (inr ()) ≠ 0
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
⊢ ∃ (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'⟩

Premises used: Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero
-- 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 (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
⊢ ((List.map toMatrix L).prod * (M' * (List.map toMatrix L').prod)).IsTwoBlockDiagonal

Tactic:
rw [Matrix.mul_assoc] at hLL'

Premises used: Matrix.mul_assoc
-- 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 (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
⊢ inr () ≠ inl i

Tactic:
simp
-- 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 (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
pos :
  ((List.map toMatrix
            (L ++ [{ i := inr (), j := inl i, hij := ⋯, c := 1 : TransvectionStruct (Fin r ⊕ Unit) 𝕜 }])).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:
refine ⟨L ++ [⟨inr unit, inl i, 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 (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
pos :
  ((List.map toMatrix L).prod * (transvection (inr ()) (inl i) 1 * M * (List.map toMatrix L').prod)).IsTwoBlockDiagonal
⊢ ((List.map toMatrix
            (L ++ [{ i := inr (), j := inl i, hij := ⋯, c := 1 : TransvectionStruct (Fin r ⊕ Unit) 𝕜 }])).prod *
        M *
      (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
simp only [List.map_append, List.prod_append, Matrix.mul_one, toMatrix_mk, List.prod_cons,
      List.prod_nil, List.map, Matrix.mul_assoc (L.map toMatrix).prod]

Premises used: List.prod_append, List.map, Matrix.mul_assoc, Matrix.TransvectionStruct.toMatrix, Matrix.TransvectionStruct.toMatrix_mk, List.prod_nil, Matrix.mul_one, List.map_append, List.prod_cons, 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 (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
⊢ ((List.map toMatrix L).prod * (transvection (inr ()) (inl i) 1 * M * (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 (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
⊢ ((List.map toMatrix L).prod * (transvection (inr ()) (inl i) 1 * M * (List.map toMatrix L').prod)).IsTwoBlockDiagonal

Tactic:
exact 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
⊢ M' (inr ()) (inr ()) ≠ 0

Tactic:
simpa [M', hM]
-- 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
⊢ M' (inr ()) (inr ()) ≠ 0

Tactic:
have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [M', hM]
-- 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
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
⊢ ∃ (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'⟩

Premises used: Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero
-- 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
⊢ inl i ≠ inr ()

Tactic:
simp