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 : 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_1 ∈ erase univ i, w i_1 = 0
hi : 1 ≤ w i
hi1 : w i = 1
⊢ i + 1 ∈ erase 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
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_1 ∈ erase univ i, w i_1 = 0
hi : 1 ≤ w i
hi1 : w i = 1
⊢ ∃ (j : Fin (n + 1)), w j = 0

Tactic:
exact ⟨i + 1, hw1 _ (by 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)
h : ∃ (i : Fin (n + 1)), w i ≤ 0 ∨ 1 ≤ w i
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)
⊢ 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)⟩

Premises used: HAdd.hAdd, OfNat.ofNat, Fin
-- 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
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:
Set.mem_iUnion.mpr ⟨j, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, 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)
h : ∃ (i : Fin (n + 1)), w i ≤ 0 ∨ 1 ≤ w i
j : Fin (n + 1)
hj : w j = 0
h₁ :
  Membership.mem (α := P) (s.faceOpposite j).closedInterior
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ 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:
refine Set.mem_iUnion.mpr ⟨j, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, 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)
h : ∃ (i : Fin (n + 1)), w i ≤ 0 ∨ 1 ≤ w i
j : Fin (n + 1)
hj : w j = 0
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
⊢ Membership.mem (α := P) (s.faceOpposite j).closedInterior
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
rw [faceOpposite, affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ hw1]

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc, 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 : 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
⊢ ∀ i ∉ {j}ᶜ, w i = 0

Tactic:
simpa using hj
-- 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
j : Fin (n + 1)
hj : w j = 0
⊢ (∀ (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:
exact ⟨fun k _ ↦ hp k, by simpa using hj⟩
-- 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
⊢ s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊆ s.closedInterior

Tactic:
Set.union_subset s.interior_subset_closedInterior (Set.iUnion_subset fun i ↦ ?_)

Premises used: Affine.Simplex.interior_subset_closedInterior, Set.iUnion_subset, Set.union_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 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
h₂ : ∀ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊆ s.closedInterior
⊢ s.interior ∪ ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior ⊆ s.closedInterior

Tactic:
refine Set.union_subset s.interior_subset_closedInterior (Set.iUnion_subset fun i ↦ ?_)

Premises used: Affine.Simplex.interior_subset_closedInterior, Set.iUnion_subset, Set.union_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 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ (s.faceOpposite i).closedInterior ⊆ s.closedInterior

Tactic:
s.closedInterior_faceOpposite_subset_closedInterior i

Premises used: Affine.Simplex.closedInterior_faceOpposite_subset_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 : LinearOrder k
inst_5 : IsOrderedAddMonoid k
inst_6 : ZeroLEOneClass k
n : ℕ
inst_7 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ (s.faceOpposite i).closedInterior ⊆ s.closedInterior

Tactic:
exact s.closedInterior_faceOpposite_subset_closedInterior i

Premises used: Affine.Simplex.closedInterior_faceOpposite_subset_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 : LinearOrder k
inst_5 : Nontrivial k
inst_6 : IsOrderedAddMonoid k
inst_7 : ZeroLEOneClass k
n : ℕ
inst_8 : NeZero n
s : Simplex k P n
⊢ s.closedInterior \ s.interior = ⋃ (i : Fin (n + 1)), (s.faceOpposite i).closedInterior

Tactic:
simpa [closedInterior_eq_interior_union] using
    fun i ↦ (s.disjoint_interior_closedInterior_faceOpposite i).symm

Premises used: Affine.Simplex.closedInterior_eq_interior_union, Affine.Simplex.disjoint_interior_closedInterior_faceOpposite, Disjoint.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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 : ℕ
s : Simplex k P n
⊢ Finset.centroid k univ s.points = s.centroid

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
inst_4 : CharZero k
n : ℕ
s : Simplex k P n
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) s.centroid

Tactic:
centroid_mem_affineSpan_of_card_eq_add_one k _ (card_fin (n + 1))

Premises used: Set.Mem, HAdd.hAdd, Finset.card_fin, centroid_mem_affineSpan_of_card_eq_add_one, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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 : ℕ
s : Simplex k P n
⊢ s.centroid = (affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeights k univ)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
⊢ t ⊂ Set.univ

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
⊢ t ⊂ Set.univ

Tactic:
have hssubset : t ⊂ Set.univ := by grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
obtain : ∀ (i : Fin (n + 1)) (hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t), False
⊢ False

Tactic:
obtain ⟨i, hi⟩ := Set.exists_of_ssubset hssubset

Premises used: Set.exists_of_ssubset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
rw :
  ∀
    (h :
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
        ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeights k univ) : P))
    (hssubset : t ⊂ Set.univ) (i : Fin (n + 1)) (hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t), False
⊢ False

Tactic:
rw [s.centroid_eq_affineCombination] at h

Premises used: Affine.Simplex.centroid_eq_affineCombination
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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 (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeights k univ) : P)
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
⊢ let w : Fin (n + 1) → k := centroidWeights k univ;
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
set w := (centroidWeights k (univ : Finset (Fin (n + 1)))) with wdef

Premises used: Finset.univ, Finset.centroidWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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 (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (centroidWeights k univ) : P)
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
h₁ :
  let w : Fin (n + 1) → k := centroidWeights k univ;
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ let w : Fin (n + 1) → k := centroidWeights k univ;
  w = centroidWeights k univ

Tactic:
set w := (centroidWeights k (univ : Finset (Fin (n + 1)))) with wdef

Premises used: Finset.univ, Finset.centroidWeights
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
⊢ Finset.Nonempty (α := Fin (n + 1)) univ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
rw rw₁ : Eq.{u_1 + 1} (α := k) 1 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1

Tactic:
rw [sum_centroidWeights_eq_one_of_nonempty _ _ (by simp)]

Premises used: Finset.sum_centroidWeights_eq_one_of_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1

Tactic:
have hw : ∑ i, w i = 1 := by rw [sum_centroidWeights_eq_one_of_nonempty _ _ (by simp)]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ Membership.mem (γ := Finset (Fin (n + 1))) univ i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ w i = 0

Tactic:
have h1 := AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan s.independent hw h
    (by simp) hi.2
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h1 : w i = 0
⊢ w i = 1 / HAdd.hAdd (α := k) (↑n : k) 1

Tactic:
simp [wdef, centroidWeights_apply, card_univ, Fintype.card_fin, Nat.cast_add,
      Nat.cast_one]

Premises used: Finset.card_univ, Fintype.card_fin, Finset.centroidWeights_apply, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h1 : w i = 0
⊢ w i = 1 / HAdd.hAdd (α := k) (↑n : k) 1

Tactic:
have h2 : w i = (1 : k) / (n + 1) := by
    simp [wdef, centroidWeights_apply, card_univ, Fintype.card_fin, Nat.cast_add,
      Nat.cast_one]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h1 : w i = 0
h2 : w i = 1 / HAdd.hAdd (α := k) (↑n : k) 1
⊢ HAdd.hAdd (α := k) (↑n : k) 1 = 0

Tactic:
simp only [h2, one_div, inv_eq_zero] at h1

Premises used: inv_eq_zero, one_div
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
hssubset : t ⊂ Set.univ
i : Fin (n + 1)
hi : Membership.mem (γ := Set (Fin (n + 1))) Set.univ i ∧ i ∉ t
w : Fin (n + 1) → k := centroidWeights k univ
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' t))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
wdef : w = centroidWeights k univ
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h2 : w i = 1 / HAdd.hAdd (α := k) (↑n : k) 1
h1 : HAdd.hAdd (α := k) (↑n : k) 1 = 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (h1 : False), False
⊢ False

Tactic:
norm_cast at h1
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
p : P
⊢ Finset.Nonempty (α := Fin (n + 1)) univ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
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
p : P
p_1 : Fin (n + 1) → V
⊢ Finset.Nonempty (α := Fin (n + 1)) univ

Tactic:
simp