awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ ∃ (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 : ∀ (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_3 : Fintype n] [inst_4 : 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype 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 have : ∀ (e : n ≃ Fin (Fintype.card n)),
  ∃ (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 (Fintype.card n) := Fintype.equivOfCardEq (by simp)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card 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 apply : ∃ (L : List (TransvectionStruct (Fin (Fintype.card n)) 𝕜)) (L' : List (TransvectionStruct (Fin (Fintype.card n)) 𝕜)) (D
  : Fin (Fintype.card n) → 𝕜),
  HMul.hMul (β := Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) (List.map toMatrix L).prod
        ((reindexAlgEquiv 𝕜 𝕜 e : (a : Matrix n n 𝕜) → Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) M :
          Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) 𝕜) *
      (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:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
have rcases : ∀ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜)
  (h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D),
  ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
Tactic: rcases exists_list_transvec_mul_mul_list_transvec_eq_diagonal M with ⟨L, L', D, h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ (L : List (TransvectionStruct n 𝕜)) (L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
    M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
have refine : M =
  (List.map toMatrix (List.map TransvectionStruct.inv L.reverse)).prod * diagonal D *
    (List.map toMatrix (List.map TransvectionStruct.inv L'.reverse)).prod
Tactic: refine ⟨L.reverse.map TransvectionStruct.inv, L'.reverse.map TransvectionStruct.inv, D, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ M =
    (List.map toMatrix (List.map TransvectionStruct.inv L.reverse)).prod * diagonal D *
      (List.map toMatrix (List.map TransvectionStruct.inv L'.reverse)).prod
have M₁ : M =
  (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod * M *
    ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
Tactic: suffices
    M =
      (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (L.map toMatrix).prod * M *
        ((L'.map toMatrix).prod * (L'.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod)
    by simpa [← h, Matrix.mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
⊢ M =
    (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod * M *
      ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
have rw : M = 1 * M * ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
Tactic: rw [reverse_inv_prod_mul_prod, prod_mul_reverse_inv_prod, Matrix.one_mul, Matrix.mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
rw : M = 1 * M * ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
⊢ M =
    (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod * M *
      ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
have rw₁ : M = 1 * M * 1
Tactic: rw [reverse_inv_prod_mul_prod, prod_mul_reverse_inv_prod, Matrix.one_mul, Matrix.mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
rw : M = 1 * M * ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
rw₁ : M = 1 * M * 1
⊢ M =
    (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod * M *
      ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
have rw₂ : M = M * 1
Tactic: rw [reverse_inv_prod_mul_prod, prod_mul_reverse_inv_prod, Matrix.one_mul, Matrix.mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 𝕜
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
rw : M = 1 * M * ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
rw₁ : M = 1 * M * 1
rw₂ : M = M * 1
⊢ M =
    (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod * M *
      ((List.map toMatrix L').prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod)
have rw₃ : M = M
Tactic: rw [reverse_inv_prod_mul_prod, prod_mul_reverse_inv_prod, Matrix.one_mul, Matrix.mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
⊢ P M
have rcases : ∀ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜)
  (h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod), P M
Tactic: rcases exists_list_transvec_mul_diagonal_mul_list_transvec M with ⟨L, L', D, h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
⊢ P M
have have : ∀ (PD : P (diagonal D)), P M
Tactic: have PD : P (diagonal D) := hdiag D (by simp [h])
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
⊢ P M
have rw : P ((List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
⊢ P M
have suffices : ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
  P E → P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
Tactic: suffices H :
    ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
      P E → P ((L₁.map toMatrix).prod * E * (L₂.map toMatrix).prod) by
    rw [h]
    apply H L L'
    exact PD
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (List.prod (List.map toMatrix []) * E * (List.map toMatrix L₂).prod)
have nil : P (E * (List.map toMatrix L₂).prod)
Tactic: simp only [Matrix.one_mul, List.prod_nil, List.map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
t : TransvectionStruct n 𝕜
L₂ : List (TransvectionStruct n 𝕜)
IH : ∀ (E : Matrix n n 𝕜) (PE : P E), P (E * (List.map toMatrix L₂).prod)
E : Matrix n n 𝕜
PE : P E
⊢ P (E * (List.map toMatrix (t :: L₂)).prod)
have nil : P (E * t.toMatrix * (List.map toMatrix L₂).prod)
Tactic: simp only [← Matrix.mul_assoc, List.prod_cons, List.map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
t : TransvectionStruct n 𝕜
L₂ : List (TransvectionStruct n 𝕜)
IH : ∀ (E : Matrix n n 𝕜) (PE : P E), P (E * (List.map toMatrix L₂).prod)
E : Matrix n n 𝕜
PE : P E
⊢ P (E * t.toMatrix * (List.map toMatrix L₂).prod)
have nil : P (E * t.toMatrix)
Tactic: apply IH
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (E * (List.map toMatrix L₂).prod)
have nil : ∀ (E : Matrix n n 𝕜) (PE : P E), P (E * List.prod (List.map toMatrix []))
Tactic: induction L₂ generalizing E with
    | nil => simpa
    | cons t L₂ IH =>
      simp only [← Matrix.mul_assoc, List.prod_cons, List.map]
      apply IH
      exact hmul _ _ PE (htransvec _)
Cleared hypotheses: L₂, E, PE
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
nil : ∀ (E : Matrix n n 𝕜) (PE : P E), P (E * List.prod (List.map toMatrix []))
⊢ P (E * (List.map toMatrix L₂).prod)
have nil₁ : ∀ (t : TransvectionStruct n 𝕜) (L₂ : List (TransvectionStruct n 𝕜))
  (IH : ∀ (E : Matrix n n 𝕜) (PE : P E), P (E * (List.map toMatrix L₂).prod)) (E : Matrix n n 𝕜) (PE : P E),
  P (E * (List.map toMatrix (t :: L₂)).prod)
Tactic: induction L₂ generalizing E with
    | nil => simpa
    | cons t L₂ IH =>
      simp only [← Matrix.mul_assoc, List.prod_cons, List.map]
      apply IH
      exact hmul _ _ PE (htransvec _)
Cleared hypotheses: L₂, E, PE
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
t : TransvectionStruct n 𝕜
L₁ : List (TransvectionStruct n 𝕜)
IH : P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
⊢ P ((List.map toMatrix (t :: L₁)).prod * E * (List.map toMatrix L₂).prod)
have cons : ∀ (IH : P ((List.map toMatrix L₁).prod * (E * (List.map toMatrix L₂).prod))),
  P (t.toMatrix * ((List.map toMatrix L₁).prod * (E * (List.map toMatrix L₂).prod)))
Tactic: simp only [Matrix.mul_assoc, List.prod_cons, List.map] at IH ⊢
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₁ L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
have nil : P (List.prod (List.map toMatrix []) * E * (List.map toMatrix L₂).prod)
Tactic: induction L₁ with
  | nil =>
    simp only [Matrix.one_mul, List.prod_nil, List.map]
    induction L₂ generalizing E with
    | nil => simpa
    | cons t L₂ IH =>
      simp only [← Matrix.mul_assoc, List.prod_cons, List.map]
      apply IH
      exact hmul _ _ PE (htransvec _)
  | cons t L₁ IH =>
    simp only [Matrix.mul_assoc, List.prod_cons, List.map] at IH ⊢
    exact hmul _ _ (htransvec _) IH
Cleared hypotheses: L₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hdiag : ∀ (D : n → 𝕜), (diagonal D).det = M.det → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
PD : P (diagonal D)
L₁ L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
nil : P (List.prod (List.map toMatrix []) * E * (List.map toMatrix L₂).prod)
⊢ P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)
have cons : ∀ (t : TransvectionStruct n 𝕜) (L₁ : List (TransvectionStruct n 𝕜))
  (IH : P ((List.map toMatrix L₁).prod * E * (List.map toMatrix L₂).prod)),
  P ((List.map toMatrix (t :: L₁)).prod * E * (List.map toMatrix L₂).prod)
Tactic: induction L₁ with
  | nil =>
    simp only [Matrix.one_mul, List.prod_nil, List.map]
    induction L₂ generalizing E with
    | nil => simpa
    | cons t L₂ IH =>
      simp only [← Matrix.mul_assoc, List.prod_cons, List.map]
      apply IH
      exact hmul _ _ PE (htransvec _)
  | cons t L₁ IH =>
    simp only [Matrix.mul_assoc, List.prod_cons, List.map] at IH ⊢
    exact hmul _ _ (htransvec _) IH
Cleared hypotheses: L₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := fun (N : Matrix n n 𝕜) ↦ N.det ≠ 0 ∧ P N
⊢ Q M
have hdiag₁ : ∀ (D : n → 𝕜), (diagonal D).det = M.det → Q (diagonal D)
Tactic: apply diagonal_transvection_induction Q M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := fun (N : Matrix n n 𝕜) ↦ N.det ≠ 0 ∧ P N
hdiag₁ : ∀ (D : n → 𝕜), (diagonal D).det = M.det → Q (diagonal D)
⊢ Q M
have htransvec₁ : ∀ (t : TransvectionStruct n 𝕜), Q t.toMatrix
Tactic: apply diagonal_transvection_induction Q M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := fun (N : Matrix n n 𝕜) ↦ N.det ≠ 0 ∧ P N
hdiag₁ : ∀ (D : n → 𝕜), (diagonal D).det = M.det → Q (diagonal D)
htransvec₁ : ∀ (t : TransvectionStruct n 𝕜), Q t.toMatrix
⊢ Q M
have hmul₁ : ∀ (A B : Matrix n n 𝕜), Q A → Q B → Q (A * B)
Tactic: apply diagonal_transvection_induction Q M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : DecidableEq n
inst_2 : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := fun (N : Matrix n n 𝕜) ↦ N.det ≠ 0 ∧ P N
⊢ P M
have this : Q M
Tactic: have : Q M := by
    apply diagonal_transvection_induction Q M
    · grind
    · intro t
      exact ⟨by simp, htransvec t⟩
    · intro A B QA QB
      exact ⟨by simp [QA.1, QB.1], hmul A B QA.1 QB.1 QA.2 QB.2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Unique (goal)
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst : Unique m
inst_1 : Unique n
M : Matrix m n A
⊢ (fun (a : A) ↦ ((of : (a : m → n → A) → Matrix m n A) fun (x : m) (x_1 : n) ↦ a : Matrix m n A))
      ((fun (M : Matrix m n A) ↦ M default default) M) =
    M
have a : ∀ (i : m) (j : n),
  (fun (a : A) ↦ ((of : (a : m → n → A) → Matrix m n A) fun (x : m) (x_1 : n) ↦ a : Matrix m n A))
      ((fun (M : Matrix m n A) ↦ M default default) M) i j =
    M i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
⊢ A.vec = B.vec ↔ A = B
have simp_rw : A.vec = B.vec ↔ ∀ (i : m) (j : n), A i j = B i j
Tactic: simp_rw [← Matrix.ext_iff, funext_iff, Prod.forall, @forall_comm m n, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
simp_rw : A.vec = B.vec ↔ ∀ (i : m) (j : n), A i j = B i j
⊢ A.vec = B.vec ↔ A = B
have simp_rw₁ : (∀ (x : n × m), A.vec x = B.vec x) ↔ ∀ (i : m) (j : n), A i j = B i j
Tactic: simp_rw [← Matrix.ext_iff, funext_iff, Prod.forall, @forall_comm m n, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
simp_rw : A.vec = B.vec ↔ ∀ (i : m) (j : n), A i j = B i j
simp_rw₁ : (∀ (x : n × m), A.vec x = B.vec x) ↔ ∀ (i : m) (j : n), A i j = B i j
⊢ A.vec = B.vec ↔ A = B
have simp_rw₂ : (∀ (a : n) (b : m), A.vec (a, b) = B.vec (a, b)) ↔ ∀ (i : m) (j : n), A i j = B i j
Tactic: simp_rw [← Matrix.ext_iff, funext_iff, Prod.forall, @forall_comm m n, vec]