awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
n : ℕ∞
inst_7 : T2Space M
inst_8 : NormalSpace M
inst_9 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
hd : s ⊆ interior t
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
h0 : ∀ᶠ (x : M) in 𝓝ˢ (interior t)ᶜ, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)
h1 : ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
x : M
hx : x ∉ t
⊢ Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
h0.self_of_nhdsSet _ fun hx' ↦ hx <| interior_subset hx'

Premises used: interior_subset, Filter.Eventually.self_of_nhdsSet
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
n : ℕ∞
inst_7 : T2Space M
inst_8 : NormalSpace M
inst_9 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
hd : s ⊆ interior t
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
h0 : ∀ᶠ (x : M) in 𝓝ˢ (interior t)ᶜ, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)
h1 : ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
x : M
hx : x ∉ t
⊢ Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact h0.self_of_nhdsSet _ fun hx' ↦ hx <| interior_subset hx'

Premises used: interior_subset, Filter.Eventually.self_of_nhdsSet
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : FiniteDimensional ℝ E
inst_8 : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
inl :
  ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single j s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
inr :
  ∀ (h : j ≠ i),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
⊢ ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)

Tactic:
rcases eq_or_ne j i with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : FiniteDimensional ℝ E
inst_8 : IsManifold I ∞ M
n : ℕ∞
s : Set M
j : ι
⊢ ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single j s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)

Tactic:
simp only [contMDiff_one, ContinuousMap.coe_one, BumpCovering.coe_single, Pi.single_eq_same]

Premises used: contMDiff_one, ContinuousMap.coe_one, Pi.single_eq_same, BumpCovering.coe_single
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : FiniteDimensional ℝ E
inst_8 : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
h : j ≠ i
⊢ ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)

Tactic:
simp only [contMDiff_zero, BumpCovering.coe_single, Pi.single_eq_of_ne h,
        ContinuousMap.coe_zero]

Premises used: Pi.single_eq_of_ne, ContinuousMap.coe_zero, contMDiff_zero, BumpCovering.coe_single
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : FiniteDimensional ℝ E
inst_8 : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
inl :
  ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single j s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
inr inr₁ :
  ∀ (h : j ≠ i),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
⊢ ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)

Tactic:
classical
    rcases eq_or_ne j i with (rfl | h)
    · simp only [contMDiff_one, ContinuousMap.coe_one, BumpCovering.coe_single, Pi.single_eq_same]
    · simp only [contMDiff_zero, BumpCovering.coe_single, Pi.single_eq_of_ne h,
        ContinuousMap.coe_zero]

Premises used: ContinuousMap.coe_zero, contMDiff_one, contMDiff_zero, eq_or_ne, ContinuousMap.coe_one, Pi.single_eq_same, BumpCovering.coe_single, rfl
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ LocallyCompactSpace H

Tactic:
haveI : LocallyCompactSpace H := I.locallyCompactSpace
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this : LocallyCompactSpace H
⊢ LocallyCompactSpace M

Tactic:
haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
refine_2 :
  ∀
    (this :
      ∃ (f : BumpCovering ι M s),
        (∀ (i : ι),
            ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
              (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)) ∧
          f.IsSubordinate (s := s) U),
    ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
refine_1 :
  ∀ (s t : Set M),
    IsClosed[inst_3] s →
      IsClosed[inst_3] t →
        Disjoint s t →
          ∃ (f : C(M, ℝ)),
            ContMDiff I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞ (⇑f : (a : M) → ℝ) ∧
              EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
                EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
                  ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U

Tactic:
have := BumpCovering.exists_isSubordinate_of_prop (ContMDiff I 𝓘(ℝ) ∞) ?_ hs U ho hU
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this :
  ∃ (f : BumpCovering ι M s),
    (∀ (i : ι),
        ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
          (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)) ∧
      f.IsSubordinate (s := s) U
refine_2 :
  ∀ (f : BumpCovering ι M s)
    (hf :
      ∀ (i : ι),
        ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
          (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ))
    (hfU : f.IsSubordinate (s := s) U), ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U

Tactic:
rcases this with ⟨f, hf, hfU⟩
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
f : BumpCovering ι M s
hf :
  ∀ (i : ι),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
hfU : f.IsSubordinate (s := s) U
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U

Tactic:
⟨f.toSmoothPartitionOfUnity hf, hfU.toSmoothPartitionOfUnity hf⟩

Premises used: BumpCovering.IsSubordinate.toSmoothPartitionOfUnity, BumpCovering.toSmoothPartitionOfUnity, Exists.intro
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
f : BumpCovering ι M s
hf :
  ∀ (i : ι),
    ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
      (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
hfU : f.IsSubordinate (s := s) U
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U

Tactic:
exact ⟨f.toSmoothPartitionOfUnity hf, hfU.toSmoothPartitionOfUnity hf⟩
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s_1 : Set M
hs_1 : IsClosed[inst_3] s_1
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s_1 ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
refine_1 :
  ∀ (f : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯)
    (hf :
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
        EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)),
    ∃ (f : C(M, ℝ)),
      ContMDiff I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞ (⇑f : (a : M) → ℝ) ∧
        EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
          EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
            ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C(M, ℝ)),
    ContMDiff I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞ (⇑f : (a : M) → ℝ) ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
        EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
rcases exists_contMDiffMap_zero_one_of_isClosed I hs ht hd with ⟨f, hf⟩

Premises used: exists_contMDiffMap_zero_one_of_isClosed
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s_1 : Set M
hs_1 : IsClosed[inst_3] s_1
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s_1 ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
f : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hf :
  EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
    EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
      ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C(M, ℝ)),
    ContMDiff I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞ (⇑f : (a : M) → ℝ) ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
        EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
⟨f, f.contMDiff, hf⟩

Premises used: ContMDiffMap.contMDiff, toContinuousMap, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s_1 : Set M
hs_1 : IsClosed[inst_3] s_1
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s_1 ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
f : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hf :
  EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
    EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
      ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C(M, ℝ)),
    ContMDiff I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞ (⇑f : (a : M) → ℝ) ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
        EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
exact ⟨f, f.contMDiff, hf⟩
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
apply :
  ∀ (x : M) (hx : x ∈ s),
    Membership.mem (γ := Set M)
      (⋃ (i : (↑s : Type uM)), (OpenPartialHomeomorph.toPartialEquiv (chartAt H (↑i : M))).source) x
⊢ ∃ (f : SmoothPartitionOfUnity (↑s : Type uM) I M s),
    f.IsSubordinate (s := s) fun (x : (↑s : Type uM)) ↦
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (↑x : M))).source

Tactic:
apply exists_isSubordinate _ hs _ (fun i ↦ (chartAt H _).open_source) (fun x hx ↦ ?_)

Premises used: SmoothPartitionOfUnity.exists_isSubordinate, chartAt, OpenPartialHomeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
x : M
hx : x ∈ s
⊢ Membership.mem (γ := Set M)
    (⋃ (i : (↑s : Type uM)), (OpenPartialHomeomorph.toPartialEquiv (chartAt H (↑i : M))).source) x

Tactic:
mem_iUnion_of_mem ⟨x, hx⟩ (mem_chart_source H x)

Premises used: mem_chart_source, Subtype.mk, Set.mem_iUnion_of_mem
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
x : M
hx : x ∈ s
⊢ Membership.mem (γ := Set M)
    (⋃ (i : (↑s : Type uM)), (OpenPartialHomeomorph.toPartialEquiv (chartAt H (↑i : M))).source) x

Tactic:
exact mem_iUnion_of_mem ⟨x, hx⟩ (mem_chart_source H x)

Premises used: Set.mem_iUnion_of_mem
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
apply :
  ∀ (x : M),
    Membership.mem (γ := Set M) univ x →
      Membership.mem (γ := Set M) (⋃ (i : M), (OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).source) x
⊢ ∃ (f : SmoothPartitionOfUnity M I M),
    f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
apply exists_isSubordinate _ isClosed_univ _ (fun i ↦ (chartAt H _).open_source) (fun x _ ↦ ?_)

Premises used: SmoothPartitionOfUnity.exists_isSubordinate, isClosed_univ, chartAt, OpenPartialHomeomorph.open_source
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
x : M
h : Membership.mem (γ := Set M) univ x
⊢ Membership.mem (γ := Set M) (⋃ (i : M), (OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).source) x

Tactic:
mem_iUnion_of_mem x (mem_chart_source H x)

Premises used: mem_chart_source, Set.mem_iUnion_of_mem
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
x : M
h : Membership.mem (γ := Set M) univ x
⊢ Membership.mem (γ := Set M) (⋃ (i : M), (OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).source) x

Tactic:
exact mem_iUnion_of_mem x (mem_chart_source H x)

Premises used: Set.mem_iUnion_of_mem
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst_9 : NormedAddCommGroup F_fiber
inst_10 : NormedSpace ℝ F_fiber
V : M → Type u_2
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → TopologicalSpace (V x)
inst_13 : (x : M) → Module ℝ (V x)
inst_14 : TopologicalSpace (TotalSpace F_fiber V)
inst_15 : FiberBundle F_fiber V
inst_16 : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
Hloc :
  ∀ (x₀ : M),
    ∃ U_x₀ ∈ 𝓝 x₀,
      ∃ (s_loc : (x : M) → V x),
        ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x⟩) U_x₀ ∧
          ∀ y ∈ U_x₀, s_loc y ∈ t y
choose :
  ∀ (W : (x₀ : M) → Set M) (h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀) (s_loc : (x₀ x : M) → V x)
    (s_smooth :
      ∀ (x₀ : M),
        ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x₀ x⟩)
          (W x₀))
    (h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y),
    ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
⊢ ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x

Tactic:
choose W h_nhds s_loc s_smooth h_mem_t using Hloc
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst_9 : NormedAddCommGroup F_fiber
inst_10 : NormedSpace ℝ F_fiber
V : M → Type u_2
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → TopologicalSpace (V x)
inst_13 : (x : M) → Module ℝ (V x)
inst_14 : TopologicalSpace (TotalSpace F_fiber V)
inst_15 : FiberBundle F_fiber V
inst_16 : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : (x₀ : M) → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : (x₀ x : M) → V x
s_smooth :
  ∀ (x₀ : M),
    ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : (x : M) → Set M := fun (x : M) ↦ interior (W x)
x_pt : M
_ : Membership.mem (γ := Set M) univ x_pt → Membership.mem (γ := Set M) (⋃ (x : M), U x) x_pt
⊢ Membership.mem (γ := Set M) univ x_pt → Membership.mem (γ := Set M) (⋃ (x : M), U x) x_pt

Tactic:
_
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst_9 : NormedAddCommGroup F_fiber
inst_10 : NormedSpace ℝ F_fiber
V : M → Type u_2
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → TopologicalSpace (V x)
inst_13 : (x : M) → Module ℝ (V x)
inst_14 : TopologicalSpace (TotalSpace F_fiber V)
inst_15 : FiberBundle F_fiber V
inst_16 : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : (x₀ : M) → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : (x₀ x : M) → V x
s_smooth :
  ∀ (x₀ : M),
    ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : (x : M) → Set M := fun (x : M) ↦ interior (W x)
x_pt : M
h : Membership.mem (γ := Set M) univ x_pt
simp : ∃ (i : M), x_pt ∈ U i
⊢ Membership.mem (γ := Set M) (⋃ (x : M), U x) x_pt

Tactic:
simp only [mem_iUnion]

Premises used: Set.mem_iUnion