case a
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ (⨆ (i : ι) (_ : p i), S i) ≤
    LinearMap.range
      (LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p))

case a
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ LinearMap.range
      (LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p)) ≤
    ⨆ (i : ι) (_ : p i), S i
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ (⨆ (i : ι) (_ : p i), S i) =
    LinearMap.range
      (LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p))
apply le_antisymm
case a
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ↑(LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p))
      (single i { val := y, property := hy }) =
    y
case a
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ (⨆ (i : ι) (_ : p i), S i) ≤
    LinearMap.range
      (LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p))
refine' iSup₂_le fun i hi y hy => ⟨Dfinsupp.single i ⟨y, hy⟩, _⟩
case a
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ↑(↑(lsum ℕ) fun i => Submodule.subtype (S i)) (single i { val := y, property := hy }) = y
case a
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ↑(LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p))
      (single i { val := y, property := hy }) =
    y
rw [LinearMap.comp_apply, filterLinearMap_apply, filter_single_pos _ _ hi]
no goals
case a
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ↑(↑(lsum ℕ) fun i => Submodule.subtype (S i)) (single i { val := y, property := hy }) = y
simp only [lsum_apply_apply, sumAddHom_single, LinearMap.toAddMonoidHom_coe, coeSubtype]
case a.intro
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
⊢ ↑(LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p)) v ∈
    ⨆ (i : ι) (_ : p i), S i
case a
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ LinearMap.range
      (LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p)) ≤
    ⨆ (i : ι) (_ : p i), S i
rintro x ⟨v, rfl⟩
case a.intro
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i ≠ 0
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (S i)) i)) i)
      (↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (i : ι) (_ : p i), S i
case a.intro
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
⊢ ↑(LinearMap.comp (↑(lsum ℕ) fun i => Submodule.subtype (S i)) (filterLinearMap R (fun i => { x // x ∈ S i }) p)) v ∈
    ⨆ (i : ι) (_ : p i), S i
refine' dfinsupp_sumAddHom_mem _ _ _ fun i _ => _
case a.intro
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i ≠ 0
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (S i)) i)) i)
      (↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
case a.intro
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i ≠ 0
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (S i)) i)) i)
      (↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (i : ι) (_ : p i), S i
refine' mem_iSup_of_mem i _
case pos
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i ≠ 0
hp : p i
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (S i)) i)) i)
      (↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i

case neg
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i ≠ 0
hp : ¬p i
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (S i)) i)) i)
      (↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
case a.intro
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i ≠ 0
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (S i)) i)) i)
      (↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
by_cases hp : p i
no goals
case pos
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i ≠ 0
hp : p i
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (S i)) i)) i)
      (↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
simp [hp]
no goals
case neg
ι : Type u_1
R : Type u_2
S✝ : Type ?u.366938
M : ι → Type ?u.366943
N : Type u_3
dec_ι : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), { x // x ∈ S i }
i : ι
x✝ : ↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i ≠ 0
hp : ¬p i
⊢ ↑((fun i => LinearMap.toAddMonoidHom ((fun i => Submodule.subtype (S i)) i)) i)
      (↑(↑(filterLinearMap R (fun i => { x // x ∈ S i }) p) v) i) ∈
    ⨆ (_ : p i), S i
simp [hp]