awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Visible
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)
y : V
hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) y
z : V
hz : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) z
hxzy : Wbtw ℝ x z y
hxz : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z
⊢ y ∈ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)

Tactic:
exact AffineSubspace.right_mem_of_wbtw hxzy (subset_affineSpan _ _ <| subset_union_left rfl)
    (affineSpan_mono _ subset_union_right <| convexHull_subset_affineSpan _ <|
      hxz.mem_convexHull_isVisible hx hz) (ne_of_mem_of_not_mem hz hx).symm

Premises used: IsVisible.mem_convexHull_isVisible, Set.subset_union_right, Ne.symm, ne_of_mem_of_not_mem, Set.subset_union_left, subset_affineSpan, affineSpan_mono, convexHull_subset_affineSpan, rfl, AffineSubspace.right_mem_of_wbtw
-- Module: Mathlib.Analysis.Convex.Visible
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)
push_cast :
  Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    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 ℝ (-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:
push_cast
-- Module: Mathlib.Analysis.Convex.Visible
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 ℝ
          (-x +ᵥ
            (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
              Set V)))

Tactic:
Submodule.rank_mono ?_

Premises used: Submodule.rank_mono
-- Module: Mathlib.Analysis.Convex.Visible
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)
refine :
  LE.le (α := Submodule ℝ V) (span ℝ (-x +ᵥ s))
    (span ℝ
      (-x +ᵥ
        (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)))
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    Module.rank ℝ
      ↥(span ℝ
          (-x +ᵥ
            (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
              Set V)))

Tactic:
refine Submodule.rank_mono ?_

Premises used: Submodule.rank_mono
-- Module: Mathlib.Analysis.Convex.Visible
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 : s ⊆ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)
⊢ LE.le (α := Submodule ℝ V) (span ℝ (-x +ᵥ s))
    (span ℝ
      (-x +ᵥ
        (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Visible
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)
⊢ s ⊆ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)

Tactic:
(subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isVisible hx

Premises used: subset_convexHull, HasSubset.Subset.trans, IsClosed.convexHull_subset_affineSpan_isVisible
-- Module: Mathlib.Analysis.Convex.Visible
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)
⊢ s ⊆ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)

Tactic:
exact (subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isVisible hx

Premises used: subset_convexHull, HasSubset.Subset.trans, IsClosed.convexHull_subset_affineSpan_isVisible
-- Module: Mathlib.Analysis.Convex.Visible
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}))
rw₂ 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}))
⊢ 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:
rw [AffineSubspace.coe_pointwise_vadd, h, span_span]

Premises used: AffineSubspace.coe_pointwise_vadd, Submodule.span_span
-- Module: Mathlib.Analysis.Convex.Visible
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)
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)
⊢ 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:
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]
-- Module: Mathlib.Analysis.Convex.Visible
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)
⊢ -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:
simp [← AffineSubspace.coe_pointwise_vadd, AffineSubspace.pointwise_vadd_span,
        vadd_set_insert, -coe_affineSpan, affineSpan_insert_zero]

Premises used: Set.vadd_set_insert, AffineSubspace.coe_pointwise_vadd, coe_affineSpan, AffineSubspace.pointwise_vadd_span, affineSpan_insert_zero
-- Module: Mathlib.Analysis.Convex.Visible
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 (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) ≤
    #(↑(HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}) :
        Type u_2)

Tactic:
rank_span_le _

Premises used: rank_span_le
-- Module: Mathlib.Analysis.Convex.Visible
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)
⊢ #(↑(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:
simp
-- Module: Mathlib.Analysis.Convex.Visible
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}))
ℝ₂ :
  #(↑(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)
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    #(↑{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

Premises used: Real, setOf, Membership.mem, Subtype, HVAdd.hVAdd, rank_span_le, And, convexHull, affineSpan, SetLike.coe, IsVisible, Submodule.span, Union.union, Module.rank, Singleton.singleton, DFunLike.coe, Neg.neg
-- 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
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → Eq.{u_2 + 1} (α := F) (∫ (x : M), g x • f x ∂μ) 0
⊢ LocallyCompactSpace H

Tactic:
have := I.locallyCompactSpace
-- 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
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
⊢ LocallyCompactSpace M

Tactic:
have := ChartedSpace.locallyCompactSpace H M
-- 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
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
⊢ SecondCountableTopology H

Tactic:
have := I.secondCountableTopology
-- 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
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
⊢ SecondCountableTopology M

Tactic:
have := ChartedSpace.secondCountable_of_sigmaCompact H M
-- 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
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
apply : ∀ (s : Set M) (hs : IsCompact s), Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
⊢ ∀ᵐ (x : M) ∂μ, f x = 0

Tactic:
apply ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero' hf (fun s hs ↦ Eq.symm ?_)

Premises used: MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero', Eq.symm
-- 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
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
⊢ ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
hs.exists_isCompact_cthickening

Premises used: IsCompact.exists_isCompact_cthickening
-- 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
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
obtain : ∀ (δ : ℝ) (δpos : 0 < δ) (hδ : IsCompact (cthickening δ s)), Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)
⊢ Eq.{u_2 + 1} (α := F) 0 (∫ (x : M) in s, f x ∂μ)

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ IsCompact (cthickening δ s) := hs.exists_isCompact_cthickening

Premises used: IsCompact.exists_isCompact_cthickening
-- 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
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 : ℕ → ℝ), StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 δ) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto' δpos

Premises used: exists_seq_strictAnti_tendsto', 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
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)
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 ∂μ)
⊢ 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

Premises used: exists_seq_strictAnti_tendsto'
-- 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
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), IsCompact K ∧ ∀ (n : ℕ), v n ⊆ K

Tactic:
⟨_, hδ, fun n ↦ thickening_subset_cthickening_of_le (u_pos n).2.le _⟩

Premises used: LT.lt.le, And.right, And.intro, Exists.intro, Metric.thickening_subset_cthickening_of_le