Theorem: Geometry.SimplicialComplex.space_eq_empty (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.space = ∅ ↔ K = ⊥
Tactic:
simp only [Set.eq_empty_iff_forall_not_mem, mem_space_iff, SimplicialComplex.ext_iff,
  @forall_swap E, mem_faces_iff, exists_prop, not_exists, not_and, faces_bot]
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 y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∀ y ∈ K, ∀ (x : E), x ∉ (convexHull 𝕜) ↑y) ↔ ∀ (x : Finset E), x ∉ K

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 : ℕ
⊢ (∀ y ∈ K, ∀ (x : E), x ∉ (convexHull 𝕜) ↑y) ↔ ∀ (x : Finset E), x ∉ K
Tactic:
simp only [← Set.eq_empty_iff_forall_not_mem, convexHull_empty_iff, coe_eq_empty]
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 y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∀ y ∈ K, y = ∅) ↔ ∀ (x : Finset E), x ∉ K

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 : ℕ
⊢ (∀ y ∈ K, y = ∅) ↔ ∀ (x : Finset E), x ∉ K
Tactic:
exact forall₂_congr fun s hs ↦ iff_false_intro (K.nonempty hs).ne_empty
State after:
no goals