awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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₁ :
  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)
⊢ M =
    (List.map toMatrix (List.map TransvectionStruct.inv L.reverse)).prod * diagonal D *
      (List.map toMatrix (List.map 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]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
rw₃ rw₄ : M = 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:
rw [reverse_inv_prod_mul_prod, prod_mul_reverse_inv_prod, Matrix.one_mul, Matrix.mul_one]

Premises used: Matrix.TransvectionStruct.prod_mul_reverse_inv_prod, Matrix.mul_one, Matrix.TransvectionStruct.reverse_inv_prod_mul_prod, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
rcases :
  ∀ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜)
    (h : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod), P M
⊢ P M

Tactic:
rcases exists_list_transvec_mul_diagonal_mul_list_transvec M with ⟨L, L', D, h⟩

Premises used: Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ (diagonal D).det = M.det

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
have : ∀ (PD : P (diagonal D)), P M
⊢ P M

Tactic:
have PD : P (diagonal D) := hdiag D (by simp [h])
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
rw : P ((List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod)
⊢ P M

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
a : P (diagonal D)
⊢ P ((List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod)

Tactic:
apply H L L'
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 (diagonal D)

Tactic:
PD
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 (diagonal D)

Tactic:
exact PD
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
suffices :
  ∀ (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

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
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 : P (E * (List.map toMatrix L₂).prod)
⊢ P (List.prod (List.map toMatrix []) * E * (List.map toMatrix L₂).prod)

Tactic:
simp only [Matrix.one_mul, List.prod_nil, List.map]

Premises used: List.map, List.prod_nil, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
E : Matrix n n 𝕜
PE : P E
⊢ P (E * List.prod (List.map toMatrix []))

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
nil : P (E * t.toMatrix * (List.map toMatrix L₂).prod)
⊢ P (E * (List.map toMatrix (t :: L₂)).prod)

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

Premises used: List.map, Matrix.mul_assoc, List.prod_cons
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
nil : P (E * t.toMatrix)
⊢ P (E * t.toMatrix * (List.map toMatrix L₂).prod)

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

Tactic:
hmul _ _ PE (htransvec _)
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)

Tactic:
exact hmul _ _ PE (htransvec _)
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 []))
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)
⊢ P (E * (List.map toMatrix 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 _)

Premises used: List.map, Matrix.mul_assoc, List.prod_cons
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
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)))
⊢ P ((List.map toMatrix (t :: L₁)).prod * E * (List.map toMatrix L₂).prod)

Tactic:
simp only [Matrix.mul_assoc, List.prod_cons, List.map] at IH ⊢

Premises used: List.map, Matrix.mul_assoc, List.prod_cons
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 (t.toMatrix * ((List.map toMatrix L₁).prod * (E * (List.map toMatrix L₂).prod)))

Tactic:
hmul _ _ (htransvec _) IH
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 (t.toMatrix * ((List.map toMatrix L₁).prod * (E * (List.map toMatrix L₂).prod)))

Tactic:
exact hmul _ _ (htransvec _) IH
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
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)
⊢ P ((List.map toMatrix 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

Premises used: List.map, Matrix.mul_assoc, List.prod_nil, List.prod_cons, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
let : P M
⊢ P M

Tactic:
let Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
hmul₁ : ∀ (A B : Matrix n n 𝕜), Q A → Q B → Q (A * B)
⊢ Q M

Tactic:
apply diagonal_transvection_induction Q M

Premises used: Matrix.diagonal_transvection_induction
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ ∀ (D : n → 𝕜), (diagonal D).det = M.det → Q (diagonal D)

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
t : TransvectionStruct n 𝕜
⊢ t.toMatrix.det ≠ 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
t : TransvectionStruct n 𝕜
⊢ Q t.toMatrix

Tactic:
exact ⟨by simp, htransvec t⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
A B : Matrix n n 𝕜
QA : Q A
QB : Q B
⊢ (A * B).det ≠ 0

Tactic:
simp [QA.1, QB.1]

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
A B : Matrix n n 𝕜
QA : Q A
QB : Q B
⊢ Q (A * B)

Tactic:
exact ⟨by simp [QA.1, QB.1], hmul A B QA.1 QB.1 QA.2 QB.2⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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

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⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
this : Q M
⊢ P M

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
this : Q M
⊢ P M

Tactic:
exact this.2

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.Matrix.Unique
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
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
⊢ (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

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Unique
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
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:
simp [Subsingleton.elim i default, Subsingleton.elim j default]

Premises used: Inhabited.default, Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.Unique
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst : Unique m
inst_1 : Unique n
a : A
⊢ (fun (M : Matrix m n A) ↦ M default default)
      ((fun (a : A) ↦ ((of : (a : m → n → A) → Matrix m n A) fun (x : m) (x_1 : n) ↦ a : Matrix m n A)) a) =
    a

Tactic:
simp