Theorem: Geometry.SimplicialComplex.facets_mono (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
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
⊢ K₁.facets ⊆ K₂.facets
Tactic:
refine' fun s hs => ⟨h hs.1, fun t ht hst => Finset.eq_of_subset_of_card_le hst _⟩
State after:
𝕜 : 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
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ s.card

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
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ s.card
Tactic:
rw [hK₁.2 hs]
State after:
𝕜 : 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
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ n + 1

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
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ n + 1
Tactic:
exact hK₂.card_le ht
State after:
no goals