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)
x_pt : M
h : Membership.mem (γ := Set M) univ x_pt
⊢ ∃ (i : M), x_pt ∈ U i

Tactic:
⟨x_pt, mem_interior_iff_mem_nhds.mpr (h_nhds x_pt)⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, 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)
x_pt : M
h : Membership.mem (γ := Set M) univ x_pt
⊢ ∃ (i : M), x_pt ∈ U i

Tactic:
exact ⟨x_pt, mem_interior_iff_mem_nhds.mpr (h_nhds x_pt)⟩
-- 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)
⊢ 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)⟩
-- 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), ρ.IsSubordinate (s := univ) U

Tactic:
SmoothPartitionOfUnity.exists_isSubordinate
      I isClosed_univ U (fun x ↦ isOpen_interior) hU_covers_univ

Premises used: SmoothPartitionOfUnity.exists_isSubordinate, isClosed_univ, isOpen_interior
-- 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)
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
⊢ ∃ (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

Premises used: SmoothPartitionOfUnity.exists_isSubordinate, isClosed_univ, isOpen_interior, Set.univ, SmoothPartitionOfUnity
-- 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)
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:
ContMDiffOn.smul_section_of_tsupport ?_ isOpen_interior (hρU j)
      ((s_smooth j).mono interior_subset)

Premises used: interior_subset, isOpen_interior, ContMDiffOn.mono, ContMDiffOn.smul_section_of_tsupport
-- 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)
j : M
refine :
  ContMDiffOn I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω)
    (⇑((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) (interior (W j))
⊢ 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:
refine ContMDiffOn.smul_section_of_tsupport ?_ isOpen_interior (hρU j)
      ((s_smooth j).mono interior_subset)

Premises used: interior_subset, isOpen_interior, ContMDiffOn.mono, ContMDiffOn.smul_section_of_tsupport
-- 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)
j : M
⊢ ContMDiffOn I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω)
    (⇑((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) (interior (W j))

Tactic:
((ρ j).contMDiff).of_le (sup_eq_left.mp rfl) |>.contMDiffOn

Premises used: sup_eq_left, ContMDiffMap.contMDiff, ContMDiff.contMDiffOn, Iff.mp, ContMDiff.of_le, DFunLike.coe
-- 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)
j : M
⊢ ContMDiffOn I 𝓘(ℝ, ℝ) (M' := ℝ) (↑n : ℕ∞ω)
    (⇑((ρ : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) j : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) (interior (W j))

Tactic:
exact ((ρ j).contMDiff).of_le (sup_eq_left.mp rfl) |>.contMDiffOn

Premises used: sup_eq_left, ContMDiffMap.contMDiff, ContMDiff.contMDiffOn, Iff.mp, ContMDiff.of_le, DFunLike.coe
-- 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)
⊢ ∀ (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
-- 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)⟩
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}
⊢ ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) (M' := TotalSpace F_fiber V) (↑n : ℕ∞ω) fun (x : M) ↦ ⟨x, s x⟩

Tactic:
apply ContMDiff.finsum_section_of_locallyFinite ?_ this

Premises used: ContMDiff.finsum_section_of_locallyFinite
-- 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)⟩
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
⊢ 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 ρ.locallyFinite.subset fun i x hx ↦ ?_

Premises used: SmoothPartitionOfUnity.locallyFinite, LocallyFinite.subset
-- 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 :
  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
⊢ 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 ⊢

Premises used: Set.mem_setOf_eq