awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (n + 1)
⊢ s.points =
    Function.comp (β := Fin (n + 1)) (s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (n + 1)))
      (⇑e.toEmbedding : (a : Fin (n + 1)) → Fin (n + 1))

Tactic:
simp [Function.comp_assoc]

Premises used: Function.comp_assoc
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
simp_rw :
  HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
        (Finset.centroid ℝ univ (s.map f.toAffineMap ⋯).points -ᵥ (s.map f.toAffineMap ⋯).circumcenter) +ᵥ
      (s.map f.toAffineMap ⋯).circumcenter =
    (f : (a : P) → P₂)
      (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) +ᵥ
        s.circumcenter)
⊢ (s.map f.toAffineMap ⋯).mongePoint = (f : (a : P) → P₂) s.mongePoint

Tactic:
simp_rw [mongePoint_eq_smul_vsub_vadd_circumcenter]

Premises used: Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
rw :
  HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
        ((s.map f.toAffineMap ⋯).centroid -ᵥ (s.map f.toAffineMap ⋯).circumcenter) +ᵥ
      (s.map f.toAffineMap ⋯).circumcenter =
    (f : (a : P) → P₂)
      (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)
⊢ HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
        (Finset.centroid ℝ univ (s.map f.toAffineMap ⋯).points -ᵥ (s.map f.toAffineMap ⋯).circumcenter) +ᵥ
      (s.map f.toAffineMap ⋯).circumcenter =
    (f : (a : P) → P₂)
      (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) +ᵥ
        s.circumcenter)

Tactic:
rw [← Simplex.centroid, ← Simplex.centroid]

Premises used: Affine.Simplex.centroid
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
        ((s.map f.toAffineMap ⋯).centroid -ᵥ (s.map f.toAffineMap ⋯).circumcenter) +ᵥ
      (s.map f.toAffineMap ⋯).circumcenter =
    (f : (a : P) → P₂)
      (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)

Tactic:
simp [centroid_map, circumcenter_map]

Premises used: Affine.Simplex.circumcenter_map, Affine.Simplex.centroid_map
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
rw :
  ((n + 1) • HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 2 - 1) : ℝ)) •
      (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
    ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)
⊢ (n + 1) • (s.mongePoint -ᵥ s.circumcenter) = ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)

Tactic:
rw [mongePoint_eq_smul_vsub_vadd_circumcenter, vadd_vsub, ← smul_assoc]

Premises used: smul_assoc, Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter, vadd_vsub
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
simp :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) •
      (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
    ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)
⊢ ((n + 1) • HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 2 - 1) : ℝ)) •
      (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
    ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)

Tactic:
simp only [Nat.cast_add, Nat.cast_ofNat, Nat.cast_one, Nat.add_one_sub_one, nsmul_eq_mul]

Premises used: Nat.cast_ofNat, Nat.add_one_sub_one, Nat.cast_add, nsmul_eq_mul, Nat.cast_one
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
field_simp :
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
    ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) •
      (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
    ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)

Tactic:
field_simp
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
norm_cast : Invertible (α := ℝ) (↑(n + 2 + 1) : ℝ)
⊢ Invertible (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1)

Tactic:
norm_cast
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
⊢ Invertible (α := ℝ) (↑(n + 2 + 1) : ℝ)

Tactic:
apply invertibleOfPos

Premises used: invertibleOfPos
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
have :
  ∀ (h : Invertible (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1)),
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
      ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
    ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)

Tactic:
have h : Invertible (n + 2 + 1 : ℝ) := by norm_cast; apply invertibleOfPos
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1)
rw :
  Finset.centroid ℝ univ s.points -ᵥ s.circumcenter =
    ∑ x : Fin (n + 2 + 1),
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) _ •
        (s.points x -ᵥ s.circumcenter)
⊢ (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
    ∑ i : Fin (n + 2 + 1), (s.points i -ᵥ s.circumcenter)

Tactic:
rw [smul_eq_iff_eq_invOf_smul, smul_sum]

Premises used: Finset.smul_sum, smul_eq_iff_eq_invOf_smul
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1)
rw :
  (affineCombination ℝ univ s.points : (a : Fin (n + 2 + 1) → ℝ) → P) (centroidWeights ℝ univ) -ᵥ s.circumcenter =
    ∑ x : Fin (n + 2 + 1),
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) _ •
        (s.points x -ᵥ s.circumcenter)
⊢ Finset.centroid ℝ univ s.points -ᵥ s.circumcenter =
    ∑ x : Fin (n + 2 + 1),
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) _ •
        (s.points x -ᵥ s.circumcenter)

Tactic:
rw [univ_centroid_eq, centroid_eq_affineCombination]

Premises used: Affine.Simplex.univ_centroid_eq, Affine.Simplex.centroid_eq_affineCombination
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1)
⊢ Eq (α := ℝ) (∑ i : Fin (n + 2 + 1), centroidWeights ℝ univ i) 1

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1)
rw :
  Eq.{u_1 + 1} (α := V) (∑ i : Fin (n + 2 + 1), centroidWeights ℝ univ i • (s.points i -ᵥ s.circumcenter))
    (∑ x : Fin (n + 2 + 1),
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) _ •
        (s.points x -ᵥ s.circumcenter))
⊢ (affineCombination ℝ univ s.points : (a : Fin (n + 2 + 1) → ℝ) → P) (centroidWeights ℝ univ) -ᵥ s.circumcenter =
    ∑ x : Fin (n + 2 + 1),
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) _ •
        (s.points x -ᵥ s.circumcenter)

Tactic:
rw [← Finset.sum_smul_vsub_const_eq_affineCombination_vsub _ _ _ _ (by simp)]

Premises used: Finset.sum_smul_vsub_const_eq_affineCombination_vsub
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1)
⊢ Eq.{u_1 + 1} (α := V) (∑ i : Fin (n + 2 + 1), centroidWeights ℝ univ i • (s.points i -ᵥ s.circumcenter))
    (∑ x : Fin (n + 2 + 1),
      @Invertible.invOf _ MulOne.toMul MulOne.toOne (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1) _ •
        (s.points x -ᵥ s.circumcenter))

Tactic:
simp only [centroidWeights_apply, card_univ, Fintype.card_fin, Nat.cast_add, Nat.cast_ofNat,
    Nat.cast_one, invOf_eq_inv]

Premises used: Finset.card_univ, Nat.cast_ofNat, Fintype.card_fin, Finset.centroidWeights_apply, Nat.cast_add, invOf_eq_inv, Nat.cast_one
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint

Tactic:
smul_vsub_vadd_mem _ _ (centroid_mem_affineSpan_of_card_eq_add_one ℝ _ (card_fin (n + 1)))
    s.circumcenter_mem_affineSpan s.circumcenter_mem_affineSpan

Premises used: Affine.Simplex.circumcenter_mem_affineSpan, Real, Set.Mem, AffineSubspace.smul_vsub_vadd_mem, Affine.Simplex.mongePoint, HAdd.hAdd, Finset.card_fin, centroid_mem_affineSpan_of_card_eq_add_one, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ Nonempty.{u_2 + 1} ↥S

Tactic:
haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty.{u_2 + 1} ↥S
simp_rw :
  (↑(HVAdd.hVAdd (β := ↥S)
          (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
            (Finset.centroid ℝ univ (s.restrict S hS).points -ᵥ (s.restrict S hS).circumcenter (n := n)))
          ((s.restrict S hS).circumcenter (n := n))) :
      P) =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) +ᵥ
      s.circumcenter
⊢ (↑((s.restrict S hS).mongePoint (n := n)) : P) = s.mongePoint

Tactic:
simp_rw [mongePoint]

Premises used: Affine.Simplex.mongePoint
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty.{u_2 + 1} ↥S
rw :
  (↑(HVAdd.hVAdd (β := ↥S)
          (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
            ((s.restrict S hS).centroid -ᵥ (s.restrict S hS).circumcenter (n := n)))
          ((s.restrict S hS).circumcenter (n := n))) :
      P) =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter
⊢ (↑(HVAdd.hVAdd (β := ↥S)
          (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
            (Finset.centroid ℝ univ (s.restrict S hS).points -ᵥ (s.restrict S hS).circumcenter (n := n)))
          ((s.restrict S hS).circumcenter (n := n))) :
      P) =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) +ᵥ
      s.circumcenter

Tactic:
rw [← Simplex.centroid, ← Simplex.centroid]

Premises used: Affine.Simplex.centroid
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty.{u_2 + 1} ↥S
⊢ (↑(HVAdd.hVAdd (β := ↥S)
          (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) •
            ((s.restrict S hS).centroid -ᵥ (s.restrict S hS).circumcenter (n := n)))
          ((s.restrict S hS).circumcenter (n := n))) :
      P) =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter

Tactic:
simp [centroid_restrict, circumcenter_restrict]

Premises used: Affine.Simplex.circumcenter_restrict, Affine.Simplex.centroid_restrict
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
simp_rw :
  HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s₁.points -ᵥ s₁.circumcenter) +ᵥ
      s₁.circumcenter =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s₂.points -ᵥ s₂.circumcenter) +ᵥ
      s₂.circumcenter
simp_rw₁ :
  HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s₂.points -ᵥ s₁.circumcenter) +ᵥ
      s₁.circumcenter =
    HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (Finset.centroid ℝ univ s₂.points -ᵥ s₂.circumcenter) +ᵥ
      s₂.circumcenter
⊢ s₁.mongePoint = s₂.mongePoint

Tactic:
simp_rw [mongePoint_eq_smul_vsub_vadd_circumcenter, centroid_eq_of_range_eq h,
    circumcenter_eq_of_range_eq h]

Premises used: Affine.Simplex.centroid_eq_of_range_eq, Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter, Affine.Simplex.circumcenter_eq_of_range_eq
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
n : ℕ
simp_rw : HMul.hMul (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 1) : ℝ)⁻¹ + HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) = 1
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex (n + 2), mongePointWeightsWithCircumcenter n i) 1

Tactic:
simp_rw [sum_pointsWithCircumcenter, mongePointWeightsWithCircumcenter, sum_const, card_fin,
    nsmul_eq_mul]

Premises used: Affine.Simplex.mongePointWeightsWithCircumcenter, Finset.card_fin, nsmul_eq_mul, Affine.Simplex.sum_pointsWithCircumcenter, Finset.sum_const
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
n : ℕ
simp : HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1 + -2 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ HMul.hMul (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 1) : ℝ)⁻¹ + HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) = 1

Tactic:
simp [field]
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + 1 + -2 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
rw :
  Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex (n + 2) → ℝ) → P)
        (HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 2 - 1) : ℝ) •
            HSub.hSub (α := PointsWithCircumcenterIndex (n + 2) → ℝ) (centroidWeightsWithCircumcenter univ)
              (circumcenterWeightsWithCircumcenter (n + 2)) +
          circumcenterWeightsWithCircumcenter (n + 2)) :
      P)
    ((affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex (n + 2) → ℝ) → P)
        (mongePointWeightsWithCircumcenter n) :
      P)
⊢ s.mongePoint =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex (n + 2) → ℝ) → P)
      (mongePointWeightsWithCircumcenter n)

Tactic:
rw [mongePoint_eq_smul_vsub_vadd_circumcenter,
    centroid_eq_affineCombination_of_pointsWithCircumcenter,
    circumcenter_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_vsub, ← map_smul,
    weightedVSub_vadd_affineCombination]

Premises used: Finset.affineCombination_vsub, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter, Finset.weightedVSub_vadd_affineCombination, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter, map_smul
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h :
  ∀ (i : PointsWithCircumcenterIndex (n + 2)),
    HAdd.hAdd (β := PointsWithCircumcenterIndex (n + 2) → ℝ)
        (HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 2 - 1) : ℝ) •
          HSub.hSub (α := PointsWithCircumcenterIndex (n + 2) → ℝ) (centroidWeightsWithCircumcenter univ)
            (circumcenterWeightsWithCircumcenter (n + 2)))
        (circumcenterWeightsWithCircumcenter (n + 2)) i =
      mongePointWeightsWithCircumcenter n i
⊢ Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex (n + 2) → ℝ) → P)
        (HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 2 - 1) : ℝ) •
            HSub.hSub (α := PointsWithCircumcenterIndex (n + 2) → ℝ) (centroidWeightsWithCircumcenter univ)
              (circumcenterWeightsWithCircumcenter (n + 2)) +
          circumcenterWeightsWithCircumcenter (n + 2)) :
      P)
    ((affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex (n + 2) → ℝ) → P)
        (mongePointWeightsWithCircumcenter n) :
      P)

Tactic:
congr with i
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i : PointsWithCircumcenterIndex (n + 2)
h :
  ∀ (a : Fin (n + 2 + 1)),
    HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 2 - 1) : ℝ) *
          (centroidWeightsWithCircumcenter univ (pointIndex a) -
            circumcenterWeightsWithCircumcenter (n + 2) (pointIndex a)) +
        circumcenterWeightsWithCircumcenter (n + 2) (pointIndex a) =
      mongePointWeightsWithCircumcenter n (pointIndex a)
h₁ :
  HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 2 - 1) : ℝ) *
        (centroidWeightsWithCircumcenter (n := n + 2) univ circumcenterIndex -
          circumcenterWeightsWithCircumcenter (n + 2) circumcenterIndex) +
      circumcenterWeightsWithCircumcenter (n + 2) circumcenterIndex =
    mongePointWeightsWithCircumcenter n circumcenterIndex
⊢ HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 2 - 1) : ℝ) *
        (centroidWeightsWithCircumcenter univ i - circumcenterWeightsWithCircumcenter (n + 2) i) +
      circumcenterWeightsWithCircumcenter (n + 2) i =
    mongePointWeightsWithCircumcenter n i

Tactic:
cases i
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
a : Fin (n + 2 + 1)
⊢ LE.le (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
a : Fin (n + 2 + 1)
⊢ HSub.hSub (α := ℕ) 2 1 = 1

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
⊢ LE.le (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
⊢ HSub.hSub (α := ℕ) 2 1 = 1

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
a : Fin (n + 2 + 1)
h :
  HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) (↑(n + 2 + 1) : ℝ)⁻¹ 0 + 0 =
    (↑(n + 1) : ℝ)⁻¹
⊢ HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 1) : ℝ) *
        HSub.hSub (α := ℝ)
          (if Membership.mem (γ := Finset (Fin (n + 2 + 1))) univ a then (↑(card (α := Fin (n + 2 + 1)) univ) : ℝ)⁻¹
          else 0)
          0 +
      0 =
    (↑(n + 1) : ℝ)⁻¹

Tactic:
rw [if_pos (mem_univ _), card_fin]

Premises used: Finset.mem_univ, if_pos, Finset.card_fin
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
a : Fin (n + 2 + 1)
⊢ HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) (↑(n + 2 + 1) : ℝ)⁻¹ 0 + 0 =
    (↑(n + 1) : ℝ)⁻¹

Tactic:
field
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
h : -1 + HAdd.hAdd (α := ℝ) (-2) (-(↑n : ℝ)) + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = -2
⊢ HDiv.hDiv (α := ℝ) (↑(n + 2 + 1) : ℝ) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 1 + 1 =
    HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ)

Tactic:
simp [field]
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
⊢ -1 + HAdd.hAdd (α := ℝ) (-2) (-(↑n : ℝ)) + HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 = -2

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.MongePoint
Goal:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
h₁ :
  ∀ (i : PointsWithCircumcenterIndex (n + 2)),
    mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i =
      HSub.hSub (β := PointsWithCircumcenterIndex (n + 2) → ℝ) (mongePointWeightsWithCircumcenter n)
        (centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ =
    mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ

Tactic:
ext i