awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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}
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {s.points i, s.centroid})
    (affineSpan k {s.points i, s.faceOppositeCentroid i})
have h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i}) s.centroid
Tactic: apply affineSpan_pair_le_of_right_mem
-- 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 : 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}
⊢ s.median i = affineSpan k {s.points i, s.centroid}
have h2 : 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
-- 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 : 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
⊢ p = s.centroid
have rw : p -ᵥ s.centroid = 0
Tactic: rw [← vsub_eq_zero_iff_eq]
-- 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 : 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
have rw : p = p
Tactic: rw [vsub_vadd]
-- 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 : 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 -ᵥ s.centroid = 0
have hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
Tactic: have hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid := by rw [vsub_vadd]
-- 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 : 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)
have hi : p ∈ s.median (↑i : Fin (n + 1))
Tactic: have hi := h 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 : 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
⊢ p -ᵥ s.centroid = 0
have h_span : ∀ (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]
-- 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 : 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
have this : AffineIndependent k (Function.update (β := fun (a : Fin (n + 1)) ↦ P) s.points i₀ s.centroid)
Tactic: have := affineIndependent_points_update_centroid s 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 : 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
⊢ LinearIndependent k u
have hindep : AffineIndependent k p
Tactic: have hindep : AffineIndependent k p := by
      have := affineIndependent_points_update_centroid s i₀
      unfold Function.update at this
      grind
-- 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 : 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 k u
have 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₀
Tactic: have h1 := (affineIndependent_iff_linearIndependent_vsub k p i₀).mp hindep
-- 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 : 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 k u
have 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₀
Tactic: simp_rw [ne_eq, p] at h1
Cleared hypotheses: h1
-- 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 : 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)) ⋯
⊢ LinearIndependent k u
have f_inj : Function.Injective f
Tactic: have f_inj : Function.Injective f := by intro x y hxy; grind
-- 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 : 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 k u
have 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)
Tactic: have h2 := h1.comp f f_inj
-- 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 : 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 k u
have 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
Tactic: convert! h2 using 1
-- 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 : 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)
⊢ p -ᵥ s.centroid = 0
have hi : 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]
-- 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 : 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
have simp : ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
Tactic: simp only [ne_eq, Subtype.exists, Subtype.mk.injEq, exists_prop]
-- 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 : 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
have rw : Fintype.card (Fin (n + 1)) - card (α := Fin (n + 1)) {i₀} = n
Tactic: rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]
-- 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 : 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
⊢ #s' = n
have rw₁ : n + 1 - card (α := Fin (n + 1)) {i₀} = n
Tactic: rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]
-- 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 : 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
⊢ #s' = n
have rw₂ : n + 1 - 1 = n
Tactic: rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]
-- 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 : 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
⊢ #s' = n
have rw₃ : n = n
Tactic: rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]
-- 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 : 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
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
have hcard : #s' = n
Tactic: have hcard : s'.card = n := by
      rw [Finset.card_compl, Fintype.card_fin, card_singleton, add_tsub_cancel_right]
-- 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 : 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
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
have hcard' : 1 < #s'
Tactic: have hcard' : 1 < #s' := by grind
-- 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 : 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 ∈ s', ∃ a_1 ∈ s', ¬a = a_1
have hcard'₁ : ∃ (a : Fin (n + 1)) (b : Fin (n + 1)), a ∈ s' ∧ b ∈ s' ∧ a ≠ b
Tactic: rw [Finset.one_lt_card_iff] at hcard'
Cleared hypotheses: hcard'
-- 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 : 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
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
have tauto : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
Tactic: tauto
Cleared hypotheses: hcard'
-- 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 : 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
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
have h₁ : ∀ (w w_1 : Fin (n + 1)), w ∈ s' → w_1 ∈ s' → w ≠ w_1 → w ∈ s' ∧ ∃ a ∈ s', ¬w = a
Tactic: tauto
Cleared hypotheses: hcard'
-- 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 : 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
⊢ ∃ a ∈ s', ∃ a_1 ∈ s', ¬a = a_1
have w : (w w_1 : Fin (n + 1)) → w ∈ s' → w_1 ∈ s' → w ≠ w_1 → Fin (n + 1)
Tactic: tauto
Cleared hypotheses: hcard'