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
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hf : ∀ (a : ι), c a ∈ s ∧ tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
Tactic: choose hcs hfU using hf
Cleared hypotheses: 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
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have rcases : ∀ (V : ι → Set M) (hsV : s ⊆ iUnion V) (hVc : ∀ (i : ι), IsClosed[inst_3] (V i))
  (hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)),
  ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
Tactic: rcases exists_subset_iUnion_closed_subset hs (fun i => (f i).isOpen_support)
    (fun x _ => hfin.point_finite x) hsub' with ⟨V, hsV, hVc, hVf⟩
-- 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
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have choose : ∀ (r : (i : ι) → ℝ) (hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut)
  (hr :
    ∀ (i : ι),
      V i ⊆
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
          (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)),
  ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
Tactic: choose r hrR hr using fun i => (f i).exists_r_pos_lt_subset_ball (hVc i) (hVf 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
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have refine_1 : LocallyFinite (X := M) fun (i : ι) ↦ support (↑((fun (i : ι) ↦ (f i).updateRIn (r i) sorry) i) : M → ℝ)
Tactic: refine ⟨ι, ⟨c, fun i => (f i).updateRIn (r i) (hrR i), hcs, ?_, fun x hx => ?_⟩, fun 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
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
refine_1 : LocallyFinite (X := M) fun (i : ι) ↦ support (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ)
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have refine_2 : ∀ (x : M) (hx : x ∈ s), ∃ (i : ι), (↑((fun (i : ι) ↦ (f i).updateRIn (r i) sorry) i) : M → ℝ) =ᶠ[𝓝 x] 1
Tactic: refine ⟨ι, ⟨c, fun i => (f i).updateRIn (r i) (hrR i), hcs, ?_, fun x hx => ?_⟩, fun 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
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
refine_1 : LocallyFinite (X := M) fun (i : ι) ↦ support (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ)
refine_2 : ∀ (x : M) (hx : x ∈ s), ∃ (i : ι), (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ) =ᶠ[𝓝 x] 1
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have refine_3 : ∀ (i : ι),
  tsupport (↑(toFun (s := s) (mk (s := s) c (fun (i : ι) ↦ (f i).updateRIn (r i) sorry) hcs sorry sorry) i) : M → ℝ) ⊆
    U
      (SmoothBumpCovering.c.{uM, uE, uH, uM} (E := E) (H := H) (I := I) (s := s)
        (mk (s := s) c (fun (i : ι) ↦ (f i).updateRIn (r i) sorry) hcs sorry sorry) i)
Tactic: refine ⟨ι, ⟨c, fun i => (f i).updateRIn (r i) (hrR i), hcs, ?_, fun x hx => ?_⟩, fun 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
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst_6 : T2Space M
inst_7 : SigmaCompactSpace M
hs : IsClosed[inst_3] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
hB :
  ∀ (x : M) (hx : x ∈ s),
    (𝓝 x).HasBasis (fun (f : SmoothBumpFunction I x) ↦ tsupport (↑f : M → ℝ) ⊆ U x) fun (f : SmoothBumpFunction I x) ↦
      support (↑f : M → ℝ)
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support (↑(f a) : M → ℝ)
hfin : LocallyFinite (X := M) fun (a : ι) ↦ support (↑(f a) : M → ℝ)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport (↑(f a) : M → ℝ) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst_3] (V i)
hVf : ∀ (i : ι), V i ⊆ support (↑(f i) : M → ℝ)
r : (i : ι) → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (c i))).source ∩
        (↑(extChartAt I (c i)) : M → E) ⁻¹' Metric.ball ((↑(extChartAt I (c i)) : M → E) (c i)) (r i)
x : M
hx : x ∈ s
⊢ ∃ (i : ι), (↑((fun (i : ι) ↦ (f i).updateRIn (r i) ⋯) i) : M → ℝ) =ᶠ[𝓝 x] 1
have refine_2 : ∀ (i : ι) (hi : x ∈ V i), (↑((fun (i : ι) ↦ (f i).updateRIn (r i) sorry) i) : M → ℝ) =ᶠ[𝓝 x] 1
Tactic: refine (mem_iUnion.1 <| hsV hx).imp fun i hi => ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
ι : Type uι
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
s : Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : (↑(fs.toFun (s := s) i) : M → ℝ) x = 1
⊢ x ∈ (extChartAt I (fs.c (s := s) i)).source
have rw : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (fs.c (s := s) i))).source
Tactic: rw [extChartAt_source]
-- 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
Tactic: have : ∀ x ∈ t, sᶜ ∈ 𝓝 x := fun x hx => hs.isOpen_compl.mem_nhds (disjoint_right.1 hd 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have rcases : ∀ (ι : Type uM) (f : SmoothBumpCovering ι I M t) (hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ),
  ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
Tactic: rcases SmoothBumpCovering.exists_isSubordinate I ht this 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have fun : ∀ (x : M) (hx : x ∈ s),
  Eq (α := ℝ)
    ((Subtype.mk (p := fun (f : M → ℝ) ↦ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f)
            (fun (x : M) ↦
              ∑ᶠ (i : ι), (((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x)
            sorry :
          (a : M) → ℝ)
        x :
      ℝ)
    (0 x : ℝ)
Tactic: refine
    ⟨⟨_, g.contMDiff_sum.of_le (by simp)⟩, fun x hx => ?_, fun x => g.sum_eq_one, fun x =>
      ⟨g.sum_nonneg x, g.sum_le_one x⟩⟩
-- 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
x : M
hx : x ∈ s
⊢ Eq (α := ℝ)
    ((Subtype.mk (p := fun (f : M → ℝ) ↦ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f)
            (fun (x : M) ↦
              ∑ᶠ (i : ι), (((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x)
            ⋯ :
          (a : M) → ℝ)
        x :
      ℝ)
    (0 x : ℝ)
have suffices : ∀ (i : ι), Eq (α := ℝ) ((((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
Tactic: suffices ∀ i, g i x = 0 by simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]
-- 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate (s := t) fun (x : M) ↦ sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity (s := t)
x : M
hx : x ∈ s
⊢ ∀ (i : ι),
    Eq (α := ℝ) ((((g : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
have refine : ∀ (i : ι), (↑(f.toFun (s := t) i) : M → ℝ) x = 0
Tactic: refine fun i => f.toSmoothPartitionOfUnity_zero_of_zero ?_
-- 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : NormalSpace M
inst_9 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have obtain : ∀ (u : Set M) (u_op : IsOpen[inst_3] u) (hsu : s ⊆ u) (hut : closure[inst_3] u ⊆ tᶜ),
  ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
Tactic: obtain ⟨u, u_op, hsu, hut⟩ := normal_exists_closure_subset hs ht.isOpen_compl
    (subset_compl_iff_disjoint_left.mpr hd.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
n : ℕ∞
inst_7 : T2Space M
inst_8 : NormalSpace M
inst_9 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have obtain : ∀ (v : Set M) (v_op : IsOpen[inst_3] v) (htv : t ⊆ v) (hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ),
  ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
Tactic: obtain ⟨v, v_op, htv, hvu⟩ := normal_exists_closure_subset ht isClosed_closure.isOpen_compl
    (subset_compl_comm.mp hut)
-- 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : NormalSpace M
inst_9 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have obtain : ∀ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) (hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u))
  (hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v))
  (hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)),
  ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
Tactic: obtain ⟨f, hfu, hfv, hf⟩ := exists_contMDiffMap_zero_one_of_isClosed I isClosed_closure
    isClosed_closure (subset_compl_iff_disjoint_left.mp hvu) (n := n)
-- 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
n : ℕ∞
inst_7 : T2Space M
inst_8 : NormalSpace M
inst_9 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u)
hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have refine_1 : ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)
Tactic: refine ⟨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
n : ℕ∞
inst_7 : T2Space M
inst_8 : NormalSpace M
inst_9 : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
u : Set M
u_op : IsOpen[inst_3] u
hsu : s ⊆ u
hut : closure[inst_3] u ⊆ tᶜ
v : Set M
v_op : IsOpen[inst_3] v
htv : t ⊆ v
hvu : closure[inst_3] v ⊆ (closure[inst_3] u)ᶜ
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hfu : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 (closure[inst_3] u)
hfv : EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 (closure[inst_3] v)
hf : ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
refine_1 : ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
      (∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have refine_2 : ∀ᶠ (x : M) in 𝓝ˢ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)
Tactic: refine ⟨f, ?_, ?_, hf⟩