awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
hjx : x ∉ m j
rw :
  (if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) =
    g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
⊢ reparam x j = g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
have rw₁ : g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) sorry) =
  g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) sorry)
Tactic: rw [A, if_neg hjx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
hjx : x ∉ m j
⊢ F1 x = F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
have this₁ : reparam x j = g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) sorry)
Tactic: have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (hypothesis)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
⊢ Measurable F1
have this₁ : F1 = fun (x : δ) ↦
  if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) sorry)) x
Tactic: have : F1 = fun x ↦ if x ∈ m j then F0 j x else F0 (g (Nat.find (Z x))) x := by
    ext x
    have A : reparam x j = if x ∈ m j then j else g (Nat.find (Z x)) := rfl
    split_ifs with hjx
    · have : reparam x j = j := by rw [A, if_pos hjx]
      simp only [hF1, this]
    · have : reparam x j = g (Nat.find (Z x)) := by rw [A, if_neg hjx]
      simp only [hF1, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this :
  F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
⊢ Measurable F1
have neg : Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
  if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) sorry)) x
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this :
  F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
have neg : Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
  F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) sorry)) x
Tactic: apply Measurable.piecewise (m_meas j) (F0_meas j)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Order (goal)
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
this :
  F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
⊢ Measurable.{u_4, u_1} (β := α) fun (x : δ) ↦
    F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
have apply : ∀ (n : ℕ), MeasurableSet.{u_4} (α := δ) {x : δ | x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k}
Tactic: apply Measurable.find (fun n ↦ F0_meas (g n)) (fun n ↦ ?_)
-- 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 : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {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 ⁻¹' Ioi 0) : ℝ≥0∞)
have hd : Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
hd : Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 0)
⊢ (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have h : MeasurableSet (s ∩ f ⁻¹' Ioi 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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
-- 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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' ({0} ∪ Ioi 0)) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
-- 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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' ({0} ∪ Ioi 0)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' insert 0 (Ioi 0)) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
-- 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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' ({0} ∪ Ioi 0)) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' insert 0 (Ioi 0)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici 0) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
-- 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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' ({0} ∪ Ioi 0)) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' insert 0 (Ioi 0)) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici 0) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici ⊥) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
-- 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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' ({0} ∪ Ioi 0)) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' insert 0 (Ioi 0)) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici 0) : ℝ≥0∞)
rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici ⊥) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' univ) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
-- 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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' ({0} ∪ Ioi 0)) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' insert 0 (Ioi 0)) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici 0) : ℝ≥0∞)
rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici ⊥) : ℝ≥0∞)
rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' univ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw₆ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ univ) : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
-- 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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (f ⁻¹' {0} ∪ f ⁻¹' Ioi 0)) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' ({0} ∪ Ioi 0)) : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' insert 0 (Ioi 0)) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici 0) : ℝ≥0∞)
rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ici ⊥) : ℝ≥0∞)
rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' univ) : ℝ≥0∞)
rw₆ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ univ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
have rw₇ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
-- 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 : 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 A : (μ : (a : Set α) → ℝ≥0∞) s =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
Tactic: have A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0) := by
    rw [← measure_union]
    · rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
    · exact disjoint_singleton_left.mpr self_notMem_Ioi
        |>.preimage f |>.inter_right' s |>.inter_left' s
    · exact hs.inter (hf measurableSet_Ioi)
-- 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∞)
⊢ (μ : (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 rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞} ∪ s ∩ f ⁻¹' Ioo 0 ∞) : ℝ≥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∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ioi 0) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞} ∪ s ∩ f ⁻¹' Ioo 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∞)
have hd : Disjoint (s ∩ f ⁻¹' {∞}) (s ∩ f ⁻¹' Ioo 0 ∞)
Tactic: rw [← measure_union]