Theorem: Geometry.SimplicialComplex.Pure.exists_face_of_card_le (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.Pure n
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
by_cases H : s ∈ K.facets
State after:
case pos
𝕜 : 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
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∈ K.facets
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k

case neg
𝕜 : 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
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∉ K.facets
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k

State before:
case pos
𝕜 : 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
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∈ K.facets
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
exact ⟨s, hs, Subset.rfl, hcard.antisymm <| h.trans (hK.2 H).ge⟩
State after:
no goals

State before:
case neg
𝕜 : 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
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∉ K.facets
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
unfold facets at H
State after:
case neg
𝕜 : 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
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∉ {s | s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t}
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k

State before:
case neg
𝕜 : 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
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∉ {s | s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t}
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
simp at H
State after:
case neg
𝕜 : 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
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∈ K → ∃ x ∈ K, s ⊆ x ∧ ¬s = x
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k

State before:
case neg
𝕜 : 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
h : k ≤ n + 1
hs : s ∈ K
hcard : s.card ≤ k
H : s ∈ K → ∃ x ∈ K, s ⊆ x ∧ ¬s = x
⊢ ∃ t ∈ K, s ⊆ t ∧ t.card = k
Tactic:
sorry
State after:
no goals