Theorem: Geometry.SimplicialComplex.facets_singleton (LeanCamCombi/Mathlib/Analysis/Convex/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 : ℕ
hK : K.faces = {s}
⊢ K.facets = {s}
Tactic:
rw [Set.eq_singleton_iff_unique_mem] at hK ⊢
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 : ℕ
hK : s ∈ K.faces ∧ ∀ x ∈ K.faces, x = s
⊢ s ∈ K.facets ∧ ∀ x ∈ K.facets, x = s

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 : ℕ
hK : s ∈ K.faces ∧ ∀ x ∈ K.faces, x = s
⊢ s ∈ K.facets ∧ ∀ x ∈ K.facets, x = s
Tactic:
exact ⟨⟨hK.1, fun t ht _ => (hK.2 _ ht).symm⟩, fun t ht => hK.2 _ ht.1⟩
State after:
no goals