awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : EMetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i

Tactic:
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_comm ι M]
    using exists_contMDiffMap_forall_mem_convex_of_local_const I
      Metric.exists_forall_closedEBall_subset_aux₂
      (Metric.exists_forall_closedEBall_subset_aux₁ hK hU hKU hfin)

Premises used: Metric.exists_forall_closedEBall_subset_aux₂, Set.mem_inter_iff, Metric.exists_forall_closedEBall_subset_aux₁, forall_comm, Set.mem_iInter, exists_contMDiffMap_forall_mem_convex_of_local_const, Set.mem_preimage, forall_and
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
rcases :
  ∀ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) (hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ))
    (hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i),
    ∃ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
      (∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)) ∧
        ∀ (i : ι), ∀ x ∈ K i, closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i
⊢ ∃ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i

Tactic:
rcases Metric.exists_contMDiffMap_forall_closedEBall_subset I hK hU hKU hfin with ⟨δ, hδ0, hδ⟩

Premises used: Metric.exists_contMDiffMap_forall_closedEBall_subset
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
⊢ ∃ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i

Tactic:
⟨δ, hδ0, fun i x hx => ?_⟩

Premises used: 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
refine : ∀ (i : ι) (x : M) (hx : x ∈ K i), closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i
⊢ ∃ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i

Tactic:
refine ⟨δ, hδ0, fun i x hx => ?_⟩
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
i : ι
x : M
hx : x ∈ K i
rw : closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
⊢ closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i

Tactic:
rw [← Metric.closedEBall_ofReal (hδ0 _).le]

Premises used: Metric.closedEBall_ofReal, LT.lt.le
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
i : ι
x : M
hx : x ∈ K i
⊢ closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i

Tactic:
hδ i x hx
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
i : ι
x : M
hx : x ∈ K i
⊢ closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i

Tactic:
exact hδ i x hx
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)

Tactic:
have h's : IsOpen (I.symm ⁻¹' s) := I.continuous_symm.isOpen_preimage _ hs
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
rcases :
  ∀ (f : E → ℝ) (f_supp : support f = (↑I.symm : E → H) ⁻¹' s) (f_diff : ContDiff ℝ (↑n : ℕ∞ω) f)
    (f_range : range f ⊆ Icc 0 1), ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
⊢ ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1

Tactic:
rcases h's.exists_contDiff_support_eq with ⟨f, f_supp, f_diff, f_range⟩

Premises used: IsOpen.exists_contDiff_support_eq
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
f : E → ℝ
f_supp : support f = (↑I.symm : E → H) ⁻¹' s
f_diff : ContDiff ℝ (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
⊢ ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1

Tactic:
⟨f ∘ I, ?_, ?_, ?_⟩

Premises used: Function.comp, ModelWithCorners.toFun', 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
f : E → ℝ
f_supp : support f = (↑I.symm : E → H) ⁻¹' s
f_diff : ContDiff ℝ (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
refine_1 : support (f ∘ (↑I : H → E)) = s
refine_2 : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (f ∘ (↑I : H → E))
refine_3 : range (f ∘ (↑I : H → E)) ⊆ Icc 0 1
⊢ ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1

Tactic:
refine ⟨f ∘ I, ?_, ?_, ?_⟩
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
f : E → ℝ
f_supp : support f = (↑I.symm : E → H) ⁻¹' s
f_diff : ContDiff ℝ (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
refine_1 : (↑I.symm : E → H) ∘ (↑I : H → E) ⁻¹' s = s
⊢ support (f ∘ (↑I : H → E)) = s

Tactic:
rw [support_comp_eq_preimage, f_supp, ← preimage_comp]

Premises used: Set.preimage_comp, Function.support_comp_eq_preimage
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
f : E → ℝ
f_supp : support f = (↑I.symm : E → H) ⁻¹' s
f_diff : ContDiff ℝ (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
⊢ (↑I.symm : E → H) ∘ (↑I : H → E) ⁻¹' s = s

Tactic:
simp only [ModelWithCorners.symm_comp_self, preimage_id_eq, id_eq]

Premises used: ModelWithCorners.symm_comp_self, Set.preimage_id_eq, id_eq
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
f : E → ℝ
f_supp : support f = (↑I.symm : E → H) ⁻¹' s
f_diff : ContDiff ℝ (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
⊢ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (f ∘ (↑I : H → E))

Tactic:
f_diff.comp_contMDiff contMDiff_model

Premises used: contMDiff_model, ContDiff.comp_contMDiff
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
f : E → ℝ
f_supp : support f = (↑I.symm : E → H) ⁻¹' s
f_diff : ContDiff ℝ (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
⊢ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (f ∘ (↑I : H → E))

Tactic:
exact f_diff.comp_contMDiff contMDiff_model

Premises used: contMDiff_model, ContDiff.comp_contMDiff
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
f : E → ℝ
f_supp : support f = (↑I.symm : E → H) ⁻¹' s
f_diff : ContDiff ℝ (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
⊢ range (f ∘ (↑I : H → E)) ⊆ Icc 0 1

Tactic:
Subset.trans (range_comp_subset_range _ _) f_range

Premises used: Set.range_comp_subset_range, Set.Subset.trans
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
f : E → ℝ
f_supp : support f = (↑I.symm : E → H) ⁻¹' s
f_diff : ContDiff ℝ (↑n : ℕ∞ω) f
f_range : range f ⊆ Icc 0 1
⊢ range (f ∘ (↑I : H → E)) ⊆ Icc 0 1

Tactic:
exact Subset.trans (range_comp_subset_range _ _) f_range

Premises used: Set.range_comp_subset_range, Set.Subset.trans
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
rcases :
  ∀ (f : SmoothPartitionOfUnity M I M)
    (hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source),
    ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x

Tactic:
rcases SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source I M with ⟨f, hf⟩

Premises used: SmoothPartitionOfUnity.exists_isSubordinate_chartAt_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 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
i : M
hs₁ :
  IsOpen[inst_2]
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H i)) : H → M) ⁻¹' s)
⊢ ∃ (g : H → ℝ),
    support g =
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).target ∩
          (↑(OpenPartialHomeomorph.symm (chartAt H i)) : H → M) ⁻¹' s ∧
      ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g ∧ range g ⊆ Icc 0 1

Tactic:
apply IsOpen.exists_contMDiff_support_eq_aux

Premises used: IsOpen.exists_contMDiff_support_eq_aux
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
i : M
⊢ IsOpen[inst_2]
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H i)) : H → M) ⁻¹' s)

Tactic:
OpenPartialHomeomorph.isOpen_inter_preimage_symm _ hs

Premises used: OpenPartialHomeomorph.isOpen_inter_preimage_symm
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
i : M
⊢ IsOpen[inst_2]
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H i)) : H → M) ⁻¹' s)

Tactic:
exact OpenPartialHomeomorph.isOpen_inter_preimage_symm _ hs

Premises used: OpenPartialHomeomorph.isOpen_inter_preimage_symm
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ ∀ (c : M),
    ∃ (g : H → ℝ),
      support g =
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
            (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s ∧
        ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g ∧ range g ⊆ Icc 0 1

Tactic:
have A : ∀ (c : M), ∃ g : H → ℝ,
      g.support = (chartAt H c).target ∩ (chartAt H c).symm ⁻¹' s ∧
      CMDiff n g ∧ Set.range g ⊆ Set.Icc 0 1 := by
    intro i
    apply IsOpen.exists_contMDiff_support_eq_aux
    exact OpenPartialHomeomorph.isOpen_inter_preimage_symm _ hs
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
A :
  ∀ (c : M),
    ∃ (g : H → ℝ),
      support g =
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
            (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s ∧
        ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g ∧ range g ⊆ Icc 0 1
choose :
  ∀ (g : (c : M) → H → ℝ)
    (g_supp :
      ∀ (c : M),
        support (g c) =
          (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
            (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s)
    (g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)) (hg : ∀ (c : M), range (g c) ⊆ Icc 0 1),
    ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x

Tactic:
choose g g_supp g_diff hg using A
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
⊢ ∀ (c : M) (x : H), 0 ≤ g c x

Tactic:
have h'g : ∀ c x, 0 ≤ g c x := fun c x ↦ (hg c (mem_range_self (f := g c) x)).1
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
⊢ ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))

Tactic:
have h''g : ∀ c x, 0 ≤ f c x * g c (chartAt H c x) :=
    fun c x ↦ mul_nonneg (f.nonneg c x) (h'g c _)
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x

Tactic:
⟨fun x ↦ ∑ᶠ c, f c x * g c (chartAt H c x), ?_, ?_, ?_⟩

Premises used: HMul.hMul, chartAt, finsum, OpenPartialHomeomorph.toFun', And.intro, Exists.intro, DFunLike.coe