-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasSum_lt {f g : α → ℝ≥0∞} {sf sg : ℝ≥0∞} {i : α} (h : ∀ a : α, f a ≤ g a) (hi : f i < g i)
    (hsf : sf ≠ ∞) (hf : HasSum f sf) (hg : HasSum g sg) : sf < sg

Proof state:
case neg.intro.intro.intro.intro
α : Type u_1
i : α
f g : α → ℝ≥0
sf : ℝ≥0
hf : HasSum (fun i => ↑(f i)) ↑sf
sg : ℝ≥0
hg : HasSum (fun i => ↑(g i)) ↑sg
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
⊢ sf < sg

Tactic:
exact NNReal.hasSum_lt h hi (ENNReal.hasSum_coe.1 hf) (ENNReal.hasSum_coe.1 hg)

Result:
no goals

Proof state:
case neg.intro.intro
α : Type u_1
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ⊤
hsg : ¬sg = ⊤
f : α → ℝ≥0
hf : HasSum (fun i => ↑(f i)) sf
g : α → ℝ≥0
hg : HasSum (fun i => ↑(g i)) sg
h : ∀ (a : α), (fun i => ↑(f i)) a ≤ (fun i => ↑(g i)) a
hi : (fun i => ↑(f i)) i < (fun i => ↑(g i)) i
⊢ sf < sg

Tactic:
lift sf to ℝ≥0 using hsf

Result:
case neg.intro.intro.intro
α : Type u_1
sg : ℝ≥0∞
i : α
hsg : ¬sg = ⊤
f g : α → ℝ≥0
hg : HasSum (fun i => ↑(g i)) sg
h : ∀ (a : α), (fun i => ↑(f i)) a ≤ (fun i => ↑(g i)) a
hi : (fun i => ↑(f i)) i < (fun i => ↑(g i)) i
sf : ℝ≥0
hf : HasSum (fun i => ↑(f i)) ↑sf
⊢ ↑sf < sg

Proof state:
case pos
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ⊤
hf : HasSum f sf
hg : HasSum g sg
hsg : sg = ⊤
⊢ sf < sg

Tactic:
exact hsg.symm ▸ lt_of_le_of_ne le_top hsf

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro
α : Type u_1
i : α
f g : α → ℝ≥0
h : ∀ (a : α), (fun i => ↑(f i)) a ≤ (fun i => ↑(g i)) a
hi : (fun i => ↑(f i)) i < (fun i => ↑(g i)) i
sf : ℝ≥0
hf : HasSum (fun i => ↑(f i)) ↑sf
sg : ℝ≥0
hg : HasSum (fun i => ↑(g i)) ↑sg
⊢ ↑sf < ↑sg

Tactic:
simp only [coe_le_coe, coe_lt_coe] at h hi ⊢

Result:
case neg.intro.intro.intro.intro
α : Type u_1
i : α
f g : α → ℝ≥0
sf : ℝ≥0
hf : HasSum (fun i => ↑(f i)) ↑sf
sg : ℝ≥0
hg : HasSum (fun i => ↑(g i)) ↑sg
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
⊢ sf < sg

Proof state:
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ⊤
hf : HasSum f sf
hg : HasSum g sg
⊢ sf < sg

Tactic:
by_cases hsg : sg = ∞

Result:
case pos
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ⊤
hf : HasSum f sf
hg : HasSum g sg
hsg : sg = ⊤
⊢ sf < sg

case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ⊤
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ⊤
⊢ sf < sg

Proof state:
case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ⊤
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ⊤
hg' : ∀ (x : α), g x ≠ ⊤
⊢ sf < sg

Tactic:
lift f to α → ℝ≥0 using fun x =>
  ne_of_lt (lt_of_le_of_lt (h x) <| lt_of_le_of_ne le_top (hg' x))

Result:
case neg.intro
α : Type u_1
g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ⊤
hg : HasSum g sg
hsg : ¬sg = ⊤
hg' : ∀ (x : α), g x ≠ ⊤
f : α → ℝ≥0
h : ∀ (a : α), (fun i => ↑(f i)) a ≤ g a
hi : (fun i => ↑(f i)) i < g i
hf : HasSum (fun i => ↑(f i)) sf
⊢ sf < sg

Proof state:
case neg.intro.intro.intro
α : Type u_1
sg : ℝ≥0∞
i : α
hsg : ¬sg = ⊤
f g : α → ℝ≥0
hg : HasSum (fun i => ↑(g i)) sg
h : ∀ (a : α), (fun i => ↑(f i)) a ≤ (fun i => ↑(g i)) a
hi : (fun i => ↑(f i)) i < (fun i => ↑(g i)) i
sf : ℝ≥0
hf : HasSum (fun i => ↑(f i)) ↑sf
⊢ ↑sf < sg

Tactic:
lift sg to ℝ≥0 using hsg

Result:
case neg.intro.intro.intro.intro
α : Type u_1
i : α
f g : α → ℝ≥0
h : ∀ (a : α), (fun i => ↑(f i)) a ≤ (fun i => ↑(g i)) a
hi : (fun i => ↑(f i)) i < (fun i => ↑(g i)) i
sf : ℝ≥0
hf : HasSum (fun i => ↑(f i)) ↑sf
sg : ℝ≥0
hg : HasSum (fun i => ↑(g i)) ↑sg
⊢ ↑sf < ↑sg

Proof state:
case neg.intro
α : Type u_1
g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ⊤
hg : HasSum g sg
hsg : ¬sg = ⊤
hg' : ∀ (x : α), g x ≠ ⊤
f : α → ℝ≥0
h : ∀ (a : α), (fun i => ↑(f i)) a ≤ g a
hi : (fun i => ↑(f i)) i < g i
hf : HasSum (fun i => ↑(f i)) sf
⊢ sf < sg

Tactic:
lift g to α → ℝ≥0 using hg'

Result:
case neg.intro.intro
α : Type u_1
sf sg : ℝ≥0∞
i : α
hsf : sf ≠ ⊤
hsg : ¬sg = ⊤
f : α → ℝ≥0
hf : HasSum (fun i => ↑(f i)) sf
g : α → ℝ≥0
hg : HasSum (fun i => ↑(g i)) sg
h : ∀ (a : α), (fun i => ↑(f i)) a ≤ (fun i => ↑(g i)) a
hi : (fun i => ↑(f i)) i < (fun i => ↑(g i)) i
⊢ sf < sg

Proof state:
case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ⊤
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ⊤
⊢ sf < sg

Tactic:
have hg' : ∀ x, g x ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top (hg.tsum_eq.symm ▸ hsg)

Result:
case neg
α : Type u_1
f g : α → ℝ≥0∞
sf sg : ℝ≥0∞
i : α
h : ∀ (a : α), f a ≤ g a
hi : f i < g i
hsf : sf ≠ ⊤
hf : HasSum f sf
hg : HasSum g sg
hsg : ¬sg = ⊤
hg' : ∀ (x : α), g x ≠ ⊤
⊢ sf < sg