Theorem: Geometry.SimplicialComplex.eq_singleton_of_singleton_mem_combiInterior (LeanCamCombi/SimplicialComplex/Basic.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ s = {x}
Tactic:
apply disjoint_interiors hs hx hxs
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ x ∈ combiInterior 𝕜 {x}

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ x ∈ combiInterior 𝕜 {x}
Tactic:
rw [combiInterior_singleton]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ x ∈ {x}

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ x ∈ {x}
Tactic:
exact Set.mem_singleton x
State after:
no goals