awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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 : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
pos : ∀ (hi : i ∈ fs), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
⊢ Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
have neg : ∀ (hi : i ∉ fs), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
Tactic: by_cases hi : i ∈ fs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ s.points j ∈ (s.face h).closedInterior ↔ j ∈ fs
have refine_1 : ∀ (hj : s.points j ∈ (s.face h).closedInterior), j ∈ fs
Tactic: refine ⟨fun hj ↦ ?_, fun hfs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
refine_1 : ∀ (hj : s.points j ∈ (s.face h).closedInterior), j ∈ fs
⊢ s.points j ∈ (s.face h).closedInterior ↔ j ∈ fs
have refine_2 : ∀ (hfs : j ∈ fs), s.points j ∈ (s.face h).closedInterior
Tactic: refine ⟨fun hj ↦ ?_, fun hfs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
hj : s.points j ∈ (s.face h).closedInterior
⊢ j ∈ fs
have refine_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)
Tactic: suffices s.points j ∈ affineSpan k (s.points '' fs) by simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
hj : s.points j ∈ (s.face h).closedInterior
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)
have refine_1 : ∀ (w : Fin (m + 1) → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1)
  (hw' : ∀ (i : Fin (m + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i))
  (hs : (affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w = s.points j),
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)
Tactic: obtain ⟨w, hw, hw', hs⟩ := hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hw' : ∀ (i : Fin (m + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hs : (affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w = s.points j
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)
have refine_1 : Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1)))))
  ((affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w : P)
Tactic: rw [← hs]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ s.points j ∈ (s.face h).closedInterior
have 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
Tactic: obtain ⟨i, rfl⟩ : ∃ i, fs.orderEmbOfFin h i = j := range_orderEmbOfFin fs h |>.ge hfs
Cleared hypotheses: j, hfs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ (s.face h).closedInterior ⊂ s.closedInterior
have obtain : ∀ (a : Fin (n + 1)) (ha : a ∉ fs), (s.face h).closedInterior ⊂ s.closedInterior
Tactic: obtain ⟨a, ha⟩ := Classical.not_forall.mp <| Finset.eq_univ_iff_forall.not.mp hfs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ (s.face h).closedInterior ⊂ s.closedInterior
have apply : ∃ x ∈ s.closedInterior, x ∉ (s.face h).closedInterior
Tactic: apply (Set.ssubset_iff_of_subset (s.closedInterior_face_subset_closedInterior h)).mpr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
have refine : ∀ (p : P) (hleft : p ∈ s.interior) (hright : p ∈ (s.face h).closedInterior), False
Tactic: refine Set.disjoint_left.mpr fun p hleft hright ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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
⊢ False
have hp : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ s.closedInterior = s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior
have h₁ : s.closedInterior ⊆ s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ s.closedInterior = s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior
have h₂ : s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊆ s.closedInterior
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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 ∈ s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior
have hp' : p ∈ (↑(affineSpan k (Set.range s.points)) : Set P)
Tactic: obtain hp' := Set.mem_of_mem_of_subset hp s.closedInterior_subset_affineSpan
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ p ∈ s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior
have 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)
Tactic: obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp'
Cleared hypotheses: p, hp, hp'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Set.mem_union, or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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)
have hp₁ : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
Tactic: rw [affineCombination_mem_closedInterior_iff hw1] at hp
Cleared hypotheses: hp, hp', h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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
⊢ 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)
have h₁ : ¬∀ (i : Fin (n + 1)), 0 < w i ∧ w i < 1
Tactic: simp_rw [affineCombination_mem_interior_iff hw1, Set.mem_Ioo] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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
⊢ 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)
have h₁ : ∃ (i : Fin (n + 1)), w i ≤ 0 ∨ 1 ≤ w i
Tactic: push +distrib Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ ∃ (j : Fin (n + 1)), w j = 0
have inl : ∀ (i : Fin (n + 1)) (hi : w i ≤ 0), ∃ (j : Fin (n + 1)), w j = 0
Tactic: obtain ⟨i, hi | hi⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ ∃ (j : Fin (n + 1)), w j = 0
have inr : ∀ (i : Fin (n + 1)) (hi : 1 ≤ w i), ∃ (j : Fin (n + 1)), w j = 0
Tactic: obtain ⟨i, hi | hi⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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
⊢ ∃ (j : Fin (n + 1)), w j = 0
have hi1 : w i = 1
Tactic: have hi1 : w i = 1 := le_antisymm (hp i).2 hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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
⊢ ∃ (j : Fin (n + 1)), w j = 0
have hw1₁ : ∀ 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
Cleared hypotheses: hw1, hi, hi1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ 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)
have h₁ : ∀ (j : Fin (n + 1)) (hj : w j = 0),
  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)
Tactic: obtain ⟨j, hj⟩ : ∃ j : Fin (n + 1), w j = 0 := by
      obtain ⟨i, hi | hi⟩ := h
      · exact ⟨i, le_antisymm hi (hp i).1⟩
      · have hi1 : w i = 1 := le_antisymm (hp i).2 hi
        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
        exact ⟨i + 1, hw1 _ (by simp)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
j : Fin (n + 1)
hj : w j = 0
⊢ 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)
have h₁ : Membership.mem (α := P) (s.faceOpposite j).closedInterior
  ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
Tactic: refine Set.mem_iUnion.mpr ⟨j, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
j : Fin (n + 1)
hj : w j = 0
⊢ Membership.mem (α := P) (s.faceOpposite j).closedInterior
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have h₁ : (∀ (i : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) {j}ᶜ i → Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧
  ∀ i ∉ {j}ᶜ, w i = 0
Tactic: rw [faceOpposite, affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ hw1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊆ s.closedInterior
have h₂ : ∀ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊆ s.closedInterior
Tactic: refine Set.union_subset s.interior_subset_closedInterior (Set.iUnion_subset fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' t)) s.centroid
⊢ False
have hssubset : t ⊂ Set.univ
Tactic: have hssubset : t ⊂ Set.univ := by grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' t)) s.centroid
hssubset : t ⊂ Set.univ
⊢ False
have obtain : ∀ (i : Fin (n + 1)) (hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t), False
Tactic: obtain ⟨i, hi⟩ := Set.exists_of_ssubset hssubset