-- Mathlib/Order/LiminfLimsup.lean
lemma isBoundedUnder_sum {κ : Type*} [AddCommMonoid R] {r : R → R → Prop}
    (hr : ∀ (v₁ v₂ : α → R), f.IsBoundedUnder r v₁ → f.IsBoundedUnder r v₂
      → f.IsBoundedUnder r (v₁ + v₂)) (hr₀ : r 0 0)
    {u : κ → α → R} (s : Finset κ) (h : ∀ k ∈ s, f.IsBoundedUnder r (u k)) :
    f.IsBoundedUnder r (∑ k ∈ s, u k)

Proof state:
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : ∀ k ∈ Finset.cons k₀ s k₀_notin_s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)

Tactic:
simp only [Finset.forall_mem_cons] at *

Result:
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)

Proof state:
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : (∀ k ∈ s, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s, u k)
h : IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)

Tactic:
simpa only [Finset.sum_cons] using hr _ _ h.1 (ih h.2)

Result:
no goals

Proof state:
case empty
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ ∅, u k)

case cons
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
a✝¹ : κ
s✝ : Finset κ
h✝ : a✝¹ ∉ s✝
a✝ : (∀ k ∈ s✝, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s✝, u k)
h : ∀ k ∈ Finset.cons a✝¹ s✝ h✝, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons a✝¹ s✝ h✝, u k)

Tactic:
case empty =>
  rw [Finset.sum_empty]
  exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩

Result:
case cons
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
a✝¹ : κ
s✝ : Finset κ
h✝ : a✝¹ ∉ s✝
a✝ : (∀ k ∈ s✝, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s✝, u k)
h : ∀ k ∈ Finset.cons a✝¹ s✝ h✝, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons a✝¹ s✝ h✝, u k)

Proof state:
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ ∅, u k)

Tactic:
rw [Finset.sum_empty]

Result:
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f 0

Proof state:
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f 0

Tactic:
exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩

Result:
no goals

Proof state:
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ ∀ᶠ (x : R) in map 0 f, r x 0

Tactic:
simp_all only [eventually_map, Pi.zero_apply, eventually_true]

Result:
no goals

Proof state:
case cons
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
a✝¹ : κ
s✝ : Finset κ
h✝ : a✝¹ ∉ s✝
a✝ : (∀ k ∈ s✝, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s✝, u k)
h : ∀ k ∈ Finset.cons a✝¹ s✝ h✝, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons a✝¹ s✝ h✝, u k)

Tactic:
case cons k₀ s k₀_notin_s ih =>
  simp only [Finset.forall_mem_cons] at *
  simpa only [Finset.sum_cons] using hr _ _ h.1 (ih h.2)

Result:
no goals

Proof state:
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
s : Finset κ
h : ∀ k ∈ s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ s, u k)

Tactic:
induction s using Finset.cons_induction

Result:
case empty
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ k ∈ ∅, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ ∅, u k)

case cons
α : Type u_6
f : Filter α
R : Type u_7
κ : Type u_8
inst✝ : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
a✝¹ : κ
s✝ : Finset κ
h✝ : a✝¹ ∉ s✝
a✝ : (∀ k ∈ s✝, IsBoundedUnder r f (u k)) → IsBoundedUnder r f (∑ k ∈ s✝, u k)
h : ∀ k ∈ Finset.cons a✝¹ s✝ h✝, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons a✝¹ s✝ h✝, u k)