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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∈ s
B :
  ∃ (c : M),
    0 <
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
refine_1 :
  Subset.{uM} (α := Set M)
    (fun (x_1 : M) ↦
      Eq (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) x_1 : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ))
    fun (x_1 : M) ↦
    Eq (α := ℝ)
      ((fun (c : M) ↦
          HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
            (g c ((↑(chartAt H c) : M → H) x)))
        x_1)
      0
⊢ Subset.{uM} (α := Set M)
    (support (M := ℝ) fun (c : M) ↦
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x)))
    {b : M |
      Membership.mem (γ := Set M)
        (support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) b : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x}

Tactic:
apply compl_subset_compl.2

Premises used: Iff.mpr, Set.compl_subset_compl
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∈ s
B :
  ∃ (c : M),
    0 <
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
c : M
hc : Eq (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ) (0 : ℝ)
⊢ Membership.mem (γ := Set M)
    (fun (x_1 : M) ↦
      Eq (α := ℝ)
        ((fun (c : M) ↦
            HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
              (g c ((↑(chartAt H c) : M → H) x)))
          x_1)
        0)
    c

Tactic:
simpa only [mul_eq_zero] using Or.inl hc

Premises used: mul_eq_zero, Or.inl
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
refine_1 :
  ∀ (x_1 : M),
    HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) x_1 : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g x_1 ((↑(chartAt H x_1) : M → H) x)) =
      0
⊢ Eq (α := ℝ)
    (∑ᶠ (c : M),
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x)))
    0

Tactic:
apply finsum_eq_zero_of_forall_eq_zero

Premises used: finsum_eq_zero_of_forall_eq_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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
pos :
  ∀
    (Hx :
      Membership.mem (γ := Set M)
        (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x),
    HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x)) =
      0
neg :
  ∀ (Hx : x ∉ tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)),
    HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x)) =
      0
⊢ HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
      (g c ((↑(chartAt H c) : M → H) x)) =
    0

Tactic:
by_cases Hx : x ∈ tsupport (f c)

Premises used: tsupport, 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
Hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
this : g c ((↑(chartAt H c) : M → H) x) = 0
⊢ HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
      (g c ((↑(chartAt H c) : M → H) x)) =
    0

Tactic:
simp only [this, mul_zero]

Premises used: MulZeroClass.mul_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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
Hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
pos : g c ((↑(chartAt H c) : M → H) x) = 0
⊢ HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
      (g c ((↑(chartAt H c) : M → H) x)) =
    0

Tactic:
suffices g c (chartAt H c x) = 0 by simp only [this, mul_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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
Hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
pos :
  x ∉
    (↑(chartAt H c) : M → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
      (↑(chartAt H c) : M → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
⊢ g c ((↑(chartAt H c) : M → H) x) = 0

Tactic:
rw [← notMem_support, g_supp, ← mem_preimage, preimage_inter]

Premises used: Set.preimage_inter, Function.notMem_support, Set.mem_preimage
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
Hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
pos :
  ∀
    (hx :
      x ∈
        (↑(chartAt H c) : M → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
          (↑(chartAt H c) : M → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s),
    x ∈ s
⊢ x ∉
    (↑(chartAt H c) : M → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
      (↑(chartAt H c) : M → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s

Tactic:
contrapose 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x c : M
Hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
hx :
  x ∈
    (↑(chartAt H c) : M → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
      (↑(chartAt H c) : M → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
⊢ (↑(chartAt H c) : M → H) x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∧ x ∈ s

Tactic:
simp only [mem_inter_iff, mem_preimage, (chartAt H c).left_inv (hf c Hx)] at hx

Premises used: chartAt, Set.mem_inter_iff, OpenPartialHomeomorph.left_inv, Set.mem_preimage
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x c : M
Hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
hx : (↑(chartAt H c) : M → H) x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∧ x ∈ s
⊢ x ∈ s

Tactic:
hx.2

Premises used: And.right
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x c : M
Hx :
  Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
hx : (↑(chartAt H c) : M → H) x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∧ x ∈ s
⊢ x ∈ s

Tactic:
exact hx.2

Premises used: And.right
-- 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
Hx : x ∉ tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)
contrapose :
  ∀
    (Hx :
      Membership.mem (γ := Set M)
        (support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x),
    Membership.mem (γ := Set M)
      (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
⊢ x ∉ support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)

Tactic:
contrapose 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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
Hx :
  Membership.mem (γ := Set M)
    (support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
⊢ Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x

Tactic:
subset_tsupport _ Hx

Premises used: subset_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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
Hx :
  Membership.mem (γ := Set M)
    (support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x
⊢ Membership.mem (γ := Set M)
    (tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)) x

Tactic:
exact subset_tsupport _ Hx

Premises used: subset_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 : ℕ∞
s : Set M
hs : IsOpen[inst_3] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate (s := univ) fun (x : M) ↦ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
g : (c : M) → H → ℝ
g_supp :
  ∀ (c : M),
    support (g c) =
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H c)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H c)) : H → M) ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n : ℕ∞ω) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g :
  ∀ (c x : M),
    0 ≤
      HMul.hMul (α := ℝ) ((((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ) x : ℝ)
        (g c ((↑(chartAt H c) : M → H) x))
x : M
hx : x ∉ s
c : M
Hx : x ∉ tsupport (α := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)
⊢ x ∉ support (M := ℝ) (⇑((f : (a : M) → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) c : C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯) : (a : M) → ℝ)

Tactic:
have : x ∉ support (f c) := by contrapose Hx; exact subset_tsupport _ Hx