Theorem: Geometry.SimplicialComplex.LocallyFiniteAt.mono (LeanCamCombi/SimplicialComplex/Finite.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
⊢ K.LocallyFiniteAt t
Tactic:
apply hX.subset
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
⊢ {t_1 | t_1 ∈ K.faces ∧ t ⊆ t_1} ⊆ {t | t ∈ K.faces ∧ s ⊆ t}

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
⊢ {t_1 | t_1 ∈ K.faces ∧ t ⊆ t_1} ⊆ {t | t ∈ K.faces ∧ s ⊆ t}
Tactic:
rintro u ⟨_, _⟩
State after:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
u : Finset E
left✝ : u ∈ K.faces
right✝ : t ⊆ u
⊢ u ∈ {t | t ∈ K.faces ∧ s ⊆ t}

State before:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hX : K.LocallyFiniteAt s
hXY : s ⊆ t
u : Finset E
left✝ : u ∈ K.faces
right✝ : t ⊆ u
⊢ u ∈ {t | t ∈ K.faces ∧ s ⊆ t}
Tactic:
exact ⟨‹u ∈ K.faces›, hXY.trans ‹t ⊆ u›⟩
State after:
no goals