Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋂ n, s n)))

Tactic:
refine Tendsto.sub ?_ ?_ <;>
      refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal <| ?_).comp <|
        tendsto_measure_iInter_atTop (fun n ↦ (hs n).nullMeasurableSet) hm ?_

Goal state after:
case refine_1.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ μ (⋂ n, s n) ≠ ∞

case refine_1.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ ∃ i, μ (s i) ≠ ∞

case refine_2.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ ν (⋂ n, s n) ≠ ∞

case refine_2.refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
d_split : ∀ (s t : Set α), MeasurableSet t → d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α), Monotone s → Tendsto (fun n ↦ d (s n)) atTop (𝓝 (d (⋃ n, s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ ∃ i, ν (s i) ≠ ∞