-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_pos_of_mem {x} (hx : x ∈ s) : ∃ i, 0 < f i x

Proof state:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
⊢ False

Tactic:
have H : ∀ i, f i x = 0 := fun i ↦ le_antisymm (h i) (f.nonneg i x)

Result:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
⊢ False

Proof state:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
this : ∑ᶠ (i : ι), 0 = 1
⊢ False

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
⊢ ∃ i, 0 < (f i) x

Tactic:
by_contra! h

Result:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
⊢ False

Proof state:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
⊢ False

Tactic:
have := f.sum_eq_one hx

Result:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
this : ∑ᶠ (i : ι), (f i) x = 1
⊢ False

Proof state:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
this : ∑ᶠ (i : ι), (f i) x = 1
⊢ False

Tactic:
simp_rw [H] at this

Result:
ι : Type uι
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H✝ : Type uH
inst✝² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H✝ M
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
this : ∑ᶠ (i : ι), 0 = 1
⊢ False