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
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
hd : s ⊆ interior t
⊢ Disjoint (interior t)ᶜ s
have rwa : s ⊆ (interior t)ᶜᶜ
Tactic: rwa [← subset_compl_iff_disjoint_left, compl_compl]
-- 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
hd : s ⊆ interior t
⊢ ∃ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)) ∧
      (∀ x ∉ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have rcases : ∀ (f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯)
  (h0 : ∀ᶠ (x : M) in 𝓝ˢ (interior t)ᶜ, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ))
  (h1 : ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ))
  (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 : ℝ) (1 : ℝ)) ∧
      (∀ x ∉ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
Tactic: rcases exists_contMDiffMap_zero_one_nhds_of_isClosed I isOpen_interior.isClosed_compl hs
    (by rwa [← subset_compl_iff_disjoint_left, compl_compl]) (n := n) with ⟨f, h0, h1, 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
hd : s ⊆ interior t
f : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
h0 : ∀ᶠ (x : M) in 𝓝ˢ (interior t)ᶜ, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)
h1 : ∀ᶠ (x : M) in 𝓝ˢ s, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (1 : ℝ)
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 : ℝ) (1 : ℝ)) ∧
      (∀ x ∉ t, Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)) ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)
have refine : ∀ (x : M) (hx : x ∉ t), Eq (α := ℝ) ((f : (a : M) → ℝ) x : ℝ) (0 : ℝ)
Tactic: refine ⟨f, h1, fun x hx ↦ ?_, hf⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : FiniteDimensional ℝ E
inst_8 : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
⊢ ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
have inl : ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
  (⇑(((BumpCovering.single j s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
Tactic: rcases eq_or_ne j i with (rfl | h)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : FiniteDimensional ℝ E
inst_8 : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
inl :
  ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single j s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
⊢ ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
have inr : ∀ (h : j ≠ i),
  ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
Tactic: rcases eq_or_ne j i with (rfl | h)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : FiniteDimensional ℝ E
inst_8 : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
⊢ ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
have inl : ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
  (⇑(((BumpCovering.single j s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
Tactic: classical
    rcases eq_or_ne j i with (rfl | h)
    · simp only [contMDiff_one, ContinuousMap.coe_one, BumpCovering.coe_single, Pi.single_eq_same]
    · simp only [contMDiff_zero, BumpCovering.coe_single, Pi.single_eq_of_ne h,
        ContinuousMap.coe_zero]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type uF
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
H : Type uH
inst_4 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_5 : TopologicalSpace M
inst_6 : ChartedSpace H M
inst_7 : FiniteDimensional ℝ E
inst_8 : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
inl :
  ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single j s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
⊢ ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
have inr : ∀ (h : j ≠ i),
  ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
    (⇑(((BumpCovering.single i s : BumpCovering ι M s) : (a : ι) → C(M, ℝ)) j : C(M, ℝ)) : (a : M) → ℝ)
Tactic: classical
    rcases eq_or_ne j i with (rfl | h)
    · simp only [contMDiff_one, ContinuousMap.coe_one, BumpCovering.coe_single, Pi.single_eq_same]
    · simp only [contMDiff_zero, BumpCovering.coe_single, Pi.single_eq_of_ne h,
        ContinuousMap.coe_zero]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (hypothesis)
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
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
have this : LocallyCompactSpace H
Tactic: haveI : LocallyCompactSpace H := I.locallyCompactSpace
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (hypothesis)
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
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this : LocallyCompactSpace H
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
have this₁ : LocallyCompactSpace M
Tactic: haveI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
-- 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
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
have refine_2 : ∀
  (this :
    ∃ (f : BumpCovering ι M s),
      (∀ (i : ι),
          ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
            (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)) ∧
        f.IsSubordinate (s := s) U),
  ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
Tactic: have := BumpCovering.exists_isSubordinate_of_prop (ContMDiff I 𝓘(ℝ) ∞) ?_ hs U ho hU
-- 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
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
refine_2 :
  ∀
    (this :
      ∃ (f : BumpCovering ι M s),
        (∀ (i : ι),
            ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
              (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)) ∧
          f.IsSubordinate (s := s) U),
    ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
have refine_1 : ∀ (s t : Set M),
  IsClosed[inst_3] s →
    IsClosed[inst_3] t →
      Disjoint s t →
        ∃ (f : C(M, ℝ)),
          ContMDiff I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞ (⇑f : (a : 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: have := BumpCovering.exists_isSubordinate_of_prop (ContMDiff I 𝓘(ℝ) ∞) ?_ hs U ho hU
-- 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
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this :
  ∃ (f : BumpCovering ι M s),
    (∀ (i : ι),
        ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
          (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)) ∧
      f.IsSubordinate (s := s) U
⊢ ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
have refine_2 : ∀ (f : BumpCovering ι M s)
  (hf :
    ∀ (i : ι),
      ContMDiff.{0, uE, uH, uM, 0, 0, 0} I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞
        (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ))
  (hfU : f.IsSubordinate (s := s) U), ∃ (f : SmoothPartitionOfUnity ι I M s), f.IsSubordinate (s := s) U
Tactic: rcases this with ⟨f, hf, hfU⟩
Cleared hypotheses: this
-- 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
inst_6 : IsManifold I ∞ M
inst_7 : T2Space M
inst_8 : SigmaCompactSpace M
s_1 : Set M
hs_1 : IsClosed[inst_3] s_1
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst_3] (U i)
hU : s_1 ⊆ ⋃ (i : ι), U i
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed[inst_3] s
ht : IsClosed[inst_3] t
hd : Disjoint s t
⊢ ∃ (f : C(M, ℝ)),
    ContMDiff I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞ (⇑f : (a : 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 refine_1 : ∀ (f : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯)
  (hf :
    EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 0 s ∧
      EqOn (β := ℝ) (⇑f : (a : M) → ℝ) 1 t ∧
        ∀ (x : M), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : M) → ℝ) x : ℝ)),
  ∃ (f : C(M, ℝ)),
    ContMDiff I (M := M) 𝓘(ℝ, ℝ) (M' := ℝ) ∞ (⇑f : (a : 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 exists_contMDiffMap_zero_one_of_isClosed I hs ht hd 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 : T2Space M
inst_8 : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst_3] s
⊢ ∃ (f : SmoothPartitionOfUnity (↑s : Type uM) I M s),
    f.IsSubordinate (s := s) fun (x : (↑s : Type uM)) ↦
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (↑x : M))).source
have apply : ∀ (x : M) (hx : x ∈ s),
  Membership.mem (γ := Set M)
    (⋃ (i : (↑s : Type uM)), (OpenPartialHomeomorph.toPartialEquiv (chartAt H (↑i : M))).source) x
Tactic: apply exists_isSubordinate _ hs _ (fun i ↦ (chartAt H _).open_source) (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 : T2Space M
inst_8 : SigmaCompactSpace M
⊢ ∃ (f : SmoothPartitionOfUnity M I M),
    f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
have apply : ∀ (x : M),
  Membership.mem (γ := Set M) univ x →
    Membership.mem (γ := Set M) (⋃ (i : M), (OpenPartialHomeomorph.toPartialEquiv (chartAt H i)).source) x
Tactic: apply exists_isSubordinate _ isClosed_univ _ (fun i ↦ (chartAt H _).open_source) (fun 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 : ℕ∞
F_fiber : Type u_1
inst_9 : NormedAddCommGroup F_fiber
inst_10 : NormedSpace ℝ F_fiber
V : M → Type u_2
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → TopologicalSpace (V x)
inst_13 : (x : M) → Module ℝ (V x)
inst_14 : TopologicalSpace (TotalSpace F_fiber V)
inst_15 : FiberBundle F_fiber V
inst_16 : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
Hloc :
  ∀ (x₀ : M),
    ∃ U_x₀ ∈ 𝓝 x₀,
      ∃ (s_loc : (x : M) → V x),
        ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x⟩) U_x₀ ∧
          ∀ y ∈ U_x₀, s_loc y ∈ t y
⊢ ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
have choose : ∀ (W : (x₀ : M) → Set M) (h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀) (s_loc : (x₀ x : M) → V x)
  (s_smooth :
    ∀ (x₀ : M),
      ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x₀ x⟩)
        (W x₀))
  (h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y),
  ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
Tactic: choose W h_nhds s_loc s_smooth h_mem_t using Hloc
Cleared hypotheses: Hloc
-- 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 : ℕ∞
F_fiber : Type u_1
inst_9 : NormedAddCommGroup F_fiber
inst_10 : NormedSpace ℝ F_fiber
V : M → Type u_2
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → TopologicalSpace (V x)
inst_13 : (x : M) → Module ℝ (V x)
inst_14 : TopologicalSpace (TotalSpace F_fiber V)
inst_15 : FiberBundle F_fiber V
inst_16 : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : (x₀ : M) → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : (x₀ x : M) → V x
s_smooth :
  ∀ (x₀ : M),
    ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : (x : M) → Set M := fun (x : M) ↦ interior (W x)
x_pt : M
h : Membership.mem (γ := Set M) univ x_pt
⊢ Membership.mem (γ := Set M) (⋃ (x : M), U x) x_pt
have simp : ∃ (i : M), x_pt ∈ U i
Tactic: simp only [mem_iUnion]
-- 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 : ℕ∞
F_fiber : Type u_1
inst_9 : NormedAddCommGroup F_fiber
inst_10 : NormedSpace ℝ F_fiber
V : M → Type u_2
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → TopologicalSpace (V x)
inst_13 : (x : M) → Module ℝ (V x)
inst_14 : TopologicalSpace (TotalSpace F_fiber V)
inst_15 : FiberBundle F_fiber V
inst_16 : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : (x₀ : M) → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : (x₀ x : M) → V x
s_smooth :
  ∀ (x₀ : M),
    ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : (x : M) → Set M := fun (x : M) ↦ interior (W x)
⊢ ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
have hU_covers_univ : Subset.{uM} (α := Set M) univ (⋃ (x : M), U x)
Tactic: have hU_covers_univ : univ ⊆ ⋃ x, U x := by
    intro x_pt _
    simp only [mem_iUnion]
    exact ⟨x_pt, mem_interior_iff_mem_nhds.mpr (h_nhds x_pt)⟩
-- 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 : ℕ∞
F_fiber : Type u_1
inst_9 : NormedAddCommGroup F_fiber
inst_10 : NormedSpace ℝ F_fiber
V : M → Type u_2
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → TopologicalSpace (V x)
inst_13 : (x : M) → Module ℝ (V x)
inst_14 : TopologicalSpace (TotalSpace F_fiber V)
inst_15 : FiberBundle F_fiber V
inst_16 : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : (x₀ : M) → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : (x₀ x : M) → V x
s_smooth :
  ∀ (x₀ : M),
    ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : (x : M) → Set M := fun (x : M) ↦ interior (W x)
hU_covers_univ : Subset.{uM} (α := Set M) univ (⋃ (x : M), U x)
⊢ ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
have obtain : ∀ (ρ : SmoothPartitionOfUnity M I M) (hρU : ρ.IsSubordinate (s := univ) U),
  ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
Tactic: obtain ⟨ρ, hρU⟩ : ∃ ρ : SmoothPartitionOfUnity M I M univ, ρ.IsSubordinate U :=
    SmoothPartitionOfUnity.exists_isSubordinate
      I isClosed_univ U (fun x ↦ isOpen_interior) hU_covers_univ
-- 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 : ℕ∞
F_fiber : Type u_1
inst_9 : NormedAddCommGroup F_fiber
inst_10 : NormedSpace ℝ F_fiber
V : M → Type u_2
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → TopologicalSpace (V x)
inst_13 : (x : M) → Module ℝ (V x)
inst_14 : TopologicalSpace (TotalSpace F_fiber V)
inst_15 : FiberBundle F_fiber V
inst_16 : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : (x₀ : M) → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : (x₀ x : M) → V x
s_smooth :
  ∀ (x₀ : M),
    ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) (fun (x : M) ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : (x : M) → Set M := fun (x : M) ↦ interior (W x)
hU_covers_univ : Subset.{uM} (α := Set M) univ (⋃ (x : M), U x)
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate (s := univ) U
s : (x : M) → V x :=
  fun (x : M) ↦
    ∑ᶠ (j : M),
      HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (s_loc j x)
j : M
⊢ ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) fun (x : M) ↦
    ⟨x,
      HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (s_loc j x)⟩
have refine : ContMDiffOn I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω)
  (⇑((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) (interior (W j))
Tactic: refine ContMDiffOn.smul_section_of_tsupport ?_ isOpen_interior (hρU j)
      ((s_smooth j).mono interior_subset)