-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem ofFunction_union_of_top_of_nonempty_inter {s t : Set α}
    (h : ∀ u, (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞) :
    OuterMeasure.ofFunction m m_empty (s ∪ t) =
      OuterMeasure.ofFunction m m_empty s + OuterMeasure.ofFunction m m_empty t

Proof state:
case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Tactic:
have hd : Disjoint (I s) (I t) := disjoint_iff_inf_le.mpr fun i hi => he ⟨i, hi⟩

Result:
case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}
hd : Disjoint (I s) (I t)
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Proof state:
case inl.intro.intro
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
i : ℕ
hs : (s ∩ f i).Nonempty
ht : (t ∩ f i).Nonempty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Tactic:
calc
  μ s + μ t ≤ ∞ := le_top
  _ = m (f i) := (h (f i) hs ht).symm
  _ ≤ ∑' i, m (f i) := ENNReal.le_tsum i

Result:
no goals

Proof state:
case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}
hd : Disjoint (I s) (I t)
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Tactic:
have hI : ∀ u ⊆ s ∪ t, μ u ≤ ∑' i : I u, μ (f i) := fun u hu =>
  calc
    μ u ≤ μ (⋃ i : I u, f i) :=
      μ.mono fun x hx =>
        let ⟨i, hi⟩ := mem_iUnion.1 (hf (hu hx))
        mem_iUnion.2 ⟨⟨i, ⟨x, hx, hi⟩⟩, hi⟩
    _ ≤ ∑' i : I u, μ (f i) := measure_iUnion_le _

Result:
case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}
hd : Disjoint (I s) (I t)
hI : ∀ u ⊆ s ∪ t, μ u ≤ ∑' (i : ↑(I u)), μ (f ↑i)
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
⊢ (OuterMeasure.ofFunction m m_empty) s + (OuterMeasure.ofFunction m m_empty) t ≤ ∑' (i : ℕ), m (f i)

Tactic:
set μ := OuterMeasure.ofFunction m m_empty

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Tactic:
rcases Classical.em (∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty) with (⟨i, hs, ht⟩ | he)

Result:
case inl.intro.intro
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
i : ℕ
hs : (s ∩ f i).Nonempty
ht : (t ∩ f i).Nonempty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Proof state:
case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Tactic:
set I := fun s => { i : ℕ | (s ∩ f i).Nonempty }

Result:
case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Proof state:
case inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
μ : OuterMeasure α := OuterMeasure.ofFunction m m_empty
he : ¬∃ i, (s ∩ f i).Nonempty ∧ (t ∩ f i).Nonempty
I : Set α → Set ℕ := fun s => {i | (s ∩ f i).Nonempty}
hd : Disjoint (I s) (I t)
hI : ∀ u ⊆ s ∪ t, μ u ≤ ∑' (i : ↑(I u)), μ (f ↑i)
⊢ μ s + μ t ≤ ∑' (i : ℕ), m (f i)

Tactic:
calc
  μ s + μ t ≤ (∑' i : I s, μ (f i)) + ∑' i : I t, μ (f i) :=
    add_le_add (hI _ subset_union_left) (hI _ subset_union_right)
  _ = ∑' i : ↑(I s ∪ I t), μ (f i) :=
    (tsum_union_disjoint (f := fun i => μ (f i)) hd ENNReal.summable ENNReal.summable).symm
  _ ≤ ∑' i, μ (f i) :=
    (tsum_le_tsum_of_inj (↑) Subtype.coe_injective (fun _ _ => zero_le _) (fun _ => le_rfl)
      ENNReal.summable ENNReal.summable)
  _ ≤ ∑' i, m (f i) := ENNReal.tsum_le_tsum fun i => ofFunction_le _

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
⊢ (OuterMeasure.ofFunction m m_empty) (s ∪ t) =
    (OuterMeasure.ofFunction m m_empty) s + (OuterMeasure.ofFunction m m_empty) t

Tactic:
refine le_antisymm (measure_union_le _ _) (le_iInf₂ fun f hf ↦ ?_)

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
h : ∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤
f : ℕ → Set α
hf : s ∪ t ⊆ ⋃ i, f i
⊢ (OuterMeasure.ofFunction m m_empty) s + (OuterMeasure.ofFunction m m_empty) t ≤ ∑' (i : ℕ), m (f i)