awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
⊢ Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 (γ - HMul.hMul (α := ℝ) 2 0))

Tactic:
exact
        tendsto_const_nhds.sub <|
          tendsto_const_nhds.mul <|
            tendsto_pow_atTop_nhds_zero_of_lt_one (le_of_lt <| half_pos <| zero_lt_one)
              (half_lt_self zero_lt_one)

Premises used: tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.sub
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
⊢ Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)

Tactic:
have hγ : Tendsto (fun m : ℕ => γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ) := by
      suffices Tendsto (fun m : ℕ => γ - 2 * (1 / 2) ^ m) atTop (𝓝 (γ - 2 * 0)) by
        simpa only [mul_zero, tsub_zero]
      exact
        tendsto_const_nhds.sub <|
          tendsto_const_nhds.mul <|
            tendsto_pow_atTop_nhds_zero_of_lt_one (le_of_lt <| half_pos <| zero_lt_one)
              (half_lt_self zero_lt_one)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
⊢ Tendsto (fun (m : ℕ) ↦ d (⋂ (n : ℕ), f m n)) atTop (𝓝 (d (⋃ (m : ℕ), ⋂ (n : ℕ), f m n)))

Tactic:
d_Union _ ?_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
refine : Monotone.{0, u_1} (β := Set α) fun (m : ℕ) ↦ ⋂ (n : ℕ), f m n
⊢ Tendsto (fun (m : ℕ) ↦ d (⋂ (n : ℕ), f m n)) atTop (𝓝 (d (⋃ (m : ℕ), ⋂ (n : ℕ), f m n)))

Tactic:
refine d_Union _ ?_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
⊢ Monotone.{0, u_1} (β := Set α) fun (m : ℕ) ↦ ⋂ (n : ℕ), f m n

Tactic:
fun n m hnm =>
        subset_iInter fun i => Subset.trans (iInter_subset (f n) i) <| f_subset_f hnm <| le_rfl

Premises used: le_rfl, Set.Subset.trans, Monotone, Set.subset_iInter, Set.iInter_subset
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
⊢ Monotone.{0, u_1} (β := Set α) fun (m : ℕ) ↦ ⋂ (n : ℕ), f m n

Tactic:
exact fun n m hnm =>
        subset_iInter fun i => Subset.trans (iInter_subset (f n) i) <| f_subset_f hnm <| le_rfl

Premises used: le_rfl, Set.Subset.trans, Set.subset_iInter, Set.iInter_subset
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
⊢ Tendsto (fun (m : ℕ) ↦ d (⋂ (n : ℕ), f m n)) atTop (𝓝 (d (⋃ (m : ℕ), ⋂ (n : ℕ), f m n)))

Tactic:
have hd : Tendsto (fun m => d (⋂ n, f m n)) atTop (𝓝 (d (⋃ m, ⋂ n, f m n))) := by
      refine d_Union _ ?_
      exact fun n m hnm =>
        subset_iInter fun i => Subset.trans (iInter_subset (f n) i) <| f_subset_f hnm <| le_rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
hd : Tendsto (fun (m : ℕ) ↦ d (⋂ (n : ℕ), f m n)) atTop (𝓝 (d (⋃ (m : ℕ), ⋂ (n : ℕ), f m n)))
⊢ γ ≤ d s

Tactic:
le_of_tendsto_of_tendsto' hγ hd fun m => ?_

Premises used: le_of_tendsto_of_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
hd : Tendsto (fun (m : ℕ) ↦ d (⋂ (n : ℕ), f m n)) atTop (𝓝 (d (⋃ (m : ℕ), ⋂ (n : ℕ), f m n)))
refine : ∀ (m : ℕ), γ - 2 * (1 / 2) ^ m ≤ d (⋂ (n : ℕ), f m n)
⊢ γ ≤ d s

Tactic:
refine le_of_tendsto_of_tendsto' hγ hd fun m => ?_

Premises used: le_of_tendsto_of_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
hd : Tendsto (fun (m : ℕ) ↦ d (⋂ (n : ℕ), f m n)) atTop (𝓝 (d (⋃ (m : ℕ), ⋂ (n : ℕ), f m n)))
m : ℕ
⊢ Tendsto (fun (n : ℕ) ↦ d (f m n)) atTop (𝓝 (d (⋂ (n : ℕ), f m n)))

Tactic:
d_Inter _ ?_ ?_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (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)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
this : ∀ (n : ℕ), ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
e : ℕ → Set α
he : ∀ (x : ℕ), MeasurableSet (e x) ∧ γ - (1 / 2) ^ x < d (e x)
he₁ : ∀ (n : ℕ), MeasurableSet (e n)
he₂ : ∀ (n : ℕ), γ - (1 / 2) ^ n < d (e n)
f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ (Finset.Ico n (m + 1)).inf e
hf : ∀ (n m : ℕ), MeasurableSet (f n m)
f_subset_f : ∀ {a b c d : ℕ} (hab : a ≤ b) (hcd : c ≤ d), f a d ⊆ f b c
f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
le_d_f : ∀ (n m : ℕ) (h : m ≤ n), γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
s : Set α := ⋃ (m : ℕ), ⋂ (n : ℕ), f m n
hγ : Tendsto (fun (m : ℕ) ↦ γ - 2 * (1 / 2) ^ m) atTop (𝓝 γ)
hd : Tendsto (fun (m : ℕ) ↦ d (⋂ (n : ℕ), f m n)) atTop (𝓝 (d (⋃ (m : ℕ), ⋂ (n : ℕ), f m n)))
m : ℕ
refine_1 : ∀ (n : ℕ), MeasurableSet (f m n)
refine_2 : ∀ (n m_1 : ℕ), n ≤ m_1 → f m m_1 ⊆ f m n
⊢ Tendsto (fun (n : ℕ) ↦ d (f m n)) atTop (𝓝 (d (⋂ (n : ℕ), f m n)))

Tactic:
refine d_Inter _ ?_ ?_