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

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
⊢ (K.skeleton k).Pure (min k n)
Tactic:
obtain hn | hn := le_total k n
State after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : k ≤ n
⊢ (K.skeleton k).Pure (min k n)

case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure (min k n)

State before:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : k ≤ n
⊢ (K.skeleton k).Pure (min k n)
Tactic:
rw [min_eq_left hn]
State after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : k ≤ n
⊢ (K.skeleton k).Pure k

State before:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : k ≤ n
⊢ (K.skeleton k).Pure k
Tactic:
exact hK.skeleton_of_le hn
State after:
no goals

State before:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure (min k n)
Tactic:
rw [min_eq_right hn]
State after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure n

State before:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure n
Tactic:
refine' ⟨fun s hs => hK.1 <| skeleton_le hs, fun s hs => _⟩
State after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
⊢ s.card = n + 1

State before:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
⊢ s.card = n + 1
Tactic:
obtain ⟨t, ht, hst⟩ := subfacet (skeleton_le hs.1)
State after:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ s.card = n + 1

State before:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ s.card = n + 1
Tactic:
rw [hs.2 ⟨facets_subset ht, (hK.2 ht).le.trans (add_le_add_right hn _)⟩ hst]
State after:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ t.card = n + 1

State before:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ t.card = n + 1
Tactic:
exact hK.2 ht
State after:
no goals