awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
have refine_1 : support (f ∘ (↑I : H → E)) = s
Tactic: refine ⟨f ∘ I, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
⊢ ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have refine_2 : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (f ∘ (↑I : H → E))
Tactic: refine ⟨f ∘ I, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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))
⊢ ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have refine_3 : range (f ∘ (↑I : H → E)) ⊆ Icc 0 1
Tactic: refine ⟨f ∘ I, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
⊢ support (f ∘ (↑I : H → E)) = s
have refine_1 : (↑I.symm : E → H) ∘ (↑I : H → E) ⁻¹' s = s
Tactic: rw [support_comp_eq_preimage, f_supp, ← preimage_comp]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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 : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
have 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
Tactic: rcases SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source I M with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
⊢ ∃ (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
have hs₁ : IsOpen[inst_2]
  ((OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).target ∩
    (↑(OpenPartialHomeomorph.symm (chartAt H i)) : H → M) ⁻¹' s)
Tactic: apply IsOpen.exists_contMDiff_support_eq_aux
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (hypothesis)
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
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
have 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
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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
have 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
Tactic: choose g g_supp g_diff hg using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (hypothesis)
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
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
have h'g : ∀ (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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (hypothesis)
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
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
have 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))
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 _)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
have 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
Tactic: refine ⟨fun x ↦ ∑ᶠ c, f c x * g c (chartAt H c x), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
have 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))
Tactic: refine ⟨fun x ↦ ∑ᶠ c, f c x * g c (chartAt H c x), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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))
⊢ ∃ (f : M → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ ∀ (x : M), 0 ≤ f x
have 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)
Tactic: refine ⟨fun x ↦ ∑ᶠ c, f c x * g c (chartAt H c x), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
have 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
Tactic: refine support_eq_iff.2 ⟨fun x hx ↦ ?_, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
⊢ (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
have 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
Tactic: refine support_eq_iff.2 ⟨fun x hx ↦ ?_, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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
⊢ 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
have 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)))
Tactic: apply ne_of_gt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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))
have 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))
Tactic: obtain ⟨c, hc⟩ : ∃ c, 0 < f c x := f.exists_pos_of_mem (mem_univ x)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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))
have refine : 0 < g c ((↑(chartAt H c) : M → H) x)
Tactic: refine ⟨c, mul_pos hc ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
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 : ℝ)
⊢ 0 < g c ((↑(chartAt H c) : M → H) x)
have apply : g c ((↑(chartAt H c) : M → H) x) ≠ 0
Tactic: apply lt_of_le_of_ne (h'g _ _) (Ne.symm _)