awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
ε : ℝ
εpos : 0 < ε
hε : x ∉ thickening ε s
⊢ ∀ᶠ (n : ℕ) in atTop, g n x = 0
have h₁ : ∀ (n : ℕ) (hn : u n < ε), g n x = 0
Tactic: filter_upwards [(tendsto_order.1 u_lim).2 _ εpos] with n hn
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
ε : ℝ
εpos : 0 < ε
hε : x ∉ thickening ε s
n : ℕ
hn : u n < ε
⊢ g n x = 0
have h₁ : x ∉ v n
Tactic: rw [← notMem_support, g_supp]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x_1 : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
ε : ℝ
εpos : 0 < ε
hε : x ∉ thickening ε s
n : ℕ
hn : u n < ε
⊢ x ∉ v n
have h₁ : ∀ (hε : x ∈ v n), x ∈ thickening ε s
Tactic: contrapose hε
Cleared hypotheses: hε
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
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
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun (x : M) ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable.{u_4, u_2} (β := F) (fun (x : M) ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
⊢ Tendsto.{0, u_2} (β := F) (fun (n : ℕ) ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), s.indicator f x ∂μ))
have D : ∀ᵐ (x : M) ∂μ, Tendsto (fun (n : ℕ) ↦ g n x • f x) atTop (𝓝 (s.indicator f x))
Tactic: have D : ∀ᵐ x ∂μ, Tendsto (fun n => g n x • f x) atTop (𝓝 (s.indicator f x)) := by
      filter_upwards with x
      by_cases hxs : x ∈ s
      · have : ∀ n, g n x = 1 := fun n ↦ hg n x hxs
        simp [this, indicator_of_mem hxs f]
      · simp_rw [indicator_of_notMem hxs f]
        apply tendsto_const_nhds.congr'
        suffices H : ∀ᶠ n in atTop, g n x = 0 by
          filter_upwards [H] with n hn using by simp [hn]
        obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ x ∉ thickening ε s := by
          rw [← hs.isClosed.closure_eq, closure_eq_iInter_thickening s] at hxs
          simpa using hxs
        filter_upwards [(tendsto_order.1 u_lim).2 _ εpos] with n hn
        rw [← notMem_support, g_supp]
        contrapose hε
        exact thickening_mono hn.le s hε
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
L : Tendsto.{0, u_2} (β := F) (fun (n : ℕ) ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
⊢ ∀ (n : ℕ), Eq.{u_2 + 1} (α := F) (∫ (x : M), g n x • f x ∂μ) 0
have refine : ∀ (n : ℕ), HasCompactSupport (g n)
Tactic: refine fun n ↦ h _ (g_diff n) ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
L : Tendsto.{0, u_2} (β := F) (fun (n : ℕ) ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
n : ℕ
⊢ HasCompactSupport (g n)
have apply : support (g n) ⊆ K
Tactic: apply HasCompactSupport.of_support_subset_isCompact K_compact
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
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
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this_3 : SecondCountableTopology H
this : SecondCountableTopology M
x : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun (n : ℕ) ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : (n : ℕ) → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
L : Tendsto.{0, u_2} (β := F) (fun (n : ℕ) ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))
⊢ Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
have this₁ : ∀ (n : ℕ), Eq.{u_2 + 1} (α := F) (∫ (x : M), g n x • f x ∂μ) 0
Tactic: have : ∀ n, ∫ x, g n x • f x ∂μ = 0 := by
    refine fun n ↦ h _ (g_diff n) ?_
    apply HasCompactSupport.of_support_subset_isCompact K_compact
    simpa [g_supp] using vK n
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
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
⊢ ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
have meas_U : MeasurableSet U
Tactic: have meas_U := hU.measurableSet
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
⊢ ∀ᵐ (x : M) ∂μ, x ∈ U → f x = 0
have rw : ∀ᵐ (x : (↑U : Type u_4)) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) μ, f (↑x : M) = 0
Tactic: rw [← ae_restrict_iff' meas_U, ae_restrict_iff_subtype meas_U]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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 }
⊢ ∀ᵐ (x : (↑U_1 : Type u_4)) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ, f (↑x : M) = 0
have change : ∀ᵐ (x : ↥U) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ, f (↑x : M) = 0
Tactic: change ∀ᵐ (x : U) ∂_, _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
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 }
⊢ ∀ᵐ (x : ↥U) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ, f (↑x : M) = 0
have this : SigmaCompactSpace.{u_4} ↥U
Tactic: haveI : SigmaCompactSpace U := isSigmaCompact_iff_sigmaCompactSpace.mp hSig
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
have 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)) μ)
Tactic: refine ae_eq_zero_of_integral_contMDiff_smul_eq_zero I ?_ fun g g_smth g_supp ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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)) μ)
⊢ ∀ᵐ (x : ↥U) ∂Measure.comap (Subtype.val (p := fun (x : M) ↦ x ∈ U_1)) μ, f (↑x : M) = 0
have 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
Tactic: refine ae_eq_zero_of_integral_contMDiff_smul_eq_zero I ?_ fun g g_smth g_supp ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (hypothesis)
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)
    (@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
have h₁ : 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 _ _)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
⊢ 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
have 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
Tactic: rw [← setIntegral_eq_integral_of_forall_compl_eq_zero (s := U) fun x hx ↦ ?_] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff (goal)
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
⊢ 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
have rw : ∀ (x : M) (hx : x ∉ (↑U : Set M)), Function.extend (Subtype.val (p := fun (x : M) ↦ x ∈ U)) g 0 x • f x = 0
Tactic: rw [← setIntegral_eq_integral_of_forall_compl_eq_zero (s := U) fun x hx ↦ ?_] at h