m : Type u_1
n : Type ?u.179625
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' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
m : Type u_1
n : Type ?u.179625
inst✝⁴ : Fintype m
inst✝³ : Fintype n
K : Type u
inst✝² : Field K
inst✝¹ : DecidableEq m
inst✝ : DecidableEq K
w : m → K
⊢ rank (↑toLin' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
have hu : univ ⊆ { i : m | w i = 0 }ᶜ ∪ { i : m | w i = 0 } := by rw [Set.compl_union_self]
m : Type u_1
n : Type ?u.179625
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' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
m : Type u_1
n : Type ?u.179625
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' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
have hd : Disjoint { i : m | w i ≠ 0 } { i : m | w i = 0 } := disjoint_compl_left
m : Type u_1
n : Type ?u.179625
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}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)) =
    ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
⊢ rank (↑toLin' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
m : Type u_1
n : Type ?u.179625
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' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
have B₁ := iSup_range_stdBasis_eq_iInf_ker_proj K (fun _ : m => K) hd hu (Set.toFinite _)
m : Type u_1
n : Type ?u.179625
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}), LinearMap.range (LinearMap.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' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
m : Type u_1
n : Type ?u.179625
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}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)) =
    ⨅ (i : m) (_ : i ∈ {i | w i = 0}), ker (proj i)
⊢ rank (↑toLin' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
have B₂ := iInfKerProjEquiv K (fun _ ↦ K) hd hu
m : Type u_1
n : Type ?u.179625
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}), LinearMap.range (LinearMap.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)
m : Type u_1
n : Type ?u.179625
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}), LinearMap.range (LinearMap.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' (diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })
rw [rank, range_diagonal, B₁, ← @rank_fun' K]
case f
m : Type u_1
n : Type ?u.179625
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}), LinearMap.range (LinearMap.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
m : Type u_1
n : Type ?u.179625
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}), LinearMap.range (LinearMap.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)
apply LinearEquiv.rank_eq
no goals
case f
m : Type u_1
n : Type ?u.179625
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}), LinearMap.range (LinearMap.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
apply B₂
no goals
m : Type u_1
n : Type ?u.179625
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}
rw [Set.compl_union_self]