awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 < ∞
h₁ : ∀ (H : f x < ∞), 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ 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

Premises used: eq_or_lt_of_le, le_top
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : f x = ∞
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞

Tactic:
simp only [H, or_false, ENNReal.zero_lt_top, not_top_lt, and_false]

Premises used: ENNReal.zero_lt_top, not_top_lt, or_false, and_false
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 : f x < ∞
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞

Tactic:
simp only [H, H.ne, and_true, false_or]

Premises used: and_true, false_or, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 ∞)

Tactic:
disjoint_left.2 fun x hx h'x => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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∞)
hd : ∀ (x : α) (hx : x ∈ s ∩ f ⁻¹' {∞}) (h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ∞), False
⊢ Disjoint (s ∩ f ⁻¹' {∞}) (s ∩ f ⁻¹' Ioo 0 ∞)

Tactic:
refine disjoint_left.2 fun x hx h'x => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 ∞
⊢ f x < ∞

Tactic:
have : f x < ∞ := h'x.2.2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 ∞
this : f x < ∞
⊢ False

Tactic:
lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm))

Premises used: lt_irrefl, And.right, LT.lt.trans_le, le_of_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 ∞
this : f x < ∞
⊢ False

Tactic:
exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm))

Premises used: lt_irrefl, And.right, LT.lt.trans_le, le_of_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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∞)
⊢ MeasurableSet (s ∩ f ⁻¹' Ioo 0 ∞)

Tactic:
hs.inter (hf measurableSet_Ioo)

Premises used: measurableSet_Ioo, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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∞)
⊢ MeasurableSet (s ∩ f ⁻¹' Ioo 0 ∞)

Tactic:
exact hs.inter (hf measurableSet_Ioo)

Premises used: measurableSet_Ioo, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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 ∩ 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)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)))
h : ∀ (i : ℤ), MeasurableSet (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ i) ((↑t : ℝ≥0∞) ^ (i + 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∞)

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]

Premises used: Iff.mpr, ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow, MeasureTheory.measure_iUnion, Set.inter_iUnion, ENNReal.one_lt_coe_iff, Set.preimage_iUnion, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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:
(this hij.symm (hij.lt_or_gt.resolve_left h)).symm

Premises used: Or.resolve_left, Ne.symm, Disjoint.symm, Ne.lt_or_gt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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:
exact (this hij.symm (hij.lt_or_gt.resolve_left h)).symm

Premises used: Or.resolve_left, Ne.symm, Disjoint.symm, Ne.lt_or_gt
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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

Tactic:
disjoint_left.2 fun x hx h'x => lt_irrefl (f x) ?_

Premises used: Iff.mpr, lt_irrefl, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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
⊢ Function.onFun.{1, u_5 + 1, 1} (β := Set α) Disjoint
    (fun (n : ℤ) ↦ s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) i j

Tactic:
refine disjoint_left.2 fun x hx h'x => lt_irrefl (f x) ?_

Premises used: Iff.mpr, lt_irrefl, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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 < (↑t : ℝ≥0∞) ^ (i + 1)

Tactic:
hx.2.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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
⊢ (↑t : ℝ≥0∞) ^ (i + 1) ≤ (↑t : ℝ≥0∞) ^ j

Tactic:
ENNReal.zpow_le_of_le (ENNReal.one_le_coe_iff.2 ht.le) h

Premises used: Iff.mpr, LT.lt.le, ENNReal.zpow_le_of_le, ENNReal.one_le_coe_iff
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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
⊢ (↑t : ℝ≥0∞) ^ j ≤ f x

Tactic:
h'x.2.1

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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
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:
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

Premises used: Iff.mpr, ENNReal.ofNNReal, LT.lt.le, ENNReal.zpow_le_of_le, And.right, And.left, HAdd.hAdd, ENNReal.one_le_coe_iff, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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∞)
n : ℤ
⊢ MeasurableSet (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))

Tactic:
hs.inter (hf measurableSet_Ico)

Premises used: measurableSet_Ico, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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∞)
n : ℤ
⊢ MeasurableSet (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))

Tactic:
exact hs.inter (hf measurableSet_Ico)

Premises used: measurableSet_Ico, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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∞)

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)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
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)))
rw₃ 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∞))
⊢ (μ : (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)))

Tactic:
rw [A, B, C, add_assoc]

Premises used: add_assoc
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})

Tactic:
isTopologicalBasis_Ioo_rat.borel_eq_generateFrom

Premises used: Real.isTopologicalBasis_Ioo_rat, TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Goal:
rw : Eq (α := MeasurableSpace ℝ) (generateFrom (range Iio)) (generateFrom (⋃ (a : ℚ), {Iio (↑a : ℝ)}))
⊢ borel ℝ = generateFrom (⋃ (a : ℚ), {Iio (↑a : ℝ)})

Tactic:
rw [borel_eq_generateFrom_Iio]

Premises used: borel_eq_generateFrom_Iio