Theorem: Geometry.SimplicialComplex.Pure.skeleton_of_le (LeanCamCombi/SimplicialComplex/Skeleton.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
⊢ (K.skeleton k).Pure k
Tactic:
refine' ⟨fun s hs => hs.2, _⟩
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
⊢ Set.Sized (k + 1) (K.skeleton k).facets

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
⊢ Set.Sized (k + 1) (K.skeleton k).facets
Tactic:
rintro s ⟨⟨hs, hscard⟩, hsmax⟩
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
s : Finset E
hsmax : ∀ ⦃t : Finset E⦄, t ∈ (K.skeleton k).faces → s ⊆ t → s = t
hs : s ∈ K
hscard : s.card ≤ k + 1
⊢ s.card = k + 1

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
s : Finset E
hsmax : ∀ ⦃t : Finset E⦄, t ∈ (K.skeleton k).faces → s ⊆ t → s = t
hs : s ∈ K
hscard : s.card ≤ k + 1
⊢ s.card = k + 1
Tactic:
obtain ⟨t, ht, hst, htcard⟩ := hK.exists_face_of_card_le (add_le_add_right h 1) hs hscard
State after:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
s : Finset E
hsmax : ∀ ⦃t : Finset E⦄, t ∈ (K.skeleton k).faces → s ⊆ t → s = t
hs : s ∈ K
hscard : s.card ≤ k + 1
t : Finset E
ht : t ∈ K
hst : s ⊆ t
htcard : t.card = k + 1
⊢ s.card = k + 1

State before:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
s : Finset E
hsmax : ∀ ⦃t : Finset E⦄, t ∈ (K.skeleton k).faces → s ⊆ t → s = t
hs : s ∈ K
hscard : s.card ≤ k + 1
t : Finset E
ht : t ∈ K
hst : s ⊆ t
htcard : t.card = k + 1
⊢ s.card = k + 1
Tactic:
rwa [hsmax ⟨ht, htcard.le⟩ hst]
State after:
no goals