Theorem: Geometry.SimplicialComplex.cells_subset_facets (LeanCamCombi/SimplicialComplex/Basic.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
⊢ K.cells ⊆ K.facets
Tactic:
rintro s ⟨hs, hscard⟩
State after:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
⊢ s ∈ K.facets

State before:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
⊢ s ∈ K.facets
Tactic:
by_contra h
State after:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
⊢ False

State before:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
⊢ False
Tactic:
obtain ⟨t, ht, hst⟩ := (not_facet_iff_subface hs).mp h
State after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
⊢ False

State before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
⊢ False
Tactic:
have := card_lt_card hst
State after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
this : s.card < t.card
⊢ False

State before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
this : s.card < t.card
⊢ False
Tactic:
have := face_dimension_le_space_dimension ht
State after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
this✝ : s.card < t.card
this : t.card ≤ FiniteDimensional.finrank 𝕜 E + 1
⊢ False

State before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
this✝ : s.card < t.card
this : t.card ≤ FiniteDimensional.finrank 𝕜 E + 1
⊢ False
Tactic:
linarith
State after:
no goals