awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
h :
  -x +ᵥ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V) =
    (↑(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
      Set V)
rw :
  Module.rank ℝ
      ↥(span ℝ
          (-x +ᵥ
            (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
              Set V))) =
    Module.rank ℝ
      ↥(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
⊢ Module.rank ℝ
      ↥(span ℝ
          (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
                (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
            Set V)) =
    Module.rank ℝ
      ↥(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
have rw₁ : Module.rank ℝ
    ↥(span ℝ
        (↑(span ℝ
              (HVAdd.hVAdd (β := Set V) (-x)
                {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
          Set V)) =
  Module.rank ℝ
    ↥(span ℝ (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
Tactic: rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
h :
  -x +ᵥ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V) =
    (↑(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
      Set V)
rw :
  Module.rank ℝ
      ↥(span ℝ
          (-x +ᵥ
            (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
              Set V))) =
    Module.rank ℝ
      ↥(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
rw₁ :
  Module.rank ℝ
      ↥(span ℝ
          (↑(span ℝ
                (HVAdd.hVAdd (β := Set V) (-x)
                  {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
            Set V)) =
    Module.rank ℝ
      ↥(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
⊢ Module.rank ℝ
      ↥(span ℝ
          (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
                (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
            Set V)) =
    Module.rank ℝ
      ↥(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
have rw₂ : Module.rank ℝ
    ↥(span ℝ
        (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) =
  Module.rank ℝ
    ↥(span ℝ (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
Tactic: rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
⊢ Module.rank ℝ
      ↥(span ℝ
          (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
                (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
            Set V)) =
    Module.rank ℝ
      ↥(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
have suffices : -x +ᵥ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V) =
  (↑(span ℝ
        (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
    Set V)
Tactic: suffices h :
        -x +ᵥ (affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V) =
          span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) by
        rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    #(↑{y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y} : Type u_2)
have ℝ : Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
  Module.rank ℝ
    ↥(span ℝ
        (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
              (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
          Set V))
Tactic: calc
    Module.rank ℝ (span ℝ (-x +ᵥ s)) ≤
      Module.rank ℝ (span ℝ
        (-x +ᵥ affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V)) := by
      push_cast
      refine Submodule.rank_mono ?_
      gcongr
      exact (subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isVisible hx
    _ = Module.rank ℝ (span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y})) := by
      suffices h :
        -x +ᵥ (affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V) =
          span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) by
        rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
      simp [← AffineSubspace.coe_pointwise_vadd, AffineSubspace.pointwise_vadd_span,
        vadd_set_insert, -coe_affineSpan, affineSpan_insert_zero]
    _ ≤ #(-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) := rank_span_le _
    _ = #{y ∈ s | IsVisible ℝ (convexHull ℝ s) x y} := by simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
ℝ :
  Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    Module.rank ℝ
      ↥(span ℝ
          (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
                (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
            Set V))
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    #(↑{y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y} : Type u_2)
have ℝ₁ : Module.rank ℝ
    ↥(span ℝ
        (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
              (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
          Set V)) =
  Module.rank ℝ
    ↥(span ℝ (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
Tactic: calc
    Module.rank ℝ (span ℝ (-x +ᵥ s)) ≤
      Module.rank ℝ (span ℝ
        (-x +ᵥ affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V)) := by
      push_cast
      refine Submodule.rank_mono ?_
      gcongr
      exact (subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isVisible hx
    _ = Module.rank ℝ (span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y})) := by
      suffices h :
        -x +ᵥ (affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V) =
          span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) by
        rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
      simp [← AffineSubspace.coe_pointwise_vadd, AffineSubspace.pointwise_vadd_span,
        vadd_set_insert, -coe_affineSpan, affineSpan_insert_zero]
    _ ≤ #(-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) := rank_span_le _
    _ = #{y ∈ s | IsVisible ℝ (convexHull ℝ s) x y} := by simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
ℝ :
  Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    Module.rank ℝ
      ↥(span ℝ
          (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
                (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
            Set V))
ℝ₁ :
  Module.rank ℝ
      ↥(span ℝ
          (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
                (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
            Set V)) =
    Module.rank ℝ
      ↥(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    #(↑{y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y} : Type u_2)
have ℝ₂ : #(↑(HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}) :
      Type u_2) =
  #(↑{y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y} : Type u_2)
Tactic: calc
    Module.rank ℝ (span ℝ (-x +ᵥ s)) ≤
      Module.rank ℝ (span ℝ
        (-x +ᵥ affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V)) := by
      push_cast
      refine Submodule.rank_mono ?_
      gcongr
      exact (subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isVisible hx
    _ = Module.rank ℝ (span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y})) := by
      suffices h :
        -x +ᵥ (affineSpan ℝ ({x} ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V) =
          span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) by
        rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
      simp [← AffineSubspace.coe_pointwise_vadd, AffineSubspace.pointwise_vadd_span,
        vadd_set_insert, -coe_affineSpan, affineSpan_insert_zero]
    _ ≤ #(-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) := rank_span_le _
    _ = #{y ∈ s | IsVisible ℝ (convexHull ℝ s) x y} := by simp
-- 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
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
have this : LocallyCompactSpace H
Tactic: have := I.locallyCompactSpace
-- 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 : LocallyCompactSpace H
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
have this₁ : LocallyCompactSpace M
Tactic: have := ChartedSpace.locallyCompactSpace H M
-- 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 : LocallyCompactSpace M
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
have this₁ : SecondCountableTopology H
Tactic: have := I.secondCountableTopology
-- 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 : SecondCountableTopology H
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
have this₁ : SecondCountableTopology M
Tactic: have := ChartedSpace.secondCountable_of_sigmaCompact H M
-- 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
⊢ ∀ᵐ (x : M) ∂μ, f x = 0
have apply : ∀ (s : Set M) (hs : IsCompact s), Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
Tactic: apply ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' hf (fun s hs ↦ Eq.symm ?_)
-- 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
⊢ Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
have obtain : ∀ (δ : ℝ) (δpos : 0 < δ) (hδ : IsCompact (cthickening δ s)), Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
Tactic: obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s) := hs.exists_isCompact_cthickening
-- 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)
⊢ Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
have obtain : ∀ (u : ℕ → ℝ) (u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ) (u_lim : Tendsto u atTop (𝓝 0)),
  Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
Tactic: obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 δ)
    ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto' δpos
-- 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
⊢ Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
have obtain : ∀ (K : Set M) (K_compact : IsCompact K) (vK : ∀ (n : ℕ), v n ⊆ K), Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
Tactic: obtain ⟨K, K_compact, vK⟩ : ∃ K, IsCompact K ∧ ∀ n, v n ⊆ K :=
    ⟨_, hδ, fun n ↦ thickening_subset_cthickening_of_le (u_pos n).2.le _⟩
-- 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
n : ℕ
⊢ ∃ (g : M → ℝ), support g = v n ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ g ∧ range g ⊆ Icc 0 1 ∧ ∀ x ∈ s, g x = 1
have rcases : ∀ (g : M → ℝ) (g_smooth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g) (g_range : range g ⊆ Icc 0 1)
  (g_supp : support g = thickening (u n) s) (hg : ∀ (x : M), x ∈ s ↔ g x = 1),
  ∃ (g : M → ℝ), support g = v n ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ g ∧ range g ⊆ Icc 0 1 ∧ ∀ x ∈ s, g x = 1
Tactic: rcases exists_contMDiff_support_eq_eq_one_iff I isOpen_thickening hs.isClosed
      (self_subset_thickening (u_pos n).1 s) with ⟨g, g_smooth, g_range, g_supp, hg⟩
-- 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
⊢ Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
have this₁ : ∀ (n : ℕ), ∃ (g : M → ℝ), support g = v n ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ g ∧ range g ⊆ Icc 0 1 ∧ ∀ x ∈ s, g x = 1
Tactic: have : ∀ n, ∃ (g : M → ℝ), support g = v n ∧ CMDiff ∞ g ∧ Set.range g ⊆ Set.Icc 0 1
          ∧ ∀ x ∈ s, g x = 1 := by
    intro n
    rcases exists_contMDiff_support_eq_eq_one_iff I isOpen_thickening hs.isClosed
      (self_subset_thickening (u_pos n).1 s) with ⟨g, g_smooth, g_range, g_supp, hg⟩
    exact ⟨g, g_supp, g_smooth, g_range, fun x hx ↦ (hg x).1 hx⟩