awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
Hx : x ∉ tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : 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 this : x ∉ support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)
Tactic: have : x ∉ support (f c) := by contrapose Hx; exact subset_tsupport _ Hx
-- 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
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
Hx : x ∉ tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)
this : x ∉ support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : 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 this₁ : Eq (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [notMem_support] at this
Cleared hypotheses: this
-- 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))
⊢ 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))
have refine_2 : ∀ (i x : M),
  Membership.mem (γ := Set M)
      (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x →
    ContMDiffAt I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) (fun (x : M) ↦ g i ((↑(chartAt H i) : M → H) x)) x
Tactic: apply SmoothPartitionOfUnity.contMDiff_finsum_smul
-- 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))
c x : M
hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) (fun (x : M) ↦ g c ((↑(chartAt H c) : M → H) x)) x
have refine_2 : ContMDiffAt I I (↑n : ℕ∞ω) (↑(chartAt H c) : M → H) x
Tactic: apply (g_diff c (chartAt H c x)).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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
⊢ ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have rcases : ∀ (f : M → ℝ) (f_supp : support f = s) (f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f) (f_pos : ∀ (x : M), 0 ≤ f x),
  ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
Tactic: rcases hs.exists_contMDiff_support_eq I with ⟨f, f_supp, f_diff, f_pos⟩
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
⊢ ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have rcases : ∀ (g : M → ℝ) (g_supp : support g = tᶜ) (g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g) (g_pos : ∀ (x : M), 0 ≤ g x),
  ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
Tactic: rcases ht.isOpen_compl.exists_contMDiff_support_eq I with ⟨g, g_supp, g_diff, g_pos⟩
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
⊢ 0 < f x + g x
have pos : ∀ (xs : x ∈ support f), 0 < f x + g x
Tactic: by_cases xs : x ∈ support f
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
pos : ∀ (xs : x ∈ support f), 0 < f x + g x
⊢ 0 < f x + g x
have neg : ∀ (xs : x ∉ support f), 0 < f x + g x
Tactic: by_cases xs : x ∈ support f
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∈ support f
⊢ 0 < f x + g x
have this : 0 < f x
Tactic: have : 0 < f x := lt_of_le_of_ne (f_pos x) (Ne.symm xs)
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∈ support f
this : 0 < f x
⊢ 0 < f x + g x
have linarith : f x + g x ≤ 0 → 0 - f x + (f x + g x - 0) + (0 - g x) = 0
Tactic: linarith [g_pos 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.72 : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.113 : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ 0 < g x
have apply : g x ≠ 0
Tactic: apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.72 : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.113 : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ g x ≠ 0
have rw : x ∈ tᶜ
Tactic: rw [← mem_support, g_supp]
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.72 : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.113 : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ x ∈ tᶜ
have contrapose : ∀ (xs : x ∉ tᶜ), x ∈ support f
Tactic: contrapose xs
Cleared hypotheses: xs
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ 0 < g x
have apply : g x ≠ 0
Tactic: classical
        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
        rw [← mem_support, g_supp]
        contrapose xs
        exact h.trans f_supp.symm.subset (by simpa using xs)
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
apply : g x ≠ 0
⊢ 0 < g x
have apply₁ : x ∈ tᶜ
Tactic: classical
        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
        rw [← mem_support, g_supp]
        contrapose xs
        exact h.trans f_supp.symm.subset (by simpa using xs)
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
apply : g x ≠ 0
apply₁ : x ∈ tᶜ
⊢ 0 < g x
have apply₂ : ∀ (xs : x ∉ tᶜ), x ∈ support f
Tactic: classical
        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
        rw [← mem_support, g_supp]
        contrapose xs
        exact h.trans f_supp.symm.subset (by simpa using xs)
Cleared hypotheses: xs
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ 0 < f x + g x
have this : 0 < g x
Tactic: have : 0 < g x := by
        classical
        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
        rw [← mem_support, g_supp]
        contrapose xs
        exact h.trans f_supp.symm.subset (by simpa using xs)
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
this : 0 < g x
⊢ 0 < f x + g x
have linarith : f x + g x ≤ 0 → 0 - g x + (f x + g x - 0) + (0 - f x) = 0
Tactic: linarith [f_pos x]
-- 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
⊢ ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have A : ∀ (x : M), 0 < f x + g x
Tactic: have A : ∀ x, 0 < f x + g x := by
    intro x
    by_cases xs : x ∈ support f
    · have : 0 < f x := lt_of_le_of_ne (f_pos x) (Ne.symm xs)
      linarith [g_pos x]
    · have : 0 < g x := by
        classical
        apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
        rw [← mem_support, g_supp]
        contrapose xs
        exact h.trans f_supp.symm.subset (by simpa using xs)
      linarith [f_pos 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have refine_1 : ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) fun (x : M) ↦ f x / (f x + g x)
Tactic: refine ⟨fun x ↦ f x / (f x + g 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
refine_1 : ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) fun (x : M) ↦ f x / (f x + g x)
⊢ ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have refine_2 : Subset (α := Set ℝ) (range fun (x : M) ↦ f x / (f x + g x)) (Icc 0 1)
Tactic: refine ⟨fun x ↦ f x / (f x + g 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
refine_1 : ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) fun (x : M) ↦ f x / (f x + g x)
refine_2 : Subset (α := Set ℝ) (range fun (x : M) ↦ f x / (f x + g x)) (Icc 0 1)
⊢ ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have refine_3 : (support (M := ℝ) fun (x : M) ↦ f x / (f x + g x)) = s
Tactic: refine ⟨fun x ↦ f x / (f x + g 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 t : Set M
hs : IsOpen[inst_3] s
ht : IsClosed[inst_3] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
refine_1 : ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω) fun (x : M) ↦ f x / (f x + g x)
refine_2 : Subset (α := Set ℝ) (range fun (x : M) ↦ f x / (f x + g x)) (Icc 0 1)
refine_3 : (support (M := ℝ) fun (x : M) ↦ f x / (f x + g x)) = s
⊢ ∃ (f : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
have refine_4 : ∀ (x : M), x ∈ t ↔ Eq (α := ℝ) ((fun (x : M) ↦ f x / (f x + g x)) x) 1
Tactic: refine ⟨fun x ↦ f x / (f x + g x), ?_, ?_, ?_, ?_⟩