-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type*} {mα : MeasurableSpace α}
    (μ : Measure α) {f : α → ℝ≥0∞} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s)
    {t : ℝ≥0} (ht : 1 < t) :
    μ s =
      μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) +
      ∑' n : ℤ, μ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1)))

Proof state:
case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ Disjoint (s ∩ f ⁻¹' {⊤}) (s ∩ f ⁻¹' Ioo 0 ⊤)

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

Result:
case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
hx : x ∈ s ∩ f ⁻¹' {⊤}
h'x : x ∈ s ∩ f ⁻¹' Ioo 0 ⊤
⊢ False

Proof state:
case h
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ MeasurableSet (s ∩ f ⁻¹' Ioi 0)

Tactic:
exact hs.inter (hf measurableSet_Ioi)

Result:
no goals

Proof state:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ (f ⁻¹' {⊤} ∪ f ⁻¹' Ioo 0 ⊤))

Tactic:
congr

Result:
case h.e_6.h.e_a
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ f ⁻¹' Ioi 0 = f ⁻¹' {⊤} ∪ f ⁻¹' Ioo 0 ⊤

Proof state:
case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 0)

Tactic:
exact disjoint_singleton_left.mpr not_mem_Ioi_self
  |>.preimage f |>.inter_right' s |>.inter_left' s

Result:
no goals

Proof state:
case hn
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)
⊢ Pairwise (Function.onFun Disjoint fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
intro i j hij

Result:
case hn
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)
i j : ℤ
hij : i ≠ j
⊢ Function.onFun Disjoint (fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i j

Proof state:
case h
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ MeasurableSet (s ∩ f ⁻¹' Ioo 0 ⊤)

Tactic:
exact hs.inter (hf measurableSet_Ioo)

Result:
no goals

Proof state:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)
i j : ℤ
hij : i ≠ j
h : i < j
⊢ Function.onFun Disjoint (fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i j

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

Result:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)
i j : ℤ
hij : i ≠ j
h : i < j
x : α
hx : x ∈ (fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i
h'x : x ∈ (fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) j
⊢ f x < f x

Proof state:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)
C : μ (s ∩ f ⁻¹' Ioo 0 ⊤) = ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
⊢ μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {⊤}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

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

Result:
no goals

Proof state:
case h.e_6.h.e_a.h.inl
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
H : f x = ⊤
⊢ 0 < f x ↔ f x = ⊤ ∨ 0 < f x ∧ f x < ⊤

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

Result:
no goals

Proof state:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)

Tactic:
rw [← measure_union]

Result:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤} ∪ s ∩ f ⁻¹' Ioo 0 ⊤)

case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ Disjoint (s ∩ f ⁻¹' {⊤}) (s ∩ f ⁻¹' Ioo 0 ⊤)

case h
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ MeasurableSet (s ∩ f ⁻¹' Ioo 0 ⊤)

Proof state:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)

Tactic:
rw [← measure_union]

Result:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ μ s = μ (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0)

case hd
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 0)

case h
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ MeasurableSet (s ∩ f ⁻¹' Ioi 0)

Proof state:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)
⊢ μ (s ∩ f ⁻¹' Ioo 0 ⊤) = ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (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]

Result:
case hn
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)
⊢ Pairwise (Function.onFun Disjoint fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

case h
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)
⊢ ∀ (i : ℤ), MeasurableSet (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1)))