awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
mpr : s ∈ 𝓝 y
⊢ f.preimage s ∈ 𝓝 x

Tactic:
apply h'
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
mpr : ∃ t ⊆ s, IsOpen[inst_1] t ∧ y ∈ t
⊢ s ∈ 𝓝 y

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ ∃ t ⊆ s, IsOpen[inst_1] t ∧ y ∈ t

Tactic:
⟨s, Set.Subset.refl _, os, ys⟩

Premises used: Set.Subset.refl, And.intro, Exists.intro
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ ∃ t ⊆ s, IsOpen[inst_1] t ∧ y ∈ t

Tactic:
exact ⟨s, Set.Subset.refl _, os, ys⟩
-- Module: Mathlib.Topology.Partial
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
x : X
s : Set X
⊢ ContinuousWithinAt f s x ↔ PTendsto (PFun.res f s) (𝓝 x) (𝓝 (f x))

Tactic:
tendsto_iff_ptendsto _ _ _ _

Premises used: Filter.tendsto_iff_ptendsto, ContinuousWithinAt, nhdsWithin
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
E : Type u_1
inst_1 : AddCommMonoid E
inst_2 : SMulWithZero ℝ E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul ℝ E
s : Set X
f_1 f g : PartitionOfUnity ι X s
h : f.toFun (s := s) = g.toFun (s := s)
mk :
  ∀ (toFun : ι → C(X, ℝ))
    (locallyFinite' : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : X) → ℝ))
    (nonneg' : 0 ≤ toFun) (sum_eq_one' : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : X) → ℝ) x) 1)
    (sum_le_one' : ∀ (x : X), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : X) → ℝ) x) 1)
    (h :
      (PartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) =
        g.toFun (s := s)),
    PartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
E : Type u_1
inst_1 : AddCommMonoid E
inst_2 : SMulWithZero ℝ E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul ℝ E
s : Set X
f g : PartitionOfUnity ι X s
toFun : ι → C(X, ℝ)
locallyFinite' : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : X) → ℝ)
nonneg' : 0 ≤ toFun
sum_eq_one' : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : X) → ℝ) x) 1
sum_le_one' : ∀ (x : X), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : X) → ℝ) x) 1
h :
  (PartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) = g.toFun (s := s)
mk :
  ∀ (toFun_1 : ι → C(X, ℝ))
    (locallyFinite'_1 : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun_1 i) : (a : X) → ℝ))
    (nonneg'_1 : 0 ≤ toFun_1) (sum_eq_one'_1 : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : X) → ℝ) x) 1)
    (sum_le_one'_1 : ∀ (x : X), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : X) → ℝ) x) 1)
    (h :
      (PartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) =
        (PartitionOfUnity.mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1).toFun (s := s)),
    PartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' =
      PartitionOfUnity.mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1
⊢ PartitionOfUnity.mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' = g

Tactic:
cases g
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
E : Type u_1
inst_1 : AddCommMonoid E
inst_2 : SMulWithZero ℝ E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
toFun : ι → C(X, ℝ)
locallyFinite' : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun i) : (a : X) → ℝ)
nonneg' : 0 ≤ toFun
sum_eq_one' : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : X) → ℝ) x) 1
sum_le_one' : ∀ (x : X), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun i : (a : X) → ℝ) x) 1
toFun_1 : ι → C(X, ℝ)
locallyFinite'_1 : LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑(toFun_1 i) : (a : X) → ℝ)
nonneg'_1 : 0 ≤ toFun_1
sum_eq_one'_1 : ∀ x ∈ s, Eq (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : X) → ℝ) x) 1
sum_le_one'_1 : ∀ (x : X), LE.le (α := ℝ) (∑ᶠ (i : ι), (toFun_1 i : (a : X) → ℝ) x) 1
h :
  (mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) =
    (mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1).toFun (s := s)
⊢ mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' =
    mk (s := s) toFun_1 locallyFinite'_1 nonneg'_1 sum_eq_one'_1 sum_le_one'_1

Tactic:
congr
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ support (M := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
f.locallyFinite'

Premises used: PartitionOfUnity.locallyFinite'
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
⊢ LocallyFinite.{u, v} (X := X) fun (i : ι) ↦ tsupport (α := ℝ) (⇑((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
f.locallyFinite.closure

Premises used: PartitionOfUnity.locallyFinite, LocallyFinite.closure, tsupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
i : ι
x : X
⊢ LE.le (α := ℝ) (0 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)

Tactic:
f.nonneg' i x

Premises used: PartitionOfUnity.nonneg'
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
⊢ Eq (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1

Tactic:
f.sum_eq_one' x hx

Premises used: PartitionOfUnity.sum_eq_one'
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
⊢ Eq (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1

Tactic:
have H := f.sum_eq_one hx
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : Eq (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
contrapose! :
  ∀ (H : ∀ (i : ι), LE.le (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)),
    Ne (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
⊢ ∃ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)

Tactic:
contrapose! H
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (i : ι), LE.le (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ Ne (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1

Tactic:
simpa only [fun i => (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one

Premises used: finsum_zero, LE.le.antisymm, zero_ne_one, PartitionOfUnity.nonneg
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
⊢ LE.le (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1

Tactic:
f.sum_le_one' x

Premises used: PartitionOfUnity.sum_le_one'
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
⊢ LE.le (α := ℝ) 0 (∑ᶠ (i : ι), (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x)

Tactic:
finsum_nonneg fun i => f.nonneg i x

Premises used: PartitionOfUnity.nonneg, finsum_nonneg
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
i : ι
x : X
⊢ LE.le (α := ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
(single_le_finsum i (f.locallyFinite.point_finite x) fun j => f.nonneg j x).trans (f.sum_le_one x)

Premises used: single_le_finsum, PartitionOfUnity.locallyFinite, PartitionOfUnity.nonneg, LocallyFinite.point_finite, PartitionOfUnity.sum_le_one, LE.le.trans
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
⊢ i ∈ ρ.finsupport (s := s) x₀ ↔
    Membership.mem (γ := Set ι)
      (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) i

Tactic:
simp only [finsupport, mem_support, Finite.mem_toFinset, mem_setOf_eq]

Premises used: Set.Finite.mem_toFinset, Set.mem_setOf_eq, Function.mem_support, PartitionOfUnity.finsupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
h :
  ∀ (x : ι),
    x ∈ (↑(ρ.finsupport (s := s) x₀) : Set ι) ↔
      Membership.mem (γ := Set ι)
        (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) x
⊢ (↑(ρ.finsupport (s := s) x₀) : Set ι) =
    support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀

Tactic:
ext
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
x : ι
h :
  x ∈ ρ.finsupport (s := s) x₀ ↔
    Membership.mem (γ := Set ι)
      (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) x
h₁ h₂ :
  Membership.mem (γ := Set ι) (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
      x ↔
    Membership.mem (γ := Set ι)
      (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) x
⊢ x ∈ (↑(ρ.finsupport (s := s) x₀) : Set ι) ↔
    Membership.mem (γ := Set ι)
      (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) x

Tactic:
rw [Finset.mem_coe, mem_finsupport]

Premises used: Finset.mem_coe, PartitionOfUnity.mem_finsupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
rw :
  Eq (α := ℝ) (∑ i ∈ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
    (∑ᶠ (i : ι), (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
rw₁ rw₂ :
  Eq (α := ℝ) (∑ i ∈ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
    (∑ i ∈ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
⊢ Eq (α := ℝ) (∑ i ∈ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1

Tactic:
rw [← ρ.sum_eq_one hx₀, finsum_eq_sum_of_support_subset _ (ρ.coe_finsupport x₀).superset]

Premises used: PartitionOfUnity.coe_finsupport, PartitionOfUnity.sum_eq_one, finsum_eq_sum_of_support_subset, Eq.superset
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
rw :
  HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 =
    1
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1

Tactic:
rw [← Finset.sum_sdiff hI, ρ.sum_finsupport hx₀]

Premises used: PartitionOfUnity.sum_finsupport, Finset.sum_sdiff
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
this :
  Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
    (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0)
rw : HAdd.hAdd (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0) 1 = 1
rw₁ : Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0) 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 =
    1

Tactic:
rw [this, add_eq_right, Finset.sum_const_zero]

Premises used: Finset.sum_const_zero, add_eq_right
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
suffices :
  Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
    (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0)
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 =
    1

Tactic:
suffices ∑ i ∈ I \ ρ.finsupport x₀, (ρ i) x₀ = ∑ i ∈ I \ ρ.finsupport x₀, 0 by
    rw [this, add_eq_right, Finset.sum_const_zero]
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
apply :
  ∀ x ∈ I \ ρ.finsupport (s := s) x₀, Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
    (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0)

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
x : ι
hx : x ∈ I \ ρ.finsupport (s := s) x₀
⊢ x ∈ I ∧ Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)

Tactic:
simp only [Finset.mem_sdiff, ρ.mem_finsupport, mem_support, Classical.not_not] at hx

Premises used: Classical.not_not, Finset.mem_sdiff, Function.mem_support, PartitionOfUnity.mem_finsupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
x : ι
hx : x ∈ I ∧ Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
x : ι
hx : x ∈ I ∧ Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport (s := s) x₀ ⊆ I
rw :
  HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀)
      (∑ x ∈ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) =
    1
rw₁ rw₂ rw₃ :
  HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 =
    1
rw₄ :
  Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
    (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0)
rw₅ rw₆ :
  ∀ (x : ι) (hx : x ∈ I \ ρ.finsupport (s := s) x₀),
    Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)
rw₇ :
  ∀ (x : ι) (hx : x ∈ I ∧ Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)),
    Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1

Tactic:
classical
  rw [← Finset.sum_sdiff hI, ρ.sum_finsupport hx₀]
  suffices ∑ i ∈ I \ ρ.finsupport x₀, (ρ i) x₀ = ∑ i ∈ I \ ρ.finsupport x₀, 0 by
    rw [this, add_eq_right, Finset.sum_const_zero]
  apply Finset.sum_congr rfl
  rintro x hx
  simp only [Finset.mem_sdiff, ρ.mem_finsupport, mem_support, Classical.not_not] at hx
  exact hx.2

Premises used: Classical.not_not, Finset.mem_sdiff, Function.mem_support, Finset.sum_congr, rfl, PartitionOfUnity.sum_finsupport, PartitionOfUnity.mem_finsupport
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module ℝ M
φ : ι → X → M
apply :
  (support.{u, u_2} (M := M) fun (i : ι) ↦
      HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (φ i x₀)) ⊆
    (↑(ρ.finsupport (s := s) x₀) : Set ι)
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i ∈ ρ.finsupport (s := s) x₀,
      HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (φ i x₀))
    (∑ᶠ (i : ι), HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (φ i x₀))

Tactic:
apply (finsum_eq_sum_of_support_subset _ _).symm

Premises used: finsum_eq_sum_of_support_subset, Eq.symm
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module ℝ M
φ : ι → X → M
⊢ (fun (i : ι) ↦ HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (φ i x₀)) =
    HSMul.hSMul (α := (i : ι) → ℝ) (β := (i : ι) → M)
      (fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) fun (i : ι) ↦ φ i x₀

Tactic:
have : (fun i ↦ (ρ i) x₀ • φ i x₀) = (fun i ↦ (ρ i) x₀) • (fun i ↦ φ i x₀) :=
    funext fun _ => (Pi.smul_apply' _ _ _).symm
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module ℝ M
φ : ι → X → M
this :
  (fun (i : ι) ↦ HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (φ i x₀)) =
    HSMul.hSMul (α := (i : ι) → ℝ) (β := (i : ι) → M)
      (fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) fun (i : ι) ↦ φ i x₀
rw :
  Subset.{u} (α := Set ι)
    ((support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) ∩
      support.{u, u_2} (M := M) fun (i : ι) ↦ φ i x₀)
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
⊢ (support.{u, u_2} (M := M) fun (i : ι) ↦
      HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (φ i x₀)) ⊆
    (↑(ρ.finsupport (s := s) x₀) : Set ι)

Tactic:
rw [ρ.coe_finsupport x₀, this, support_smul]

Premises used: PartitionOfUnity.coe_finsupport, Function.support_smul
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module ℝ M
φ : ι → X → M
this :
  (fun (i : ι) ↦ HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (φ i x₀)) =
    HSMul.hSMul (α := (i : ι) → ℝ) (β := (i : ι) → M)
      (fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) fun (i : ι) ↦ φ i x₀
⊢ Subset.{u} (α := Set ι)
    ((support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) ∩
      support.{u, u_2} (M := M) fun (i : ι) ↦ φ i x₀)
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module ℝ M
φ : ι → X → M
this :
  (fun (i : ι) ↦ HSMul.hSMul (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (φ i x₀)) =
    HSMul.hSMul (α := (i : ι) → ℝ) (β := (i : ι) → M)
      (fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) fun (i : ι) ↦ φ i x₀
⊢ Subset.{u} (α := Set ι)
    ((support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) ∩
      support.{u, u_2} (M := M) fun (i : ι) ↦ φ i x₀)
    (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
rcases :
  ∀ (t : Set X) (t_in : t ∈ 𝓝 x₀)
    (ht :
      Set.Finite.{u} (α := ι)
        {i : ι |
          ((fun (i : ι) ↦ (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
              t).Nonempty}),
    Set.Finite.{u} (α := ι)
      {i : ι |
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}
⊢ Set.Finite.{u} (α := ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}

Tactic:
rcases ρ.locallyFinite x₀ with ⟨t, t_in, ht⟩

Premises used: PartitionOfUnity.locallyFinite
-- Module: Mathlib.Topology.PartitionOfUnity
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht :
  Set.Finite.{u} (α := ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          t).Nonempty}
apply :
  Subset.{u} (α := Set ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          t).Nonempty}
⊢ Set.Finite.{u} (α := ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}

Tactic:
apply ht.subset

Premises used: Set.Finite.subset