awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
⊢ LinearIndependent k u

Tactic:
have hi : LinearIndependent k u := by
    set p : Fin (n + 1) → P := fun x => if x = i₀ then s.centroid else s.points x
    have hindep : AffineIndependent k p := by
      have := affineIndependent_points_update_centroid s i₀
      unfold Function.update at this
      grind
    have h1 := (affineIndependent_iff_linearIndependent_vsub k p i₀).mp hindep
    simp_rw [ne_eq, p] at h1
    set f : {x // x ∈ ({i₀}ᶜ : Finset (Fin (n + 1)))} → {x // x ≠ i₀} :=
      have h (x : {x // x ∈ ({i₀}ᶜ : Finset (Fin (n + 1)))}) : x.val ≠ i₀ := by
        grind [mem_compl, Finset.notMem_singleton]
      fun x => ⟨x.val, h x⟩
    have f_inj : Function.Injective f := by intro x y hxy; grind
    have h2 := h1.comp f f_inj
    convert! h2 using 1
    grind only [mem_compl, Finset.notMem_singleton]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
simp : ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
⊢ ∃ (i : ↥s') (j : ↥s'), i ≠ j

Tactic:
simp only [ne_eq, Subtype.exists, Subtype.mk.injEq, exists_prop]

Premises used: Subtype.exists, exists_prop, ne_eq, Subtype.mk.injEq
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
rw : Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i₀} = n
rw₁ : n + 1 - card (α := Fin (n + 1)) {i₀} = n
rw₂ : n + 1 - 1 = n
rw₃ rw₄ : n = n
⊢ #s' = n

Tactic:
rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]

Premises used: Fintype.card_fin, Finset.card_compl, add_tsub_cancel_right, Finset.card_singleton
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
⊢ #s' = n

Tactic:
have hcard : s'.card = n := by
      rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
hcard : #s' = n
⊢ 1 < #s'

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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
hcard : #s' = n
⊢ 1 < #s'

Tactic:
have hcard' : 1 < #s' := 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
hcard : #s' = n
hcard' : 1 < #s'
⊢ ∃ (a : Fin (n + 1)) (b : Fin (n + 1)), a ∈ s' ∧ b ∈ s' ∧ a ≠ b

Tactic:
rw [Finset.one_lt_card_iff] at hcard'

Premises used: Finset.one_lt_card_iff
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
hcard : #s' = n
hcard' : ∃ (a : Fin (n + 1)) (b : Fin (n + 1)), a ∈ s' ∧ b ∈ s' ∧ a ≠ b
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
h₁ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s' ∧ ∃ a ∈ s', ¬w = a
w : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
h₂ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s' ∧ ∃ a ∈ s', ¬w = a
w₁ : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
h₃ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s'
h₄ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → ∃ a ∈ s', ¬w = a
w₂ : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
h₅ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s'
h₆ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → ∃ a ∈ s', ¬w = a
w₃ : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
h₇ h₈ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → ∃ a ∈ s', ¬w = a
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1

Tactic:
tauto
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
⊢ ∃ (i : ↥s') (j : ↥s'), i ≠ j

Tactic:
have he : ∃ i j : s', i ≠ j := by
    simp only [ne_eq, Subtype.exists, Subtype.mk.injEq, exists_prop]
    have hcard : s'.card = n := by
      rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]
    have hcard' : 1 < #s' := by grind
    rw [Finset.one_lt_card_iff] at hcard'
    tauto
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
he : ∃ (i : ↥s') (j : ↥s'), i ≠ j
choose : ∀ (i j : ↥s') (hij : i ≠ j), p -ᵥ s.centroid = 0
⊢ p -ᵥ s.centroid = 0

Tactic:
choose i j hij using he
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
⊢ Disjoint (α := Set ↥s') {i} {j}

Tactic:
simp [hij]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
⊢ Disjoint (α := Set ↥s') {i} {j}

Tactic:
have h_ij : Disjoint ({i} : Set {x // x ∈ s'}) {j} := by simp [hij]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint (α := Set ↥s') {i} {j}
simp_rw : Disjoint (α := Submodule k V) (Submodule.span k (u '' {i})) (Submodule.span k (u '' {j}))
⊢ Disjoint (α := Submodule k V) (k ∙ u i) (k ∙ u j)

Tactic:
simp_rw [← Set.image_singleton, hi.disjoint_span_image h_ij]

Premises used: Set.image_singleton, LinearIndependent.disjoint_span_image
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint (α := Set ↥s') {i} {j}
⊢ Disjoint (α := Submodule k V) (k ∙ u i) (k ∙ u j)

Tactic:
have h_disjoint : Disjoint (Submodule.span k {u i}) (Submodule.span k {u j}) := by
    simp_rw [← Set.image_singleton, hi.disjoint_span_image h_ij]
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint (α := Set ↥s') {i} {j}
h_disjoint : Disjoint (α := Submodule k V) (k ∙ u i) (k ∙ u j)
⊢ p -ᵥ s.centroid = 0

Tactic:
Submodule.disjoint_def.1 h_disjoint _ (h_span i) (h_span j)

Premises used: Iff.mp, Submodule.disjoint_def
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun (i : ↥s') ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.centroid
h_span : ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)
hi : LinearIndependent k u
i j : ↥s'
hij : i ≠ j
h_ij : Disjoint (α := Set ↥s') {i} {j}
h_disjoint : Disjoint (α := Submodule k V) (k ∙ u i) (k ∙ u j)
⊢ p -ᵥ s.centroid = 0

Tactic:
exact Submodule.disjoint_def.1 h_disjoint _ (h_span i) (h_span j)

Premises used: Iff.mp, Submodule.disjoint_def
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
⊢ AffineIndependent k s.points

Tactic:
obtain h := s.independent

Premises used: Affine.Simplex.independent
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
h : AffineIndependent k s.points
rw :
  ∀
    (h :
      LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
        s.points (↑i : Fin (n + 1)) -ᵥ s.points 0),
    LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
      s.faceOppositeCentroid (↑i : Fin (n + 1)) -ᵥ s.faceOppositeCentroid 0
⊢ AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (i : Fin (n + 1)) ↦ s.faceOppositeCentroid i

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k _ 0] at h ⊢

Premises used: affineIndependent_iff_linearIndependent_vsub, 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 : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
h :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.points (↑i : Fin (n + 1)) -ᵥ s.points 0
simp_rw :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points 0 -ᵥ s.points (↑i : Fin (n + 1)))
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.faceOppositeCentroid (↑i : Fin (n + 1)) -ᵥ s.faceOppositeCentroid 0

Tactic:
simp_rw [faceOppositeCentroid_vsub_faceOppositeCentroid]

Premises used: Affine.Simplex.faceOppositeCentroid_vsub_faceOppositeCentroid
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
h :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.points (↑i : Fin (n + 1)) -ᵥ s.points 0
x : { x : Fin (n + 1) // x ≠ 0 }
⊢ Ne.{u_1 + 1} (α := k) (-(↑n : k))⁻¹ 0

Tactic:
simpa using NeZero.ne n

Premises used: NeZero.ne
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
h :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.points (↑i : Fin (n + 1)) -ᵥ s.points 0
h₁ :
  ∀ (i : { x : Fin (n + 1) // x ≠ 0 }),
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points 0 -ᵥ s.points (↑i : Fin (n + 1))) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := { x : Fin (n + 1) // x ≠ 0 } → kˣ) (β := { x : Fin (n + 1) // x ≠ 0 } → V)
        (fun (x : { x : Fin (n + 1) // x ≠ 0 }) ↦ Units.mk0 (-(↑n : k))⁻¹ ⋯)
        (fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.points 0) i
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points 0 -ᵥ s.points (↑i : Fin (n + 1)))

Tactic:
convert! h.units_smul fun _ ↦ Units.mk0 (-n)⁻¹ (by simpa using NeZero.ne n) with i

Premises used: Nat.cast, Units.mk0, Inv.inv, LinearIndependent.units_smul, Neg.neg
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
h :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦
    s.points (↑i : Fin (n + 1)) -ᵥ s.points 0
i : { x : Fin (n + 1) // x ≠ 0 }
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.points 0 -ᵥ s.points (↑i : Fin (n + 1))) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := { x : Fin (n + 1) // x ≠ 0 } → kˣ) (β := { x : Fin (n + 1) // x ≠ 0 } → V)
      (fun (x : { x : Fin (n + 1) // x ≠ 0 }) ↦ Units.mk0 (-(↑n : k))⁻¹ ⋯)
      (fun (i : { x : Fin (n + 1) // x ≠ 0 }) ↦ s.points (↑i : Fin (n + 1)) -ᵥ s.points 0) i

Tactic:
simp [← smul_neg]

Premises used: smul_neg
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.medial.points i = s.faceOppositeCentroid i

Tactic:
rfl

Premises used: Affine.Simplex.faceOppositeCentroid, Finset.centroid, 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
inst_6 : CharZero k
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : ∀ (i : Fin (m + 1)), (s.reindex e).medial.points i = (s.medial.reindex e).points i
⊢ (s.reindex e).medial = s.medial.reindex e

Tactic:
ext i
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
inst_6 : CharZero k
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
⊢ (s.reindex e).medial.points i = (s.medial.reindex e).points i

Tactic:
simp [medial_points]

Premises used: Affine.Simplex.medial_points
-- 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
V₂ : Type u_4
P₂ : Type u_5
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : CharZero k
n : ℕ
inst_8 : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
h : ∀ (i : Fin (n + 1)), (s.map f hf).medial.points i = (s.medial.map f hf).points i
⊢ (s.map f hf).medial = s.medial.map f hf

Tactic:
ext i
-- 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
V₂ : Type u_4
P₂ : Type u_5
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : CharZero k
n : ℕ
inst_8 : NeZero n
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Function.Injective.{u_3 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : Fin (n + 1)
⊢ (s.map f hf).medial.points i = (s.medial.map f hf).points i

Tactic:
simp [medial_points]

Premises used: Affine.Simplex.medial_points
-- 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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
⊢ s.medial.points 0 ∈ Set.range s.medial.points

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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)

Tactic:
have hmem1 : s.medial.points 0 ∈ affineSpan k (Set.range s.medial.points) :=
    mem_affineSpan _ (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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
apply : (↑(affineSpan k (Set.range (s.faceOpposite 0).points)) : Set P) ⊆ (↑(affineSpan k (Set.range s.points)) : Set P)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) (s.medial.points 0)

Tactic:
apply Set.mem_of_mem_of_subset (s.faceOppositeCentroid_mem_affineSpan_face 0)

Premises used: Affine.Simplex.faceOppositeCentroid_mem_affineSpan_face, Set.mem_of_mem_of_subset, 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 : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
⊢ Set.range (s.faceOpposite 0).points ⊆ Set.range s.points

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 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hmem1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.medial.points)) (s.medial.points 0)
⊢ (↑(affineSpan k (Set.range (s.faceOpposite 0).points)) : Set P) ⊆ (↑(affineSpan k (Set.range s.points)) : Set P)

Tactic:
exact affineSpan_mono k (by simp)

Premises used: affineSpan_mono