awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (hypothesis)
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
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            t ⊆ s → LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            t ⊆ sᶜ → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have f_succ : ∀ (n m : ℕ) (hnm : n ≤ m), f n (m + 1) = f n m ∩ e (m + 1)
Tactic: have f_succ n m (hnm : n ≤ m) : f n (m + 1) = f n m ∩ e (m + 1) := by
    have : n ≤ m + 1 := le_of_lt (Nat.succ_le_succ hnm)
    simp_rw [f, ← Finset.insert_Ico_right_eq_Ico_add_one this, Finset.inf_insert,
      Set.inter_comm]
    rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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)
n m : ℕ
h : m ≤ n
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
have refine_1 : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (f m m)
Tactic: refine Nat.le_induction ?_ ?_ n h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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)
n m : ℕ
h : m ≤ n
refine_1 : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (f m m)
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
have refine_2 : ∀ (n : ℕ) (hmn : m ≤ n),
  γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n) → γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1) ≤ d (f m (n + 1))
Tactic: refine Nat.le_induction ?_ ?_ n h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (hypothesis)
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)
n m : ℕ
h : m ≤ n
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (f m m)
have this₁ : γ - (1 / 2) ^ m < d (e m)
Tactic: have := he₂ m
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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_1 : ∀ (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)
n m : ℕ
h : m ≤ n
this : γ - (1 / 2) ^ m < d (e m)
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (f m m)
have refine_1 : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (e m)
Tactic: simp_rw [f, Nat.Ico_succ_singleton, Finset.inf_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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_1 : ∀ (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)
n m : ℕ
h : m ≤ n
this : γ - (1 / 2) ^ m < d (e m)
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (e m)
have linarith : d (e m) < γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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_1 : ∀ (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)
n m : ℕ
h : m ≤ n
this : γ - (1 / 2) ^ m < d (e m)
linarith : d (e m) < γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m → HMul.hMul (α := ℝ) 1 1 = 1
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m ≤ d (e m)
have linarith₁ : d (e m) < γ - 2 * (1 / 2) ^ m + (1 / 2) ^ m →
  1 * γ - 1 * (1 / 2) ^ m -
        (1 * (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (e m))) : ℝ) -
          1 * (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (e m))) : ℝ)) +
      (1 * (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (e m))) : ℝ) -
          1 * (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (e m))) : ℝ) -
        (1 * γ - HMul.hMul (α := ℝ) 1 2 * (1 * (1 / 2) ^ m) + 1 * (1 / 2) ^ m)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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)
n_1 m : ℕ
h : m ≤ n_1
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
⊢ γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1) ≤ d (f m (n + 1))
have refine_2 : γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1)) ≤ γ + d (f m (n + 1))
Tactic: refine le_of_add_le_add_left (a := γ) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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)
n_1 m : ℕ
h : m ≤ n_1
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
⊢ γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1)) = γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ (n + 1)))
have rw : γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n * (1 / 2)) = γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ n * (1 / 2)))
Tactic: rw [pow_succ, mul_one_div, _root_.sub_half]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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)
n_1 m : ℕ
h : m ≤ n_1
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
rw :
  γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n * (1 / 2)) = γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ n * (1 / 2)))
⊢ γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1)) = γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ (n + 1)))
have rw₁ : γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n / 2) = γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ n / 2))
Tactic: rw [pow_succ, mul_one_div, _root_.sub_half]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
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)
n_1 m : ℕ
h : m ≤ n_1
n : ℕ
hmn : m ≤ n
ih : γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n ≤ d (f m n)
rw :
  γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n * (1 / 2)) = γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ n * (1 / 2)))
rw₁ : γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n / 2) = γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ n / 2))
⊢ γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ (n + 1)) = γ + (γ - 2 * (1 / 2) ^ m + ((1 / 2) ^ n - (1 / 2) ^ (n + 1)))
have rw₂ : γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n / 2) = γ + (γ - 2 * (1 / 2) ^ m + (1 / 2) ^ n / 2)
Tactic: rw [pow_succ, mul_one_div, _root_.sub_half]