-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem diagonal_transvection_induction (P : Matrix n n 𝕜 → Prop) (M : Matrix n n 𝕜)
    (hdiag : ∀ D : n → 𝕜, det (diagonal D) = det M → P (diagonal D))
    (htransvec : ∀ t : TransvectionStruct n 𝕜, P t.toMatrix) (hmul : ∀ A B, P A → P B → P (A * B)) :
    P M

Proof state:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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

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

Result:
case intro.intro.intro
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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

Proof state:
case a
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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

Result:
no goals

Proof state:
case intro.intro.intro.nil.cons.PE
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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 𝕜), 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 _)

Result:
no goals

Proof state:
case intro.intro.intro
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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)

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

Result:
no goals

Proof state:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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]

Result:
no goals

Proof state:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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

Tactic:
rw [h]

Result:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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 ((List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod)

Proof state:
case intro.intro.intro
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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

Tactic:
have PD : P (diagonal D) := hdiag D (by simp [h])

Result:
case intro.intro.intro
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : 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