awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
by_contra! :
  ∀
    (h :
      ¬Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∧
        ∀ (u : Finset E) (_ : u ∈ K.faces),
          Ne (α := Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) :
              Set E)
            ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)),
    False
⊢ Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∨
    ∃ u ∈ K.faces,
      Eq (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  ¬Disjoint (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
⊢ Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)

Tactic:
rw [not_disjoint_iff_nonempty_inter] at h

Premises used: Set.not_disjoint_iff_nonempty_inter
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
⊢ False

Tactic:
h.2 (s ∩ t) (K.down_closed hs inter_subset_left ?_) ?_

Premises used: Geometry.SimplicialComplex.down_closed, Inter.inter, And.right, Finset.inter_subset_left
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
refine_1 : (s ∩ t).Nonempty
refine_2 :
  Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑(s ∩ t) : Set E) : Set E)
⊢ False

Tactic:
refine h.2 (s ∩ t) (K.down_closed hs inter_subset_left ?_) ?_

Premises used: Geometry.SimplicialComplex.down_closed, Inter.inter, And.right, Finset.inter_subset_left
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
⊢ (s ∩ t).Nonempty

Tactic:
simpa [← coe_inter] using convexHull_nonempty_iff.1 (h.1.mono (K.inter_subset_convexHull hs ht))

Premises used: Geometry.SimplicialComplex.inter_subset_convexHull, Set.Nonempty.mono, And.left, Iff.mp, convexHull_nonempty_iff, Finset.coe_inter
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
h :
  Set.Nonempty.{u_2} (α := E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) ∧
    ∀ (u : Finset E) (_ : u ∈ K.faces),
      Ne (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑u : Set E) : Set E)
refine_2 :
  Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
refine_2₁ refine_2₂ :
  Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
⊢ Eq (α := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑(s ∩ t) : Set E) : Set E)

Tactic:
rw [coe_inter, convexHull_inter_convexHull hs ht]

Premises used: Geometry.SimplicialComplex.convexHull_inter_convexHull, Finset.coe_inter
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
faces : Set (Finset E)
indep : ∀ s ∈ faces, AffineIndependent 𝕜 (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
down_closed : IsLowerSet faces
inter_subset_convexHull :
  ∀ s ∈ faces,
    ∀ t ∈ faces,
      Subset (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
⊢ faces \ {∅} = {f : Finset E | f ∈ faces ∧ f.Nonempty}

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
faces : Set (Finset E)
indep : ∀ s ∈ faces, AffineIndependent 𝕜 (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
down_closed : IsLowerSet faces
inter_subset_convexHull :
  ∀ s ∈ faces,
    ∀ t ∈ faces,
      Subset (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
⊢ faces \ {∅} = {f : Finset E | f ∈ faces ∧ f.Nonempty}

Tactic:
have : faces \ {∅} = {f ∈ faces | f.Nonempty} := by grind
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
faces : Set (Finset E)
indep : ∀ s ∈ faces, AffineIndependent 𝕜 (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
down_closed : IsLowerSet faces
inter_subset_convexHull :
  ∀ s ∈ faces,
    ∀ t ∈ faces,
      Subset (α := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ∩ (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) ((↑s : Set E) ∩ (↑t : Set E)) : Set E)
this : faces \ {∅} = {f : Finset E | f ∈ faces ∧ f.Nonempty}
⊢ IsRelLowerSet (faces \ {∅}) Finset.Nonempty

Tactic:
simpa only [this] using down_closed.isRelLowerSet_sep Finset.Nonempty

Premises used: IsLowerSet.isRelLowerSet_sep, Finset.Nonempty
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
⊢ x ∈ K.vertices ↔ {x} ∈ K.faces

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Geometry.SimplicialComplex.vertices
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
h : ∀ (x : E), x ∈ K.vertices ↔ Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x
⊢ K.vertices = ⋃ k ∈ K.faces, (↑k : Set E)

Tactic:
ext x
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
⊢ x ∈ K.vertices ↔ Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x

Tactic:
⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun h => ?_⟩

Premises used: Iff.mpr, Finset.mem_singleton_self, Set.mem_biUnion, Iff.intro, Finset.mem_coe
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
h : ∀ (h : Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x), x ∈ K.vertices
⊢ x ∈ K.vertices ↔ Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x

Tactic:
refine ⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun h => ?_⟩
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
h : Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x
h₁ : ∀ (s : Finset E) (hs : s ∈ K.faces) (hx : x ∈ (↑s : Set E)), x ∈ K.vertices
⊢ x ∈ K.vertices

Tactic:
obtain ⟨s, hs, hx⟩ := mem_iUnion₂.1 h

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
h : Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x
s : Finset E
hs : s ∈ K.faces
hx : x ∈ (↑s : Set E)
⊢ x ∈ K.vertices

Tactic:
K.down_closed hs (Finset.singleton_subset_iff.2 <| mem_coe.1 hx) (singleton_nonempty _)

Premises used: Iff.mpr, Set.Mem, setOf, Finset.singleton_nonempty, Finset.singleton_subset_iff, Geometry.SimplicialComplex.down_closed, Iff.mp, Geometry.SimplicialComplex.vertices, Finset.mem_coe
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
h : Membership.mem (γ := Set E) (⋃ k ∈ K.faces, (↑k : Set E)) x
s : Finset E
hs : s ∈ K.faces
hx : x ∈ (↑s : Set E)
⊢ x ∈ K.vertices

Tactic:
exact K.down_closed hs (Finset.singleton_subset_iff.2 <| mem_coe.1 hx) (singleton_nonempty _)

Premises used: Iff.mpr, Finset.singleton_nonempty, Finset.singleton_subset_iff, Geometry.SimplicialComplex.down_closed, Iff.mp, Finset.mem_coe
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
⊢ K.vertices ⊆ K.space

Tactic:
vertices_eq.subset.trans <| iUnion₂_mono fun x _ => subset_convexHull 𝕜 (x : Set E)

Premises used: Geometry.SimplicialComplex.vertices_eq, subset_convexHull, HasSubset.Subset.trans, Eq.subset, Set.iUnion₂_mono, SetLike.coe
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x ↔ x ∈ s

Tactic:
⟨fun h => ?_, fun h => subset_convexHull 𝕜 _ h⟩

Premises used: subset_convexHull, SetLike.coe, Iff.intro
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
refine : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x), x ∈ s
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x ↔ x ∈ s

Tactic:
refine ⟨fun h => ?_, fun h => subset_convexHull 𝕜 _ h⟩
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑{x} : Set E) : Set E) x

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x

Tactic:
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x
by_contra : ∀ (H : ¬x ∈ s), False
⊢ x ∈ s

Tactic:
by_contra H
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h_1 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x
H : ¬x ∈ s
rwa :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑({x} ∩ s) : Set E) : Set E) x)
    (H : ¬x ∈ s), False
rwa₁ :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑∅ : Set E) : Set E) x) (H : ¬x ∈ s), False
rwa₂ : ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ∅ : Set E) x) (H : ¬x ∈ s), False
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : Membership.mem (γ := Set E) ∅ x) (H : ¬x ∈ s), False
⊢ False

Tactic:
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at h

Premises used: Iff.mpr, Finset.coe_empty, convexHull_empty, Finset.disjoint_iff_inter_eq_empty, Disjoint.symm, Iff.mp, Finset.disjoint_singleton_right, Finset.coe_inter
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x
have have₁ have₂ :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x),
    x ∈ s
have₃ :
  ∀ (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((↑{x} : Set E) ∩ (↑s : Set E)) : Set E) x)
    (H : ¬x ∈ s), False
⊢ x ∈ s

Tactic:
classical
  have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
  by_contra H
  rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
    coe_empty, convexHull_empty] at h

Premises used: Finset.coe_empty, convexHull_empty, Finset.coe_inter
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) ↔
    s ⊆ t

Tactic:
⟨fun h _ hxs =>
    (vertex_mem_convexHull_iff
          (K.down_closed hs (Finset.singleton_subset_iff.2 hxs) <| singleton_nonempty _) ht).1
      (h (subset_convexHull 𝕜 (E := E) s hxs)),
    convexHull_mono⟩

Premises used: Iff.mpr, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, subset_convexHull, Finset.singleton_nonempty, Finset.singleton_subset_iff, Geometry.SimplicialComplex.down_closed, convexHull_mono, SetLike.coe, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
⊢ s ∈ K.facets ↔ s ∈ K.faces ∧ ∀ t ∈ K.faces, s ⊆ t → s = t

Tactic:
mem_sep_iff

Premises used: Set.Mem, Geometry.SimplicialComplex.facets, Set.mem_sep_iff
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
⊢ K.facets ⊆ K.faces

Tactic:
fun _ hs => hs.1

Premises used: Set.Subset, And.left
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t

Tactic:
⟨fun hs' : ¬(_ ∧ _) => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
refine_1 : ∀ (hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)), ∃ t ∈ K.faces, s ⊂ t
refine_2 : (∃ t ∈ K.faces, s ⊂ t) → s ∉ K.facets
⊢ s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t

Tactic:
refine ⟨fun hs' : ¬(_ ∧ _) => ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : ¬(s ∈ K.faces ∧ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t)
⊢ ∀ (_ : s ∈ K.faces), ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t

Tactic:
push Not at hs'

Premises used: Not
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : ∀ (_ : s ∈ K.faces), ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
refine_1 : ∀ (t : Finset E) (ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t), ∃ t ∈ K.faces, s ⊂ t
⊢ ∃ t ∈ K.faces, s ⊂ t

Tactic:
obtain ⟨t, ht⟩ := hs' hs
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : ∀ (_ : s ∈ K.faces), ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
t : Finset E
ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t ∈ K.faces, s ⊂ t

Tactic:
⟨t, ht.1, ⟨ht.2.1, fun hts => ht.2.2 (Subset.antisymm ht.2.1 hts)⟩⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Finset.Subset.antisymm
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
hs' : ∀ (_ : s ∈ K.faces), ∃ t ∈ K.faces, s ⊆ t ∧ s ≠ t
t : Finset E
ht : t ∈ K.faces ∧ s ⊆ t ∧ s ≠ t
⊢ ∃ t ∈ K.faces, s ⊂ t

Tactic:
exact ⟨t, ht.1, ⟨ht.2.1, fun hts => ht.2.2 (Subset.antisymm ht.2.1 hts)⟩⟩
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs_1 : 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
⊢ s = t

Tactic:
have := hs' ht.1 ht.2.1
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs_1 : 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
⊢ t ∈ K.faces ∧ t ⊂ t

Tactic:
rw [this] at ht
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs_1 : 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
ht₁ : t ∈ K.faces ∧ t ⊂ t
⊢ s ∈ K.faces

Tactic:
rw [this] at ht
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs_1 : 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
ht₁ : t ∈ K.faces ∧ t ⊂ t
hs₁ : s ∈ K.faces
⊢ ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t

Tactic:
rw [this] at ht
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs_1 : 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
ht₁ : t ∈ K.faces ∧ t ⊂ t
hs₁ : s ∈ K.faces
hs'₁ : ∀ ⦃t : Finset E⦄, t ∈ K.faces → s ⊆ t → s = t
⊢ s = t

Tactic:
rw [this] at ht
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs_1 : 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

Tactic:
ht.2.2 (Subset.refl t)

Premises used: Finset.Subset.refl, And.right