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 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
fun :
  ∀ (x : M) (hx : x ∈ s),
    Eq (α := ℝ)
      ((Subtype.mk (p := fun (f : M → ℝ) ↦ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f)
              (fun (x : M) ↦
                ∑ᶠ (i : ι), (((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x)
              ⋯ :
            (a : M) → ℝ)
          x :
        ℝ)
      (0 x : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, 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:
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⟩⟩
-- 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 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this_1 : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
x : M
hx : x ∈ s
this :
  ∀ (i : ι),
    Eq (α := ℝ) ((((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ)
    ((Subtype.mk (p := fun (f : M → ℝ) ↦ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f)
            (fun (x : M) ↦
              ∑ᶠ (i : ι), (((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x)
            ⋯ :
          (a : M) → ℝ)
        x :
      ℝ)
    (0 x : ℝ)

Tactic:
simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]

Premises used: finsum_zero, Pi.zero_apply, ContMDiffMap.coeFn_mk
-- 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 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
x : M
hx : x ∈ s
suffices :
  ∀ (i : ι),
    Eq (α := ℝ) ((((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ)
    ((Subtype.mk (p := fun (f : M → ℝ) ↦ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f)
            (fun (x : M) ↦
              ∑ᶠ (i : ι), (((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x)
            ⋯ :
          (a : M) → ℝ)
        x :
      ℝ)
    (0 x : ℝ)

Tactic:
suffices ∀ i, g i x = 0 by simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]
-- 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 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
x : M
hx : x ∈ s
⊢ ∀ (i : ι),
    Eq (α := ℝ) ((((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
fun i => f.toSmoothPartitionOfUnity_zero_of_zero ?_

Premises used: SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero
-- 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 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
x : M
hx : x ∈ s
refine : ∀ (i : ι), (↑(f.toFun (s := t) i) : M → ℝ) x = 0
⊢ ∀ (i : ι),
    Eq (α := ℝ) ((((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
refine fun i => f.toSmoothPartitionOfUnity_zero_of_zero ?_

Premises used: SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero
-- 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 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
x : M
hx : x ∈ s
i : ι
⊢ (↑(f.toFun (s := t) i) : M → ℝ) x = 0

Tactic:
notMem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)

Premises used: SmoothBumpCovering.IsSubordinate.support_subset, Set.subset_compl_comm, Function.notMem_support, Iff.mp
-- 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 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
x : M
hx : x ∈ s
i : ι
⊢ (↑(f.toFun (s := t) i) : M → ℝ) x = 0

Tactic:
exact notMem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)

Premises used: SmoothBumpCovering.IsSubordinate.support_subset, Set.subset_compl_comm, Function.notMem_support, Iff.mp
-- 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
ht : IsClosed[inst_3] t
hd : Disjoint s t
obtain :
  ∀ (u : Set M) (u_op : IsOpen[inst_3] u) (hsu : s ⊆ u) (hut : closure[inst_3] u ⊆ tᶜ),
    ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
      (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
obtain ⟨u, u_op, hsu, hut⟩ := normal_exists_closure_subset hs ht.isOpen_compl
    (subset_compl_iff_disjoint_left.mpr hd.symm)

Premises used: Iff.mpr, IsClosed.isOpen_compl, Set.subset_compl_iff_disjoint_left, Disjoint.symm, normal_exists_closure_subset
-- 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
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
obtain :
  ∀ (v : Set M) (v_op : IsOpen[inst_3] v) (htv : t ⊆ v) (hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ),
    ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
      (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
obtain ⟨v, v_op, htv, hvu⟩ := normal_exists_closure_subset ht isClosed_closure.isOpen_compl
    (subset_compl_comm.mp hut)

Premises used: IsClosed.isOpen_compl, Set.subset_compl_comm, Iff.mp, normal_exists_closure_subset
-- 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
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
obtain :
  ∀ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) (hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u))
    (hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v))
    (hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)),
    ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
      (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
obtain ⟨f, hfu, hfv, hf⟩ := exists_contMDiffMap_zero_one_of_isClosed I isClosed_closure
    isClosed_closure (subset_compl_iff_disjoint_left.mp hvu) (n := n)

Premises used: exists_contMDiffMap_zero_one_of_isClosed, Set.subset_compl_iff_disjoint_left, Iff.mp, isClosed_closure
-- 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
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u)
hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
⟨f, ?_, ?_, hf⟩

Premises used: And.intro, Exists.intro
-- 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
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u)
hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
refine_1 : ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)
refine_2 : ∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
refine ⟨f, ?_, ?_, 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : NormalSpace M
inst_9 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u)
hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
eventually_of_mem (mem_of_superset (u_op.mem_nhdsSet.mpr hsu) subset_closure) hfu

Premises used: Iff.mpr, subset_closure, Filter.eventually_of_mem, IsOpen.mem_nhdsSet, Filter.mem_of_superset
-- 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
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u)
hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact eventually_of_mem (mem_of_superset (u_op.mem_nhdsSet.mpr hsu) subset_closure) hfu

Premises used: Iff.mpr, subset_closure, Filter.eventually_of_mem, IsOpen.mem_nhdsSet, Filter.mem_of_superset
-- 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
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u)
hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
eventually_of_mem (mem_of_superset (v_op.mem_nhdsSet.mpr htv) subset_closure) hfv

Premises used: Iff.mpr, subset_closure, Filter.eventually_of_mem, IsOpen.mem_nhdsSet, Filter.mem_of_superset
-- 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
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u)
hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
exact eventually_of_mem (mem_of_superset (v_op.mem_nhdsSet.mpr htv) subset_closure) hfv

Premises used: Iff.mpr, subset_closure, Filter.eventually_of_mem, IsOpen.mem_nhdsSet, Filter.mem_of_superset
-- 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
rwa : s ⊆ (interior t)ᶜᶜ
rwa₁ rwa₂ rwa₃ rwa₄ : s ⊆ interior t
⊢ Disjoint (interior t)ᶜ s

Tactic:
rwa [← subset_compl_iff_disjoint_left, compl_compl]

Premises used: compl_compl, Set.subset_compl_iff_disjoint_left
-- 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
rcases :
  ∀ (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 : ℝ)),
    ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
      (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        (∀ x ∉ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
          ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
      (∀ x ∉ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
rcases exists_contMDiffMap_zero_one_nhds_of_isClosed I isOpen_interior.isClosed_compl hs
    (by rwa [← subset_compl_iff_disjoint_left, compl_compl]) (n := n) with ⟨f, h0, h1, hf⟩

Premises used: isOpen_interior, exists_contMDiffMap_zero_one_nhds_of_isClosed, IsOpen.isClosed_compl
-- 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 : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
      (∀ x ∉ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
⟨f, h1, fun x hx ↦ ?_, hf⟩

Premises used: And.intro, Exists.intro
-- 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 : ℝ)
refine : ∀ (x : M) (hx : x ∉ t), Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
      (∀ x ∉ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)

Tactic:
refine ⟨f, h1, fun x hx ↦ ?_, hf⟩