awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 :
  HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
      (s_loc i x) ≠
    0
⊢ Ne (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
left_ne_zero_of_smul hx

Premises used: left_ne_zero_of_smul
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 :
  HSMul.hSMul (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
      (s_loc i x) ≠
    0
⊢ Ne (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact left_ne_zero_of_smul hx

Premises used: left_ne_zero_of_smul
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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⟩

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
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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

Tactic:
⟨⟨s, hs⟩, fun x ↦ ?_⟩

Premises used: ContMDiffSection.mk, Exists.intro
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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⟩
refine : ∀ (x : M), (ContMDiffSection.mk (V := V) s hs : (a : M) → V a) x ∈ t x
⊢ ∃ (s : Cₛ^(↑n : ℕ∞ω)⟮I; F_fiber, V⟯), ∀ (x : M), (s : (a : M) → V a) x ∈ t x

Tactic:
refine ⟨⟨s, hs⟩, fun x ↦ ?_⟩
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
apply :
  ∀ (i : M),
    Ne (α := ℝ) ((((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ) →
      s_loc i x ∈ t x
⊢ (ContMDiffSection.mk (V := V) s hs : (a : M) → V a) x ∈ t x

Tactic:
apply (ht_conv x).finsum_mem (ρ.nonneg · x) (ρ.sum_eq_one (mem_univ x))

Premises used: SmoothPartitionOfUnity.nonneg, SmoothPartitionOfUnity.sum_eq_one, Set.mem_univ, Convex.finsum_mem
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ℝ)
⊢ 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)
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
⊢ x ∈ W j

Tactic:
have h_x_in_Umap_j : x ∈ W j := interior_subset (hρU j h_x_in_tsupport_ρj)
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
h_x_in_Umap_j : x ∈ W j
⊢ s_loc j x ∈ t x

Tactic:
h_mem_t j x h_x_in_Umap_j
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
h_x_in_Umap_j : x ∈ W j
⊢ s_loc j x ∈ t x

Tactic:
exact h_mem_t j x h_x_in_Umap_j
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
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
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
Hloc : ∀ (x : M), ∃ U ∈ 𝓝 x, ∃ (g : M → F), ContMDiffOn I 𝓘(ℝ, F) (↑n : ℕ∞ω) g U ∧ ∀ y ∈ U, g y ∈ t y
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯), ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)

Tactic:
let ⟨s, hs⟩ := exists_contMDiffSection_forall_mem_convex_of_local I (fun _ ↦ F) t ht
    (fun x₀ ↦ let ⟨U, hU, g, hgs, hgt⟩ := Hloc x₀
      ⟨U, hU, g, fun y hy ↦ Bundle.contMDiffWithinAt_section |>.mpr <| hgs y hy, hgt⟩)
  ⟨⟨s, (Bundle.contMDiffAt_section _ |>.mp <| s.contMDiff ·)⟩, hs⟩

Premises used: Iff.mpr, _private.0.exists_contMDiffMap_forall_mem_convex_of_local.match_1, Real, exists_contMDiffSection_forall_mem_convex_of_local, Membership.mem, Exists, nhds, Bundle.TotalSpace.mk', WithTop.some, Subtype.mk, _private.0.exists_contMDiffMap_forall_mem_convex_of_local.match_2, And, And.intro, ContMDiffSection.contMDiff, Bundle.contMDiffAt_section, Exists.intro, Iff.mp, modelWithCornersSelf, Bundle.contMDiffWithinAt_section, DFunLike.coe, ModelWithCorners.prod, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
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
inst_9 : SigmaCompactSpace M
inst_10 : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
Hloc : ∀ (x : M), ∃ (c : F), ∀ᶠ (y : M) in 𝓝 x, c ∈ t y
⊢ ∃ (g : C^(↑n : ℕ∞ω)⟮I, M; 𝓘(ℝ, F), F⟯), ∀ (x : M), Membership.mem (α := F) (t x) ((g : (a : M) → F) x : F)

Tactic:
exists_contMDiffMap_forall_mem_convex_of_local I ht fun x =>
    let ⟨c, hc⟩ := Hloc x
    ⟨_, hc, fun _ => c, contMDiffOn_const, fun _ => id⟩

Premises used: Real, setOf, Membership.mem, Exists, nhds, id, WithTop.some, And, exists_contMDiffMap_forall_mem_convex_of_local, And.intro, Exists.intro, contMDiffOn_const, modelWithCornersSelf, _private.0.exists_contMDiffMap_forall_mem_convex_of_local_const.match_1, ContMDiffOn