-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma inf_apply {s : Set α} (hs : MeasurableSet s) :
    (μ ⊓ ν) s = sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t n) =
    sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}

Tactic:
refine le_antisymm (le_sInf fun m ⟨t, ht₁⟩ ↦ ?_) (le_iInf₂ fun t' ht' ↦ ?_)

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
m : ℝ≥0∞
x✝ : m ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t : Set α
ht₁ : m = μ (t ∩ s) + ν (tᶜ ∩ s)
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t n) ≤ m

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} ≤ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hadd : μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n)
⊢ sInf {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)} ≤ ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n)

Tactic:
exact le_trans (sInf_le ⟨t, rfl⟩) hadd

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∀ (x : ℕ), (if x = 1 then 0 else if x = 0 then 0 else μ (t' x) ⊓ ν (t' x)) = 0

Tactic:
simp only [ite_eq_left_iff]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∀ (x : ℕ), ¬x = 1 → ¬x = 0 → μ (t' x) ⊓ ν (t' x) = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
n : ℕ
hn₁ : ¬n = 1
hn₀ : ¬n = 0
⊢ μ (t' n) ⊓ ν (t' n) = 0

Tactic:
simp only [ht', if_neg hn₀, if_neg hn₁, measure_empty, iInf_pair, le_refl, inf_of_le_left]

Result:
no goals

Proof state:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
simp only [iInf_image, coe_toOuterMeasure, iInf_pair]

Result:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
⊢ μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n)

Tactic:
have hle₁ : μ (t ∩ s) ≤ ∑' (n : {k | μ (t' k) ≤ ν (t' k)}), μ (t' n) :=
  (measure_mono inter_subset_left).trans <| measure_biUnion_le _ (to_countable _) _

Result:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
⊢ μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n)

Proof state:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n => if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ μ (t' 0) ⊓ ν (t' 0) + μ (t' 1) ⊓ ν (t' 1) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
exact add_le_add (inf_le_left.trans <| by simp [ht']) (inf_le_right.trans <| by simp [ht'])

Result:
no goals

Proof state:
case refine_2.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (b : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑b) = μ (t' ↑b) ⊓ ν (t' ↑b)

Tactic:
rw [Subtype.forall]

Result:
case refine_2.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
heq : {k | μ (t' k) ≤ ν (t' k)} ∪ {k | ν (t' k) < μ (t' k)} = univ
⊢ ∀ (a : ℕ) (b : a ∈ {k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑⟨a, b⟩) = μ (t' ↑⟨a, b⟩) ⊓ ν (t' ↑⟨a, b⟩)

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
⊢ μ (t ∩ s) + ν (tᶜ ∩ s) ≤ ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n)

Tactic:
refine (add_le_add hle₁ hle₂).trans ?_

Result:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α := ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
ht : t = ⋃ n ∈ {k | μ (t' k) ≤ ν (t' k)}, t' n
hle₁ : μ (t ∩ s) ≤ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n)
hcap : tᶜ ∩ s ⊆ ⋃ n ∈ {k | ν (t' k) < μ (t' k)}, t' n
hle₂ : ν (tᶜ ∩ s) ≤ ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n)
⊢ ∑' (n : ↑{k | μ (t' k) ≤ ν (t' k)}), μ (t' ↑n) + ∑' (n : ↑{k | ν (t' k) < μ (t' k)}), ν (t' ↑n) ≤
    ∑' (n : ℕ), μ (t' n) ⊓ ν (t' n)