case intro.intro.intro
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
⊢ P M
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
⊢ P M
rcases exists_list_transvec_mul_diagonal_mul_list_transvec M with ⟨L, L', D, h⟩
case intro.intro.intro
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
⊢ P M
case intro.intro.intro
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
⊢ P M
have PD : P (diagonal D) := hdiag D (by simp [h])
case intro.intro.intro
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
⊢ P M

case H
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
⊢ ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
case intro.intro.intro
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
⊢ P M
suffices H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P ((L₁.map toMatrix).prod ⬝ E ⬝ (L₂.map toMatrix).prod)
case H
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
L₁ L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
case H
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
⊢ ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
intro L₁ L₂ E PE
case H.nil
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (List.prod (List.map toMatrix []) ⬝ E ⬝ List.prod (List.map toMatrix L₂))

case H.cons
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
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.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
⊢ P (List.prod (List.map toMatrix (t :: L₁)) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
case H
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
L₁ L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
induction' L₁ with t L₁ IH
no goals
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
⊢ det (diagonal D) = det M
simp [h]
case intro.intro.intro
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
⊢ P (List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L'))
case intro.intro.intro
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
⊢ P M
rw [h]
case intro.intro.intro.a
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
⊢ P (diagonal D)
case intro.intro.intro
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
⊢ P (List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L'))
apply H L L'
no goals
case intro.intro.intro.a
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
H :
  ∀ (L₁ L₂ : List (TransvectionStruct n 𝕜)) (E : Matrix n n 𝕜),
    P E → P (List.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
⊢ P (diagonal D)
exact PD
case H.nil
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ List.prod (List.map toMatrix L₂))
case H.nil
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (List.prod (List.map toMatrix []) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
simp only [Matrix.one_mul, List.prod_nil, List.map]
case H.nil.nil
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
E✝ : Matrix n n 𝕜
PE✝ : P E✝
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ List.prod (List.map toMatrix []))

case H.nil.cons
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
E✝ : Matrix n n 𝕜
PE✝ : P E✝
t : TransvectionStruct n 𝕜
L₂ : List (TransvectionStruct n 𝕜)
IH : ∀ (E : Matrix n n 𝕜), P E → P (E ⬝ List.prod (List.map toMatrix L₂))
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ List.prod (List.map toMatrix (t :: L₂)))
case H.nil
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
L₂ : List (TransvectionStruct n 𝕜)
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ List.prod (List.map toMatrix L₂))
induction' L₂ with t L₂ IH generalizing E
no goals
case H.nil.nil
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
E✝ : Matrix n n 𝕜
PE✝ : P E✝
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ List.prod (List.map toMatrix []))
simpa
case H.nil.cons
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
E✝ : Matrix n n 𝕜
PE✝ : P E✝
t : TransvectionStruct n 𝕜
L₂ : List (TransvectionStruct n 𝕜)
IH : ∀ (E : Matrix n n 𝕜), P E → P (E ⬝ List.prod (List.map toMatrix L₂))
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ toMatrix t ⬝ List.prod (List.map toMatrix L₂))
case H.nil.cons
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
E✝ : Matrix n n 𝕜
PE✝ : P E✝
t : TransvectionStruct n 𝕜
L₂ : List (TransvectionStruct n 𝕜)
IH : ∀ (E : Matrix n n 𝕜), P E → P (E ⬝ List.prod (List.map toMatrix L₂))
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ List.prod (List.map toMatrix (t :: L₂)))
simp only [← Matrix.mul_assoc, List.prod_cons, mul_eq_mul, List.map]
case H.nil.cons.PE
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
E✝ : Matrix n n 𝕜
PE✝ : P E✝
t : TransvectionStruct n 𝕜
L₂ : List (TransvectionStruct n 𝕜)
IH : ∀ (E : Matrix n n 𝕜), P E → P (E ⬝ List.prod (List.map toMatrix L₂))
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ toMatrix t)
case H.nil.cons
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
E✝ : Matrix n n 𝕜
PE✝ : P E✝
t : TransvectionStruct n 𝕜
L₂ : List (TransvectionStruct n 𝕜)
IH : ∀ (E : Matrix n n 𝕜), P E → P (E ⬝ List.prod (List.map toMatrix L₂))
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ toMatrix t ⬝ List.prod (List.map toMatrix L₂))
apply IH
no goals
case H.nil.cons.PE
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
PD : P (diagonal D)
E✝ : Matrix n n 𝕜
PE✝ : P E✝
t : TransvectionStruct n 𝕜
L₂ : List (TransvectionStruct n 𝕜)
IH : ∀ (E : Matrix n n 𝕜), P E → P (E ⬝ List.prod (List.map toMatrix L₂))
E : Matrix n n 𝕜
PE : P E
⊢ P (E ⬝ toMatrix t)
exact hmul _ _ PE (htransvec _)
case H.cons
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
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.prod (List.map toMatrix L₁) ⬝ (E ⬝ List.prod (List.map toMatrix L₂)))
⊢ P (toMatrix t ⬝ (List.prod (List.map toMatrix L₁) ⬝ (E ⬝ List.prod (List.map toMatrix L₂))))
case H.cons
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
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.prod (List.map toMatrix L₁) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
⊢ P (List.prod (List.map toMatrix (t :: L₁)) ⬝ E ⬝ List.prod (List.map toMatrix L₂))
simp only [Matrix.mul_assoc, List.prod_cons, mul_eq_mul, List.map] at IH⊢
no goals
case H.cons
n : Type u_1
p : Type ?u.330443
R : Type u₂
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
inst✝ : Fintype n
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 (toMatrix t)
hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A ⬝ B)
L L' : List (TransvectionStruct n 𝕜)
D : n → 𝕜
h : M = List.prod (List.map toMatrix L) ⬝ diagonal D ⬝ List.prod (List.map toMatrix L')
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.prod (List.map toMatrix L₁) ⬝ (E ⬝ List.prod (List.map toMatrix L₂)))
⊢ P (toMatrix t ⬝ (List.prod (List.map toMatrix L₁) ⬝ (E ⬝ List.prod (List.map toMatrix L₂))))
exact hmul _ _ (htransvec _) IH