awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
⊢ Eq (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x) 1

Tactic:
f.sum_eq_one' x hx

Premises used: SmoothPartitionOfUnity.sum_eq_one'
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
by_contra! :
  ∀
    (h :
      ∀ (i : ι),
        LE.le (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
          (0 : ℝ)),
    False
⊢ ∃ (i : ι),
    LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)

Tactic:
by_contra! h
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ℝ)
⊢ ∀ (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)
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ℝ)
⊢ Eq (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x) 1

Tactic:
have := f.sum_eq_one hx
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
⊢ Eq (α := ℝ) (∑ᶠ (i : ι), 0) 1

Tactic:
simp_rw [H] at this
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ι), 0) 1
⊢ False

Tactic:
simpa
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
⊢ LE.le (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x) 1

Tactic:
f.sum_le_one' x

Premises used: SmoothPartitionOfUnity.sum_le_one'
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
⊢ ContMDiff I 𝓘(ℝ, ℝ) (M' := ℝ) ∞ fun (x : M) ↦
    ∑ᶠ (i : ι), (((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x

Tactic:
contMDiff_finsum (fun i => (f i).contMDiff) f.locallyFinite

Premises used: SmoothPartitionOfUnity.locallyFinite, ContMDiffMap.contMDiff, contMDiff_finsum, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
i : ι
x : M
⊢ LE.le (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
f.toPartitionOfUnity.le_one i x

Premises used: SmoothPartitionOfUnity.toPartitionOfUnity, PartitionOfUnity.le_one
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
⊢ LE.le (α := ℝ) 0 (∑ᶠ (i : ι), (((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x)

Tactic:
f.toPartitionOfUnity.sum_nonneg x

Premises used: SmoothPartitionOfUnity.toPartitionOfUnity, PartitionOfUnity.sum_nonneg
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
g : ι → M → F
t : Set F
x : M
hx : x ∈ s
hg :
  ∀ (i : ι),
    Ne (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ) →
      g i x ∈ t
ht : Convex ℝ t
⊢ ∑ᶠ (i : ι),
      HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g i x) ∈
    t

Tactic:
ht.finsum_mem (fun _ => f.nonneg _ _) (f.sum_eq_one hx) hg

Premises used: SmoothPartitionOfUnity.nonneg, Set.Mem, SmoothPartitionOfUnity.sum_eq_one, Convex.finsum_mem
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ℕ∞
g : M → F
i : ι
hg :
  ∀ (x : M),
    Membership.mem (γ := Set M)
        (tsupport (α := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x →
      ContMDiffAt I 𝓘(ℝ, F) (↑n : ℕ∞ω) g x
⊢ ContMDiff I 𝓘(ℝ, F) (M' := F) (↑n : ℕ∞ω) fun (x : M) ↦
    HSMul.hSMul (α := ℝ) ((((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (g x)

Tactic:
contMDiff_of_tsupport fun x hx =>
    ((f i).contMDiff.contMDiffAt.of_le (mod_cast le_top)).smul <| hg x
      <| tsupport_smul_subset_left _ _ hx

Premises used: ContMDiffAt.smul, ContMDiffMap.contMDiff, contMDiff_of_tsupport, ContMDiffAt.of_le, ContMDiff.contMDiffAt, DFunLike.coe, tsupport_smul_subset_left
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ℕ∞
g : ι → M → F
hg :
  ∀ (i : ι) (x : M),
    Membership.mem (γ := Set M)
        (tsupport (α := ℝ) (⇑((f : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x →
      ContMDiffAt I 𝓘(ℝ, F) (↑n : ℕ∞ω) (g i) x
⊢ ContMDiff 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)

Tactic:
(contMDiff_finsum fun i ↦ f.contMDiff_smul (hg i)) <|
f.locallyFinite.subset fun _ ↦ support_smul_subset_left _ _

Premises used: SmoothPartitionOfUnity.locallyFinite, Function.support_smul_subset_left, LocallyFinite.subset, contMDiff_finsum, SmoothPartitionOfUnity.contMDiff_smul, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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₀

Tactic:
_root_.contMDiffAt_finsum (f.locallyFinite.smul_left _) fun i ↦ ?_

Premises used: SmoothPartitionOfUnity.locallyFinite, LocallyFinite.smul_left, contMDiffAt_finsum
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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₀
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₀
⊢ 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₀

Tactic:
refine _root_.contMDiffAt_finsum (f.locallyFinite.smul_left _) fun i ↦ ?_

Premises used: SmoothPartitionOfUnity.locallyFinite, LocallyFinite.smul_left, contMDiffAt_finsum
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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₀
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₀
⊢ 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)

Premises used: tsupport, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ι
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:
ContMDiffAt.smul ((f i).contMDiff.of_le (mod_cast le_top)).contMDiffAt (hφ i hx)

Premises used: ContMDiffAt.smul, ContMDiffMap.contMDiff, ContMDiff.of_le, ContMDiff.contMDiffAt, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ι
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:
exact ContMDiffAt.smul ((f i).contMDiff.of_le (mod_cast le_top)).contMDiffAt (hφ i hx)

Premises used: ContMDiffAt.smul, ContMDiffMap.contMDiff, ContMDiff.of_le, ContMDiff.contMDiffAt, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ι
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:
contMDiffAt_of_notMem (compl_subset_compl.mpr
      (tsupport_smul_subset_left (f i) (g i)) hx) n

Premises used: Iff.mpr, contMDiffAt_of_notMem, WithTop.some, Set.compl_subset_compl, DFunLike.coe, tsupport_smul_subset_left
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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 : ι
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:
exact contMDiffAt_of_notMem (compl_subset_compl.mpr
      (tsupport_smul_subset_left (f i) (g i)) hx) n

Premises used: Iff.mpr, contMDiffAt_of_notMem, WithTop.some, Set.compl_subset_compl, DFunLike.coe, tsupport_smul_subset_left
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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₀
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₀
⊢ 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₀

Tactic:
simp only [← contMDiffAt_iff_contDiffAt] at *

Premises used: contMDiffAt_iff_contDiffAt
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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₀ →
      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:
f.contMDiffAt_finsum hφ

Premises used: SmoothPartitionOfUnity.contMDiffAt_finsum
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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₀ →
      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:
exact f.contMDiffAt_finsum hφ

Premises used: SmoothPartitionOfUnity.contMDiffAt_finsum
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
i : ι
⊢ i ∈ ρ.finsupport (s := s) x₀ ↔
    Membership.mem (γ := Set ι)
      (support (M := ℝ) fun (i : ι) ↦
        (((ρ : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x₀)
      i

Tactic:
ρ.toPartitionOfUnity.mem_finsupport x₀

Premises used: Set.Mem, setOf, SmoothPartitionOfUnity.toPartitionOfUnity, PartitionOfUnity.mem_finsupport
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
⊢ (↑(ρ.finsupport (s := s) x₀) : Set ι) =
    support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x₀

Tactic:
ρ.toPartitionOfUnity.coe_finsupport x₀

Premises used: setOf, PartitionOfUnity.coe_finsupport, SmoothPartitionOfUnity.toPartitionOfUnity
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
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
ρ : SmoothPartitionOfUnity ι I M s
x₀ : M
hx₀ : x₀ ∈ s
⊢ Eq (α := ℝ)
    (∑ i ∈ ρ.finsupport (s := s) x₀,
      (((ρ : (a : ι) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x₀)
    1

Tactic:
ρ.toPartitionOfUnity.sum_finsupport hx₀

Premises used: SmoothPartitionOfUnity.toPartitionOfUnity, SmoothPartitionOfUnity.finsupport, PartitionOfUnity.sum_finsupport
-- Module: Mathlib.Geometry.Manifold.PartitionOfUnity
Goal:
ι : Type uι
E : Type uE
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type uH
inst_2 : TopologicalSpace H
I_1 : ModelWithCorners ℝ E H
M : Type uM
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
s : Set M
ρ : SmoothPartitionOfUnity ι I_1 M s
x₀ : M
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C^∞⟮I_1, M; 𝓘(ℝ, ℝ), ℝ⟯) i : C^∞⟮I_1, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x₀) 1

Tactic:
ρ.toPartitionOfUnity.sum_finsupport' hx₀ hI

Premises used: SmoothPartitionOfUnity.toPartitionOfUnity, PartitionOfUnity.sum_finsupport'