awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
⊢ ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivializationAt F Z x))) :
            M × F → TotalSpace F Z)
          ((fun (p : H × F) ↦ ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) p.1, id p.2))
            ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)))).proj
      (E := Z) =
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)
have h : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((fun (p : E × F) ↦ ((↑I.symm : E → H) p.1, id p.2)) (z, w)).1 ∈
  Trivialization.baseSet (trivializationAt F Z x)
Tactic: apply Trivialization.proj_symm_apply'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffWithinAt I s (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩)
h's : s ⊆ Trivialization.baseSet (trivializationAt F Z (TotalSpace.proj.{u_4, u_9, u_10} (F := F) (E := Z) ⟨x, v⟩))
z : E
w : F
hz : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
⊢ ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = (z, w)
have right : ∀ (u : H)
  (hz :
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) ((↑I : H → E) u)) ∈ s ∧
      ∃ (y : H), (↑I : H → E) y = (↑I : H → E) u),
  ∃ (y : ModelProd H F), Prod.map (↑I : H → E) id y = ((↑I : H → E) u, w)
Tactic: rcases hz.2 with ⟨u, rfl⟩
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F)) (TotalSpace.proj (E := Z) ⁻¹' s) p
have suffices : UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F))
  (TotalSpace.proj (E := Z) ⁻¹' (s ∩ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))))) p
Tactic: suffices UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F))
    (π F Z ⁻¹' (s ∩ (trivializationAt F Z p.proj).baseSet)) p from this.mono (by simp)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F : Type u_9
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
Z : M → Type u_10
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffWithinAt I s (p.proj (E := Z))
⊢ UniqueMDiffWithinAt (I.prod 𝓘(𝕜, F))
    (TotalSpace.proj (E := Z) ⁻¹' (s ∩ Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))))) p
have apply : Trivialization.baseSet (trivializationAt F Z (p.proj (E := Z))) ∈ nhds (p.proj (E := Z))
Tactic: apply UniqueMDiffWithinAt.bundle_preimage_aux (hs.inter _) inter_subset_right
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Metrizable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
⊢ MetrizableSpace M
have this : LocallyCompactSpace H
Tactic: haveI := I.locallyCompactSpace
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Metrizable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
this : LocallyCompactSpace H
⊢ MetrizableSpace M
have this₁ : LocallyCompactSpace M
Tactic: haveI := ChartedSpace.locallyCompactSpace H M
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Metrizable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
this_1 : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ MetrizableSpace M
have this₁ : SecondCountableTopology H
Tactic: haveI := I.secondCountableTopology
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Metrizable (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
H : Type u_2
inst_3 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : SigmaCompactSpace M
inst_7 : T2Space M
this_1 : LocallyCompactSpace H
this_2 : LocallyCompactSpace M
this : SecondCountableTopology H
⊢ MetrizableSpace M
have this₁ : SecondCountableTopology M
Tactic: haveI := ChartedSpace.secondCountable_of_sigmaCompact 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
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
s_1 : Set M
f_1 : SmoothPartitionOfUnity ι I M s_1
n : ℕ∞
s : Set M
f g : SmoothPartitionOfUnity ι I M s
h : f.toFun (s := s) = g.toFun (s := s)
⊢ f = g
have mk : ∀ (toFun : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯)
  (locallyFinite' : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : M) → ℝ))
  (nonneg' : ∀ (i : ι) (x : M), LE.le (α := ℝ) (0 : ℝ) ((toFun i : (a : M) → ℝ) x : ℝ))
  (sum_eq_one' : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1)
  (sum_le_one' : ∀ (x : M), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1)
  (h : (mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) = g.toFun (s := s)),
  mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' = g
Tactic: cases f
Cleared hypotheses: f, 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
s_1 : Set M
f : SmoothPartitionOfUnity ι I M s_1
n : ℕ∞
s : Set M
g : SmoothPartitionOfUnity ι I M s
toFun : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite' : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : M) → ℝ)
nonneg' : ∀ (i : ι) (x : M), LE.le (α := ℝ) (0 : ℝ) ((toFun i : (a : M) → ℝ) x : ℝ)
sum_eq_one' : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1
sum_le_one' : ∀ (x : M), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : M) → ℝ) x) 1
h : (mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) = g.toFun (s := s)
⊢ mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' = g
have mk : ∀ (toFun_1 : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯)
  (locallyFinite'_1 : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun_1 i) : (a : M) → ℝ))
  (nonneg'_1 : ∀ (i : ι) (x : M), LE.le (α := ℝ) (0 : ℝ) ((toFun_1 i : (a : M) → ℝ) x : ℝ))
  (sum_eq_one'_1 : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : M) → ℝ) x) 1)
  (sum_le_one'_1 : ∀ (x : M), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : M) → ℝ) x) 1)
  (h :
    (mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) =
      (mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1).toFun (s := s)),
  mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' =
    mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1
Tactic: cases g
Cleared hypotheses: g, h
-- 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
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
⊢ ∃ (i : ι),
    LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
have by_contra! : ∀
  (h :
    ∀ (i : ι),
      LE.le (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)),
  False
Tactic: by_contra! h
-- 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
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h :
  ∀ (i : ι),
    LE.le (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
⊢ False
have H₁ : ∀ (i : ι), Eq (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
Tactic: have H : ∀ i, f i x = 0 := fun i ↦ le_antisymm (h i) (f.nonneg i x)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type uH
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h :
  ∀ (i : ι),
    LE.le (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
H :
  ∀ (i : ι),
    Eq (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
⊢ False
have this : Eq (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x) 1
Tactic: have := f.sum_eq_one hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (hypothesis)
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H_1 : Type uH
inst_2 : TopologicalSpace H_1
I : ModelWithCorners ℝ E H_1
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H_1 M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h :
  ∀ (i : ι),
    LE.le (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
H :
  ∀ (i : ι),
    Eq (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
this : Eq (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x) 1
⊢ False
have this₁ : Eq (α := ℝ) (∑ᶠ (i : ι), 0) 1
Tactic: simp_rw [H] at this
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
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
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ :
  ∀ (i : ι),
    Membership.mem (γ := Set M)
        (tsupport (α := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x₀ →
      ContMDiffAt I 𝓘(ℝ, F) (↑n : ℕ∞ω) (g i) x₀
⊢ ContMDiffAt I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω)
    (fun (x : M) ↦
      ∑ᶠ (i : ι),
        HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (g i x))
    x₀
have refine : ∀ (i : ι),
  ContMDiffAt I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω)
    (fun (x : M) ↦
      HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g i x))
    x₀
Tactic: refine _root_.contMDiffAt_finsum (f.locallyFinite.smul_left _) fun 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
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ :
  ∀ (i : ι),
    Membership.mem (γ := Set M)
        (tsupport (α := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x₀ →
      ContMDiffAt I 𝓘(ℝ, F) (↑n : ℕ∞ω) (g i) x₀
i : ι
⊢ ContMDiffAt I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω)
    (fun (x : M) ↦
      HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g i x))
    x₀
have pos : ∀
  (hx :
    Membership.mem (γ := Set M)
      (tsupport (α := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x₀),
  ContMDiffAt I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω)
    (fun (x : M) ↦
      HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g i x))
    x₀
Tactic: by_cases hx : x₀ ∈ tsupport (f 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
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ :
  ∀ (i : ι),
    Membership.mem (γ := Set M)
        (tsupport (α := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x₀ →
      ContMDiffAt I 𝓘(ℝ, F) (↑n : ℕ∞ω) (g i) x₀
i : ι
pos :
  ∀
    (hx :
      Membership.mem (γ := Set M)
        (tsupport (α := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x₀),
    ContMDiffAt I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω)
      (fun (x : M) ↦
        HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (g i x))
      x₀
⊢ ContMDiffAt I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω)
    (fun (x : M) ↦
      HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g i x))
    x₀
have neg : ∀ (hx : x₀ ∉ tsupport (α := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)),
  ContMDiffAt I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω)
    (fun (x : M) ↦
      HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g i x))
    x₀
Tactic: by_cases hx : x₀ ∈ tsupport (f 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
n : ℕ∞
s : Set E
f : SmoothPartitionOfUnity ι 𝓘(ℝ, E) E s
x₀ : E
g : ι → E → F
hφ :
  ∀ (i : ι),
    Membership.mem (γ := Set E)
        (tsupport (α := ℝ)
          (⇑((f : (a : ι) → C^∞⟮𝓘(ℝ, E), E; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮𝓘(ℝ, E), E; 𝓘(ℝ, ℝ), ℝ⟯) : (a : E) → ℝ))
        x₀ →
      ContDiffAt ℝ (↑n : ℕ∞ω) (g i) x₀
⊢ ContDiffAt.{0, uE, uF} ℝ (F := F) (↑n : ℕ∞ω)
    (fun (x : E) ↦
      ∑ᶠ (i : ι),
        HSMul.hSMul (α := ℝ)
          ((((f : (a : ι) → C^∞⟮𝓘(ℝ, E), E; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮𝓘(ℝ, E), E; 𝓘(ℝ, ℝ), ℝ⟯) : (a : E) → ℝ) x : ℝ) (g i x))
    x₀
have simp : ∀
  (hφ :
    ∀ (i : ι),
      Membership.mem (γ := Set E)
          (tsupport (α := ℝ)
            (⇑((f : (a : ι) → C^∞⟮𝓘(ℝ, E), E; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮𝓘(ℝ, E), E; 𝓘(ℝ, ℝ), ℝ⟯) : (a : E) → ℝ))
          x₀ →
        ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, F) (↑n : ℕ∞ω) (g i) x₀),
  ContMDiffAt 𝓘(ℝ, E) 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω)
    (fun (x : E) ↦
      ∑ᶠ (i : ι),
        HSMul.hSMul (α := ℝ)
          ((((f : (a : ι) → C^∞⟮𝓘(ℝ, E), E; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮𝓘(ℝ, E), E; 𝓘(ℝ, ℝ), ℝ⟯) : (a : E) → ℝ) x : ℝ) (g i x))
    x₀
Tactic: simp only [← contMDiffAt_iff_contDiffAt] at *
Cleared hypotheses: hφ
-- 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
s : Set M
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) → ℝ)
i : ι
⊢ LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦
    mulSupport (M := ℝ) fun (x : M) ↦
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ) x : ℝ)
have simp : LocallyFinite.{uι, uM} (X := M) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(M, ℝ)) i : C(M, ℝ)) : (a : M) → ℝ)
Tactic: simp only [mulSupport_one_sub]
-- 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
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι 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:
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 : LocallyCompactSpace H
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι 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 (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
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have 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 → ℝ)
Tactic: have hB := fun x hx => SmoothBumpFunction.nhds_basis_support (I := I) (hU 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
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) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have rcases : ∀ (ι : 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 → ℝ)),
  ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
Tactic: rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with
    ⟨ι, c, f, hf, hsub', hfin⟩
-- 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 → ℝ)
⊢ ∃ (ι : Type uM) (f : SmoothBumpCovering ι I M s), f.IsSubordinate (s := s) U
have hcs : ∀ (a : ι), c a ∈ s
Tactic: choose hcs hfU using hf
Cleared hypotheses: hf