Theorem: Geometry.SimplicialComplex.pure_unique (LeanCamCombi/SimplicialComplex/Pure.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.faces.Nonempty
ha : K.Pure a
hb : K.Pure b
⊢ a = b
Tactic:
obtain ⟨s, hs⟩ := hK
State after:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
ha : K.Pure a
hb : K.Pure b
s : Finset E
hs : s ∈ K.faces
⊢ a = b

State before:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
ha : K.Pure a
hb : K.Pure b
s : Finset E
hs : s ∈ K.faces
⊢ a = b
Tactic:
obtain ⟨t, ht, -⟩ := ha.exists_facet hs
State after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
ha : K.Pure a
hb : K.Pure b
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ a = b

State before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ : Finset E
ha : K.Pure a
hb : K.Pure b
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ a = b
Tactic:
exact add_right_cancel ((ha.2 ht).symm.trans <| hb.2 ht)
State after:
no goals