case refine'_1
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t

case refine'_2
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ (∃ t, t ∈ K.faces ∧ s ⊂ t) → ¬s ∈ facets K
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ ¬s ∈ facets K ↔ ∃ t, t ∈ K.faces ∧ s ⊂ t
refine' ⟨fun hs' : ¬(_ ∧ _) => _, _⟩
case refine'_1
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
hs' : s ∈ K.faces → Exists fun ⦃t⦄ => t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
case refine'_1
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
push_neg at hs'
case refine'_1.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs : s ∈ K.faces
hs' : s ∈ K.faces → Exists fun ⦃t⦄ => t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
t : Finset E
ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
case refine'_1
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
hs' : s ∈ K.faces → Exists fun ⦃t⦄ => t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
obtain ⟨t, ht⟩ := hs' hs
no goals
case refine'_1.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs : s ∈ K.faces
hs' : s ∈ K.faces → Exists fun ⦃t⦄ => t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
t : Finset E
ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t, t ∈ K.faces ∧ s ⊂ t
exact ⟨t, ht.1, ⟨ht.2.1, fun hts => ht.2.2 (Subset.antisymm ht.2.1 hts)⟩⟩
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
⊢ False
case refine'_2
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hs : s ∈ K.faces
⊢ (∃ t, t ∈ K.faces ∧ s ⊂ t) → ¬s ∈ facets K
rintro ⟨t, ht⟩ ⟨hs, hs'⟩
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
⊢ False
have := hs' ht.1 ht.2.1
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ t ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ s ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
rw [this] at ht
no goals
case refine'_2.intro.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.69803
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t✝ : Finset E
x : E
hs✝ : s ∈ K.faces
t : Finset E
ht : t ∈ K.faces ∧ t ⊂ t
hs : s ∈ K.faces
hs' : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
this : s = t
⊢ False
exact ht.2.2 (Subset.refl t)