[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ ker (↑toLin' (diagonal w)) = ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
rw [← comap_bot, ← iInf_ker_proj, comap_iInf]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ ⨅ (i : m), comap (↑toLin' (diagonal w)) (ker (proj i)) =
    ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
have := fun i : m => ker_comp (toLin' (diagonal w)) (proj i)
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
this : ∀ (i : m), ker (comp (proj i) (↑toLin' (diagonal w))) = comap (↑toLin' (diagonal w)) (ker (proj i))
⊢ ⨅ (i : m), comap (↑toLin' (diagonal w)) (ker (proj i)) =
    ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
simp only [comap_iInf, ← this, proj_diagonal, ker_smul']
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
this : ∀ (i : m), ker (comp (proj i) (↑toLin' (diagonal w))) = comap (↑toLin' (diagonal w)) (ker (proj i))
⊢ ⨅ (i : m) (_ : w i ≠ 0), ker (proj i) =
    ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
have : univ ⊆ {i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ := by rw [Set.union_compl_self]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
this : ∀ (i : m), ker (comp (proj i) (↑toLin' (diagonal w))) = comap (↑toLin' (diagonal w)) (ker (proj i))
⊢ univ ⊆ {i | w i = 0} ∪ {i | w i = 0}ᶜ
[PROOFSTEP]
rw [Set.union_compl_self]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
this✝ : ∀ (i : m), ker (comp (proj i) (↑toLin' (diagonal w))) = comap (↑toLin' (diagonal w)) (ker (proj i))
this : univ ⊆ {i | w i = 0} ∪ {i | w i = 0}ᶜ
⊢ ⨅ (i : m) (_ : w i ≠ 0), ker (proj i) =
    ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
exact (iSup_range_stdBasis_eq_iInf_ker_proj K (fun _ : m => K) disjoint_compl_right this (Set.toFinite _)).symm
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ LinearMap.range (↑toLin' (diagonal w)) =
    ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
dsimp only [mem_setOf_eq]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ LinearMap.range (↑toLin' (diagonal w)) =
    ⨆ (i : m) (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
rw [← Submodule.map_top, ← iSup_range_stdBasis, Submodule.map_iSup]
[GOAL]
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ ⨆ (i : m), Submodule.map (↑toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i)) =
    ⨆ (i : m) (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
congr
[GOAL]
case e_s
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
⊢ (fun i => Submodule.map (↑toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i))) = fun i =>
    ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
funext i
[GOAL]
case e_s.h
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
K : Type u
inst✝¹ : Semifield K
inst✝ : DecidableEq m
w : m → K
i : m
⊢ Submodule.map (↑toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i)) =
    ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
[PROOFSTEP]
rw [← LinearMap.range_comp, diagonal_comp_stdBasis, ← range_smul']
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
have hu : univ ⊆ {i : m | w i = 0}ᶜ ∪ {i : m | w i = 0} := by rw [Set.compl_union_self]
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
⊢ univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
[PROOFSTEP]
rw [Set.compl_union_self]
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
have hd : Disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := disjoint_compl_left
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
have B₁ := iSup_range_stdBasis_eq_iInf_ker_proj K (fun _ : m => K) hd hu (Set.toFinite _)
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
B₁ :
  ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), range (stdBasis K (fun x => K) i) = ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
have B₂ := iInfKerProjEquiv K (fun _ ↦ K) hd hu
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
B₁ :
  ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), range (stdBasis K (fun x => K) i) = ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
B₂ : { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i
⊢ rank (↑toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
[PROOFSTEP]
rw [LinearMap.rank, range_diagonal, B₁, ← @rank_fun' K]
[GOAL]
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
B₁ :
  ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), range (stdBasis K (fun x => K) i) = ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
B₂ : { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i
⊢ Module.rank K { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } = Module.rank K ({ i // w i ≠ 0 } → K)
[PROOFSTEP]
apply LinearEquiv.rank_eq
[GOAL]
case f
m : Type u_1
n : Type u_2
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
hu : univ ⊆ {i | w i = 0}ᶜ ∪ {i | w i = 0}
hd : Disjoint {i | w i ≠ 0} {i | w i = 0}
B₁ :
  ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), range (stdBasis K (fun x => K) i) = ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
B₂ : { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } ≃ₗ[K] (i : ↑{i | w i ≠ 0}) → (fun x => K) ↑i
⊢ { x // x ∈ ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i) } ≃ₗ[K] { i // w i ≠ 0 } → K
[PROOFSTEP]
apply B₂
