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 f' : M → F
μ : Measure M
U : Opens M
⊢ BorelSpace.{u_4} ↥U

Tactic:
inferInstanceAs (BorelSpace (U : Set M))

Premises used: _private.0.instBorelSpaceSubtypeMemOpens._proof_1
-- 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 : Set M
hU : IsOpen[inst_7] U
hSig : IsSigmaCompact 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
⊢ MeasurableSet U

Tactic:
have meas_U := hU.measurableSet
-- 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 : Set M
hU : IsOpen[inst_7] U
hSig : IsSigmaCompact 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
meas_U : MeasurableSet U
rw : ∀ᵐ (x : (↑U : Type u_4)) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) μ, f (↑x : M) = 0
⊢ ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0

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

Premises used: ae_restrict_iff_subtype, MeasureTheory.ae_restrict_iff'
-- 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 μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U_1 → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
change : ∀ᵐ (x : ↥U) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ, f (↑x : M) = 0
⊢ ∀ᵐ (x : (↑U_1 : Type u_4)) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ, f (↑x : M) = 0

Tactic:
change ∀ᵐ (x : U) ∂_, _
-- 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 μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U_1 → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
⊢ SigmaCompactSpace.{u_4} ↥U

Tactic:
haveI : SigmaCompactSpace U := isSigmaCompact_iff_sigmaCompactSpace.mp hSig
-- 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 μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U_1 → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
⊢ ∀ᵐ (x : ↥U) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ, f (↑x : M) = 0

Tactic:
ae_eq_zero_of_integral_contMDiff_smul_eq_zero I ?_ fun g g_smth g_supp ↦ ?_

Premises used: ae_eq_zero_of_integral_contMDiff_smul_eq_zero, Set.Mem
-- 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 μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U_1 → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
refine_1 :
  LocallyIntegrable.{u_4, u_2} (ε := F) (fun (x : ↥U) ↦ f (↑x : M))
    (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ)
refine_2 :
  ∀ (g : ↥U → ℝ) (g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g) (g_supp : HasCompactSupport g),
    Eq.{u_2 + 1} (α := F)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
        (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
      0
⊢ ∀ᵐ (x : ↥U) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ, f (↑x : M) = 0

Tactic:
refine ae_eq_zero_of_integral_contMDiff_smul_eq_zero I ?_ fun g g_smth g_supp ↦ ?_

Premises used: 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 : M → F
μ : Measure M
U_1 : Set M
hU : IsOpen[inst_7] U_1
hSig : IsSigmaCompact U_1
hf : LocallyIntegrableOn f U_1 μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U_1 → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
⊢ LocallyIntegrable.{u_4, u_2} (ε := F) (fun (x : ↥U) ↦ f (↑x : M))
    (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ)

Tactic:
(locallyIntegrable_comap meas_U).mpr hf

Premises used: Iff.mpr, Set.Mem, MeasureTheory.locallyIntegrable_comap
-- 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 μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U_1 → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
meas_U : MeasurableSet U_1
U : Opens M := { carrier := U_1, is_open' := hU }
this : SigmaCompactSpace.{u_4} ↥U
⊢ LocallyIntegrable.{u_4, u_2} (ε := F) (fun (x : ↥U) ↦ f (↑x : M))
    (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ)

Tactic:
exact (locallyIntegrable_comap meas_U).mpr hf

Premises used: Iff.mpr, MeasureTheory.locallyIntegrable_comap
-- 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 μ
h :
  ∀ (g : M → ℝ),
    ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → tsupport g ⊆ U_1 → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
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
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0

Tactic:
specialize h (Subtype.val.extend g 0) (g_smth.extend_zero g_supp)
    (g_supp.extend_zero continuous_subtype_val) ((g_supp.tsupport_extend_zero_subset
      continuous_subtype_val).trans <| Subtype.coe_image_subset _ _)

Premises used: continuous_subtype_val, HasSubset.Subset.trans, Subtype.coe_image_subset, ContMDiff.extend_zero, Function.extend, HasCompactSupport.tsupport_extend_zero_subset, HasCompactSupport.extend_zero, OfNat.ofNat, Subtype.val
-- 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
refine_2 :
  ∀
    (h :
      Eq.{u_2 + 1} (α := F)
        (∫ (x : M) in (↑U : Set M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0),
    Eq.{u_2 + 1} (α := F)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
        (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
      0
rw : ∀ (x : M) (hx : x ∉ (↑U : Set M)), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x = 0
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
    0

Tactic:
rw [← setIntegral_eq_integral_of_forall_compl_eq_zero (s := U) fun x hx ↦ ?_] at h

Premises used: MeasureTheory.setIntegral_eq_integral_of_forall_compl_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 : 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) in (↑U : Set M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0
refine_2 :
  ∀
    (h :
      Eq.{u_2 + 1} (α := F)
        (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
          (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
          Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 (↑x : M) • f (↑x : M))
        0),
    Eq.{u_2 + 1} (α := F)
      (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
        (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
      0
refine_2₁ : MeasurableSet (↑U : Set M)
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
    0

Tactic:
rw [← integral_subtype_comap] at h

Premises used: MeasureTheory.integral_subtype_comap
-- 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)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
      Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 (↑x : M) • f (↑x : M))
    0
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
      g x • f (↑x : M))
    0

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

Premises used: Subtype.val_injective, Function.Injective.extend_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 : 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)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
      g x • f (↑x : M))
    0
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
    0

Tactic:
h

Premises used: Set.Mem
-- 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)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ (↑U : Set M)))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ (↑U : Set M))) μ) fun (x : (↑(↑U : Set M) : Type u_4)) ↦
      g x • f (↑x : M))
    0
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : M) ↦ x ∈ U_1))
      (Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ) fun (x : ↥U) ↦ g x • f (↑x : M))
    0

Tactic:
exact h
-- 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) in (↑U : Set M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0
⊢ MeasurableSet (↑U : Set M)

Tactic:
meas_U
-- 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) in (↑U : Set M), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x ∂μ) 0
⊢ MeasurableSet (↑U : Set M)

Tactic:
exact meas_U
-- 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 : M
hx : x ∉ (↑U : Set M)
rw : HSMul.hSMul (α := ℝ) (0 x) (f x) = 0
rw₁ : (∃ (a : ↥U), (↑a : M) = x) → x ∈ (↑U : Set M)
⊢ Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x = 0

Tactic:
rw [Function.extend_apply' _ _ _ (mt _ hx)]

Premises used: mt, Function.extend_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 : 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 : M
hx : x ∉ (↑U : Set M)
⊢ HSMul.hSMul (α := ℝ) (0 x) (f x) = 0

Tactic:
apply zero_smul

Premises used: zero_smul
-- 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:
x.2

Premises used: Subtype.property