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
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))
refine_1 :
  (support (M := ℝ) fun (x : M) ↦
      ∑ᶠ (c : M),
        HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (g c ((↑(chartAt H c) : M → H) x))) =
    s
refine_2 :
  ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) fun (x : M) ↦
    ∑ᶠ (c : M),
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
refine_3 :
  ∀ (x : M),
    LE.le (α := ℝ) 0
      ((fun (x : M) ↦
          (∑ᶠ (c : M),
              HMul.hMul (α := ℝ)
                ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
                (g c ((↑(chartAt H c) : M → H) x)) :
            ℝ))
        x)
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x

Tactic:
refine ⟨fun x ↦ ∑ᶠ c, f c x * g c (chartAt H c 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
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))
⊢ (support (M := ℝ) fun (x : M) ↦
      ∑ᶠ (c : M),
        HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (g c ((↑(chartAt H c) : M → H) x))) =
    s

Tactic:
support_eq_iff.2 ⟨fun x hx ↦ ?_, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Function.support_eq_iff, And.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
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))
refine_1 :
  ∀ (x : M) (hx : x ∈ s),
    Ne (α := ℝ)
      (∑ᶠ (c : M),
        HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (g c ((↑(chartAt H c) : M → H) x)))
      0
refine_1₁ :
  ∀ (x : M) (hx : x ∉ s),
    Eq (α := ℝ)
      (∑ᶠ (c : M),
        HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (g c ((↑(chartAt H c) : M → H) x)))
      0
⊢ (support (M := ℝ) fun (x : M) ↦
      ∑ᶠ (c : M),
        HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (g c ((↑(chartAt H c) : M → H) x))) =
    s

Tactic:
refine support_eq_iff.2 ⟨fun x hx ↦ ?_, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Function.support_eq_iff, And.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
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))
x : M
hx : x ∈ s
refine_1 :
  LT.lt (α := ℝ) 0
    (∑ᶠ (c : M),
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x)))
⊢ Ne (α := ℝ)
    (∑ᶠ (c : M),
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x)))
    0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- 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))
x : M
hx : x ∈ s
⊢ ∃ (c : M),
    LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)

Tactic:
f.exists_pos_of_mem (mem_univ x)

Premises used: SmoothPartitionOfUnity.exists_pos_of_mem, Set.mem_univ
-- 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))
x : M
hx : x ∈ s
obtain :
  ∀ (c : M)
    (hc :
      LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)),
    ∃ (c : 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))
⊢ ∃ (c : 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:
obtain ⟨c, hc⟩ : ∃ c, 0 < f c x := f.exists_pos_of_mem (mem_univ x)

Premises used: SmoothPartitionOfUnity.exists_pos_of_mem, Set.mem_univ
-- 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))
x : M
hx : x ∈ s
c : M
hc : LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
⊢ ∃ (c : 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:
⟨c, mul_pos hc ?_⟩

Premises used: mul_pos, 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
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))
x : M
hx : x ∈ s
c : M
hc : LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
refine : 0 < g c ((↑(chartAt H c) : M → H) x)
⊢ ∃ (c : 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:
refine ⟨c, mul_pos hc ?_⟩
-- 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))
x : M
hx : x ∈ s
c : M
hc : LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
apply : g c ((↑(chartAt H c) : M → H) x) ≠ 0
⊢ 0 < g c ((↑(chartAt H c) : M → H) x)

Tactic:
apply lt_of_le_of_ne (h'g _ _) (Ne.symm _)

Premises used: Ne.symm, lt_of_le_of_ne
-- 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))
x : M
hx : x ∈ s
c : M
hc : LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
rw :
  x ∈
    (↑(chartAt H c) : M → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
      (↑(chartAt H c) : M → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
⊢ g c ((↑(chartAt H c) : M → H) x) ≠ 0

Tactic:
rw [← mem_support, g_supp, ← mem_preimage, preimage_inter]

Premises used: Set.preimage_inter, Function.mem_support, Set.mem_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
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))
x : M
hx : x ∈ s
c : M
hc : LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
⊢ Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x

Tactic:
have Hx : x ∈ tsupport (f c) := subset_tsupport _ (ne_of_gt hc)
-- 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))
x : M
hx : x ∈ s
c : M
hc : LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
Hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
⊢ x ∈
    (↑(chartAt H c) : M → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
      (↑(chartAt H c) : M → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s

Tactic:
simp [(chartAt H c).left_inv (hf c Hx), hx, (chartAt H c).map_source (hf c Hx)]

Premises used: chartAt, OpenPartialHomeomorph.left_inv, OpenPartialHomeomorph.map_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
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))
x : M
hx : x ∈ s
⊢ ∃ (c : 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 B : ∃ c, 0 < f c x * g c (chartAt H c x) := by
        obtain ⟨c, hc⟩ : ∃ c, 0 < f c x := f.exists_pos_of_mem (mem_univ x)
        refine ⟨c, mul_pos hc ?_⟩
        apply lt_of_le_of_ne (h'g _ _) (Ne.symm _)
        rw [← mem_support, g_supp, ← mem_preimage, preimage_inter]
        have Hx : x ∈ tsupport (f c) := subset_tsupport _ (ne_of_gt hc)
        simp [(chartAt H c).left_inv (hf c Hx), hx, (chartAt H c).map_source (hf c 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
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))
x : M
hx : x ∈ s
B :
  ∃ (c : 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))
refine_1 :
  HasFiniteSupport (M := ℝ) fun (c : M) ↦
    HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
      (g c ((↑(chartAt H c) : M → H) x))
⊢ LT.lt (α := ℝ) 0
    (∑ᶠ (c : M),
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x)))

Tactic:
apply finsum_pos (fun c ↦ h''g c x) B

Premises used: finsum_pos
-- 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))
x : M
hx : x ∈ s
B :
  ∃ (c : 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))
refine_1 :
  Subset.{uM} (α := Set M)
    (support (M := ℝ) fun (c : M) ↦
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x)))
    {b : M |
      Membership.mem (γ := Set M)
        (support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) b : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x}
⊢ HasFiniteSupport (M := ℝ) fun (c : M) ↦
    HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
      (g c ((↑(chartAt H c) : M → H) x))

Tactic:
apply (f.locallyFinite.point_finite x).subset

Premises used: SmoothPartitionOfUnity.locallyFinite, Set.Finite.subset, LocallyFinite.point_finite