m : Type u_1
n : Type ?u.147890
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)
m : Type u_1
n : Type ?u.147890
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)
dsimp only [mem_setOf_eq]
m : Type u_1
n : Type ?u.147890
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)
m : Type u_1
n : Type ?u.147890
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)
rw [← Submodule.map_top, ← iSup_range_stdBasis, Submodule.map_iSup]
case e_s
m : Type u_1
n : Type ?u.147890
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)
m : Type u_1
n : Type ?u.147890
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)
congr
case e_s.h
m : Type u_1
n : Type ?u.147890
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)
case e_s
m : Type u_1
n : Type ?u.147890
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)
funext i
no goals
case e_s.h
m : Type u_1
n : Type ?u.147890
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)
rw [← LinearMap.range_comp, diagonal_comp_stdBasis, ← range_smul']