[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f g : α →ₛ β
H : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
g : α →ₛ β
toFun✝ : α → β
measurableSet_fiber'✝ : ∀ (x : β), MeasurableSet (toFun✝ ⁻¹' {x})
finite_range'✝ : Set.Finite (range toFun✝)
H : ↑{ toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ } = ↑g
⊢ { toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
toFun✝¹ : α → β
measurableSet_fiber'✝¹ : ∀ (x : β), MeasurableSet (toFun✝¹ ⁻¹' {x})
finite_range'✝¹ : Set.Finite (range toFun✝¹)
toFun✝ : α → β
measurableSet_fiber'✝ : ∀ (x : β), MeasurableSet (toFun✝ ⁻¹' {x})
finite_range'✝ : Set.Finite (range toFun✝)
H :
  ↑{ toFun := toFun✝¹, measurableSet_fiber' := measurableSet_fiber'✝¹, finite_range' := finite_range'✝¹ } =
    ↑{ toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ }
⊢ { toFun := toFun✝¹, measurableSet_fiber' := measurableSet_fiber'✝¹, finite_range' := finite_range'✝¹ } =
    { toFun := toFun✝, measurableSet_fiber' := measurableSet_fiber'✝, finite_range' := finite_range'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : IsEmpty α
⊢ Set.Finite (range fun a => isEmptyElim a)
[PROOFSTEP]
simp [range_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∀ (y : β), y ∈ SimpleFunc.range f → p y) ↔ ∀ (x : α), p (↑f x)
[PROOFSTEP]
simp only [mem_range, Set.forall_range_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∃ y, y ∈ SimpleFunc.range f ∧ p y) ↔ ∃ x, p (↑f x)
[PROOFSTEP]
simpa only [mem_range, exists_prop] using Set.exists_range_iff
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α✝
α : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty α
b : β
⊢ ↑(SimpleFunc.range (const α b)) = ↑{b}
[PROOFSTEP]
simp [Function.const]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
inst✝ : MeasurableSpace α
b : β
⊢ ↑(SimpleFunc.range (const α b)) ⊆ ↑{b}
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
⊢ ∃ c, ∀ (x : α), ↑f x = c
[PROOFSTEP]
have hf_meas := @SimpleFunc.measurableSet_fiber α _ ⊥ f
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet (↑f ⁻¹' {x})
⊢ ∃ c, ∀ (x : α), ↑f x = c
[PROOFSTEP]
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hf_meas 
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
[PROOFSTEP]
cases' isEmpty_or_nonempty α with h h
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
h : IsEmpty α
⊢ ∃ c, ∀ (x : α), ↑f x = c
[PROOFSTEP]
simp only [IsEmpty.forall_iff, exists_const]
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ↑f ⁻¹' {x} = ∅ ∨ ↑f ⁻¹' {x} = univ
h : Nonempty α
⊢ ∃ c, ∀ (x : α), ↑f x = c
[PROOFSTEP]
specialize hf_meas (f h.some)
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅ ∨ ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
[PROOFSTEP]
cases' hf_meas with hf_meas hf_meas
[GOAL]
case inr.inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ ∃ c, ∀ (x : α), ↑f x = c
[PROOFSTEP]
exfalso
[GOAL]
case inr.inl.h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ False
[PROOFSTEP]
refine' Set.not_mem_empty h.some _
[GOAL]
case inr.inl.h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ Nonempty.some h ∈ ∅
[PROOFSTEP]
rw [← hf_meas, Set.mem_preimage]
[GOAL]
case inr.inl.h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = ∅
⊢ ↑f (Nonempty.some h) ∈ {↑f (Nonempty.some h)}
[PROOFSTEP]
exact Set.mem_singleton _
[GOAL]
case inr.inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
⊢ ∃ c, ∀ (x : α), ↑f x = c
[PROOFSTEP]
refine' ⟨f h.some, fun x => _⟩
[GOAL]
case inr.inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
⊢ ↑f x = ↑f (Nonempty.some h)
[PROOFSTEP]
have : x ∈ f ⁻¹' {f h.some} := by
  rw [hf_meas]
  exact Set.mem_univ x
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
⊢ x ∈ ↑f ⁻¹' {↑f (Nonempty.some h)}
[PROOFSTEP]
rw [hf_meas]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
⊢ x ∈ univ
[PROOFSTEP]
exact Set.mem_univ x
[GOAL]
case inr.inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
h : Nonempty α
hf_meas : ↑f ⁻¹' {↑f (Nonempty.some h)} = univ
x : α
this : x ∈ ↑f ⁻¹' {↑f (Nonempty.some h)}
⊢ ↑f x = ↑f (Nonempty.some h)
[PROOFSTEP]
rwa [Set.mem_preimage, Set.mem_singleton_iff] at this 
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
inst✝ : Nonempty β
f : α →ₛ β
⊢ ∃ c, f = const α c
[PROOFSTEP]
letI : MeasurableSpace α := ⊥
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
⊢ ∃ c, f = const α c
[PROOFSTEP]
obtain ⟨c, h_eq⟩ := simpleFunc_bot f
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
⊢ ∃ c, f = const α c
[PROOFSTEP]
refine' ⟨c, _⟩
[GOAL]
case intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
⊢ f = const α c
[PROOFSTEP]
ext1 x
[GOAL]
case intro.H
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α✝
α : Type u_5
inst✝ : Nonempty β
f : α →ₛ β
this : MeasurableSpace α := ⊥
c : β
h_eq : ∀ (x : α), ↑f x = c
x : α
⊢ ↑f x = ↑(const α c) x
[PROOFSTEP]
rw [h_eq x, SimpleFunc.coe_const, Function.const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
⊢ MeasurableSet {a | r a (↑f a)}
[PROOFSTEP]
have : {a | r a (f a)} = ⋃ b ∈ range f, {a | r a b} ∩ f ⁻¹' { b } :=
  by
  ext a
  suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
  exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
⊢ {a | r a (↑f a)} = ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ a ∈ {a | r a (↑f a)} ↔ a ∈ ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
[PROOFSTEP]
suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
this : r a (↑f a) ↔ ∃ i, r a (↑f i) ∧ ↑f a = ↑f i
⊢ a ∈ {a | r a (↑f a)} ↔ a ∈ ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
[PROOFSTEP]
simpa
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
a : α
⊢ r a (↑f a) ↔ ∃ i, r a (↑f i) ∧ ↑f a = ↑f i
[PROOFSTEP]
exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (↑f a)} = ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
⊢ MeasurableSet {a | r a (↑f a)}
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
r : α → β → Prop
f : α →ₛ β
h : ∀ (b : β), MeasurableSet {a | r a b}
this : {a | r a (↑f a)} = ⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b}
⊢ MeasurableSet (⋃ (b : β) (_ : b ∈ range ↑f), {a | r a b} ∩ ↑f ⁻¹' {b})
[PROOFSTEP]
exact MeasurableSet.biUnion f.finite_range.countable fun b _ => MeasurableSet.inter (h b) (f.measurableSet_fiber _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
μ : Measure α
⊢ ∑ y in SimpleFunc.range f, ↑↑μ (↑f ⁻¹' {y}) = ↑↑μ univ
[PROOFSTEP]
rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet sᶜ
f g : α →ₛ β
⊢ ↑(piecewise sᶜ hs f g) = ↑(piecewise s (_ : MeasurableSet s) g f)
[PROOFSTEP]
simp [hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet sᶜ
f g : α →ₛ β
⊢ Set.piecewise sᶜ ↑f ↑g = Set.piecewise s ↑g ↑f
[PROOFSTEP]
convert Set.piecewise_compl s f g
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ ↑(piecewise univ (_ : MeasurableSet univ) f g) = ↑f
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ Set.piecewise univ ↑f ↑g = ↑f
[PROOFSTEP]
convert Set.piecewise_univ f g
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ ↑(piecewise ∅ (_ : MeasurableSet ∅) f g) = ↑g
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ Set.piecewise ∅ ↑f ↑g = ↑g
[PROOFSTEP]
convert Set.piecewise_empty f g
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
hs_nonempty : Set.Nonempty s
hs_ne_univ : s ≠ univ
x y : β
⊢ SimpleFunc.range (piecewise s hs (const α x) (const α y)) = {x, y}
[PROOFSTEP]
simp only [← Finset.coe_inj, coe_range, coe_piecewise, range_piecewise, coe_const, Finset.coe_insert,
  Finset.coe_singleton, hs_nonempty.image_const, (nonempty_compl.2 hs_ne_univ).image_const, singleton_union,
  Function.const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → α →ₛ γ
⊢ (range fun a => ↑(g (↑f a)) a) ⊆ ⋃ (i : β) (_ : i ∈ range ↑f), range ↑(g i)
[PROOFSTEP]
rintro _ ⟨a, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → α →ₛ γ
a : α
⊢ (fun a => ↑(g (↑f a)) a) a ∈ ⋃ (i : β) (_ : i ∈ range ↑f), range ↑(g i)
[PROOFSTEP]
simp
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → α →ₛ γ
a : α
⊢ ∃ i y, ↑(g (↑f i)) y = ↑(g (↑f a)) a
[PROOFSTEP]
exact ⟨a, a, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : DecidableEq γ
g : β → γ
f : α →ₛ β
⊢ ↑(SimpleFunc.range (map g f)) = ↑(Finset.image g (SimpleFunc.range f))
[PROOFSTEP]
simp only [coe_range, coe_map, Finset.coe_image, range_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ ↑(map g f) ⁻¹' s = ↑f ⁻¹' ↑(Finset.filter (fun b => g b ∈ s) (SimpleFunc.range f))
[PROOFSTEP]
simp only [coe_range, sep_mem_eq, coe_map, Finset.coe_filter, ← mem_preimage, inter_comm, preimage_inter_range, ←
  Finset.mem_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ g ∘ ↑f ⁻¹' s = ↑f ⁻¹' (g ⁻¹' s)
[PROOFSTEP]
exact preimage_comp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β →ₛ γ
g : α → β
hgm : Measurable g
⊢ ↑(SimpleFunc.range (comp f g hgm)) ⊆ ↑(SimpleFunc.range f)
[PROOFSTEP]
simp only [coe_range, coe_comp, Set.range_comp_subset_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
⊢ ∀ (x : γ), MeasurableSet (Function.extend g ↑f₁ ↑f₂ ⁻¹' {x})
[PROOFSTEP]
letI : MeasurableSpace γ := ⊤
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
this : MeasurableSpace γ := ⊤
⊢ ∀ (x : γ), MeasurableSet (Function.extend g ↑f₁ ↑f₂ ⁻¹' {x})
[PROOFSTEP]
haveI : MeasurableSingletonClass γ := ⟨fun _ => trivial⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f₁ : α →ₛ γ
g : α → β
hg : MeasurableEmbedding g
f₂ : β →ₛ γ
this✝ : MeasurableSpace γ := ⊤
this : MeasurableSingletonClass γ
⊢ ∀ (x : γ), MeasurableSet (Function.extend g ↑f₁ ↑f₂ ⁻¹' {x})
[PROOFSTEP]
exact fun x => hg.measurable_extend f₁.measurable f₂.measurable (measurableSet_singleton _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ↑(pair f g) ⁻¹' {(b, c)} = ↑f ⁻¹' {b} ∩ ↑g ⁻¹' {c}
[PROOFSTEP]
rw [← singleton_prod_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
g : α →ₛ γ
b : β
c : γ
⊢ ↑(pair f g) ⁻¹' {b} ×ˢ {c} = ↑f ⁻¹' {b} ∩ ↑g ⁻¹' {c}
[PROOFSTEP]
exact pair_preimage _ _ _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ bind f (const α) = f
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
f : α →ₛ β
a✝ : α
⊢ ↑(bind f (const α)) a✝ = ↑f a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : Nonempty α
inst✝ : One β
x : β
⊢ x ∈ SimpleFunc.range 1 ↔ x ∈ {1}
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
⊢ SimpleFunc.range f = ∅
[PROOFSTEP]
rw [← Finset.not_nonempty_iff_eq_empty]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
⊢ ¬Finset.Nonempty (SimpleFunc.range f)
[PROOFSTEP]
by_contra h
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
h : Finset.Nonempty (SimpleFunc.range f)
⊢ False
[PROOFSTEP]
obtain ⟨y, hy_mem⟩ := h
[GOAL]
case intro
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : y ∈ SimpleFunc.range f
⊢ False
[PROOFSTEP]
rw [SimpleFunc.mem_range, Set.mem_range] at hy_mem 
[GOAL]
case intro
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
hy_mem : ∃ y_1, ↑f y_1 = y
⊢ False
[PROOFSTEP]
obtain ⟨x, hxy⟩ := hy_mem
[GOAL]
case intro.intro
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
β : Type u_5
hα : IsEmpty α
f : α →ₛ β
y : β
x : α
hxy : ↑f x = y
⊢ False
[PROOFSTEP]
rw [isEmpty_iff] at hα 
[GOAL]
case intro.intro
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
β : Type u_5
hα : α → False
f : α →ₛ β
y : β
x : α
hxy : ↑f x = y
⊢ False
[PROOFSTEP]
exact hα x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α
K : Type u_5
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ↑(Finset.sup s f) a = Finset.sup s fun c => ↑(f c) a
[PROOFSTEP]
refine' Finset.induction_on s rfl _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α
K : Type u_5
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s : Finset γ
a : α
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    ¬a_1 ∈ s →
      (↑(Finset.sup s f) a = Finset.sup s fun c => ↑(f c) a) →
        ↑(Finset.sup (insert a_1 s) f) a = Finset.sup (insert a_1 s) fun c => ↑(f c) a
[PROOFSTEP]
intro a s _ ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α
K : Type u_5
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : γ → α →ₛ β
s✝ : Finset γ
a✝¹ : α
a : γ
s : Finset γ
a✝ : ¬a ∈ s
ih : ↑(Finset.sup s f) a✝¹ = Finset.sup s fun c => ↑(f c) a✝¹
⊢ ↑(Finset.sup (insert a s) f) a✝¹ = Finset.sup (insert a s) fun c => ↑(f c) a✝¹
[PROOFSTEP]
rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ↑(restrict f s) = indicator s ↑f
[PROOFSTEP]
rw [restrict, dif_pos hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ↑(piecewise s hs f 0) = indicator s ↑f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
f : α →ₛ β
⊢ restrict f univ = f
[PROOFSTEP]
simp [restrict]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
f : α →ₛ β
⊢ restrict f ∅ = 0
[PROOFSTEP]
simp [restrict]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α
K : Type u_5
inst✝¹ : Zero β
inst✝ : Zero γ
g : β → γ
hg : g 0 = 0
f : α →ₛ β
s : Set α
x : α
hs : MeasurableSet s
⊢ ↑(map g (restrict f s)) x = ↑(restrict (map g f) s) x
[PROOFSTEP]
simp [hs, Set.indicator_comp_of_zero hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α
K : Type u_5
inst✝¹ : Zero β
inst✝ : Zero γ
g : β → γ
hg : g 0 = 0
f : α →ₛ β
s : Set α
x : α
hs : ¬MeasurableSet s
⊢ ↑(map g (restrict f s)) x = ↑(restrict (map g f) s) x
[PROOFSTEP]
simp [restrict_of_not_measurable hs, hg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
a : α
⊢ ↑(restrict f s) a = indicator s (↑f) a
[PROOFSTEP]
simp only [f.coe_restrict hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
t : Set β
ht : ¬0 ∈ t
⊢ ↑(restrict f s) ⁻¹' t = s ∩ ↑f ⁻¹' t
[PROOFSTEP]
simp [hs, indicator_preimage_of_not_mem _ _ ht, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hs : MeasurableSet s
⊢ r ∈ SimpleFunc.range (restrict f s) ↔ r = 0 ∧ s ≠ univ ∨ r ∈ ↑f '' s
[PROOFSTEP]
rw [← Finset.mem_coe, coe_range, coe_restrict _ hs, mem_range_indicator]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range (restrict f s)
h0 : r ≠ 0
hs : MeasurableSet s
⊢ r ∈ ↑f '' s
[PROOFSTEP]
simpa [mem_restrict_range hs, h0, -mem_range] using hr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range (restrict f s)
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ↑f '' s
[PROOFSTEP]
rw [restrict_of_not_measurable hs] at hr 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
K : Type u_5
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ SimpleFunc.range 0
h0 : r ≠ 0
hs : ¬MeasurableSet s
⊢ r ∈ ↑f '' s
[PROOFSTEP]
exact (h0 <| eq_zero_of_mem_range_zero hr).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α
K : Type u_5
inst✝¹ : Zero β
inst✝ : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : MeasurableSet s
x : α
⊢ ↑(restrict f s) x ≤ ↑(restrict g s) x
[PROOFSTEP]
simp only [coe_restrict _ hs, indicator_le_indicator (H x)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : MeasurableSpace α
K : Type u_5
inst✝¹ : Zero β
inst✝ : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : ¬MeasurableSet s
⊢ restrict f s ≤ restrict g s
[PROOFSTEP]
simp only [restrict_of_not_measurable hs, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
K : Type u_5
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ ↑(approx i f n) a = Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else 0
[PROOFSTEP]
dsimp only [approx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
K : Type u_5
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ ↑(Finset.sup (Finset.range n) fun k => restrict (const α (i k)) {a | i k ≤ f a}) a =
    Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else 0
[PROOFSTEP]
rw [finset_sup_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
K : Type u_5
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ (Finset.sup (Finset.range n) fun c => ↑(restrict (const α (i c)) {a | i c ≤ f a}) a) =
    Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else 0
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
K : Type u_5
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
⊢ (fun c => ↑(restrict (const α (i c)) {a | i c ≤ f a}) a) = fun k => if i k ≤ f a then i k else 0
[PROOFSTEP]
funext k
[GOAL]
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
K : Type u_5
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ ↑(restrict (const α (i k)) {a | i k ≤ f a}) a = if i k ≤ f a then i k else 0
[PROOFSTEP]
rw [restrict_apply]
[GOAL]
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
K : Type u_5
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ indicator {a | i k ≤ f a} (↑(const α (i k))) a = if i k ≤ f a then i k else 0
case e_f.h.hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
K : Type u_5
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet {a | i k ≤ f a}
[PROOFSTEP]
rfl
[GOAL]
case e_f.h.hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁷ : MeasurableSpace α
K : Type u_5
inst✝⁶ : SemilatticeSup β
inst✝⁵ : OrderBot β
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
inst✝² : OrderClosedTopology β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
n : ℕ
a : α
hf : Measurable f
k : ℕ
⊢ MeasurableSet {a | i k ≤ f a}
[PROOFSTEP]
exact hf measurableSet_Ici
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
K : Type u_5
inst✝⁷ : SemilatticeSup β
inst✝⁶ : OrderBot β
inst✝⁵ : Zero β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderClosedTopology β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
inst✝ : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
⊢ ↑(approx i (f ∘ g) n) a = ↑(approx i f n) (g a)
[PROOFSTEP]
rw [approx_apply _ hf, approx_apply _ (hf.comp hg)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁸ : MeasurableSpace α
K : Type u_5
inst✝⁷ : SemilatticeSup β
inst✝⁶ : OrderBot β
inst✝⁵ : Zero β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderClosedTopology β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
inst✝ : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
⊢ (Finset.sup (Finset.range n) fun k => if i k ≤ (f ∘ g) a then i k else 0) =
    Finset.sup (Finset.range n) fun k => if i k ≤ f (g a) then i k else 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
⊢ ⨆ (n : ℕ), ↑(approx i f n) a = ⨆ (k : ℕ) (_ : i k ≤ f a), i k
[PROOFSTEP]
refine' le_antisymm (iSup_le fun n => _) (iSup_le fun k => iSup_le fun hk => _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n : ℕ
⊢ ↑(approx i f n) a ≤ ⨆ (k : ℕ) (_ : i k ≤ f a), i k
[PROOFSTEP]
rw [approx_apply a hf, h_zero]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n : ℕ
⊢ (Finset.sup (Finset.range n) fun k => if i k ≤ f a then i k else ⊥) ≤ ⨆ (k : ℕ) (_ : i k ≤ f a), i k
[PROOFSTEP]
refine' Finset.sup_le fun k _ => _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
⊢ (if i k ≤ f a then i k else ⊥) ≤ ⨆ (k : ℕ) (_ : i k ≤ f a), i k
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
h : i k ≤ f a
⊢ i k ≤ ⨆ (k : ℕ) (_ : i k ≤ f a), i k
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
h : ¬i k ≤ f a
⊢ ⊥ ≤ ⨆ (k : ℕ) (_ : i k ≤ f a), i k
[PROOFSTEP]
exact le_iSup_of_le k (le_iSup (fun _ : i k ≤ f a => i k) h)
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
h : ¬i k ≤ f a
⊢ ⊥ ≤ ⨆ (k : ℕ) (_ : i k ≤ f a), i k
[PROOFSTEP]
exact bot_le
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
⊢ i k ≤ ⨆ (n : ℕ), ↑(approx i f n) a
[PROOFSTEP]
refine' le_iSup_of_le (k + 1) _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
⊢ i k ≤ ↑(approx i f (k + 1)) a
[PROOFSTEP]
rw [approx_apply a hf]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
⊢ i k ≤ Finset.sup (Finset.range (k + 1)) fun k => if i k ≤ f a then i k else 0
[PROOFSTEP]
have : k ∈ Finset.range (k + 1) := Finset.mem_range.2 (Nat.lt_succ_self _)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
this : k ∈ Finset.range (k + 1)
⊢ i k ≤ Finset.sup (Finset.range (k + 1)) fun k => if i k ≤ f a then i k else 0
[PROOFSTEP]
refine' le_trans (le_of_eq _) (Finset.le_sup this)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁶ : MeasurableSpace α
K : Type u_5
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
k : ℕ
hk : i k ≤ f a
this : k ∈ Finset.range (k + 1)
⊢ i k = if i k ≤ f a then i k else 0
[PROOFSTEP]
rw [if_pos hk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
q : ℚ
⊢ ennrealRatEmbed (Encodable.encode q) = ↑(Real.toNNReal ↑q)
[PROOFSTEP]
rw [ennrealRatEmbed, Encodable.encodek]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
q : ℚ
⊢ ENNReal.ofReal ↑(Option.getD (Option.some q) 0) = ↑(Real.toNNReal ↑q)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ↑(eapprox f n) a < ⊤
[PROOFSTEP]
simp only [eapprox, approx, finset_sup_apply, Finset.mem_range, ENNReal.bot_eq_zero, restrict]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ (Finset.sup (Finset.range n) fun c =>
      ↑(if hs : MeasurableSet {a | ennrealRatEmbed c ≤ f a} then
            piecewise {a | ennrealRatEmbed c ≤ f a} hs (const α (ennrealRatEmbed c)) 0
          else 0)
        a) <
    ⊤
[PROOFSTEP]
rw [Finset.sup_lt_iff (α := ℝ≥0∞) WithTop.zero_lt_top]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ∀ (b : ℕ),
    b ∈ Finset.range n →
      ↑(if hs : MeasurableSet {a | ennrealRatEmbed b ≤ f a} then
              piecewise {a | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
            else 0)
          a <
        ⊤
[PROOFSTEP]
intro b _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
⊢ ↑(if hs : MeasurableSet {a | ennrealRatEmbed b ≤ f a} then
          piecewise {a | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
        else 0)
      a <
    ⊤
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ ↑(piecewise {a | ennrealRatEmbed b ≤ f a} h✝ (const α (ennrealRatEmbed b)) 0) a < ⊤
[PROOFSTEP]
simp only [coe_zero, coe_piecewise, piecewise_eq_indicator, coe_const]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ Set.piecewise {a | ennrealRatEmbed b ≤ f a} (Function.const α (ennrealRatEmbed b)) 0 a < ⊤
[PROOFSTEP]
calc
  {a : α | ennrealRatEmbed b ≤ f a}.indicator (fun _ => ennrealRatEmbed b) a ≤ ennrealRatEmbed b :=
    indicator_le_self _ _ a
  _ < ⊤ := ENNReal.coe_lt_top
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ ↑0 a < ⊤
[PROOFSTEP]
exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ (n : ℕ), ↑(eapprox f n) a = f a
[PROOFSTEP]
rw [eapprox, iSup_approx_apply ennrealRatEmbed f a hf rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a
[PROOFSTEP]
refine' le_antisymm (iSup_le fun i => iSup_le fun hi => hi) (le_of_not_gt _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ¬f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False
[PROOFSTEP]
rcases ENNReal.lt_iff_exists_rat_btwn.1 h with ⟨q, _, lt_q, q_lt⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ False
[PROOFSTEP]
have : (Real.toNNReal q : ℝ≥0∞) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k :=
  by
  refine' le_iSup_of_le (Encodable.encode q) _
  rw [ennrealRatEmbed_encode q]
  refine' le_iSup_of_le (le_of_lt q_lt) _
  exact le_rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
[PROOFSTEP]
refine' le_iSup_of_le (Encodable.encode q) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)
[PROOFSTEP]
rw [ennrealRatEmbed_encode q]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ⨆ (_ : ↑(Real.toNNReal ↑q) ≤ f a), ↑(Real.toNNReal ↑q)
[PROOFSTEP]
refine' le_iSup_of_le (le_of_lt q_lt) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
⊢ ↑(Real.toNNReal ↑q) ≤ ↑(Real.toNNReal ↑q)
[PROOFSTEP]
exact le_rfl
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : f a > ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
q : ℚ
left✝ : 0 ≤ q
lt_q : ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(Real.toNNReal ↑q)
q_lt : ↑(Real.toNNReal ↑q) < f a
this : ↑(Real.toNNReal ↑q) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (lt_of_le_of_lt this lt_q)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
a : α
⊢ ∑ k in Finset.range (Nat.zero + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f Nat.zero) a
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.zero_add, Finset.sum_singleton, Finset.range_one]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
a : α
⊢ ↑(↑(eapproxDiff f 0) a) = ↑(eapprox f 0) a
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ∑ k in Finset.range (Nat.succ n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f (Nat.succ n)) a
[PROOFSTEP]
erw [Finset.sum_range_succ, Nat.succ_eq_add_one, IH, eapproxDiff, coe_map, Function.comp_apply, coe_sub, Pi.sub_apply,
  ENNReal.coe_toNNReal, add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a - ↑(eapprox f (Nat.add n 0)) a ≠ ⊤
[PROOFSTEP]
apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a - ↑(eapprox f (Nat.add n 0)) a ≤ ↑(eapprox f (n + 1)) a
[PROOFSTEP]
rw [tsub_le_iff_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k in Finset.range (n + 1), ↑(↑(eapproxDiff f k) a) = ↑(eapprox f n) a
⊢ ↑(eapprox f (Nat.add n 0 + 1)) a ≤ ↑(eapprox f (n + 1)) a + ↑(eapprox f (Nat.add n 0)) a
[PROOFSTEP]
exact le_self_add
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : MeasurableSpace α
K : Type u_5
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∑' (n : ℕ), ↑(↑(eapproxDiff f n) a) = f a
[PROOFSTEP]
simp_rw [ENNReal.tsum_eq_iSup_nat' (tendsto_add_atTop_nat 1), sum_eapproxDiff, iSup_eapprox_apply f hf a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ lintegral f μ = ∑ x in s, x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
refine' Finset.sum_bij_ne_zero (fun r _ _ => r) _ _ _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ SimpleFunc.range f) (h₂ : a * ↑↑μ (↑f ⁻¹' {a}) ≠ 0), (fun r x x => r) a h₁ h₂ ∈ s
[PROOFSTEP]
simpa only [forall_range_iff, mul_ne_zero_iff, and_imp]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a₁ a₂ : ℝ≥0∞) (h₁₁ : a₁ ∈ SimpleFunc.range f) (h₁₂ : a₁ * ↑↑μ (↑f ⁻¹' {a₁}) ≠ 0) (h₂₁ : a₂ ∈ SimpleFunc.range f)
    (h₂₂ : a₂ * ↑↑μ (↑f ⁻¹' {a₂}) ≠ 0), (fun r x x => r) a₁ h₁₁ h₁₂ = (fun r x x => r) a₂ h₂₁ h₂₂ → a₁ = a₂
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
a₁✝ a₂✝ : ℝ≥0∞
h₁₁✝ : a₁✝ ∈ SimpleFunc.range f
h₁₂✝ : a₁✝ * ↑↑μ (↑f ⁻¹' {a₁✝}) ≠ 0
h₂₁✝ : a₂✝ ∈ SimpleFunc.range f
h₂₂✝ : a₂✝ * ↑↑μ (↑f ⁻¹' {a₂✝}) ≠ 0
a✝ : (fun r x x => r) a₁✝ h₁₁✝ h₁₂✝ = (fun r x x => r) a₂✝ h₂₁✝ h₂₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
assumption
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (b : ℝ≥0∞), b ∈ s → b * ↑↑μ (↑f ⁻¹' {b}) ≠ 0 → ∃ a h₁ h₂, b = (fun r x x => r) a h₁ h₂
[PROOFSTEP]
intro b _ hb
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * ↑↑μ (↑f ⁻¹' {b}) ≠ 0
⊢ ∃ a h₁ h₂, b = (fun r x x => r) a h₁ h₂
[PROOFSTEP]
refine' ⟨b, _, hb, rfl⟩
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * ↑↑μ (↑f ⁻¹' {b}) ≠ 0
⊢ b ∈ SimpleFunc.range f
[PROOFSTEP]
rw [mem_range, ← preimage_singleton_nonempty]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * ↑↑μ (↑f ⁻¹' {b}) ≠ 0
⊢ Set.Nonempty (↑f ⁻¹' {b})
[PROOFSTEP]
exact nonempty_of_measure_ne_zero (mul_ne_zero_iff.1 hb).2
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
⊢ ∀ (a : ℝ≥0∞) (h₁ : a ∈ SimpleFunc.range f) (h₂ : a * ↑↑μ (↑f ⁻¹' {a}) ≠ 0),
    a * ↑↑μ (↑f ⁻¹' {a}) = (fun r x x => r) a h₁ h₂ * ↑↑μ (↑f ⁻¹' {(fun r x x => r) a h₁ h₂})
[PROOFSTEP]
intros
[GOAL]
case refine'_4
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ s
a✝ : ℝ≥0∞
h₁✝ : a✝ ∈ SimpleFunc.range f
h₂✝ : a✝ * ↑↑μ (↑f ⁻¹' {a✝}) ≠ 0
⊢ a✝ * ↑↑μ (↑f ⁻¹' {a✝}) = (fun r x x => r) a✝ h₁✝ h₂✝ * ↑↑μ (↑f ⁻¹' {(fun r x x => r) a✝ h₁✝ h₂✝})
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ lintegral (map g f) μ = ∑ x in SimpleFunc.range f, g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
simp only [lintegral, range_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ ∑ x in Finset.image g (SimpleFunc.range f), x * ↑↑μ (↑(map g f) ⁻¹' {x}) =
    ∑ x in SimpleFunc.range f, g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
refine' Finset.sum_image' _ fun b hb => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
b : β
hb : b ∈ SimpleFunc.range f
⊢ g b * ↑↑μ (↑(map g f) ⁻¹' {g b}) =
    ∑ x in Finset.filter (fun c' => g c' = g b) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
rcases mem_range.1 hb with ⟨a, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ g (↑f a) * ↑↑μ (↑(map g f) ⁻¹' {g (↑f a)}) =
    ∑ x in Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, Finset.mul_sum]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ ∑ x in Finset.filter (fun b => g b = g (↑f a)) (SimpleFunc.range f), g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) =
    ∑ x in Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f), g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
refine' Finset.sum_congr _ _
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ Finset.filter (fun b => g b = g (↑f a)) (SimpleFunc.range f) =
    Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f)
[PROOFSTEP]
congr
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
⊢ ∀ (x : β),
    x ∈ Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f) →
      g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
intro x
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
⊢ x ∈ Finset.filter (fun c' => g c' = g (↑f a)) (SimpleFunc.range f) →
    g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
simp only [Finset.mem_filter]
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
⊢ x ∈ SimpleFunc.range f ∧ g x = g (↑f a) → g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
rintro ⟨_, h⟩
[GOAL]
case intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : ↑f a ∈ SimpleFunc.range f
x : β
left✝ : x ∈ SimpleFunc.range f
h : g x = g (↑f a)
⊢ g (↑f a) * ↑↑μ (↑f ⁻¹' {x}) = g x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ lintegral (f + g) μ =
    ∑ x in SimpleFunc.range (pair f g), (x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) + x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}))
[PROOFSTEP]
rw [add_eq_map₂, map_lintegral]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), (x.fst + x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x}) =
    ∑ x in SimpleFunc.range (pair f g), (x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) + x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}))
[PROOFSTEP]
exact Finset.sum_congr rfl fun a _ => add_mul _ _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), (x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) + x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x})) =
    ∑ x in SimpleFunc.range (pair f g), x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) +
      ∑ x in SimpleFunc.range (pair f g), x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x})
[PROOFSTEP]
rw [Finset.sum_add_distrib]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) +
      ∑ x in SimpleFunc.range (pair f g), x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}) =
    lintegral (map Prod.fst (pair f g)) μ + lintegral (map Prod.snd (pair f g)) μ
[PROOFSTEP]
rw [map_lintegral, map_lintegral]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
⊢ ∀ (x y : Measure α), lintegral f (x + y) = lintegral f x + lintegral f y
[PROOFSTEP]
simp [lintegral, mul_add, Finset.sum_add_distrib]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
c : ℝ≥0∞
μ : Measure α
⊢ AddHom.toFun
      { toFun := lintegral f,
        map_add' :=
          (_ :
            ∀ (a a_1 : Measure α),
              ∑ x in SimpleFunc.range f, x * ↑↑(a + a_1) (↑f ⁻¹' {x}) =
                ∑ x in SimpleFunc.range f, x * ↑↑a (↑f ⁻¹' {x}) + ∑ x in SimpleFunc.range f, x * ↑↑a_1 (↑f ⁻¹' {x})) }
      (c • μ) =
    ↑(RingHom.id ℝ≥0∞) c •
      AddHom.toFun
        { toFun := lintegral f,
          map_add' :=
            (_ :
              ∀ (a a_1 : Measure α),
                ∑ x in SimpleFunc.range f, x * ↑↑(a + a_1) (↑f ⁻¹' {x}) =
                  ∑ x in SimpleFunc.range f, x * ↑↑a (↑f ⁻¹' {x}) + ∑ x in SimpleFunc.range f, x * ↑↑a_1 (↑f ⁻¹' {x})) }
        μ
[PROOFSTEP]
simp [lintegral, mul_left_comm _ c, Finset.mul_sum, Measure.smul_apply c]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ lintegral f (Measure.sum μ) = ∑' (i : ι), lintegral f (μ i)
[PROOFSTEP]
simp only [lintegral, Measure.sum_apply, f.measurableSet_preimage, ← Finset.tsum_subtype, ← ENNReal.tsum_mul_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ ∑' (x : { x // x ∈ SimpleFunc.range f }) (i : ι), ↑x * ↑↑(μ i) (↑f ⁻¹' {↑x}) =
    ∑' (i : ι) (x : { x // x ∈ SimpleFunc.range f }), ↑x * ↑↑(μ i) (↑f ⁻¹' {↑x})
[PROOFSTEP]
apply ENNReal.tsum_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : ↑(restrict f s) x ≠ 0
hxs : x ∈ s
x✝ : ↑↑μ (↑(restrict f s) ⁻¹' {↑(restrict f s) x}) ≠ 0
⊢ ↑(restrict f s) x ∈ SimpleFunc.range f
[PROOFSTEP]
simp only [f.restrict_apply hs, indicator_of_mem hxs, mem_range_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : ↑(restrict f s) x ≠ 0
hxs : ¬x ∈ s
⊢ ↑(restrict f s) x = 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ↑f b = 0
⊢ ↑f b * ↑↑μ (↑(restrict f s) ⁻¹' {↑f b}) = ↑f b * ↑↑μ (↑f ⁻¹' {↑f b} ∩ s)
[PROOFSTEP]
simp only [hb, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ¬↑f b = 0
⊢ ↑f b * ↑↑μ (↑(restrict f s) ⁻¹' {↑f b}) = ↑f b * ↑↑μ (↑f ⁻¹' {↑f b} ∩ s)
[PROOFSTEP]
rw [restrict_preimage_singleton _ hs hb, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
s : Set α
μ : Measure α
⊢ lintegral f (Measure.restrict μ s) = ∑ y in SimpleFunc.range f, y * ↑↑μ (↑f ⁻¹' {y} ∩ s)
[PROOFSTEP]
simp only [lintegral, Measure.restrict_apply, f.measurableSet_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ lintegral (restrict f s) μ = lintegral f (Measure.restrict μ s)
[PROOFSTEP]
rw [f.restrict_lintegral hs, lintegral_restrict]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
⊢ lintegral (const α c) μ = c * ↑↑μ univ
[PROOFSTEP]
rw [lintegral]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ
[PROOFSTEP]
cases isEmpty_or_nonempty α
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : IsEmpty α
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ
[PROOFSTEP]
simp [μ.eq_zero_of_isEmpty]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ ∑ x in SimpleFunc.range (const α c), x * ↑↑μ (↑(const α c) ⁻¹' {x}) = c * ↑↑μ univ
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * ↑↑μ (Function.const α c ⁻¹' {c}) = c * ↑↑μ univ
[PROOFSTEP]
unfold Function.const
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * ↑↑μ ((fun x => c) ⁻¹' {c}) = c * ↑↑μ univ
[PROOFSTEP]
rw [preimage_const_of_mem (mem_singleton c)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
s : Set α
⊢ lintegral (const α c) (Measure.restrict μ s) = c * ↑↑μ s
[PROOFSTEP]
rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ lintegral (restrict (const α c) s) μ = c * ↑↑μ s
[PROOFSTEP]
rw [restrict_lintegral_eq_lintegral_restrict _ hs, const_lintegral_restrict]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ lintegral (map Prod.fst (pair f g)) μ ⊔ lintegral (map Prod.snd (pair f g)) μ ≤
    ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x})
[PROOFSTEP]
rw [map_lintegral, map_lintegral]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ (∑ x in SimpleFunc.range (pair f g), x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x})) ⊔
      ∑ x in SimpleFunc.range (pair f g), x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}) ≤
    ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x})
[PROOFSTEP]
refine' sup_le _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) ≤
    ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x})
[PROOFSTEP]
refine' Finset.sum_le_sum fun a _ => mul_le_mul_right' _ _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}) ≤
    ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x})
[PROOFSTEP]
refine' Finset.sum_le_sum fun a _ => mul_le_mul_right' _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.fst ≤ a.fst ⊔ a.snd
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.snd ≤ a.fst ⊔ a.snd
[PROOFSTEP]
exact le_sup_left
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
a : ℝ≥0∞ × ℝ≥0∞
x✝ : a ∈ SimpleFunc.range (pair f g)
⊢ a.snd ≤ a.fst ⊔ a.snd
[PROOFSTEP]
exact le_sup_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), (x.fst ⊔ x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x}) = lintegral (f ⊔ g) μ
[PROOFSTEP]
rw [sup_eq_map₂, map_lintegral]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
hfg : f ≤ g
hμν : μ ≤ ν
⊢ lintegral (f ⊔ g) μ = lintegral g μ
[PROOFSTEP]
rw [sup_of_le_right hfg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), ↑↑μ (↑f ⁻¹' {y}) = ↑↑ν (↑g ⁻¹' {y})
⊢ lintegral f μ = lintegral g ν
[PROOFSTEP]
simp only [lintegral, ← H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), ↑↑μ (↑f ⁻¹' {y}) = ↑↑ν (↑g ⁻¹' {y})
⊢ ∑ x in SimpleFunc.range f, x * ↑↑μ (↑f ⁻¹' {x}) = ∑ x in SimpleFunc.range g, x * ↑↑μ (↑f ⁻¹' {x})
[PROOFSTEP]
apply lintegral_eq_of_subset
[GOAL]
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), ↑↑μ (↑f ⁻¹' {y}) = ↑↑ν (↑g ⁻¹' {y})
⊢ ∀ (x : α), ↑f x ≠ 0 → ↑↑μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ SimpleFunc.range g
[PROOFSTEP]
simp only [H]
[GOAL]
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), ↑↑μ (↑f ⁻¹' {y}) = ↑↑ν (↑g ⁻¹' {y})
⊢ ∀ (x : α), ↑f x ≠ 0 → ↑↑ν (↑g ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ SimpleFunc.range g
[PROOFSTEP]
intros
[GOAL]
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), ↑↑μ (↑f ⁻¹' {y}) = ↑↑ν (↑g ⁻¹' {y})
x✝ : α
a✝¹ : ↑f x✝ ≠ 0
a✝ : ↑↑ν (↑g ⁻¹' {↑f x✝}) ≠ 0
⊢ ↑f x✝ ∈ SimpleFunc.range g
[PROOFSTEP]
exact mem_range_of_measure_ne_zero ‹_›
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
h : ↑f =ᵐ[μ] ↑g
y : ℝ≥0∞
x : α
hx : ↑f x = ↑g x
⊢ x ∈ ↑f ⁻¹' {y} ↔ x ∈ ↑g ⁻¹' {y}
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
β : Type u_5
inst✝ : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), ↑f a = ↑g (m' a)
h : ∀ (s : Set β), MeasurableSet s → ↑↑μ' s = ↑↑μ (m' ⁻¹' s)
y : ℝ≥0∞
⊢ ↑↑μ (↑f ⁻¹' {y}) = ↑↑μ' (↑g ⁻¹' {y})
[PROOFSTEP]
simp only [preimage, eq]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ ν : Measure α
β : Type u_5
inst✝ : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), ↑f a = ↑g (m' a)
h : ∀ (s : Set β), MeasurableSet s → ↑↑μ' s = ↑↑μ (m' ⁻¹' s)
y : ℝ≥0∞
⊢ ↑↑μ {x | ↑g (m' x) ∈ {y}} = ↑↑μ' {x | ↑g x ∈ {y}}
[PROOFSTEP]
exact (h (g ⁻¹' { y }) (g.measurableSet_preimage _)).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
x : α
⊢ x ∈ support ↑f ↔ x ∈ ⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y}
[PROOFSTEP]
simp only [mem_support, Set.mem_preimage, mem_filter, mem_range_self, true_and_iff, exists_prop, mem_iUnion,
  Set.mem_range, mem_singleton_iff, exists_eq_right']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝² : Zero β
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (support ↑f)
[PROOFSTEP]
rw [f.support_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝² : Zero β
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β
inst✝ : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet (⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y})
[PROOFSTEP]
exact Finset.measurableSet_biUnion _ fun y _ => measurableSet_fiber _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
⊢ SimpleFunc.FinMeasSupp f μ ↔ ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
⊢ SimpleFunc.FinMeasSupp f μ → ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
[PROOFSTEP]
refine' fun h y hy => lt_of_le_of_lt (measure_mono _) h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
h : SimpleFunc.FinMeasSupp f μ
y : β
hy : y ≠ 0
⊢ ↑f ⁻¹' {y} ⊆ {x | (fun x => ↑f x = OfNat.ofNat 0 x) x}ᶜ
[PROOFSTEP]
exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
⊢ (∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤) → SimpleFunc.FinMeasSupp f μ
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ SimpleFunc.FinMeasSupp f μ
[PROOFSTEP]
rw [finMeasSupp_iff_support, support_eq]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ↑↑μ (⋃ (y : β) (_ : y ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f)), ↑f ⁻¹' {y}) < ⊤
[PROOFSTEP]
refine' lt_of_le_of_lt (measure_biUnion_finset_le _ _) (sum_lt_top _)
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f : α →ₛ β
H : ∀ (y : β), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ ∀ (a : β), a ∈ filter (fun y => y ≠ 0) (SimpleFunc.range f) → ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
[PROOFSTEP]
exact fun y hy => (H y (Finset.mem_filter.1 hy).2).ne
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝² : Zero β✝
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β✝
β : Type u_5
inst✝ : AddMonoid β
f g : α →ₛ β
hf : SimpleFunc.FinMeasSupp f μ
hg : SimpleFunc.FinMeasSupp g μ
⊢ SimpleFunc.FinMeasSupp (f + g) μ
[PROOFSTEP]
rw [add_eq_map₂]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝² : Zero β✝
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β✝
β : Type u_5
inst✝ : AddMonoid β
f g : α →ₛ β
hf : SimpleFunc.FinMeasSupp f μ
hg : SimpleFunc.FinMeasSupp g μ
⊢ SimpleFunc.FinMeasSupp (map (fun p => p.fst + p.snd) (pair f g)) μ
[PROOFSTEP]
exact hf.map₂ hg (zero_add 0)
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝² : Zero β✝
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β✝
β : Type u_5
inst✝ : MonoidWithZero β
f g : α →ₛ β
hf : SimpleFunc.FinMeasSupp f μ
hg : SimpleFunc.FinMeasSupp g μ
⊢ SimpleFunc.FinMeasSupp (f * g) μ
[PROOFSTEP]
rw [mul_eq_map₂]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝² : Zero β✝
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β✝
β : Type u_5
inst✝ : MonoidWithZero β
f g : α →ₛ β
hf : SimpleFunc.FinMeasSupp f μ
hg : SimpleFunc.FinMeasSupp g μ
⊢ SimpleFunc.FinMeasSupp (map (fun p => p.fst * p.snd) (pair f g)) μ
[PROOFSTEP]
exact hf.map₂ hg (zero_mul 0)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
⊢ lintegral f μ < ⊤
[PROOFSTEP]
refine' sum_lt_top fun a ha => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha : a ∈ SimpleFunc.range f
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
[PROOFSTEP]
rcases eq_or_ne a ∞ with (rfl | ha)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
ha : ⊤ ∈ SimpleFunc.range f
⊢ ⊤ * ↑↑μ (↑f ⁻¹' {⊤}) ≠ ⊤
[PROOFSTEP]
simp only [ae_iff, Ne.def, Classical.not_not] at hf 
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
ha : ⊤ ∈ SimpleFunc.range f
hf : ↑↑μ {a | ↑f a = ⊤} = 0
⊢ ⊤ * ↑↑μ (↑f ⁻¹' {⊤}) ≠ ⊤
[PROOFSTEP]
simp [Set.preimage, hf]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
[PROOFSTEP]
by_cases ha0 : a = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
ha0 : a = 0
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
[PROOFSTEP]
subst a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
ha✝ : 0 ∈ SimpleFunc.range f
ha : 0 ≠ ⊤
⊢ 0 * ↑↑μ (↑f ⁻¹' {0}) ≠ ⊤
[PROOFSTEP]
rwa [zero_mul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
hm : SimpleFunc.FinMeasSupp f μ
hf : ∀ᵐ (a : α) ∂μ, ↑f a ≠ ⊤
a : ℝ≥0∞
ha✝ : a ∈ SimpleFunc.range f
ha : a ≠ ⊤
ha0 : ¬a = 0
⊢ a * ↑↑μ (↑f ⁻¹' {a}) ≠ ⊤
[PROOFSTEP]
exact mul_ne_top ha (finMeasSupp_iff.1 hm _ ha0).ne
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
h : lintegral f μ ≠ ⊤
⊢ SimpleFunc.FinMeasSupp f μ
[PROOFSTEP]
refine' finMeasSupp_iff.2 fun b hb => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
h : lintegral f μ ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {b}) < ⊤
[PROOFSTEP]
rw [f.lintegral_eq_of_subset' (Finset.subset_insert b _)] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x in insert b (SimpleFunc.range f \ {0}), x * ↑↑μ (↑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ ↑↑μ (↑f ⁻¹' {b}) < ⊤
[PROOFSTEP]
refine' ENNReal.lt_top_of_mul_ne_top_right _ hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst✝¹ : Zero β
inst✝ : Zero γ
μ : Measure α
f✝ : α →ₛ β
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x in insert b (SimpleFunc.range f \ {0}), x * ↑↑μ (↑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ b * ↑↑μ (↑f ⁻¹' {b}) ≠ ⊤
[PROOFSTEP]
exact (lt_top_of_sum_ne_top h (Finset.mem_insert_self _ _)).ne
[GOAL]
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
⊢ P f
[PROOFSTEP]
generalize h : f.range \ {0} = s
[GOAL]
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
s : Finset γ
h : SimpleFunc.range f \ {0} = s
⊢ P f
[PROOFSTEP]
rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h 
[GOAL]
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
s : Finset γ
h : range ↑f \ {0} = ↑s
⊢ P f
[PROOFSTEP]
induction s using Finset.induction generalizing f with
| empty =>
  rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h 
  convert h_ind 0 MeasurableSet.univ
  ext x
  simp [h]
| @insert x s hxs ih =>
  have mx := f.measurableSet_preimage { x }
  let g := SimpleFunc.piecewise (f ⁻¹' { x }) mx 0 f
  have Pg : P g := by
    apply ih
    simp only [SimpleFunc.coe_piecewise, range_piecewise]
    rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert, insert_diff_self_of_not_mem,
      diff_eq_empty.mpr, Set.empty_union]
    · rw [Set.image_subset_iff]
      convert Set.subset_univ _
      exact preimage_const_of_mem (mem_singleton _)
    · rwa [Finset.mem_coe]
  convert h_add _ Pg (h_ind x mx)
  · ext1 y
    by_cases hy : y ∈ f ⁻¹' { x }
    · simpa [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
    · simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
  rw [disjoint_iff_inf_le]
  rintro y
  by_cases hy : y ∈ f ⁻¹' { x }
  · simp [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
  · simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
s : Finset γ
h : range ↑f \ {0} = ↑s
⊢ P f
[PROOFSTEP]
induction s using Finset.induction generalizing f with
| empty =>
  rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h 
  convert h_ind 0 MeasurableSet.univ
  ext x
  simp [h]
| @insert x s hxs ih =>
  have mx := f.measurableSet_preimage { x }
  let g := SimpleFunc.piecewise (f ⁻¹' { x }) mx 0 f
  have Pg : P g := by
    apply ih
    simp only [SimpleFunc.coe_piecewise, range_piecewise]
    rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert, insert_diff_self_of_not_mem,
      diff_eq_empty.mpr, Set.empty_union]
    · rw [Set.image_subset_iff]
      convert Set.subset_univ _
      exact preimage_const_of_mem (mem_singleton _)
    · rwa [Finset.mem_coe]
  convert h_add _ Pg (h_ind x mx)
  · ext1 y
    by_cases hy : y ∈ f ⁻¹' { x }
    · simpa [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
    · simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
  rw [disjoint_iff_inf_le]
  rintro y
  by_cases hy : y ∈ f ⁻¹' { x }
  · simp [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
  · simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
[GOAL]
case empty
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : range ↑f \ {0} = ↑∅
⊢ P f
[PROOFSTEP]

| empty =>
  rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h 
  convert h_ind 0 MeasurableSet.univ
  ext x
  simp [h]
[GOAL]
case empty
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : range ↑f \ {0} = ↑∅
⊢ P f
[PROOFSTEP]
rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h 
[GOAL]
case empty
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
⊢ P f
[PROOFSTEP]
convert h_ind 0 MeasurableSet.univ
[GOAL]
case h.e'_1
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
⊢ f = piecewise univ (_ : MeasurableSet univ) (const α 0) (const α 0)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_1.H
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
f : α →ₛ γ
h : ↑f = Function.const α 0
x : α
⊢ ↑f x = ↑(piecewise univ (_ : MeasurableSet univ) (const α 0) (const α 0)) x
[PROOFSTEP]
simp [h]
[GOAL]
case insert
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
⊢ P f
[PROOFSTEP]

| @insert x s hxs ih =>
  have mx := f.measurableSet_preimage { x }
  let g := SimpleFunc.piecewise (f ⁻¹' { x }) mx 0 f
  have Pg : P g := by
    apply ih
    simp only [SimpleFunc.coe_piecewise, range_piecewise]
    rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert, insert_diff_self_of_not_mem,
      diff_eq_empty.mpr, Set.empty_union]
    · rw [Set.image_subset_iff]
      convert Set.subset_univ _
      exact preimage_const_of_mem (mem_singleton _)
    · rwa [Finset.mem_coe]
  convert h_add _ Pg (h_ind x mx)
  · ext1 y
    by_cases hy : y ∈ f ⁻¹' { x }
    · simpa [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
    · simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
  rw [disjoint_iff_inf_le]
  rintro y
  by_cases hy : y ∈ f ⁻¹' { x }
  · simp [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
  · simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
[GOAL]
case insert
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
⊢ P f
[PROOFSTEP]
have mx := f.measurableSet_preimage { x }
[GOAL]
case insert
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
⊢ P f
[PROOFSTEP]
let g := SimpleFunc.piecewise (f ⁻¹' { x }) mx 0 f
[GOAL]
case insert
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ P f
[PROOFSTEP]
have Pg : P g := by
  apply ih
  simp only [SimpleFunc.coe_piecewise, range_piecewise]
  rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert, insert_diff_self_of_not_mem,
    diff_eq_empty.mpr, Set.empty_union]
  · rw [Set.image_subset_iff]
    convert Set.subset_univ _
    exact preimage_const_of_mem (mem_singleton _)
  · rwa [Finset.mem_coe]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ P g
[PROOFSTEP]
apply ih
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ range ↑g \ {0} = ↑s
[PROOFSTEP]
simp only [SimpleFunc.coe_piecewise, range_piecewise]
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ (↑0 '' (↑f ⁻¹' {x}) ∪ ↑f '' (↑f ⁻¹' {x})ᶜ) \ {0} = ↑s
[PROOFSTEP]
rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert, insert_diff_self_of_not_mem,
  diff_eq_empty.mpr, Set.empty_union]
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑0 '' (↑f ⁻¹' {x}) ⊆ {0}
[PROOFSTEP]
rw [Set.image_subset_iff]
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑f ⁻¹' {x} ⊆ ↑0 ⁻¹' {0}
[PROOFSTEP]
convert Set.subset_univ _
[GOAL]
case h.e'_4
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ↑0 ⁻¹' {0} = univ
[PROOFSTEP]
exact preimage_const_of_mem (mem_singleton _)
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
⊢ ¬x ∈ ↑s
[PROOFSTEP]
rwa [Finset.mem_coe]
[GOAL]
case insert
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ P f
[PROOFSTEP]
convert h_add _ Pg (h_ind x mx)
[GOAL]
case h.e'_1
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ f = g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)
[PROOFSTEP]
ext1 y
[GOAL]
case h.e'_1.H
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y
[PROOFSTEP]
by_cases hy : y ∈ f ⁻¹' { x }
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : y ∈ ↑f ⁻¹' {x}
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y
[PROOFSTEP]
simpa [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : ¬y ∈ ↑f ⁻¹' {x}
⊢ ↑f y = ↑(g + piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) y
[PROOFSTEP]
simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
[GOAL]
case insert
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ Disjoint (support ↑g) (support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)))
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case insert
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
⊢ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) ≤ ⊥
[PROOFSTEP]
rintro y
[GOAL]
case insert
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥
[PROOFSTEP]
by_cases hy : y ∈ f ⁻¹' { x }
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : y ∈ ↑f ⁻¹' {x}
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥
[PROOFSTEP]
simp [piecewise_eq_of_mem _ _ _ hy, -piecewise_eq_indicator]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
γ✝ : Type u_3
δ : Type u_4
α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddMonoid γ
P : (α →ₛ γ) → Prop
h_ind : ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), P (piecewise s hs (const α c) (const α 0))
h_add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ↑f) (support ↑g) → P f → P g → P (f + g)
x : γ
s : Finset γ
hxs : ¬x ∈ s
ih : ∀ (f : α →ₛ γ), range ↑f \ {0} = ↑s → P f
f : α →ₛ γ
h : range ↑f \ {0} = ↑(insert x s)
mx : MeasurableSet (↑f ⁻¹' {x})
g : α →ₛ γ := piecewise (↑f ⁻¹' {x}) mx 0 f
Pg : P g
y : α
hy : ¬y ∈ ↑f ⁻¹' {x}
⊢ y ∈ support ↑g ⊓ support ↑(piecewise (↑f ⁻¹' {x}) mx (const α x) (const α 0)) → y ∈ ⊥
[PROOFSTEP]
simp [piecewise_eq_of_not_mem _ _ _ hy, -piecewise_eq_indicator]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ P f
[PROOFSTEP]
convert h_iSup (fun n => (eapprox f n).measurable) (monotone_eapprox f) _ using 1
[GOAL]
case h.e'_1
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ f = fun x => ⨆ (n : ℕ), ↑(eapprox f n) x
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_1.h
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
x : α
⊢ f x = ⨆ (n : ℕ), ↑(eapprox f n) x
[PROOFSTEP]
rw [iSup_eapprox_apply f hf]
[GOAL]
α : Type u_1
inst✝ : MeasurableSpace α
P : (α → ℝ≥0∞) → Prop
h_ind : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → P (Set.indicator s fun x => c)
h_add : ∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → P f → P g → P (f + g)
h_iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), P (f n)) → P fun x => ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), P ↑(eapprox f n)
[PROOFSTEP]
exact fun n =>
  SimpleFunc.induction (fun c s hs => h_ind c hs) (fun f g hfg hf hg => h_add hfg f.measurable g.measurable hf hg)
    (eapprox f n)
