mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp

Goal state before:
pp: case refine_1
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞

pp: case refine_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp

Goal state before:
pp: case refine_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case pos
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∈ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x ↦ (f i) x • g i x) x₀

pp: case neg
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∉ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x ↦ (f i) x • g i x) x₀

Tactic:
·

Goal state after:
case pos
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∈ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x ↦ (f i) x • g i x) x₀
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case neg
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∉ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x ↦ (f i) x • g i x) x₀

Tactic:
·

Goal state after:
case neg
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∉ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x ↦ (f i) x • g i x) x₀
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_6
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ (fun v₁ v₂ ↦ v₁.carrier ⊆ v₂.carrier ∧ ∀ i ∈ v₁.carrier, v₁.toFun i = v₂.toFun i) v
    { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯, closure_subset := ⋯,
      pred_of_mem := ⋯, apply_eq := ⋯ }

pp: case refine_7
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ ¬(fun v₁ v₂ ↦ v₁.carrier ⊆ v₂.carrier ∧ ∀ i ∈ v₁.carrier, v₁.toFun i = v₂.toFun i)
      { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
        closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }
      v

pp: case refine_8
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ IsCompact
    (closure
      ({ toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
            closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }.toFun
        i))

Tactic:
·

Goal state after:
case refine_6
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ (fun v₁ v₂ ↦ v₁.carrier ⊆ v₂.carrier ∧ ∀ i ∈ v₁.carrier, v₁.toFun i = v₂.toFun i) v
    { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯, closure_subset := ⋯,
      pred_of_mem := ⋯, apply_eq := ⋯ }
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_7
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ ¬(fun v₁ v₂ ↦ v₁.carrier ⊆ v₂.carrier ∧ ∀ i ∈ v₁.carrier, v₁.toFun i = v₂.toFun i)
      { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
        closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }
      v

pp: case refine_8
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ IsCompact
    (closure
      ({ toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
            closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }.toFun
        i))

Tactic:
·

Goal state after:
case refine_7
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ ¬(fun v₁ v₂ ↦ v₁.carrier ⊆ v₂.carrier ∧ ∀ i ∈ v₁.carrier, v₁.toFun i = v₂.toFun i)
      { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
        closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }
      v
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_8
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ IsCompact
    (closure
      ({ toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
            closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }.toFun
        i))

Tactic:
·

Goal state after:
case refine_8
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
⊢ IsCompact
    (closure
      ({ toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
            closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }.toFun
        i))
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_3
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed[inst✝⁴] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f ↦ tsupport ↑f ⊆ U x) fun f ↦ support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a ↦ support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst✝⁴] (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
i : ι
⊢ tsupport
      ↑({ c := c, toFun := fun i ↦ (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
              eventuallyEq_one' := ⋯ }.toFun
          i) ⊆
    U
      ({ c := c, toFun := fun i ↦ (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
            eventuallyEq_one' := ⋯ }.c
        i)

Tactic:
·

Goal state after:
case refine_3
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed[inst✝⁴] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f ↦ tsupport ↑f ⊆ U x) fun f ↦ support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a ↦ support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst✝⁴] (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
i : ι
⊢ tsupport
      ↑({ c := c, toFun := fun i ↦ (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
              eventuallyEq_one' := ⋯ }.toFun
          i) ⊆
    U
      ({ c := c, toFun := fun i ↦ (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
            eventuallyEq_one' := ⋯ }.c
        i)
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝¹ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this✝ :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
this : ∀ (i : ι), i ∈ v.carrier
⊢ ∀ (i : ι), IsCompact (closure (v.toFun i))

pp: case refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier

Tactic:
·

Goal state after:
case refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝¹ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this✝ :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
this : ∀ (i : ι), i ∈ v.carrier
⊢ ∀ (i : ι), IsCompact (closure (v.toFun i))
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier

Tactic:
·

Goal state after:
case refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
inst✝¹ : T2Space M
inst✝ : IsManifold I ∞ M
i : ι
x : M
⊢ ∃ t, ⇑(fs.toSmoothPartitionOfUnity i) =ᶠ[𝓝 x] ↑(fs.toFun i) * ∏ j ∈ t with WellOrderingRel j i, (1 - ↑(fs.toFun j))

Tactic:
simpa using! fs.toBumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq i x

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case h.refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ s ⊆ ⋃ i, closure (v i)

pp: case h.refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ ∀ (i : ι), IsClosed ((fun i ↦ closure (v i)) i)

Tactic:
·

Goal state after:
case h.refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ s ⊆ ⋃ i, closure (v i)
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case h.refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ ∀ (i : ι), IsClosed ((fun i ↦ closure (v i)) i)

Tactic:
·

Goal state after:
case h.refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ ∀ (i : ι), IsClosed ((fun i ↦ closure (v i)) i)
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
n : ℕ∞
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
hd : Disjoint s t
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
have : ∀ x ∈ t, sᶜ ∈ 𝓝 x := fun x hx => hs.isOpen_compl.mem_nhds (disjoint_right.1 hd hx)
  rcases SmoothBumpCovering.exists_isSubordinate I ht this with ⟨ι, f, hf⟩
  set g := f.toSmoothPartitionOfUnity
  refine
    ⟨⟨_, g.contMDiff_sum.of_le (by simp)⟩, fun x hx => ?_, fun x => g.sum_eq_one, fun x =>
      ⟨g.sum_nonneg x, g.sum_le_one x⟩⟩
  suffices ∀ i, g i x = 0 by simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]
  refine fun i => f.toSmoothPartitionOfUnity_zero_of_zero ?_
  exact notMem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hut : closure[inst✝⁶] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst✝⁶] v
htv : t ⊆ v
hvu : closure[inst✝⁶] v ⊆ (closure[inst✝⁶] u)ᶜ
f : C^↑n⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (⇑f) 0 (closure[inst✝⁶] u)
hfv : EqOn (⇑f) 1 (closure[inst✝⁶] v)
hf : ∀ (x : M), f x ∈ Icc 0 1
⊢ ∀ᶠ (x : M) in 𝓝ˢ s, f x = 0

pp: case refine_2
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hut : closure[inst✝⁶] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst✝⁶] v
htv : t ⊆ v
hvu : closure[inst✝⁶] v ⊆ (closure[inst✝⁶] u)ᶜ
f : C^↑n⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (⇑f) 0 (closure[inst✝⁶] u)
hfv : EqOn (⇑f) 1 (closure[inst✝⁶] v)
hf : ∀ (x : M), f x ∈ Icc 0 1
⊢ ∀ᶠ (x : M) in 𝓝ˢ t, f x = 1

Tactic:
·

Goal state after:
case refine_1
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hut : closure[inst✝⁶] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst✝⁶] v
htv : t ⊆ v
hvu : closure[inst✝⁶] v ⊆ (closure[inst✝⁶] u)ᶜ
f : C^↑n⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (⇑f) 0 (closure[inst✝⁶] u)
hfv : EqOn (⇑f) 1 (closure[inst✝⁶] v)
hf : ∀ (x : M), f x ∈ Icc 0 1
⊢ ∀ᶠ (x : M) in 𝓝ˢ s, f x = 0