awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
hfs : j ∈ fs
⊢ ∃ (i : Fin (m + 1)), (fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i = j

Tactic:
range_orderEmbOfFin fs h |>.ge hfs

Premises used: Eq.ge, Set.Mem, setOf, Finset.range_orderEmbOfFin, Set.range
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
hfs : j ∈ fs
refine_2 :
  ∀ (i : Fin (m + 1))
    (hfs :
      Membership.mem (α := Fin (n + 1)) fs ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i : Fin (n + 1))),
    s.points ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i) ∈ (s.face h).closedInterior
⊢ s.points j ∈ (s.face h).closedInterior

Tactic:
obtain ⟨i, rfl⟩ : ∃ i, fs.orderEmbOfFin h i = j := range_orderEmbOfFin fs h |>.ge hfs

Premises used: Eq.ge, Finset.range_orderEmbOfFin, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (m + 1)
hfs : Membership.mem (α := Fin (n + 1)) fs ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i : Fin (n + 1))
⊢ s.points ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i) ∈ (s.face h).closedInterior

Tactic:
point_mem_closedInterior _ _

Premises used: Set.Mem, Affine.Simplex.point_mem_closedInterior
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (m + 1)
hfs : Membership.mem (α := Fin (n + 1)) fs ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i : Fin (n + 1))
⊢ s.points ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i) ∈ (s.face h).closedInterior

Tactic:
exact point_mem_closedInterior _ _

Premises used: Affine.Simplex.point_mem_closedInterior
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
obtain : ∀ (a : Fin (n + 1)) (ha : a ∉ fs), (s.face h).closedInterior ⊂ s.closedInterior
⊢ (s.face h).closedInterior ⊂ s.closedInterior

Tactic:
obtain ⟨a, ha⟩ := Classical.not_forall.mp <| Finset.eq_univ_iff_forall.not.mp hfs

Premises used: Finset.eq_univ_iff_forall, Iff.not, Iff.mp, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
a : Fin (n + 1)
ha : a ∉ fs
apply : ∃ x ∈ s.closedInterior, x ∉ (s.face h).closedInterior
⊢ (s.face h).closedInterior ⊂ s.closedInterior

Tactic:
apply (Set.ssubset_iff_of_subset (s.closedInterior_face_subset_closedInterior h)).mpr

Premises used: Iff.mpr, Affine.Simplex.closedInterior_face_subset_closedInterior, Set.ssubset_iff_of_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
a : Fin (n + 1)
ha : a ∉ fs
hs : s.points a ∈ (s.face h).closedInterior
⊢ a ∈ fs

Tactic:
simpa using hs
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
a : Fin (n + 1)
ha : a ∉ fs
⊢ ∃ x ∈ s.closedInterior, x ∉ (s.face h).closedInterior

Tactic:
exact ⟨s.points a, s.point_mem_closedInterior a, fun hs ↦ ha (by simpa using hs)⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
⊢ Disjoint s.interior (s.face h).closedInterior

Tactic:
Set.disjoint_left.mpr fun p hleft hright ↦ ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
refine : ∀ (p : P) (hleft : p ∈ s.interior) (hright : p ∈ (s.face h).closedInterior), False
⊢ Disjoint s.interior (s.face h).closedInterior

Tactic:
refine Set.disjoint_left.mpr fun p hleft hright ↦ ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
p : P
hleft : p ∈ s.interior
hright : p ∈ (s.face h).closedInterior
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) p

Tactic:
have hp : p ∈ affineSpan k (Set.range s.points) :=
    Set.mem_of_mem_of_subset hleft <| s.interior_subset_closedInterior.trans <|
      s.closedInterior_subset_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
hfs : fs ≠ univ
m : ℕ
h : #fs = m + 1
p : P
hleft : p ∈ s.interior
hright : p ∈ (s.face h).closedInterior
hp : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) p
⊢ False

Tactic:
grind [affineCombination_mem_interior_iff, affineCombination_mem_closedInterior_face_iff_mem_Icc,
    eq_affineCombination_of_mem_affineSpan_of_fintype]

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype, Affine.Simplex.affineCombination_mem_interior_iff, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
i j : Fin (n + 1)
⊢ s.points j ∈ (s.faceOpposite i).closedInterior ↔ j ≠ i

Tactic:
simp [faceOpposite]

Premises used: Affine.Simplex.faceOpposite
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
inst_6 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ (s.faceOpposite i).closedInterior ⊆ s.closedInterior

Tactic:
s.closedInterior_face_subset_closedInterior _

Premises used: Affine.Simplex.closedInterior_face_subset_closedInterior, Affine.Simplex.faceOpposite
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ Ne (α := Finset (Fin (n + 1))) {i}ᶜ univ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
h₁ : s.closedInterior ⊆ s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior
h₂ : s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊆ s.closedInterior
⊢ s.closedInterior = s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior

Tactic:
apply Set.Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
p : P
hp : p ∈ s.closedInterior
⊢ p ∈ (↑(affineSpan k (Set.range s.points)) : Set P)

Tactic:
obtain hp' := Set.mem_of_mem_of_subset hp s.closedInterior_subset_affineSpan

Premises used: Set.mem_of_mem_of_subset, Affine.Simplex.closedInterior_subset_affineSpan
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
p : P
hp : p ∈ s.closedInterior
hp' : p ∈ (↑(affineSpan k (Set.range s.points)) : Set P)
h₁ :
  ∀ (w : Fin (n + 1) → k) (hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1)
    (hp :
      Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P))
    (hp' :
      Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
        ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)),
    Membership.mem (α := P) (s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior)
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ p ∈ s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior

Tactic:
obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp'

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h₁ :
  ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ∉ s.interior →
    Membership.mem.{u_4, u_4} (α := P) (γ := Set P) (⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior)
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
rw [Set.mem_union, or_iff_not_imp_left]

Premises used: Set.mem_union, Classical.or_iff_not_imp_left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h : ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ∉ s.interior
⊢ ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)

Tactic:
rw [affineCombination_mem_closedInterior_iff hw1] at hp

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h : ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ∉ s.interior
hp₁ : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
⊢ Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
rw [affineCombination_mem_closedInterior_iff hw1] at hp

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h : ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ∉ s.interior
hp₁ : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp'₁ :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ∉ s.interior

Tactic:
rw [affineCombination_mem_closedInterior_iff hw1] at hp

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h : ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ∉ s.interior
⊢ ¬∀ (i : Fin (n + 1)), 0 < w i ∧ w i < 1

Tactic:
simp_rw [affineCombination_mem_interior_iff hw1, Set.mem_Ioo] at h

Premises used: Set.mem_Ioo, Affine.Simplex.affineCombination_mem_interior_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h : ¬∀ (i : Fin (n + 1)), 0 < w i ∧ w i < 1
⊢ ∃ (i : Fin (n + 1)), w i ≤ 0 ∨ 1 ≤ w i

Tactic:
push +distrib Not at h

Premises used: Not
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
h : ∃ (i : Fin (n + 1)), w i ≤ 0 ∨ 1 ≤ w i
inl : ∀ (i : Fin (n + 1)) (hi : w i ≤ 0), ∃ (j : Fin (n + 1)), w j = 0
inr : ∀ (i : Fin (n + 1)) (hi : 1 ≤ w i), ∃ (j : Fin (n + 1)), w j = 0
⊢ ∃ (j : Fin (n + 1)), w j = 0

Tactic:
obtain ⟨i, hi | hi⟩ := h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hi : w i ≤ 0
⊢ ∃ (j : Fin (n + 1)), w j = 0

Tactic:
⟨i, le_antisymm hi (hp i).1⟩

Premises used: le_antisymm, And.left, Exists.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hi : w i ≤ 0
⊢ ∃ (j : Fin (n + 1)), w j = 0

Tactic:
exact ⟨i, le_antisymm hi (hp i).1⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hi : 1 ≤ w i
⊢ w i = 1

Tactic:
have hi1 : w i = 1 := le_antisymm (hp i).2 hi
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hw1 : ∑ i : Fin (n + 1), w i = w i
hi : 1 ≤ w i
hi1 : w i = 1
⊢ Membership.mem (γ := Finset (Fin (n + 1))) univ i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hi : 1 ≤ w i
hi1 : w i = 1
⊢ ∀ i_1 ∈ erase univ i, w i_1 = 0

Tactic:
rw [← hi1, ← Finset.sum_erase_add _ _ (show i ∈ Finset.univ by simp), add_eq_right,
          Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)] at hw1

Premises used: Finset.sum_eq_zero_iff_of_nonneg, Finset.sum_erase_add, And.left, add_eq_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hi : 1 ≤ w i
hi1 : w i = 1
hw1₁ : ∀ i_1 ∈ erase univ i, w i_1 = 0
⊢ 1 ≤ w i

Tactic:
rw [← hi1, ← Finset.sum_erase_add _ _ (show i ∈ Finset.univ by simp), add_eq_right,
          Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)] at hw1

Premises used: Finset.sum_eq_zero_iff_of_nonneg, Finset.sum_erase_add, And.left, add_eq_right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hp' :
  Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hi : 1 ≤ w i
hi1 : w i = 1
hw1₁ : ∀ i_1 ∈ erase univ i, w i_1 = 0
hi₁ : 1 ≤ w i
⊢ w i = 1

Tactic:
rw [← hi1, ← Finset.sum_erase_add _ _ (show i ∈ Finset.univ by simp), add_eq_right,
          Finset.sum_eq_zero_iff_of_nonneg (fun j _ ↦ (hp j).1)] at hw1

Premises used: Finset.sum_eq_zero_iff_of_nonneg, Finset.sum_erase_add, And.left, add_eq_right