ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
⊢ a₁ ≤ a₂
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum f a₁
hg : HasSum g a₂
⊢ a₁ ≤ a₂
rw [← hasSum_extend_zero he] at hf
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
⊢ extend e f 0 c ≤ g c
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
⊢ a₁ ≤ a₂
refine hasSum_le (fun c => ?_) hf hg
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
i : ι
⊢ extend e f 0 (e i) ≤ g (e i)

case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
h : ¬c ∈ Set.range e
⊢ extend e f 0 c ≤ g c
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
⊢ extend e f 0 c ≤ g c
obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
i : ι
⊢ f i ≤ g (e i)
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
i : ι
⊢ extend e f 0 (e i) ≤ g (e i)
rw [he.extend_apply]
no goals
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
i : ι
⊢ f i ≤ g (e i)
exact h _
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
h : ¬c ∈ Set.range e
⊢ OfNat.ofNat 0 c ≤ g c
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
h : ¬c ∈ Set.range e
⊢ extend e f 0 c ≤ g c
rw [extend_apply' _ _ _ h]
no goals
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
h : ¬c ∈ Set.range e
⊢ OfNat.ofNat 0 c ≤ g c
exact hs _ h