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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
⊢ (s.reindex e).faceOppositeCentroid i = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) i
have h : ((s.reindex e).faceOpposite i).centroid = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) i
Tactic: rw [faceOppositeCentroid]
-- 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
⊢ ((s.reindex e).faceOpposite i).centroid = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) i
have h : ∀ [inst_6 : NeZero m] (e : Fin (m + 1) ≃ Fin (m + 1)) (i : Fin (m + 1)),
  ((s.reindex e).faceOpposite i).centroid = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (m + 1))) i
Tactic: obtain rfl : m = n := by simpa using Fintype.card_eq.2 ⟨e⟩
Cleared hypotheses: n, inst_5, e, 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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).median = s.median ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have h : ∀ (i : Fin (m + 1)) (x : P), x ∈ (s.reindex e).median i ↔ x ∈ (s.median ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
Tactic: ext 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
i : Fin (n + 1)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
have rw : s.centroid -ᵥ s.points i = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
Tactic: rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
rw :
  s.centroid -ᵥ s.points i = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
Tactic: rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
rw :
  s.centroid -ᵥ s.points i = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) •
    HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
rw :
  s.centroid -ᵥ s.points i = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) •
      HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
have rw₃ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1) * HAdd.hAdd (α := k) (↑n : k) 1) •
    (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
rw :
  s.centroid -ᵥ s.points i = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) •
      HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1) * HAdd.hAdd (α := k) (↑n : k) 1) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
have rw₄ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  ((↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ * HAdd.hAdd (α := k) (↑n : k) 1) •
    (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
rw :
  s.centroid -ᵥ s.points i = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) •
      HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1) * HAdd.hAdd (α := k) (↑n : k) 1) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ * HAdd.hAdd (α := k) (↑n : k) 1) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
have rw₅ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  ((↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ * HAdd.hAdd (α := k) (↑n : k) 1)) •
    (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
rw :
  s.centroid -ᵥ s.points i = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) •
      HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1) * HAdd.hAdd (α := k) (↑n : k) 1) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ * HAdd.hAdd (α := k) (↑n : k) 1) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₅ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ * HAdd.hAdd (α := k) (↑n : k) 1)) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
have rw₆ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  HMul.hMul (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
rw :
  s.centroid -ᵥ s.points i = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i)
rw₂ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) •
      HAdd.hAdd (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1) * HAdd.hAdd (α := k) (↑n : k) 1) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * (HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ * HAdd.hAdd (α := k) (↑n : k) 1) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₅ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    ((↑n : k) * ((HAdd.hAdd (α := k) (↑n : k) 1)⁻¹ * HAdd.hAdd (α := k) (↑n : k) 1)) •
      (s.faceOppositeCentroid i -ᵥ s.centroid)
rw₆ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
    HMul.hMul (α := k) (↑n : k) 1 • (s.faceOppositeCentroid i -ᵥ s.centroid)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
have rw₇ : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid) =
  HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k) (s.faceOppositeCentroid i -ᵥ s.centroid)
Tactic: rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i}) s.centroid
have h : s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
Tactic: have h : s.centroid = ((n : k) * (1 / (n + 1))) • (s.faceOppositeCentroid i -ᵥ s.points i)
    +ᵥ s.points i := by
    rw [eq_vadd_iff_vsub_eq, centroid_vsub_point_eq_smul_vsub,
      faceOppositeCentroid_vsub_point_eq_smul_vsub, smul_smul, one_div, mul_assoc,
      inv_mul_cancel₀ (by norm_cast), mul_one]
-- 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)
h :
  s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i}) s.centroid
have rw : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i})
  (((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i)
Tactic: rw [h]
-- 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)
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i})
    (affineSpan k {s.points i, s.centroid})
have h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.centroid}) (s.faceOppositeCentroid i)
Tactic: apply affineSpan_pair_le_of_right_mem
-- 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)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.centroid}) (s.faceOppositeCentroid i)
have h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.centroid})
  (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) +ᵥ s.centroid)
Tactic: rw [faceOppositeCentroid_eq_smul_vsub_vadd_point]
-- 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)
⊢ 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)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (-(s.points i -ᵥ s.centroid)) =
  HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid)
Tactic: rw [← neg_vsub_eq_vsub_rev]
-- 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)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (-(s.points i -ᵥ s.centroid)) =
    HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid)
have this : -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)
Tactic: have : -(s.points i -ᵥ s.centroid) = (-1 : k) • (s.points i -ᵥ s.centroid) := by simp
-- 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)
this : -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (-(s.points i -ᵥ s.centroid)) =
    HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid)
have rw : HMul.hMul (α := k) (↑n : k)⁻¹ (-1) • (s.points i -ᵥ s.centroid) =
  HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid)
Tactic: rw [this, smul_smul]
-- 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)
this : -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)
⊢ HMul.hMul (α := k) (↑n : k)⁻¹ (-1) • (s.points i -ᵥ s.centroid) =
    HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid)
have e_a : HMul.hMul (α := k) (↑n : k)⁻¹ (-1) = HDiv.hDiv (α := k) (-1) (↑n : k)
Tactic: congr 1
-- 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)
this : -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)
⊢ HMul.hMul (α := k) (↑n : k)⁻¹ (-1) = HDiv.hDiv (α := k) (-1) (↑n : k)
have e_a : -(↑n : k)⁻¹ = HDiv.hDiv (α := k) (-1) (↑n : k)
Tactic: rw [mul_neg_one, inv_eq_one_div, neg_div]
-- 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)
this : -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)
e_a : -(↑n : k)⁻¹ = HDiv.hDiv (α := k) (-1) (↑n : k)
⊢ HMul.hMul (α := k) (↑n : k)⁻¹ (-1) = HDiv.hDiv (α := k) (-1) (↑n : k)
have e_a₁ : -HDiv.hDiv (α := k) 1 (↑n : k) = HDiv.hDiv (α := k) (-1) (↑n : k)
Tactic: rw [mul_neg_one, inv_eq_one_div, neg_div]
-- 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)
this : -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)
e_a : -(↑n : k)⁻¹ = HDiv.hDiv (α := k) (-1) (↑n : k)
e_a₁ : -HDiv.hDiv (α := k) 1 (↑n : k) = HDiv.hDiv (α := k) (-1) (↑n : k)
⊢ HMul.hMul (α := k) (↑n : k)⁻¹ (-1) = HDiv.hDiv (α := k) (-1) (↑n : k)
have e_a₂ : -HDiv.hDiv (α := k) 1 (↑n : k) = -HDiv.hDiv (α := k) 1 (↑n : k)
Tactic: rw [mul_neg_one, inv_eq_one_div, neg_div]
-- 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)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.centroid})
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) +ᵥ s.centroid)
have 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)
Tactic: 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]
-- 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)
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})
    (HSMul.hSMul.{u_1, u_2, u_2} (α := k) (↑n : k)⁻¹ (s.centroid -ᵥ s.points i) +ᵥ s.centroid)
have h₁ : 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: rw [h]
-- 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)
⊢ s.median i = affineSpan k {s.points i, s.centroid}
have h1 : 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 _ _ _