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 : ℕ∞
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)
⊢ ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
have this : ∀ (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)⟩
Tactic: have (j : M) : CMDiff n (T% (fun x ↦ (ρ j x) • (s_loc j x))) := by
    refine ContMDiffOn.smul_section_of_tsupport ?_ isOpen_interior (hρU j)
      ((s_smooth j).mono interior_subset)
    exact ((ρ j).contMDiff).of_le (sup_eq_left.mp rfl) |>.contMDiffOn
-- 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)
this :
  ∀ (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)⟩
⊢ ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) fun (x : M) ↦ ⟨x, s x⟩
have apply : LocallyFinite (X := M) fun (i : M) ↦
  {x : M |
    HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (s_loc i x) ≠
      0}
Tactic: apply ContMDiff.finsum_section_of_locallyFinite ?_ 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 : ℕ∞
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)
this :
  ∀ (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)⟩
⊢ LocallyFinite (X := M) fun (i : M) ↦
    {x : M |
      HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (s_loc i x) ≠
        0}
have apply : ∀ (i x : M)
  (hx :
    Membership.mem (γ := Set M)
      {x : M |
        HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
            (s_loc i x) ≠
          0}
      x),
  Membership.mem (γ := Set M)
    (support (M := ℝ) (⇑((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
Tactic: apply ρ.locallyFinite.subset fun i x 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 : ℕ∞
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)
this :
  ∀ (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)⟩
i x : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (s_loc i x) ≠
        0}
    x
⊢ Membership.mem (γ := Set M)
    {x : M |
      Ne (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)}
    x
have hx₁ : HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
    (s_loc i x) ≠
  0
Tactic: rw [mem_setOf_eq] at hx ⊢
Cleared hypotheses: 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 : ℕ∞
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)
this :
  ∀ (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)⟩
⊢ ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
have hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) fun (x : M) ↦ ⟨x, s x⟩
Tactic: have hs : CMDiff n (T% s) := by
    apply ContMDiff.finsum_section_of_locallyFinite ?_ this
    -- Future: can grind do this?
    apply ρ.locallyFinite.subset fun i x hx ↦ ?_
    rw [support]
    rw [mem_setOf_eq] at hx ⊢
    exact left_ne_zero_of_smul hx
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : FiniteDimensional ℝ E
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
inst_8 : T2Space M
n : ℕ∞
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)
this :
  ∀ (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)⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) fun (x : M) ↦ ⟨x, s x⟩
⊢ ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x
have refine : ∀ (x : M), (ContMDiffSection.mk (V := V) s hs : (a : M) → V a) x ∈ t x
Tactic: refine ⟨⟨s, hs⟩, 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)
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)
this :
  ∀ (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)⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) fun (x : M) ↦ ⟨x, s x⟩
x : M
⊢ (ContMDiffSection.mk (V := V) s hs : (a : M) → V a) x ∈ t x
have apply : ∀ (i : M),
  Ne (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ) →
    s_loc i x ∈ t x
Tactic: apply (ht_conv x).finsum_mem (ρ.nonneg · x) (ρ.sum_eq_one (mem_univ 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 : ℕ∞
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)
this :
  ∀ (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)⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) fun (x : M) ↦ ⟨x, s x⟩
x j : M
h_ρjx_ne_zero :
  Ne (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
⊢ s_loc j x ∈ t x
have h_x_in_tsupport_ρj : Membership.mem (γ := Set M)
  (tsupport (α := ℝ) (⇑((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
Tactic: have h_x_in_tsupport_ρj : x ∈ tsupport (ρ j) := subset_closure (mem_support.mpr h_ρjx_ne_zero)
-- 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)
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)
this :
  ∀ (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)⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) fun (x : M) ↦ ⟨x, s x⟩
x j : M
h_ρjx_ne_zero :
  Ne (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
h_x_in_tsupport_ρj :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
⊢ s_loc j x ∈ t x
have h_x_in_Umap_j : x ∈ W j
Tactic: have h_x_in_Umap_j : x ∈ W j := interior_subset (hρU j h_x_in_tsupport_ρj)
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i
have rcases : ∀ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) (hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ))
  (hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i),
  ∃ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i
Tactic: rcases Metric.exists_contMDiffMap_forall_closedEBall_subset I hK hU hKU hfin with ⟨δ, hδ0, 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
⊢ ∃ (δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯),
    (∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i
have refine : ∀ (i : ι) (x : M) (hx : x ∈ K i), closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i
Tactic: refine ⟨δ, hδ0, fun i x hx => ?_⟩
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst_4 : MetricSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I ∞ M
inst_7 : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : M) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
i : ι
x : M
hx : x ∈ K i
⊢ closedBall x ((δ : (a : M) → ℝ) x) ⊆ U i
have rw : closedEBall x (ENNReal.ofReal ((δ : (a : M) → ℝ) x)) ⊆ U i
Tactic: rw [← Metric.closedEBall_ofReal (hδ0 _).le]
-- 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
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
⊢ ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
Tactic: have h's : IsOpen (I.symm ⁻¹' s) := I.continuous_symm.isOpen_preimage _ hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.PartitionOfUnity (goal)
Goal:
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst_3 : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst_2] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((↑I.symm : E → H) ⁻¹' s)
⊢ ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have rcases : ∀ (f : E → ℝ) (f_supp : support f = (↑I.symm : E → H) ⁻¹' s) (f_diff : ContDiff ℝ (↑n : ℕ∞ω) f)
  (f_range : range f ⊆ Icc 0 1), ∃ (f : H → ℝ), support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
Tactic: rcases h's.exists_contDiff_support_eq with ⟨f, f_supp, f_diff, f_range⟩