case pos
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
β : Type ?u.336123
γ : Type ?u.336126
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
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
by_cases hsg : sg = ⊤
no goals
case pos
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
exact hsg.symm ▸ lt_of_le_of_ne le_top hsf
case neg
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
case neg
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
have hg' : ∀ x, g x ≠ ⊤ := ENNReal.ne_top_of_tsum_ne_top (hg.tsum_eq.symm ▸ hsg)
case neg.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
case neg
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
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))
case neg.intro.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
case neg.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
lift g to α → ℝ≥0 using hg'
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
case neg.intro.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
lift sf to ℝ≥0 using hsf
case neg.intro.intro.intro.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
case neg.intro.intro.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
lift sg to ℝ≥0 using hsg
case neg.intro.intro.intro.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
case neg.intro.intro.intro.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
simp only [coe_le_coe, coe_lt_coe] at h hi⊢
no goals
case neg.intro.intro.intro.intro
α : Type u_1
β : Type ?u.336123
γ : Type ?u.336126
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
exact NNReal.hasSum_lt h hi (ENNReal.hasSum_coe.1 hf) (ENNReal.hasSum_coe.1 hg)