Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: case pos
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
hs : s.card = M.rank
e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
  (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
he : e = (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
i : m
hi : i ∈ s
⊢ 1 = ((Sum.elim (fun x ↦ 1) fun x ↦ 0) ∘ ⇑e) i

pp: case neg
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
hs : s.card = M.rank
e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
  (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
he : e = (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
i : m
hi : i ∉ s
⊢ 0 = ((Sum.elim (fun x ↦ 1) fun x ↦ 0) ∘ ⇑e) i

Tactic:
<;>

Goal state after:
case pos
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
hs : s.card = M.rank
e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
  (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
he : e = (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
i : m
hi : i ∈ s
⊢ 1 = ((Sum.elim (fun x ↦ 1) fun x ↦ 0) ∘ ⇑e) i

case neg
m : Type um
R : Type uR
inst✝² : Field R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
L L' : List (TransvectionStruct m R)
D : m → R
hM0 : M = (List.map toMatrix L).prod * diagonal D * (List.map toMatrix L').prod
E : m → R := fun i ↦ if D i = 0 then 1 else (D i)⁻¹
E_def : E = fun i ↦ if D i = 0 then 1 else (D i)⁻¹
s : Finset m := {i | D i ≠ 0}
s_def : s = {i | D i ≠ 0}
V : Matrix m m R := diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
V_def : V = diagonal E * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod
U : Matrix m m R := (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
U_def : U = (List.map (toMatrix ∘ TransvectionStruct.inv) L'.reverse).prod
hUdet : IsUnit U.det
hVdet : IsUnit V.det
hM : V * M * U = diagonal fun i ↦ if i ∈ s then 1 else 0
hs : s.card = M.rank
e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank) :=
  (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
he : e = (Equiv.sumCompl fun x ↦ x ∈ s).symm.trans ((Finset.equivFinOfCardEq hs).sumCongr (Fintype.equivFinOfCardEq ⋯))
i : m
hi : i ∉ s
⊢ 0 = ((Sum.elim (fun x ↦ 1) fun x ↦ 0) ∘ ⇑e) i