case refine'_1
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
⊢ ∑ a in ∅, iSup (f a) = ⨆ (n : ι), ∑ a in ∅, f a n

case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n) →
        ∑ a in insert a s, iSup (f a) = ⨆ (n : ι), ∑ a in insert a s, f a n
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
⊢ ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
refine' Finset.induction_on s _ _
no goals
case refine'_1
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
⊢ ∑ a in ∅, iSup (f a) = ⨆ (n : ι), ∑ a in ∅, f a n
simp
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s✝ : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
a : α
s : Finset α
has : ¬a ∈ s
ih : ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
⊢ ∑ a in insert a s, iSup (f a) = ⨆ (n : ι), ∑ a in insert a s, f a n
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n) →
        ∑ a in insert a s, iSup (f a) = ⨆ (n : ι), ∑ a in insert a s, f a n
intro a s has ih
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s✝ : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
a : α
s : Finset α
has : ¬a ∈ s
ih : ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
⊢ iSup (f a) + ∑ a in s, iSup (f a) = ⨆ (n : ι), f a n + ∑ a in s, f a n
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s✝ : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
a : α
s : Finset α
has : ¬a ∈ s
ih : ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
⊢ ∑ a in insert a s, iSup (f a) = ⨆ (n : ι), ∑ a in insert a s, f a n
simp only [Finset.sum_insert has]
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s✝ : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
a : α
s : Finset α
has : ¬a ∈ s
ih : ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
⊢ Monotone fun n => ∑ a in s, f a n
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s✝ : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
a : α
s : Finset α
has : ¬a ∈ s
ih : ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
⊢ iSup (f a) + ∑ a in s, iSup (f a) = ⨆ (n : ι), f a n + ∑ a in s, f a n
rw [ih, iSup_add_iSup_of_monotone (hf a)]
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s✝ : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
a : α
s : Finset α
has : ¬a ∈ s
ih : ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
i j : ι
h : i ≤ j
⊢ (fun n => ∑ a in s, f a n) i ≤ (fun n => ∑ a in s, f a n) j
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s✝ : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
a : α
s : Finset α
has : ¬a ∈ s
ih : ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
⊢ Monotone fun n => ∑ a in s, f a n
intro i j h
no goals
case refine'_2
α✝ : Type ?u.147988
β : Type ?u.147991
γ : Type ?u.147994
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝¹ : Set ℝ≥0∞
α : Type u_1
ι : Type u_2
inst✝ : SemilatticeSup ι
s✝ : Finset α
f : α → ι → ℝ≥0∞
hf : ∀ (a : α), Monotone (f a)
a : α
s : Finset α
has : ¬a ∈ s
ih : ∑ a in s, iSup (f a) = ⨆ (n : ι), ∑ a in s, f a n
i j : ι
h : i ≤ j
⊢ (fun n => ∑ a in s, f a n) i ≤ (fun n => ∑ a in s, f a n) j
exact Finset.sum_le_sum fun a _ => hf a h