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
i : Fin (n + 1)
h :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) =
    HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.centroid})
    (HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid) +ᵥ s.centroid)

Tactic:
smul_vsub_rev_vadd_mem_affineSpan_pair _ _ _

Premises used: smul_vsub_rev_vadd_mem_affineSpan_pair, Set.Mem
-- 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)
h :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) =
    HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.centroid})
    (HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid) +ᵥ s.centroid)

Tactic:
exact smul_vsub_rev_vadd_mem_affineSpan_pair _ _ _

Premises used: smul_vsub_rev_vadd_mem_affineSpan_pair
-- 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.median i ≤ affineSpan k {s.points i, s.centroid}

Tactic:
have h1 : s.median i ≤ line[k, s.points i, s.centroid] := by
    unfold median
    apply affineSpan_pair_le_of_right_mem
    rw [faceOppositeCentroid_eq_smul_vsub_vadd_point]
    have h : (n : k)⁻¹ • (s.centroid -ᵥ s.points i) = (-1 / n : k) • (s.points i -ᵥ s.centroid)
        := by
      rw [← neg_vsub_eq_vsub_rev]
      have : -(s.points i -ᵥ s.centroid) = (-1 : k) • (s.points i -ᵥ s.centroid) := by simp
      rw [this, smul_smul]
      congr 1
      rw [mul_neg_one, inv_eq_one_div, neg_div]
    rw [h]
    exact smul_vsub_rev_vadd_mem_affineSpan_pair _ _ _
-- 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)
h1 : s.median i ≤ affineSpan k {s.points i, s.centroid}
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i}) s.centroid
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {s.points i, s.centroid})
    (affineSpan k {s.points i, s.faceOppositeCentroid i})

Tactic:
apply affineSpan_pair_le_of_right_mem

Premises used: affineSpan_pair_le_of_right_mem
-- 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)
h1 : s.median i ≤ affineSpan k {s.points i, s.centroid}
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i}) s.centroid

Tactic:
centroid_mem_median s i

Premises used: Set.Mem, Affine.Simplex.centroid_mem_median
-- 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)
h1 : s.median i ≤ affineSpan k {s.points i, s.centroid}
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i}) s.centroid

Tactic:
exact centroid_mem_median s i

Premises used: Affine.Simplex.centroid_mem_median
-- 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)
h1 : s.median i ≤ affineSpan k {s.points i, s.centroid}
⊢ affineSpan k {s.points i, s.centroid} ≤ s.median i

Tactic:
have h2 : line[k, s.points i, s.centroid] ≤ s.median i := by
    rw [median]
    apply affineSpan_pair_le_of_right_mem
    exact centroid_mem_median s 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
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
i : Fin (n + 1)
h1 : s.median i ≤ affineSpan k {s.points i, s.centroid}
h2 : affineSpan k {s.points i, s.centroid} ≤ s.median i
⊢ s.median i = affineSpan k {s.points i, s.centroid}

Tactic:
le_antisymm h1 h2

Premises used: le_antisymm
-- 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)
h1 : s.median i ≤ affineSpan k {s.points i, s.centroid}
h2 : affineSpan k {s.points i, s.centroid} ≤ s.median i
⊢ s.median i = affineSpan k {s.points i, s.centroid}

Tactic:
exact le_antisymm h1 h2

Premises used: le_antisymm
-- 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
rw : p -ᵥ s.centroid = 0
⊢ p = s.centroid

Tactic:
rw [← vsub_eq_zero_iff_eq]

Premises used: vsub_eq_zero_iff_eq
-- 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
rw rw₁ : p = p
⊢ p = (p -ᵥ s.centroid) +ᵥ s.centroid

Tactic:
rw [vsub_vadd]

Premises used: vsub_vadd
-- 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
⊢ p = (p -ᵥ s.centroid) +ᵥ s.centroid

Tactic:
have hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid := by rw [vsub_vadd]
-- 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
i : ↥s'
⊢ p ∈ s.median (↑i : Fin (n + 1))

Tactic:
have hi := h 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
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
i : ↥s'
hi : p ∈ s.median (↑i : Fin (n + 1))
⊢ Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)

Tactic:
grind only [median_eq_line_point_centroid, vadd_right_mem_affineSpan_pair,
      Submodule.smul_mem, Submodule.mem_span_singleton_self]

Premises used: vadd_right_mem_affineSpan_pair, Affine.Simplex.median_eq_line_point_centroid, Submodule.mem_span_singleton_self, Submodule.smul_mem
-- 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
⊢ ∀ (i : ↥s'), Membership.mem (γ := Submodule k V) (k ∙ u i) (p -ᵥ s.centroid)

Tactic:
have h_span : ∀ i : s', p -ᵥ s.centroid ∈ (Submodule.span k ({u i} : Set V)) := by
    intro i
    have hi := h i
    grind only [median_eq_line_point_centroid, vadd_right_mem_affineSpan_pair,
      Submodule.smul_mem, Submodule.mem_span_singleton_self]
-- 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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
⊢ AffineIndependent k (Function.update (β := fun (a : Fin (n + 1)) ↦ P) s.points i₀ s.centroid)

Tactic:
have := affineIndependent_points_update_centroid s 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
n : ℕ
inst_4 : NeZero n
inst_5 : CharZero k
s : Simplex k P n
hn : 1 < n
p_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
this :
  AffineIndependent.{u_1, u_2, u_3, 0} k (P := P) fun (a : Fin (n + 1)) ↦
    if h : a = i₀ then Eq.ndrec (motive := fun (a : Fin (n + 1)) ↦ P) s.centroid ⋯ else s.points a
⊢ AffineIndependent k p

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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
⊢ AffineIndependent k p

Tactic:
have hindep : AffineIndependent k p := by
      have := affineIndependent_points_update_centroid s i₀
      unfold Function.update at this
      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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ i₀ }) ↦ p (↑i : Fin (n + 1)) -ᵥ p i₀

Tactic:
have h1 := (affineIndependent_iff_linearIndependent_vsub k p i₀).mp hindep
-- 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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 : LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // x ≠ i₀ }) ↦ p (↑i : Fin (n + 1)) -ᵥ p i₀
⊢ LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
    (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
      if True then s.centroid else s.points i₀

Tactic:
simp_rw [ne_eq, p] at h1

Premises used: ne_eq
-- 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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
    (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
      if True then s.centroid else s.points i₀
x : ↥{i₀}ᶜ
⊢ (↑x : Fin (n + 1)) ≠ i₀

Tactic:
grind [mem_compl, Finset.notMem_singleton]

Premises used: Finset.notMem_singleton, Finset.mem_compl
-- 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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
    (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
      if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x : Fin (n + 1) // x ≠ i₀ } :=
  have h : ∀ (x : ↥{i₀}ᶜ), (↑x : Fin (n + 1)) ≠ i₀ := ⋯;
  fun (x : ↥{i₀}ᶜ) ↦ Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ i₀) (↑x : Fin (n + 1)) ⋯
x y : ↥{i₀}ᶜ
hxy : f x = f y
⊢ x = y

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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
    (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
      if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x : Fin (n + 1) // x ≠ i₀ } :=
  have h : ∀ (x : ↥{i₀}ᶜ), (↑x : Fin (n + 1)) ≠ i₀ := ⋯;
  fun (x : ↥{i₀}ᶜ) ↦ Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ i₀) (↑x : Fin (n + 1)) ⋯
⊢ Function.Injective f

Tactic:
have f_inj : Function.Injective f := by intro x y hxy; 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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
    (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
      if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x : Fin (n + 1) // x ≠ i₀ } :=
  have h : ∀ (x : ↥{i₀}ᶜ), (↑x : Fin (n + 1)) ≠ i₀ := ⋯;
  fun (x : ↥{i₀}ᶜ) ↦ Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ i₀) (↑x : Fin (n + 1)) ⋯
f_inj : Function.Injective f
⊢ LinearIndependent.{0, u_1, u_2} k (M := V)
    ((fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
        (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
          if True then s.centroid else s.points i₀) ∘
      f)

Tactic:
have h2 := h1.comp f f_inj
-- 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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
    (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
      if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x : Fin (n + 1) // x ≠ i₀ } :=
  have h : ∀ (x : ↥{i₀}ᶜ), (↑x : Fin (n + 1)) ≠ i₀ := ⋯;
  fun (x : ↥{i₀}ᶜ) ↦ Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ i₀) (↑x : Fin (n + 1)) ⋯
f_inj : Function.Injective f
h2 :
  LinearIndependent.{0, u_1, u_2} k (M := V)
    ((fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
        (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
          if True then s.centroid else s.points i₀) ∘
      f)
⊢ LinearIndependent.{0, u_1, u_2} k (M := V)
    ((fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
        (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
          if True then s.centroid else s.points i₀) ∘
      f)

Tactic:
h2
-- 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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
    (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
      if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x : Fin (n + 1) // x ≠ i₀ } :=
  have h : ∀ (x : ↥{i₀}ᶜ), (↑x : Fin (n + 1)) ≠ i₀ := ⋯;
  fun (x : ↥{i₀}ᶜ) ↦ Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ i₀) (↑x : Fin (n + 1)) ⋯
f_inj : Function.Injective f
h2 :
  LinearIndependent.{0, u_1, u_2} k (M := V)
    ((fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
        (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
          if True then s.centroid else s.points i₀) ∘
      f)
h₁ :
  u =
    (fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
        (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
          if True then s.centroid else s.points i₀) ∘
      f
⊢ LinearIndependent k u

Tactic:
convert! h2 using 1
-- 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_1 : P
h : ∀ (i : Fin (n + 1)), p_1 ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p_1 = (p_1 -ᵥ 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_1 -ᵥ s.centroid)
p : Fin (n + 1) → P := fun (x : Fin (n + 1)) ↦ if x = i₀ then s.centroid else s.points x
hindep : AffineIndependent k p
h1 :
  LinearIndependent.{0, u_1, u_2} k (M := V) fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
    (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
      if True then s.centroid else s.points i₀
f : ↥{i₀}ᶜ → { x : Fin (n + 1) // x ≠ i₀ } :=
  have h : ∀ (x : ↥{i₀}ᶜ), (↑x : Fin (n + 1)) ≠ i₀ := ⋯;
  fun (x : ↥{i₀}ᶜ) ↦ Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ≠ i₀) (↑x : Fin (n + 1)) ⋯
f_inj : Function.Injective f
h2 :
  LinearIndependent.{0, u_1, u_2} k (M := V)
    ((fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
        (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
          if True then s.centroid else s.points i₀) ∘
      f)
⊢ u =
    (fun (i : { x : Fin (n + 1) // ¬x = i₀ }) ↦
        (if (↑i : Fin (n + 1)) = i₀ then s.centroid else s.points (↑i : Fin (n + 1))) -ᵥ
          if True then s.centroid else s.points i₀) ∘
      f

Tactic:
grind only [mem_compl, Finset.notMem_singleton]

Premises used: Finset.notMem_singleton, Finset.mem_compl