Theorem: Geometry.SimplicialComplex.pure_iff (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
⊢ K.Pure n ↔ ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
Tactic:
refine' ⟨fun hK s hs => _, fun hK => ⟨fun s hs => _, fun s hs => _⟩⟩
State after:
case refine'_1
𝕜 : 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.Pure n
s : Finset E
hs : s ∈ K
⊢ ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t

case refine'_2
𝕜 : 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 : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K
⊢ s.card ≤ n + 1

case refine'_3
𝕜 : 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 : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
⊢ s.card = n + 1

State before:
case refine'_1
𝕜 : 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.Pure n
s : Finset E
hs : s ∈ K
⊢ ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
Tactic:
obtain ⟨t, ht, hst⟩ := hK.exists_facet hs
State after:
case refine'_1.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
hK : K.Pure n
s : Finset E
hs : s ∈ K
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t

State before:
case refine'_1.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
hK : K.Pure n
s : Finset E
hs : s ∈ K
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
Tactic:
exact ⟨t, ht.1, hK.2 ht, hst⟩
State after:
no goals

State before:
case refine'_2
𝕜 : 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 : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K
⊢ s.card ≤ n + 1
Tactic:
obtain ⟨t, _, htcard, hst⟩ := hK hs
State after:
case refine'_2.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
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K
t : Finset E
left✝ : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card ≤ n + 1

State before:
case refine'_2.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
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K
t : Finset E
left✝ : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card ≤ n + 1
Tactic:
exact (Finset.card_le_card hst).trans_eq htcard
State after:
no goals

State before:
case refine'_3
𝕜 : 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 : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
⊢ s.card = n + 1
Tactic:
obtain ⟨t, ht, htcard, hst⟩ := hK hs.1
State after:
case refine'_3.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
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
t : Finset E
ht : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card = n + 1

State before:
case refine'_3.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
hK : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
t : Finset E
ht : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card = n + 1
Tactic:
rwa [hs.2 ht hst]
State after:
no goals