Theorem: Geometry.SimplicialComplex.eq_bot_of_forall_not_mem (LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.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 y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
K : SimplicialComplex 𝕜 E
h : ∀ (s : Finset E), s ∉ K
⊢ K = ⊥
Tactic:
ext s
State after:
case faces.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K✝ K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
K : SimplicialComplex 𝕜 E
h : ∀ (s : Finset E), s ∉ K
s : Finset E
⊢ s ∈ K.faces ↔ s ∈ ⊥.faces

State before:
case faces.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K✝ K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
K : SimplicialComplex 𝕜 E
h : ∀ (s : Finset E), s ∉ K
s : Finset E
⊢ s ∈ K.faces ↔ s ∈ ⊥.faces
Tactic:
exact iff_of_false (h s) id
State after:
no goals