case nil
n : Type u_1
p : Type ?u.35992
R : Type u₂
𝕜 : Type ?u.35997
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
⊢ List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse [])) ⬝ List.prod (List.map toMatrix []) = 1

case cons
n : Type u_1
p : Type ?u.35992
R : Type u₂
𝕜 : Type ?u.35997
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝ List.prod (List.map toMatrix L) = 1
⊢ List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse (t :: L))) ⬝
      List.prod (List.map toMatrix (t :: L)) =
    1
n : Type u_1
p : Type ?u.35992
R : Type u₂
𝕜 : Type ?u.35997
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
L : List (TransvectionStruct n R)
⊢ List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝ List.prod (List.map toMatrix L) = 1
induction' L with t L IH
no goals
case nil
n : Type u_1
p : Type ?u.35992
R : Type u₂
𝕜 : Type ?u.35997
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
⊢ List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse [])) ⬝ List.prod (List.map toMatrix []) = 1
simp
case cons
n : Type u_1
p : Type ?u.35992
R : Type u₂
𝕜 : Type ?u.35997
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝ List.prod (List.map toMatrix L) = 1
⊢ List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝
        (toMatrix (TransvectionStruct.inv t) ⬝ toMatrix t) ⬝
      List.prod (List.map toMatrix L) =
    1
case cons
n : Type u_1
p : Type ?u.35992
R : Type u₂
𝕜 : Type ?u.35997
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝ List.prod (List.map toMatrix L) = 1
⊢ List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse (t :: L))) ⬝
      List.prod (List.map toMatrix (t :: L)) =
    1
suffices
  (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod ⬝ (t.inv.toMatrix ⬝ t.toMatrix) ⬝
      (L.map toMatrix).prod = 1
  by simpa [Matrix.mul_assoc]
no goals
case cons
n : Type u_1
p : Type ?u.35992
R : Type u₂
𝕜 : Type ?u.35997
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝ List.prod (List.map toMatrix L) = 1
⊢ List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝
        (toMatrix (TransvectionStruct.inv t) ⬝ toMatrix t) ⬝
      List.prod (List.map toMatrix L) =
    1
simpa [inv_mul] using IH
no goals
n : Type u_1
p : Type ?u.35992
R : Type u₂
𝕜 : Type ?u.35997
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝ List.prod (List.map toMatrix L) = 1
this :
  List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse L)) ⬝
        (toMatrix (TransvectionStruct.inv t) ⬝ toMatrix t) ⬝
      List.prod (List.map toMatrix L) =
    1
⊢ List.prod (List.map (toMatrix ∘ TransvectionStruct.inv) (List.reverse (t :: L))) ⬝
      List.prod (List.map toMatrix (t :: L)) =
    1
simpa [Matrix.mul_assoc]