case inl
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
f : α → β
⊢ map f (0 • μ) = 0 • map f μ

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
⊢ map f (c • μ) = c • map f μ
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
⊢ map f (c • μ) = c • map f μ
rcases eq_or_ne c 0 with (rfl | hc)
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
⊢ map f (c • μ) = c • map f μ

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : ¬AEMeasurable f
⊢ map f (c • μ) = c • map f μ
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
⊢ map f (c • μ) = c • map f μ
by_cases hf : AEMeasurable f μ
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
f : α → β
⊢ map f (0 • μ) = 0 • map f μ
simp
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
hfc : AEMeasurable f
⊢ map f (c • μ) = c • map f μ
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
⊢ map f (c • μ) = c • map f μ
have hfc : AEMeasurable f (c • μ) :=
  ⟨hf.mk f, hf.measurable_mk, (ae_smul_measure_iff hc).2 hf.ae_eq_mk⟩
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
hfc : AEMeasurable f
⊢ c • ↑(mapₗ (AEMeasurable.mk f hfc)) μ = c • ↑(mapₗ (AEMeasurable.mk f hf)) μ
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
hfc : AEMeasurable f
⊢ map f (c • μ) = c • map f μ
simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc,
  LinearMap.map_smulₛₗ, RingHom.id_apply]
case pos.e_a
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
hfc : AEMeasurable f
⊢ ↑(mapₗ (AEMeasurable.mk f hfc)) μ = ↑(mapₗ (AEMeasurable.mk f hf)) μ
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
hfc : AEMeasurable f
⊢ c • ↑(mapₗ (AEMeasurable.mk f hfc)) μ = c • ↑(mapₗ (AEMeasurable.mk f hf)) μ
congr 1
case pos.e_a
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
hfc : AEMeasurable f
⊢ AEMeasurable.mk f hfc =ᶠ[ae μ] AEMeasurable.mk f hf
case pos.e_a
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
hfc : AEMeasurable f
⊢ ↑(mapₗ (AEMeasurable.mk f hfc)) μ = ↑(mapₗ (AEMeasurable.mk f hf)) μ
apply mapₗ_congr hfc.measurable_mk hf.measurable_mk
no goals
case pos.e_a
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : AEMeasurable f
hfc : AEMeasurable f
⊢ AEMeasurable.mk f hfc =ᶠ[ae μ] AEMeasurable.mk f hf
exact EventuallyEq.trans ((ae_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : ¬AEMeasurable f
hfc : ¬AEMeasurable f
⊢ map f (c • μ) = c • map f μ
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : ¬AEMeasurable f
⊢ map f (c • μ) = c • map f μ
have hfc : ¬AEMeasurable f (c • μ) := by
  intro hfc
  exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_smul_measure_iff hc).1 hfc.ae_eq_mk⟩
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : ¬AEMeasurable f
hfc : ¬AEMeasurable f
⊢ map f (c • μ) = c • map f μ
simp [map_of_not_aemeasurable hf, map_of_not_aemeasurable hfc]
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : ¬AEMeasurable f
hfc : AEMeasurable f
⊢ False
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : ¬AEMeasurable f
⊢ ¬AEMeasurable f
intro hfc
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.187403
δ : Type ?u.187406
ι : Type ?u.187409
R : Type ?u.187412
R' : Type ?u.187415
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
c : ℝ≥0∞
μ : Measure α
f : α → β
hc : c ≠ 0
hf : ¬AEMeasurable f
hfc : AEMeasurable f
⊢ False
exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_smul_measure_iff hc).1 hfc.ae_eq_mk⟩