awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞} ∪ s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
hd : Disjoint (s ∩ f ⁻¹' {∞}) (s ∩ f ⁻¹' Ioo 0 ∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
have h : MeasurableSet (s ∩ f ⁻¹' Ioo 0 ∞)
Tactic: rw [← measure_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞} ∪ s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞)) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞)) : ℝ≥0∞)
have h : f ⁻¹' Ioi 0 = f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
⊢ f ⁻¹' Ioi 0 = f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞
have h : ∀ (x : α), x ∈ f ⁻¹' Ioi 0 ↔ x ∈ f ⁻¹' {∞} ∪ f ⁻¹' Ioo 0 ∞
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
x : α
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞
have h : ∀ (H : f x = ∞), 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞
Tactic: obtain (H | H) : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
x : α
h : ∀ (H : f x = ∞), 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞
have h₁ : ∀ (H : f x < ∞), 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞
Tactic: obtain (H | H) : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
⊢ Disjoint (s ∩ f ⁻¹' {∞}) (s ∩ f ⁻¹' Ioo 0 ∞)
have hd : ∀ (x : α) (hx : x ∈ s ∩ f ⁻¹' {∞}) (h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ∞), False
Tactic: refine disjoint_left.2 fun x hx h'x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
x : α
hx : x ∈ s ∩ f ⁻¹' {∞}
h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ∞
⊢ False
have this : f x < ∞
Tactic: have : f x < ∞ := h'x.2.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have B : (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
Tactic: have B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞) := by
    rw [← measure_union]
    · rw [← inter_union_distrib_left]
      congr
      ext x
      simp only [mem_singleton_iff, mem_union, mem_Ioo, mem_Ioi, mem_preimage]
      obtain (H | H) : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top
      · simp only [H, or_false, ENNReal.zero_lt_top, not_top_lt, and_false]
      · simp only [H, H.ne, and_true, false_or]
    · refine disjoint_left.2 fun x hx h'x => ?_
      have : f x < ∞ := h'x.2.2
      exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm))
    · exact hs.inter (hf measurableSet_Ioo)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
    (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
have hn : Pairwise (α := ℤ)
  (Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦
    s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
Tactic: rw [← measure_iUnion,
      ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow (ENNReal.one_lt_coe_iff.2 ht) ENNReal.coe_ne_top,
      preimage_iUnion, inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
hn :
  Pairwise (α := ℤ)
    (Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦
      s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
    (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
have h : ∀ (i : ℤ), MeasurableSet (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ i) ((↑t : ℝ≥0∞) ^ (i + 1)))
Tactic: rw [← measure_iUnion,
      ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow (ENNReal.one_lt_coe_iff.2 ht) ENNReal.coe_ne_top,
      preimage_iUnion, inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
i j : ℤ
hij : i ≠ j
⊢ Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
    (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j
have hn : ∀
  (this :
    ∀ ⦃i j : ℤ⦄ (hij : i ≠ j) (h : i < j),
      Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
        (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j)
  (h : ¬i < j),
  Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
    (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j
Tactic: wlog h : i < j generalizing i j
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
i j : ℤ
hij : i ≠ j
hn :
  ∀
    (this :
      ∀ ⦃i j : ℤ⦄ (hij : i ≠ j) (h : i < j),
        Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
          (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j)
    (h : ¬i < j),
    Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
      (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j
⊢ Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
    (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j
have wlog : ∀ ⦃i j : ℤ⦄ (hij : i ≠ j) (h : i < j),
  Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
    (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j
Tactic: wlog h : i < j generalizing i j
Cleared hypotheses: i, j, hij
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
i j : ℤ
hij : i ≠ j
h : i < j
⊢ Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
    (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j
have refine : ∀ (x : α)
  (hx : Membership.mem (γ := Set α) ((fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i) x)
  (h'x : Membership.mem (γ := Set α) ((fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) j) x),
  f x < f x
Tactic: refine disjoint_left.2 fun x hx h'x => lt_irrefl (f x) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have C : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
  (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
Tactic: have C : μ (s ∩ f ⁻¹' Ioo 0 ∞) =
      ∑' n : ℤ, μ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by
    rw [← measure_iUnion,
      ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow (ENNReal.one_lt_coe_iff.2 ht) ENNReal.coe_ne_top,
      preimage_iUnion, inter_iUnion]
    · intro i j hij
      wlog h : i < j generalizing i j
      · exact (this hij.symm (hij.lt_or_gt.resolve_left h)).symm
      refine disjoint_left.2 fun x hx h'x => lt_irrefl (f x) ?_
      calc
        f x < (t : ℝ≥0∞) ^ (i + 1) := hx.2.2
        _ ≤ (t : ℝ≥0∞) ^ j := ENNReal.zpow_le_of_le (ENNReal.one_le_coe_iff.2 ht.le) h
        _ ≤ f x := h'x.2.1
    · intro n
      exact hs.inter (hf measurableSet_Ico)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
C :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
    (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
    ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
Tactic: rw [A, B, C, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
C :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
    (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
    ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
Tactic: rw [A, B, C, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
C :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
    (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
    ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
Tactic: rw [A, B, C, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
B :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
C :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)
    (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥0∞)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
        (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have rw₃ : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)) =
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
      (∑' (n : ℤ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞))
Tactic: rw [A, B, C, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), {Iio (↑a : ℝ)})
have rw : Eq (α := MeasurableSpace ℝ) (generateFrom (range Iio)) (generateFrom (⋃ (a : ℚ), {Iio (↑a : ℝ)}))
Tactic: rw [borel_eq_generateFrom_Iio]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (goal)
Goal:
⊢ Eq (α := MeasurableSpace ℝ) (generateFrom (range Iio)) (generateFrom (⋃ (a : ℚ), {Iio (↑a : ℝ)}))
have refine : ∀ (t : Set ℝ), Membership.mem (γ := Set (Set ℝ)) (range Iio) t → MeasurableSet t
Tactic: refine le_antisymm
    (generateFrom_le ?_)
    (generateFrom_mono <| iUnion_subset fun q ↦ singleton_subset_iff.mpr <| mem_range_self _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Real (hypothesis)
Goal:
a : ℝ
⊢ MeasurableSet (Iio a)
have this : IsLUB (range Rat.cast ∩ Iio a) a
Tactic: have : IsLUB (range ((↑) : ℚ → ℝ) ∩ Iio a) a := by
    simp [isLUB_iff_le_iff, mem_upperBounds, ← le_iff_forall_rat_lt_imp_le]