awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
U_1 : Set M
hU : IsOpen[inst_7] U_1
hSig : IsSigmaCompact U_1
hf : LocallyIntegrableOn f U_1 μ
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : Eq.{u_2 + 1} (α := F) (∫ (x : M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0
x : ↥U
hx : (↑x : M) ∉ (↑U : Set M)
⊢ (↑x : M) ∈ (↑U : Set M)

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
U : Set M
hU : IsOpen[inst_7] U
hf : LocallyIntegrableOn f U μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
⊢ ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0

Tactic:
haveI := I.locallyCompactSpace
  haveI := ChartedSpace.locallyCompactSpace H M
  haveI := hU.locallyCompactSpace
  haveI := I.secondCountableTopology
  haveI := ChartedSpace.secondCountable_of_sigmaCompact H M
  hU.ae_eq_zero_of_integral_contMDiff_smul_eq_zero' _
    (isSigmaCompact_iff_sigmaCompactSpace.mpr inferInstance) hf h

Premises used: Iff.mpr, inferInstance, isSigmaCompact_iff_sigmaCompactSpace, IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero'
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
apply :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • (f - f') x ∂μ) 0
⊢ ∀ᵐ (x : M) ∂μ, (f - f') x = 0

Tactic:
apply ae_eq_zero_of_integral_contMDiff_smul_eq_zero I (hf.sub hf')

Premises used: ae_eq_zero_of_integral_contMDiff_smul_eq_zero, MeasureTheory.LocallyIntegrable.sub
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
simp : Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x - g x • f' x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • (f - f') x ∂μ) 0

Tactic:
simp only [Pi.sub_apply, smul_sub]

Premises used: smul_sub, Pi.sub_apply
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
rw : Eq.{u_2 + 1} (α := F) (∫ (a : M), g a • f a ∂μ) (∫ (a : M), g a • f' a ∂μ)
hf₁ : Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f x) μ
hg : Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f' x) μ
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x - g x • f' x ∂μ) 0

Tactic:
rw [integral_sub, sub_eq_zero]

Premises used: sub_eq_zero, MeasureTheory.integral_sub
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ Eq.{u_2 + 1} (α := F) (∫ (a : M), g a • f a ∂μ) (∫ (a : M), g a • f' a ∂μ)

Tactic:
h g g_diff g_supp
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ Eq.{u_2 + 1} (α := F) (∫ (a : M), g a • f a ∂μ) (∫ (a : M), g a • f' a ∂μ)

Tactic:
exact h g g_diff g_supp
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f x) μ

Tactic:
hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp

Premises used: ContMDiff.continuous, MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f x) μ

Tactic:
exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp

Premises used: ContMDiff.continuous, MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f' x) μ

Tactic:
hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp

Premises used: ContMDiff.continuous, MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
g : M → ℝ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ Integrable.{u_2, u_4} (ε := F) (fun (x : M) ↦ g x • f' x) μ

Tactic:
exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp

Premises used: ContMDiff.continuous, MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
⊢ ∀ᵐ (x : M) ∂μ, (f - f') x = 0

Tactic:
have : ∀ᵐ x ∂μ, (f - f') x = 0 := by
    apply ae_eq_zero_of_integral_contMDiff_smul_eq_zero I (hf.sub hf')
    intro g g_diff g_supp
    simp only [Pi.sub_apply, smul_sub]
    rw [integral_sub, sub_eq_zero]
    · exact h g g_diff g_supp
    · exact hf.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
    · exact hf'.integrable_smul_left_of_hasCompactSupport g_diff.continuous g_supp
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0
h₁ : ∀ (x : M) (hx : (f - f') x = 0), f x = f' x
⊢ ∀ᵐ (x : M) ∂μ, f x = f' x

Tactic:
filter_upwards [this] with x hx
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
H : Type u_3
inst_6 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : IsManifold I ∞ M
inst_10 : MeasurableSpace M
inst_11 : BorelSpace M
inst_12 : T2Space M
f f' : M → F
μ : Measure M
inst_13 : SigmaCompactSpace M
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g →
      HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) (∫ (x : M), g x • f' x ∂μ)
this : ∀ᵐ (x : M) ∂μ, (f - f') x = 0
x : M
hx : (f - f') x = 0
⊢ f x = f' x

Tactic:
simpa [sub_eq_zero] using hx

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
f : E → F
μ : Measure E
hf : LocallyIntegrable f μ
h : ∀ (g : E → ℝ), ContDiff ℝ ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : E), g x • f x ∂μ) 0
⊢ ∀ᵐ (x : E) ∂μ, f x = 0

Tactic:
ae_eq_zero_of_integral_contMDiff_smul_eq_zero 𝓘(ℝ, E) hf
    (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)

Premises used: Real, ae_eq_zero_of_integral_contMDiff_smul_eq_zero, ContMDiff.contDiff, modelWithCornersSelf
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
f f' : E → F
μ : Measure E
hf : LocallyIntegrable f μ
hf' : LocallyIntegrable f' μ
h :
  ∀ (g : E → ℝ),
    ContDiff ℝ ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : E), g x • f x ∂μ) (∫ (x : E), g x • f' x ∂μ)
⊢ ∀ᵐ (x : E) ∂μ, f x = f' x

Tactic:
ae_eq_of_integral_contMDiff_smul_eq 𝓘(ℝ, E) hf hf'
    (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)

Premises used: Real, ae_eq_of_integral_contMDiff_smul_eq, ContMDiff.contDiff, modelWithCornersSelf
-- Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
f : E → F
μ : Measure E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : LocallyIntegrableOn f U μ
h :
  ∀ (g : E → ℝ),
    ContDiff ℝ ∞ g → HasCompactSupport g → tsupport g ⊆ U → Eq.{u_2 + 1} (α := F) (∫ (x : E), g x • f x ∂μ) 0
⊢ ∀ᵐ (x : E) ∂μ, x ∈ U → f x = 0

Tactic:
hU.ae_eq_zero_of_integral_contMDiff_smul_eq_zero 𝓘(ℝ, E) hf
    (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)

Premises used: Real, ContMDiff.contDiff, modelWithCornersSelf, IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F_1 : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
inst_6 : SMulCommClass ℝ 𝕜 F_1
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
K_1 K₁ K₂ : Compacts E_1
B : Type u_5
E : Type u_6
F : Type u_7
inst_11 : NormedAddCommGroup E
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace ℝ E
inst_14 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
inst_15 : ContDiffMapSupportedInClass B E F n K
f : B
⊢ HasCompactSupport (⇑f : (a : E) → F)

Tactic:
have := HasCompactSupport.intro K.isCompact (map_zero_on_compl f)
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F_1 : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
inst_6 : SMulCommClass ℝ 𝕜 F_1
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
K_1 K₁ K₂ : Compacts E_1
B : Type u_5
E : Type u_6
F : Type u_7
inst_11 : NormedAddCommGroup E
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace ℝ E
inst_14 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
inst_15 : ContDiffMapSupportedInClass B E F n K
f : B
this : HasCompactSupport (⇑f : (a : E) → F)
rcases :
  ∀ (C : ℝ) (hC : ∀ (x : E), ‖(f : (a : E) → F) x‖ ≤ C),
    ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C

Tactic:
rcases (map_continuous f).bounded_above_of_compact_support this with ⟨C, hC⟩

Premises used: Continuous.bounded_above_of_compact_support, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F_1 : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
inst_6 : SMulCommClass ℝ 𝕜 F_1
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
K_1 K₁ K₂ : Compacts E_1
B : Type u_5
E : Type u_6
F : Type u_7
inst_11 : NormedAddCommGroup E
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace ℝ E
inst_14 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
inst_15 : ContDiffMapSupportedInClass B E F n K
f : B
this : HasCompactSupport (⇑f : (a : E) → F)
C : ℝ
hC : ∀ (x : E), ‖(f : (a : E) → F) x‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C

Tactic:
map_bounded (BoundedContinuousFunction.ofNormedAddCommGroup f (map_continuous f) C hC)

Premises used: BoundedContinuousMapClass.map_bounded, BoundedContinuousFunction.ofNormedAddCommGroup, ContinuousMapClass.map_continuous, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E_1 : Type u_2
F_1 : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E_1
inst_2 : NormedSpace ℝ E_1
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : NormedSpace 𝕜 F_1
inst_6 : SMulCommClass ℝ 𝕜 F_1
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n_1 n₁ n₂ k : ℕ∞
K_1 K₁ K₂ : Compacts E_1
B : Type u_5
E : Type u_6
F : Type u_7
inst_11 : NormedAddCommGroup E
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace ℝ E
inst_14 : NormedSpace ℝ F
n : ℕ∞
K : Compacts E
inst_15 : ContDiffMapSupportedInClass B E F n K
f : B
this : HasCompactSupport (⇑f : (a : E) → F)
C : ℝ
hC : ∀ (x : E), ‖(f : (a : E) → F) x‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : E), dist ((f : (a : E) → F) x) ((f : (a : E) → F) y) ≤ C

Tactic:
exact map_bounded (BoundedContinuousFunction.ofNormedAddCommGroup f (map_continuous f) C hC)

Premises used: BoundedContinuousMapClass.map_bounded, BoundedContinuousFunction.ofNormedAddCommGroup, ContinuousMapClass.map_continuous, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
f g : 𝓓^{n}_{K}(E, F)
h : Eq (α := (a : E) → F) ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) f) ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) g)
mk :
  ∀ (toFun : E → F) (contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun) (zero_on_compl' : EqOn toFun 0 (↑K : Set E)ᶜ)
    (h :
      Eq (α := (a : E) → F)
        ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun)
          { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' })
        ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) g)),
    { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' : 𝓓^{n}_{K}(E, F) } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace ℝ F'
inst_9 : NormedSpace 𝕜 F'
inst_10 : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
g : 𝓓^{n}_{K}(E, F)
toFun : E → F
contDiff' : ContDiff ℝ (↑n : ℕ∞ω) toFun
zero_on_compl' : EqOn toFun 0 (↑K : Set E)ᶜ
h :
  Eq (α := (a : E) → F)
    ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' })
    ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun) g)
mk :
  ∀ (toFun_1 : E → F) (contDiff'_1 : ContDiff ℝ (↑n : ℕ∞ω) toFun_1) (zero_on_compl'_1 : EqOn toFun_1 0 (↑K : Set E)ᶜ)
    (h :
      Eq (α := (a : E) → F)
        ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun)
          { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' })
        ((fun (f : 𝓓^{n}_{K}(E, F)) ↦ f.toFun)
          { toFun := toFun_1, contDiff' := contDiff'_1, zero_on_compl' := zero_on_compl'_1 })),
    { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' : 𝓓^{n}_{K}(E, F) } =
      { toFun := toFun_1, contDiff' := contDiff'_1, zero_on_compl' := zero_on_compl'_1 }
⊢ { toFun := toFun, contDiff' := contDiff', zero_on_compl' := zero_on_compl' : 𝓓^{n}_{K}(E, F) } = g

Tactic:
cases g