α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
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})
α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
m : MeasurableSpace α
μ ν✝ : Measure α
inst✝ : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H : ∀ (y : ℝ≥0∞), ↑↑μ (↑f ⁻¹' {y}) = ↑↑ν (↑g ⁻¹' {y})
⊢ lintegral f μ = lintegral g ν
simp only [lintegral, ← H]
case hs
α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
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
α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
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})
apply lintegral_eq_of_subset
case hs
α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
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
case hs
α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
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
simp only [H]
case hs
α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
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
case hs
α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
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
intros
no goals
case hs
α : Type u_2
β : Type u_1
γ : Type ?u.900789
δ : Type ?u.900792
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
exact mem_range_of_measure_ne_zero ‹_›