-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem extend_iUnion_le_tsum_nat' (s : ℕ → Set α) :
    extend m (⋃ i, s i) ≤ ∑' i, extend m (s i)

Proof state:
case pos
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ m (⋃ i, s i) ⋯ ≤ tsum ?m.10586

Tactic:
apply msU h

Result:
no goals

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
by_cases h : ∀ i, P (s i)

Result:
case pos
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

case neg
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ¬∀ (i : ℕ), P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Proof state:
case neg
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ¬∀ (i : ℕ), P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
obtain ⟨i, hi⟩ := not_forall.1 h

Result:
case neg.intro
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ¬∀ (i : ℕ), P (s i)
i : ℕ
hi : ¬P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Proof state:
case pos
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
rw [extend_eq _ (PU h), congr_arg tsum _]

Result:
case pos
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ m (⋃ i, s i) ⋯ ≤ tsum ?m.10586

α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ ℕ → ℝ≥0∞

α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ (fun i => extend m (s i)) = ?m.10586

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
⊢ (fun i => extend m (s i)) = fun i => m (s i) ⋯

Tactic:
funext i

Result:
case h
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
i : ℕ
⊢ extend m (s i) = m (s i) ⋯

Proof state:
case h
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ∀ (i : ℕ), P (s i)
i : ℕ
⊢ extend m (s i) = m (s i) ⋯

Tactic:
apply extend_eq _ (h i)

Result:
no goals

Proof state:
case neg.intro
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
s : ℕ → Set α
h : ¬∀ (i : ℕ), P (s i)
i : ℕ
hi : ¬P (s i)
⊢ extend m (⋃ i, s i) ≤ ∑' (i : ℕ), extend m (s i)

Tactic:
exact le_trans (le_iInf fun h => hi.elim h) (ENNReal.le_tsum i)

Result:
no goals