case h₀
α : Type u_1
β : Type ?u.204885
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s → f i < g i
a : α
Hlt : ∀ (i : α), i ∈ {a} → f i < g i
⊢ ∑ i in {a}, f i < ∑ i in {a}, g i

case h₁
α : Type u_1
β : Type ?u.204885
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s✝ : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s✝ → f i < g i
a : α
s : Finset α
as : ¬a ∈ s
hs✝ : Finset.Nonempty s
IH : (∀ (i : α), i ∈ s → f i < g i) → ∑ i in s, f i < ∑ i in s, g i
Hlt : ∀ (i : α), i ∈ cons a s as → f i < g i
⊢ ∑ i in cons a s as, f i < ∑ i in cons a s as, g i
α : Type u_1
β : Type ?u.204885
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
hs : Finset.Nonempty s
f g : α → ℝ≥0∞
Hlt : ∀ (i : α), i ∈ s → f i < g i
⊢ ∑ i in s, f i < ∑ i in s, g i
induction' hs using Finset.Nonempty.cons_induction with a a s as _ IH
no goals
case h₀
α : Type u_1
β : Type ?u.204885
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s → f i < g i
a : α
Hlt : ∀ (i : α), i ∈ {a} → f i < g i
⊢ ∑ i in {a}, f i < ∑ i in {a}, g i
simp [Hlt _ (Finset.mem_singleton_self _)]
case h₁
α : Type u_1
β : Type ?u.204885
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s✝ : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s✝ → f i < g i
a : α
s : Finset α
as : ¬a ∈ s
hs✝ : Finset.Nonempty s
IH : (∀ (i : α), i ∈ s → f i < g i) → ∑ i in s, f i < ∑ i in s, g i
Hlt : ∀ (i : α), i ∈ cons a s as → f i < g i
⊢ f a + ∑ i in s, f i < g a + ∑ i in s, g i
case h₁
α : Type u_1
β : Type ?u.204885
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s✝ : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s✝ → f i < g i
a : α
s : Finset α
as : ¬a ∈ s
hs✝ : Finset.Nonempty s
IH : (∀ (i : α), i ∈ s → f i < g i) → ∑ i in s, f i < ∑ i in s, g i
Hlt : ∀ (i : α), i ∈ cons a s as → f i < g i
⊢ ∑ i in cons a s as, f i < ∑ i in cons a s as, g i
simp only [as, Finset.sum_cons, not_false_iff]
no goals
case h₁
α : Type u_1
β : Type ?u.204885
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
s✝ : Finset α
f g : α → ℝ≥0∞
Hlt✝ : ∀ (i : α), i ∈ s✝ → f i < g i
a : α
s : Finset α
as : ¬a ∈ s
hs✝ : Finset.Nonempty s
IH : (∀ (i : α), i ∈ s → f i < g i) → ∑ i in s, f i < ∑ i in s, g i
Hlt : ∀ (i : α), i ∈ cons a s as → f i < g i
⊢ f a + ∑ i in s, f i < g a + ∑ i in s, g i
exact
  ENNReal.add_lt_add (Hlt _ (Finset.mem_cons_self _ _))
    (IH fun i hi => Hlt _ (Finset.mem_cons.2 <| Or.inr hi))