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
inst_4 : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
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)
hw : Finset.sum (ι := Fin (n - 1 + 1)) univ (centroidWeights k univ) = 1
⊢ Eq.{u_5 + 1} (α := P₂)
    ((affineCombination k univ ((⇑f : (a : P) → P₂) ∘ (s.faceOpposite i).points) : (a : Fin (n - 1 + 1) → k) → P₂)
        (centroidWeights k univ) :
      P₂)
    ((f : (a : P) → P₂)
        ((affineCombination k univ (s.faceOpposite i).points : (a : Fin (n - 1 + 1) → k) → P) (centroidWeights k univ) :
          P) :
      P₂)

Tactic:
rw [Finset.map_affineCombination]

Premises used: Finset.map_affineCombination
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
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)
hw : card (α := Fin (n - 1 + 1)) univ ≠ 0
⊢ Finset.sum (ι := Fin (n - 1 + 1)) univ (centroidWeights k univ) = 1

Tactic:
rw [sum_centroidWeights_eq_one_of_card_ne_zero]

Premises used: Finset.sum_centroidWeights_eq_one_of_card_ne_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : CharZero k
V₂ : Type u_4
P₂ : Type u_5
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AffineSpace V₂ P₂
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)
⊢ card (α := Fin (n - 1 + 1)) univ ≠ 0

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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
rw : s.faceOppositeCentroid i = (↑((s.restrict S hS).faceOppositeCentroid i) : P)
⊢ (↑((s.restrict S hS).faceOppositeCentroid i) : P) = s.faceOppositeCentroid i

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- 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 : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ Nonempty.{u_3 + 1} ↥S

Tactic:
haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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 : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_3 + 1} ↥S
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)

Tactic:
simp only [coe_subtype, Subtype.val_injective]

Premises used: Subtype.val_injective, AffineSubspace.coe_subtype
-- 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 : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_3 + 1} ↥S
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)

Tactic:
have hf : Function.Injective (S.subtype) := by
    simp only [coe_subtype, Subtype.val_injective]
-- 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 : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_3 + 1} ↥S
hf : Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)
⊢ s.faceOppositeCentroid i = (↑((s.restrict S hS).faceOppositeCentroid i) : P)

Tactic:
(s.restrict S hS).faceOppositeCentroid_map S.subtype hf (i := i)

Premises used: AffineSubspace.subtype, Affine.Simplex.map, Affine.Simplex.faceOppositeCentroid_map, Affine.Simplex.restrict
-- 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 : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_3 + 1} ↥S
hf : Function.Injective.{u_3 + 1, u_3 + 1} (α := ↥S) (β := P) (⇑S.subtype : (a : ↥S) → P)
⊢ s.faceOppositeCentroid i = (↑((s.restrict S hS).faceOppositeCentroid i) : P)

Tactic:
exact (s.restrict S hS).faceOppositeCentroid_map S.subtype hf (i := i)

Premises used: AffineSubspace.subtype, Affine.Simplex.faceOppositeCentroid_map, Affine.Simplex.restrict
-- 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
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
h :
  ∀ (i : Fin (n + 1)),
    (s.reindex e).faceOppositeCentroid i = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) i
⊢ (s.reindex e).faceOppositeCentroid = s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))

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
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
h : ((s.reindex e).faceOpposite i).centroid = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) i
⊢ (s.reindex e).faceOppositeCentroid i = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) i

Tactic:
rw [faceOppositeCentroid]

Premises used: Affine.Simplex.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
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)
⊢ m = n

Tactic:
simpa using Fintype.card_eq.2 ⟨e⟩

Premises used: Iff.mpr, Fintype.card_eq, Nonempty.intro
-- 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
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
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
⊢ ((s.reindex e).faceOpposite i).centroid = (s.faceOppositeCentroid ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1))) i

Tactic:
obtain rfl : m = n := by simpa using Fintype.card_eq.2 ⟨e⟩

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m : ℕ
inst_4 : NeZero m
s : Simplex k P m
inst_5 : 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:
centroid_eq_of_range_eq <| Affine.Simplex.range_faceOpposite_reindex s e i

Premises used: Affine.Simplex.faceOppositeCentroid, Affine.Simplex.centroid_eq_of_range_eq, Affine.Simplex.range_faceOpposite_reindex, Finset.centroid
-- 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 : ℕ
inst_4 : NeZero m
s : Simplex k P m
inst_5 : 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:
exact centroid_eq_of_range_eq <| Affine.Simplex.range_faceOpposite_reindex s e i

Premises used: Affine.Simplex.centroid_eq_of_range_eq, Affine.Simplex.range_faceOpposite_reindex
-- 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
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
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
⊢ (s.reindex e).median = s.median ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))

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
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
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:
simp [median]

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

Tactic:
simp [median, map_span, Set.image_pair]

Premises used: Set.image_pair, Affine.Simplex.median, AffineSubspace.map_span
-- 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 : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ AffineSubspace.map S.subtype ((s.restrict S hS).median i) = s.median i

Tactic:
simp [median, map_span, Set.image_pair]

Premises used: Set.image_pair, Affine.Simplex.median, AffineSubspace.map_span
-- 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
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i ∈ s.median i

Tactic:
simp [median, right_mem_affineSpan_pair]

Premises used: Affine.Simplex.median, right_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
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i ∈ s.median i

Tactic:
simp [median, left_mem_affineSpan_pair]

Premises used: Affine.Simplex.median, left_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)
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)
rw₇ 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)
⊢ s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points 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]

Premises used: mul_assoc, smul_smul, Affine.Simplex.faceOppositeCentroid_vsub_point_eq_smul_vsub, one_div, mul_one, inv_mul_cancel₀, eq_vadd_iff_vsub_eq, Affine.Simplex.centroid_vsub_point_eq_smul_vsub
-- 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.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]
-- 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 :
  s.centroid = ((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i
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)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i}) s.centroid

Tactic:
rw [h]
-- 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 :
  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})
    (((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i)

Tactic:
smul_vsub_vadd_mem_affineSpan_pair _ _ _

Premises used: Set.Mem, smul_vsub_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)
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})
    (((↑n : k) * (1 / HAdd.hAdd (α := k) (↑n : k) 1)) • (s.faceOppositeCentroid i -ᵥ s.points i) +ᵥ s.points i)

Tactic:
exact smul_vsub_vadd_mem_affineSpan_pair _ _ _

Premises used: smul_vsub_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)
h : Membership.mem (γ := AffineSubspace k P) (affineSpan k {s.points i, s.centroid}) (s.faceOppositeCentroid i)
⊢ LE.le (α := AffineSubspace k P) (affineSpan k {s.points i, s.faceOppositeCentroid i})
    (affineSpan k {s.points i, s.centroid})

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

Tactic:
rw [faceOppositeCentroid_eq_smul_vsub_vadd_point]

Premises used: Affine.Simplex.faceOppositeCentroid_eq_smul_vsub_vadd_point
-- 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)
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)
⊢ 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:
rw [← neg_vsub_eq_vsub_rev]

Premises used: neg_vsub_eq_vsub_rev
-- 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.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)

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
i : Fin (n + 1)
⊢ -(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
-- 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)
this : -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)
rw :
  HMul.hMul (α := k) (↑n : k)⁻¹ (-1) • (s.points i -ᵥ s.centroid) =
    HDiv.hDiv (α := k) (-1) (↑n : k) • (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)

Tactic:
rw [this, smul_smul]

Premises used: smul_smul
-- 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)
this : -(s.points i -ᵥ s.centroid) = HSMul.hSMul.{u_1, u_2, u_2} (α := k) (-1) (s.points i -ᵥ s.centroid)
e_a : HMul.hMul (α := k) (↑n : k)⁻¹ (-1) = HDiv.hDiv (α := k) (-1) (↑n : k)
⊢ HMul.hMul (α := k) (↑n : k)⁻¹ (-1) • (s.points i -ᵥ s.centroid) =
    HDiv.hDiv (α := k) (-1) (↑n : k) • (s.points i -ᵥ s.centroid)

Tactic:
congr 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
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)
e_a₂ 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)

Tactic:
rw [mul_neg_one, inv_eq_one_div, neg_div]

Premises used: neg_div, inv_eq_one_div, mul_neg_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : 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)

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]
-- 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)
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)
⊢ 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 [h]