case h₁
α : Type u_1
β : Type ?u.863516
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
⊢ (⨅ (i : ι), ∑ a in ∅, f i a) = ∑ a in ∅, ⨅ (i : ι), f i a

case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
⊢ (⨅ (i : ι), ∑ a in Finset.cons a s ha, f i a) = ∑ a in Finset.cons a s ha, ⨅ (i : ι), f i a
α : Type u_1
β : Type ?u.863516
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
s : Finset α
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
⊢ (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
induction' s using Finset.cons_induction_on with a s ha ih
no goals
case h₁
α : Type u_1
β : Type ?u.863516
a b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
⊢ (⨅ (i : ι), ∑ a in ∅, f i a) = ∑ a in ∅, ⨅ (i : ι), f i a
simp only [Finset.sum_empty, ciInf_const]
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
⊢ (⨅ (i : ι), f i a + ∑ a in s, f i a) = (⨅ (i : ι), f i a) + ⨅ (i : ι), ∑ a in s, f i a
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
⊢ (⨅ (i : ι), ∑ a in Finset.cons a s ha, f i a) = ∑ a in Finset.cons a s ha, ⨅ (i : ι), f i a
simp only [Finset.sum_cons, ← ih]
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
i j : ι
⊢ ∃ k, f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
⊢ (⨅ (i : ι), f i a + ∑ a in s, f i a) = (⨅ (i : ι), f i a) + ⨅ (i : ι), ∑ a in s, f i a
refine (iInf_add_iInf fun i j => ?_).symm
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
i j k : ι
hk : ∀ (a_1 : α), a_1 ∈ Finset.cons a s ha → f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
i j : ι
⊢ ∃ k, f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
refine (h (Finset.cons a s ha) i j).imp fun k hk => ?_
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ (x : α), x ∈ s → f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
i j k : ι
hk : ∀ (a_1 : α), a_1 ∈ Finset.cons a s ha → f k a_1 ≤ f i a_1 ∧ f k a_1 ≤ f j a_1
⊢ f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
rw [Finset.forall_mem_cons] at hk
no goals
case h₂
α : Type u_1
β : Type ?u.863516
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
ι : Sort u_2
f✝ g : ι → ℝ≥0∞
f : ι → α → ℝ≥0∞
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ (a : α), a ∈ t → f k a ≤ f i a ∧ f k a ≤ f j a
a : α
s : Finset α
ha : ¬a ∈ s
ih : (⨅ (i : ι), ∑ a in s, f i a) = ∑ a in s, ⨅ (i : ι), f i a
i j k : ι
hk : (f k a ≤ f i a ∧ f k a ≤ f j a) ∧ ∀ (x : α), x ∈ s → f k x ≤ f i x ∧ f k x ≤ f j x
⊢ f k a + ∑ a in s, f k a ≤ f i a + ∑ a in s, f j a
exact add_le_add hk.1.1 (Finset.sum_le_sum fun a ha => (hk.2 a ha).2)