no goals
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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)))
rw [A, B, C, add_assoc]
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ MeasurableSet (s ∩ f ⁻¹' Ioi 0)
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ ↑↑μ s = ↑↑μ (s ∩ f ⁻¹' {0}) + ↑↑μ (s ∩ f ⁻¹' Ioi 0)
rw [← measure_union]
case e_a
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ s = s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ ↑↑μ s = ↑↑μ (s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0)
congr 1
case e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
⊢ x ∈ s ↔ x ∈ s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0
case e_a
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ s = s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0
ext x
case e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
this : 0 = f x ∨ 0 < f x
⊢ x ∈ s ↔ x ∈ s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0
case e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
⊢ x ∈ s ↔ x ∈ s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0
have : 0 = f x ∨ 0 < f x := eq_or_lt_of_le bot_le
case e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
this : f x = 0 ∨ 0 < f x
⊢ x ∈ s ↔ x ∈ s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0
case e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
this : 0 = f x ∨ 0 < f x
⊢ x ∈ s ↔ x ∈ s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0
rw [eq_comm] at this
no goals
case e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
this : f x = 0 ∨ 0 < f x
⊢ x ∈ s ↔ x ∈ s ∩ f ⁻¹' {0} ∪ s ∩ f ⁻¹' Ioi 0
simp only [← and_or_left, this, mem_singleton_iff, mem_inter_iff, and_true_iff, mem_union,
  mem_Ioi, mem_preimage]
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
hx : x ∈ s ∩ f ⁻¹' {0}
h'x : x ∈ s ∩ f ⁻¹' Ioi 0
⊢ False
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ Disjoint (s ∩ f ⁻¹' {0}) (s ∩ f ⁻¹' Ioi 0)
refine disjoint_left.2 fun x hx h'x => ?_
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
hx : x ∈ s ∩ f ⁻¹' {0}
h'x : x ∈ s ∩ f ⁻¹' Ioi 0
this : 0 < f x
⊢ False
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
hx : x ∈ s ∩ f ⁻¹' {0}
h'x : x ∈ s ∩ f ⁻¹' Ioi 0
⊢ False
have : 0 < f x := h'x.2
no goals
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
x : α
hx : x ∈ s ∩ f ⁻¹' {0}
h'x : x ∈ s ∩ f ⁻¹' Ioi 0
this : 0 < f x
⊢ False
exact lt_irrefl 0 (this.trans_le hx.2.le)
no goals
case h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ MeasurableSet (s ∩ f ⁻¹' Ioi 0)
exact hs.inter (hf measurableSet_Ioi)
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤)
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤)
rw [← measure_union]
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤))
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤)
rw [← inter_union_distrib_left]
case e_a.e_a
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤))
congr
case e_a.e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : α
⊢ x ∈ f ⁻¹' Ioi 0 ↔ x ∈ f ⁻¹' {⊤} ∪ f ⁻¹' Ioo 0 ⊤
case e_a.e_a
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤
ext x
case e_a.e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : α
⊢ 0 < f x ↔ f x = ⊤ ∨ 0 < f x ∧ f x < ⊤
case e_a.e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : α
⊢ x ∈ f ⁻¹' Ioi 0 ↔ x ∈ f ⁻¹' {⊤} ∪ f ⁻¹' Ioo 0 ⊤
simp only [mem_singleton_iff, mem_union, mem_Ioo, mem_Ioi, mem_preimage]
case e_a.e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 = ⊤ ∨ f x < ⊤
⊢ 0 < f x ↔ f x = ⊤ ∨ 0 < f x ∧ f x < ⊤
case e_a.e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : α
⊢ 0 < f x ↔ f x = ⊤ ∨ 0 < f x ∧ f x < ⊤
have H : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top
case e_a.e_a.h.inl
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 < ⊤

case e_a.e_a.h.inr
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 < ⊤
case e_a.e_a.h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 = ⊤ ∨ f x < ⊤
⊢ 0 < f x ↔ f x = ⊤ ∨ 0 < f x ∧ f x < ⊤
cases' H with H H
no goals
case e_a.e_a.h.inl
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 < ⊤
simp only [H, eq_self_iff_true, or_false_iff, WithTop.zero_lt_top, not_top_lt,
  and_false_iff]
no goals
case e_a.e_a.h.inr
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 < ⊤
simp only [H, H.ne, and_true_iff, false_or_iff]
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤)
refine disjoint_left.2 fun x hx h'x => ?_
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤
this : f x < ⊤
⊢ False
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
have : f x < ∞ := h'x.2.2
no goals
case hd
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤
this : f x < ⊤
⊢ False
exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm))
no goals
case h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤)
exact hs.inter (hf measurableSet_Ioo)
case hn
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 (Disjoint on fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

case h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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)))
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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)))
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]
case hn
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : ℤ
⊢ i ≠ j → (Disjoint on fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i j
case hn
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 (Disjoint on fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
intro i j
case hn
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : ℤ
⊢ i ≠ j → Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
case hn
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : ℤ
⊢ i ≠ j → (Disjoint on fun n => s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i j
simp only [Function.onFun]
case hn
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
⊢ Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
case hn
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 : ℤ
⊢ i ≠ j → Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
intro hij
case hn.inr
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
this :
  ∀ ⦃i j : ℤ⦄, i ≠ j → i < j → Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
h : ¬i < j
⊢ Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))

α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
⊢ Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
case hn
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
⊢ Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
wlog h : i < j generalizing i j
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∈ s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))
h'x : x ∈ s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1))
⊢ f x < f x
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
⊢ Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
refine disjoint_left.2 fun x hx h'x => lt_irrefl (f x) ?_
no goals
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ∈ s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))
h'x : x ∈ s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1))
⊢ f x < 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
no goals
case hn.inr
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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
this :
  ∀ ⦃i j : ℤ⦄, i ≠ j → i < j → Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
h : ¬i < j
⊢ Disjoint (s ∩ f ⁻¹' Ico (↑t ^ i) (↑t ^ (i + 1))) (s ∩ f ⁻¹' Ico (↑t ^ j) (↑t ^ (j + 1)))
exact (this hij.symm (hij.lt_or_lt.resolve_left h)).symm
case h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤)
n : ℤ
⊢ MeasurableSet (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
case h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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)))
intro n
no goals
case h
α : Type u_1
β : Type ?u.1709267
γ : Type ?u.1709270
γ₂ : Type ?u.1709273
δ : Type ?u.1709276
ι : Sort y
s✝ t✝ u : Set α
inst✝ : MeasurableSpace α
μ : MeasureTheory.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 ⊤)
n : ℤ
⊢ MeasurableSet (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
exact hs.inter (hf measurableSet_Ico)