Theorem: Geometry.SimplicialComplex.skeleton_nonempty_iff (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)
⊢ (K.skeleton k).faces.Nonempty ↔ K.faces.Nonempty
Tactic:
refine' ⟨Set.Nonempty.mono skeleton_le, _⟩
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)
⊢ K.faces.Nonempty → (K.skeleton k).faces.Nonempty

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)
⊢ K.faces.Nonempty → (K.skeleton k).faces.Nonempty
Tactic:
rintro ⟨s, hs⟩
State after:
case 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)
s : Finset E
hs : s ∈ K.faces
⊢ (K.skeleton k).faces.Nonempty

State before:
case 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)
s : Finset E
hs : s ∈ K.faces
⊢ (K.skeleton k).faces.Nonempty
Tactic:
obtain ⟨x, hx⟩ := K.nonempty hs
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)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ (K.skeleton k).faces.Nonempty

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)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ (K.skeleton k).faces.Nonempty
Tactic:
refine' ⟨{x}, K.down_closed' hs (singleton_subset_iff.2 hx) <| singleton_nonempty _, _⟩
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)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ {x}.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)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ {x}.card ≤ k + 1
Tactic:
rw [card_singleton]
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)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ 1 ≤ 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)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ 1 ≤ k + 1
Tactic:
exact le_add_self
State after:
no goals