awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
        (-(SignType.sign : (a : R) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) : SignType) ∨
      Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) (0 : R) ∨ w i = 0 ↔
    w i ≤ 0

Tactic:
simp [sign_eq_neg_one_iff, le_iff_eq_or_lt, or_comm]

Premises used: le_iff_eq_or_lt, or_comm, sign_eq_neg_one_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  WOppSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    w i ≤ 0
rw₁ rw₂ : w i ≤ 0 ↔ w i ≤ 0
⊢ WOppSide (affineSpan R (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) (s.points i) ↔
    w i ≤ 0

Tactic:
rw [wOppSide_comm, s.wOppSide_affineSpan_faceOpposite_point_left_iff hw]

Premises used: Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff, AffineSubspace.wOppSide_comm
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
s : Finset ι
hs : s ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
⊢ (∃ (v : ι), s = {v}) ∨ ∃ x ∈ G.edgeSet, x.toFinset = s

Tactic:
simp only [Set.mem_union, Set.mem_setOf_eq, Set.mem_image] at hs

Premises used: Set.mem_union, Set.mem_image, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
s : Finset ι
hs : (∃ (v : ι), s = {v}) ∨ ∃ x ∈ G.edgeSet, x.toFinset = s
inl :
  ∀ (v : ι),
    Finset.Nonempty (α := ι) {v} ∧
      ∀ ⦃b : Finset ι⦄, b ≤ {v} → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
inr :
  ∀ (e : Sym2 ι) (he : e ∈ G.edgeSet),
    e.toFinset.Nonempty ∧
      ∀ ⦃b : Finset ι⦄,
        b ≤ e.toFinset → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
⊢ s.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ s → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
rcases hs with ⟨v, rfl⟩ | ⟨e, he, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
v : ι
⊢ Finset.Nonempty (α := ι) {v} ∧
    ∀ ⦃b : Finset ι⦄, b ≤ {v} → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
inr : e.toFinset.Nonempty
inr₁ :
  ∀ ⦃b : Finset ι⦄, b ≤ e.toFinset → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
⊢ e.toFinset.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ e.toFinset → b.Nonempty → b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
⊢ e.toFinset.Nonempty

Tactic:
Finset.nonempty_iff_ne_empty.mpr (Sym2.toFinset_ne_empty e)

Premises used: Iff.mpr, Finset.nonempty_iff_ne_empty, Sym2.toFinset_ne_empty
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
⊢ e.toFinset.Nonempty

Tactic:
exact Finset.nonempty_iff_ne_empty.mpr (Sym2.toFinset_ne_empty e)

Premises used: Iff.mpr, Finset.nonempty_iff_ne_empty, Sym2.toFinset_ne_empty
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
b : Finset ι
hb_sub : b ≤ e.toFinset
hb_nonempty : b.Nonempty
pos : ∀ (h : #b = 1), b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
neg : ∀ (h : ¬#b = 1), b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet
⊢ b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
by_cases h : b.card = 1

Premises used: Finset.card
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
b : Finset ι
hb_sub : b ≤ e.toFinset
hb_nonempty : b.Nonempty
h : #b = 1
⊢ b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
grind [Finset.card_eq_one, Finset.eq_of_subset_of_card_le hb_sub, Sym2.card_toFinset]

Premises used: Finset.card_eq_one, Sym2.card_toFinset, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
e : Sym2 ι
he : e ∈ G.edgeSet
b : Finset ι
hb_sub : b ≤ e.toFinset
hb_nonempty : b.Nonempty
h : ¬#b = 1
⊢ b ∈ {s : Finset ι | ∃ (v : ι), s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
grind [Finset.card_eq_one, Finset.eq_of_subset_of_card_le hb_sub, Sym2.card_toFinset]

Premises used: Finset.card_eq_one, Sym2.card_toFinset, Finset.eq_of_subset_of_card_le
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
v : ι
⊢ (∃ (v_1 : ι), Eq (α := Finset ι) {v} {v_1}) ∨ ∃ x ∈ G.edgeSet, x.toFinset = {v}

Tactic:
Or.inl ⟨v, rfl⟩

Premises used: Exists.intro, Or.inl, rfl
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
ι : Type u_1
inst : DecidableEq ι
G : SimpleGraph ι
v : ι
⊢ (∃ (v_1 : ι), Eq (α := Finset ι) {v} {v_1}) ∨ ∃ x ∈ G.edgeSet, x.toFinset = {v}

Tactic:
exact Or.inl ⟨v, rfl⟩

Premises used: Or.inl
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
a :
  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)
⊢ 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)

Tactic:
apply subset_of_eq

Premises used: subset_of_eq
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
a : AffineIndependent 𝕜 (P := E) (ι := ↥(s ∪ t)) (Subtype.val (p := fun (x : E) ↦ x ∈ s ∪ t))
a₁ : s ⊆ s ∪ t
a₂ : t ⊆ s ∪ t
⊢ 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)

Tactic:
rw [AffineIndependent.convexHull_inter (R := 𝕜) (s := s ∪ t)]

Premises used: AffineIndependent.convexHull_inter
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
a : (↑(s ∪ t) : Set E) ⊆ ⋃ s ∈ abstract.faces, (↑s : Set E)
⊢ AffineIndependent 𝕜 (P := E) (ι := ↥(s ∪ t)) (Subtype.val (p := fun (x : E) ↦ x ∈ s ∪ t))

Tactic:
apply indep.mono

Premises used: AffineIndependent.mono
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
a : (↑s : Set E) ∪ (↑t : Set E) ⊆ ⋃ s ∈ abstract.faces, (↑s : Set E)
⊢ (↑(s ∪ t) : Set E) ⊆ ⋃ s ∈ abstract.faces, (↑s : Set E)

Tactic:
simp only [Finset.coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ (↑s : Set E) ∪ (↑t : Set E) ⊆ ⋃ s ∈ abstract.faces, (↑s : Set E)

Tactic:
Set.union_subset (Set.subset_biUnion_of_mem hs) (Set.subset_biUnion_of_mem ht)

Premises used: Set.subset_biUnion_of_mem, Set.union_subset
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ (↑s : Set E) ∪ (↑t : Set E) ⊆ ⋃ s ∈ abstract.faces, (↑s : Set E)

Tactic:
exact Set.union_subset (Set.subset_biUnion_of_mem hs) (Set.subset_biUnion_of_mem ht)

Premises used: Set.subset_biUnion_of_mem, Set.union_subset
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ s ⊆ s ∪ t

Tactic:
Finset.subset_union_left

Premises used: Finset.subset_union_left
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ s ⊆ s ∪ t

Tactic:
exact Finset.subset_union_left

Premises used: Finset.subset_union_left
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ t ⊆ s ∪ t

Tactic:
Finset.subset_union_right

Premises used: Finset.subset_union_right
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DecidableEq E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep :
  AffineIndependent 𝕜 (P := E) (ι := { x : E // Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x })
    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (⋃ s ∈ abstract.faces, (↑s : Set E)) x))
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ t ⊆ s ∪ t

Tactic:
exact Finset.subset_union_right

Premises used: Finset.subset_union_right
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq 𝕜
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
⊢ AffineIndependent 𝕜 (P := ι →₀ 𝕜) (ι :=
    { x : ι →₀ 𝕜 //
      Membership.mem (γ := Set (ι →₀ 𝕜))
        (⋃ (s : Finset (ι →₀ 𝕜)),
          ⋃ (_ :
            Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
              (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
            (↑s : Set (ι →₀ 𝕜)))
        x })
    (Subtype.val (p := fun (x : ι →₀ 𝕜) ↦
      Membership.mem (γ := Set (ι →₀ 𝕜))
        (⋃ (s : Finset (ι →₀ 𝕜)),
          ⋃ (_ :
            Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
              (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
            (↑s : Set (ι →₀ 𝕜)))
        x))

Tactic:
(Finsupp.linearIndependent_single_one 𝕜 ι).affineIndependent.range.mono fun x hx => ?_

Premises used: AffineIndependent.mono, LinearIndependent.affineIndependent, AffineIndependent.range, Finsupp.linearIndependent_single_one
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq 𝕜
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
refine :
  ∀ (x : ι →₀ 𝕜)
    (hx :
      Membership.mem (γ := Set (ι →₀ 𝕜))
        (⋃ (s : Finset (ι →₀ 𝕜)),
          ⋃ (_ :
            Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
              (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
            (↑s : Set (ι →₀ 𝕜)))
        x),
    Membership.mem (γ := Set (ι →₀ 𝕜)) (Set.range fun (i : ι) ↦ Finsupp.single i 1) x
⊢ AffineIndependent 𝕜 (P := ι →₀ 𝕜) (ι :=
    { x : ι →₀ 𝕜 //
      Membership.mem (γ := Set (ι →₀ 𝕜))
        (⋃ (s : Finset (ι →₀ 𝕜)),
          ⋃ (_ :
            Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
              (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
            (↑s : Set (ι →₀ 𝕜)))
        x })
    (Subtype.val (p := fun (x : ι →₀ 𝕜) ↦
      Membership.mem (γ := Set (ι →₀ 𝕜))
        (⋃ (s : Finset (ι →₀ 𝕜)),
          ⋃ (_ :
            Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
              (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
            (↑s : Set (ι →₀ 𝕜)))
        x))

Tactic:
refine (Finsupp.linearIndependent_single_one 𝕜 ι).affineIndependent.range.mono fun x hx => ?_

Premises used: AffineIndependent.mono, LinearIndependent.affineIndependent, AffineIndependent.range, Finsupp.linearIndependent_single_one
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq 𝕜
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
x : ι →₀ 𝕜
hx :
  Membership.mem (γ := Set (ι →₀ 𝕜))
    (⋃ (s : Finset (ι →₀ 𝕜)),
      ⋃ (_ :
        Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
          (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) s),
        (↑s : Set (ι →₀ 𝕜)))
    x
⊢ ∃ (i : Finset (ι →₀ 𝕜)) (_ :
    Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
      (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) i),
    x ∈ i

Tactic:
simp only [Set.mem_iUnion, Finset.mem_coe] at hx

Premises used: Set.mem_iUnion, Finset.mem_coe
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq 𝕜
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
x : ι →₀ 𝕜
hx :
  ∃ (i : Finset (ι →₀ 𝕜)) (_ :
    Membership.mem (γ := Set (Finset (ι →₀ 𝕜)))
      (PreAbstractSimplicialComplex.faces (abstract.map fun (i : ι) ↦ Finsupp.single i 1)) i),
    x ∈ i
obtain :
  ∀ w ∈ abstract.faces,
    ∀
      (hx :
        Membership.mem (γ := Finset (ι →₀ 𝕜))
          ((fun (s : Finset ι) ↦ (Finset.image (fun (i : ι) ↦ Finsupp.single i 1) s : Finset (ι →₀ 𝕜))) w) x),
      Membership.mem (γ := Set (ι →₀ 𝕜)) (Set.range fun (i : ι) ↦ Finsupp.single i 1) x
⊢ Membership.mem (γ := Set (ι →₀ 𝕜)) (Set.range fun (i : ι) ↦ Finsupp.single i 1) x

Tactic:
obtain ⟨_, ⟨_, _, rfl⟩, hx⟩ := hx

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : DecidableEq 𝕜
inst_2 : Field 𝕜
inst_3 : LinearOrder 𝕜
inst_4 : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
x : ι →₀ 𝕜
w : Finset ι
left : w ∈ abstract.faces
hx :
  Membership.mem (γ := Finset (ι →₀ 𝕜))
    ((fun (s : Finset ι) ↦ (Finset.image (fun (i : ι) ↦ Finsupp.single i 1) s : Finset (ι →₀ 𝕜))) w) x
⊢ Membership.mem (γ := Set (ι →₀ 𝕜)) (Set.range fun (i : ι) ↦ Finsupp.single i 1) x

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 : Finset E
hs : s ∈ K.faces
⊢ s.Nonempty

Tactic:
K.isRelLowerSet_faces hs |>.1

Premises used: Geometry.SimplicialComplex.toPreAbstractSimplicialComplex, And.left, PreAbstractSimplicialComplex.isRelLowerSet_faces
-- 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 : ∅ ∈ K.faces
⊢ False

Tactic:
simpa using nonempty_of_mem_faces h

Premises used: Geometry.SimplicialComplex.nonempty_of_mem_faces
-- 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.space ↔ ∃ s ∈ K.faces, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E) x

Tactic:
simp [space]

Premises used: Geometry.SimplicialComplex.space
-- 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
⊢ Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
    (⋃ x ∈ K.faces, (convexHull 𝕜 : (a : Set E) → Set E) (↑x : Set E) : Set E)

Tactic:
subset_biUnion_of_mem hs

Premises used: Set.subset_biUnion_of_mem
-- 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
h :
  Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
⊢ (convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) ⊆ K.space

Tactic:
convert! subset_biUnion_of_mem hs

Premises used: Set.subset_biUnion_of_mem
-- 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
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑s : Set E) : Set E)

Tactic:
rfl
-- 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 : Set E) ⊆ K.space

Tactic:
(subset_convexHull 𝕜 _).trans <| convexHull_subset_space hs

Premises used: Geometry.SimplicialComplex.convexHull_subset_space, subset_convexHull, HasSubset.Subset.trans
-- 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
⊢ 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)

Tactic:
(K.inter_subset_convexHull hs ht).antisymm <|
    subset_inter (convexHull_mono Set.inter_subset_left) <|
      convexHull_mono Set.inter_subset_right

Premises used: Geometry.SimplicialComplex.inter_subset_convexHull, Set.inter_subset_left, convexHull_mono, Set.subset_inter, HasSubset.Subset.antisymm, Set.inter_subset_right
-- 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
hst : t ⊆ s
ht : t.Nonempty
⊢ t ∈ K.faces

Tactic:
(K.isRelLowerSet_faces hs).2 hst ht

Premises used: Geometry.SimplicialComplex.toPreAbstractSimplicialComplex, And.right, PreAbstractSimplicialComplex.isRelLowerSet_faces