Theorem: Geometry.SimplicialComplex.facets_eq_empty_iff (LeanCamCombi/Mathlib/Analysis/Convex/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.facets = ∅ ↔ K = ⊥
Tactic:
refine' ⟨fun h => _, _⟩
State after:
case refine'_1
𝕜 : 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
h : K.facets = ∅
⊢ K = ⊥

case refine'_2
𝕜 : 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 = ⊥ → K.facets = ∅

State before:
case refine'_1
𝕜 : 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
h : K.facets = ∅
⊢ K = ⊥
Tactic:
ext s
State after:
case refine'_1.faces.h
𝕜 : 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
h : K.facets = ∅
s : Finset E
⊢ s ∈ K.faces ↔ s ∈ ⊥.faces

State before:
case refine'_1.faces.h
𝕜 : 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
h : K.facets = ∅
s : Finset E
⊢ s ∈ K.faces ↔ s ∈ ⊥.faces
Tactic:
refine' iff_of_false (fun hs => _) (Set.not_mem_empty _)
State after:
case refine'_1.faces.h
𝕜 : 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
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
⊢ False

State before:
case refine'_1.faces.h
𝕜 : 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
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
⊢ False
Tactic:
obtain ⟨t, ht, -⟩ := subfacet hs
State after:
case refine'_1.faces.h.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
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ False

State before:
case refine'_1.faces.h.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
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ False
Tactic:
exact h.subset ht
State after:
no goals

State before:
case refine'_2
𝕜 : 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 = ⊥ → K.facets = ∅
Tactic:
rintro rfl
State after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
⊢ ⊥.facets = ∅

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
⊢ ⊥.facets = ∅
Tactic:
exact facets_bot
State after:
no goals