awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Partial (hypothesis)
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_1 : Set Y
os : IsOpen[inst_1] s_1
x : X
y : Y
ys : y ∈ s_1
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s_1 ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : PTendsto' f (𝓝 x) (𝓝 y)
⊢ f.preimage s ∈ 𝓝 x
have this₁ : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
Tactic: rw [ptendsto'_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Partial (hypothesis)
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
⊢ f.preimage s ∈ 𝓝 x
have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
Tactic: have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x := by
    intro s hs
    have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy
    rw [ptendsto'_def] at this
    exact this s hs
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
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
⊢ f.preimage s ∈ 𝓝 x
have mpr : s ∈ 𝓝 y
Tactic: apply h'
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
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
⊢ s ∈ 𝓝 y
have mpr : ∃ t ⊆ s, IsOpen[inst_1] t ∧ y ∈ t
Tactic: rw [mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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)
⊢ f = g
have 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 : (mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) = g.toFun (s := s)),
  mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : (mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one').toFun (s := s) = g.toFun (s := s)
⊢ mk (s := s) toFun locallyFinite' nonneg' sum_eq_one' sum_le_one' = g
have 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 :
    (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: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
⊢ ∃ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
have H : Eq (α := ℝ) (∑ᶠ (i : ι), (((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x) 1
Tactic: have H := f.sum_eq_one hx
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ ∃ (i : ι), LT.lt (α := ℝ) (0 : ℝ) ((((f : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ)
have 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
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ (↑(ρ.finsupport (s := s) x₀) : Set ι) =
    support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
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
have h : x ∈ ρ.finsupport (s := s) x₀ ↔
  Membership.mem (γ := Set ι) (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
    x
Tactic: rw [Finset.mem_coe, mem_finsupport]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ x ∈ (↑(ρ.finsupport (s := s) x₀) : Set ι) ↔
    Membership.mem (γ := Set ι)
      (support (M := ℝ) fun (i : ι) ↦ (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) x
have 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
Tactic: rw [Finset.mem_coe, mem_finsupport]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
⊢ Eq (α := ℝ) (∑ i ∈ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1
have 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₀)
Tactic: rw [← ρ.sum_eq_one hx₀, finsum_eq_sum_of_support_subset _ (ρ.coe_finsupport x₀).superset]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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₀)
⊢ Eq (α := ℝ) (∑ i ∈ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1
have 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₀)
Tactic: rw [← ρ.sum_eq_one hx₀, finsum_eq_sum_of_support_subset _ (ρ.coe_finsupport x₀).superset]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1
have rw : HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 = 1
Tactic: rw [← Finset.sum_sdiff hI, ρ.sum_finsupport hx₀]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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)
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 =
    1
have rw : HAdd.hAdd (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0) 1 = 1
Tactic: rw [this, add_eq_right, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 =
    1
have rw₁ : Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0) 0
Tactic: rw [this, add_eq_right, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 =
    1
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [this, add_eq_right, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 =
    1
have suffices : Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
  (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0)
Tactic: suffices ∑ i ∈ I \ ρ.finsupport x₀, (ρ i) x₀ = ∑ i ∈ I \ ρ.finsupport x₀, 0 by
    rw [this, add_eq_right, Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
    (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0)
have apply : ∀ x ∈ I \ ρ.finsupport (s := s) x₀, Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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₀
⊢ Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1
have 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
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
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1
have rw₁ : HAdd.hAdd (α := ℝ) (∑ x ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀) 1 = 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
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1
have rw₄ : Eq (α := ℝ) (∑ i ∈ I \ ρ.finsupport (s := s) x₀, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀)
  (∑ i ∈ I \ ρ.finsupport (s := s) x₀, 0)
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
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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)
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1
have rw₅ : ∀ x ∈ I \ ρ.finsupport (s := s) x₀, Eq (α := ℝ) ((((ρ : (a : ι) → C(X, ℝ)) x : C(X, ℝ)) : (a : X) → ℝ) x₀ : ℝ) (0 : ℝ)
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
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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 : ℝ)
⊢ Eq (α := ℝ) (∑ i ∈ I, (((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x₀) 1
have 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 : ℝ)
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
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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
⊢ 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₀))
have 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 ι)
Tactic: apply (finsum_eq_sum_of_support_subset _ _).symm
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (hypothesis)
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
⊢ (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 ι)
have 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₀
Tactic: have : (fun i ↦ (ρ i) x₀ • φ i x₀) = (fun i ↦ (ρ i) x₀) • (fun i ↦ φ i x₀) :=
    funext fun _ => (Pi.smul_apply' _ _ _).symm
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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₀
⊢ (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 ι)
have 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₀)
Tactic: rw [ρ.coe_finsupport x₀, this, support_smul]
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
Goal:
ι : Type u
X : Type v
inst : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ Set.Finite.{u} (α := ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}
have 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₀}
Tactic: rcases ρ.locallyFinite x₀ with ⟨t, t_in, ht⟩
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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}
⊢ Set.Finite.{u} (α := ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}
have 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}
Tactic: apply ht.subset
-- Lean 4 proof step from Mathlib.Topology.PartitionOfUnity (goal)
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}
i : ι
hi :
  Membership.mem (γ := Set ι)
    {i : ι | Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)) x₀}
    i
⊢ Membership.mem (γ := Set ι)
    {i : ι |
      ((fun (i : ι) ↦ (support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) : Set X)) i ∩
          t).Nonempty}
    i
have simp : Membership.mem (γ := Set ι)
  {i : ι | (t ∩ support (M := ℝ) (⇑((ρ : (a : ι) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ)).Nonempty} i
Tactic: simp only [inter_comm]