-- Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean
theorem IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero' {U : Set M} (hU : IsOpen U)
    (hSig : IsSigmaCompact U) (hf : LocallyIntegrableOn f U μ)
    (h : ∀ g : M → ℝ,
      ContMDiff I 𝓘(ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U → ∫ x, g x • f x ∂μ = 0) :
    ∀ᵐ x ∂μ, x ∈ U → f x = 0

Proof state:
case refine_2
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : ∫ (x : ↑↑U), Function.extend Subtype.val g 0 ↑x • f ↑x ∂Measure.comap Subtype.val μ = 0
⊢ ∫ (x : ↥U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0

Tactic:
simp_rw [Subtype.val_injective.extend_apply] at h

Result:
case refine_2
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : ∫ (x : ↑↑U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0
⊢ ∫ (x : ↥U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0

Proof state:
case intro
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
x : ↥U
hx : ↑x ∉ ↑U
⊢ ↑x ∈ ↑U

Tactic:
exact x.2

Result:
no goals

Proof state:
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
x : M
hx : x ∉ ↑U
⊢ (∃ a, ↑a = x) → x ∈ ↑U

Tactic:
rintro ⟨x, rfl⟩

Result:
case intro
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
x : ↥U
hx : ↑x ∉ ↑U
⊢ ↑x ∈ ↑U

Proof state:
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U : Set M
hU : IsOpen U
hSig : IsSigmaCompact U
hf : LocallyIntegrableOn f U μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0
meas_U : MeasurableSet U
⊢ ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0

Tactic:
rw [← ae_restrict_iff' meas_U, ae_restrict_iff_subtype meas_U]

Result:
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U : Set M
hU : IsOpen U
hSig : IsSigmaCompact U
hf : LocallyIntegrableOn f U μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U → ∫ (x : M), g x • f x ∂μ = 0
meas_U : MeasurableSet U
⊢ ∀ᵐ (x : ↑U) ∂Measure.comap Subtype.val μ, f ↑x = 0

Proof state:
case refine_1
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U✝ → ∫ (x : M), g x • f x ∂μ = 0
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
⊢ LocallyIntegrable (fun x => f ↑x) (Measure.comap Subtype.val μ)

Tactic:
exact (locallyIntegrable_comap meas_U).mpr hf

Result:
no goals