-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem WithDensityᵥEq.congr_ae {f g : α → E} (h : f =ᵐ[μ] g) :
    μ.withDensityᵥ f = μ.withDensityᵥ g

Proof state:
case pos.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ f) i = ↑(μ.withDensityᵥ g) i

Tactic:
rw [withDensityᵥ_apply hf hi, withDensityᵥ_apply (hf.congr h) hi]

Result:
case pos.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ

Proof state:
case pos.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ

Tactic:
exact integral_congr_ae (ae_restrict_of_ae h)

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
⊢ μ.withDensityᵥ f = μ.withDensityᵥ g

Tactic:
have hg : ¬Integrable g μ := by intro hg; exact hf (hg.congr h.symm)

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
hg : ¬Integrable g μ
⊢ μ.withDensityᵥ f = μ.withDensityᵥ g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
hg : Integrable g μ
⊢ False

Tactic:
exact hf (hg.congr h.symm)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
⊢ ¬Integrable g μ

Tactic:
intro hg

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
hg : Integrable g μ
⊢ False

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
⊢ μ.withDensityᵥ f = μ.withDensityᵥ g

Tactic:
ext i hi

Result:
case pos.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ f) i = ↑(μ.withDensityᵥ g) i

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
⊢ μ.withDensityᵥ f = μ.withDensityᵥ g

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f μ
⊢ μ.withDensityᵥ f = μ.withDensityᵥ g

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
⊢ μ.withDensityᵥ f = μ.withDensityᵥ g

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f μ
hg : ¬Integrable g μ
⊢ μ.withDensityᵥ f = μ.withDensityᵥ g

Tactic:
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]

Result:
no goals