m : Type u_1
n : Type ?u.94396
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)
m : Type u_1
n : Type ?u.94396
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)
rw [← comap_bot, ← iInf_ker_proj, comap_iInf]
m : Type u_1
n : Type ?u.94396
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)
m : Type u_1
n : Type ?u.94396
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)
have := fun i : m => ker_comp (toLin' (diagonal w)) (proj i)
m : Type u_1
n : Type ?u.94396
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)
m : Type u_1
n : Type ?u.94396
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)
simp only [comap_iInf, ← this, proj_diagonal, ker_smul']
m : Type u_1
n : Type ?u.94396
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)
m : Type u_1
n : Type ?u.94396
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)
have : univ ⊆ { i : m | w i = 0 } ∪ { i : m | w i = 0 }ᶜ := by rw [Set.union_compl_self]
no goals
m : Type u_1
n : Type ?u.94396
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)
exact (iSup_range_stdBasis_eq_iInf_ker_proj K (fun _ : m => K) disjoint_compl_right this
  (Set.toFinite _)).symm
no goals
m : Type u_1
n : Type ?u.94396
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}ᶜ
rw [Set.union_compl_self]