-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem mongePoint_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ}
    (s : Simplex ℝ P (n + 2)) :
    s.mongePoint =
      (univ : Finset (PointsWithCircumcenterIndex (n + 2))).affineCombination ℝ
        s.pointsWithCircumcenter (mongePointWeightsWithCircumcenter n)

Proof state:
case h.e_6.h.h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i : PointsWithCircumcenterIndex (n + 2)
⊢ ((↑(n + 2 + 1) / ↑(n + 2 - 1)) •
          (centroidWeightsWithCircumcenter univ - circumcenterWeightsWithCircumcenter (n + 2)) +
        circumcenterWeightsWithCircumcenter (n + 2))
      i =
    mongePointWeightsWithCircumcenter n i

Tactic:
rw [Pi.add_apply, Pi.smul_apply, smul_eq_mul, Pi.sub_apply]

Result:
case h.e_6.h.h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i : PointsWithCircumcenterIndex (n + 2)
⊢ ↑(n + 2 + 1) / ↑(n + 2 - 1) *
        (centroidWeightsWithCircumcenter univ i - circumcenterWeightsWithCircumcenter (n + 2) i) +
      circumcenterWeightsWithCircumcenter (n + 2) i =
    mongePointWeightsWithCircumcenter n i

Proof state:
case h.e_6.h.h.pointIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
a✝ : Fin (n + 2 + 1)
⊢ ↑(n + 2 + 1) / ↑(n + 1) * ((if a✝ ∈ univ then (↑(#univ))⁻¹ else 0) - 0) + 0 = (↑(n + 1))⁻¹

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

Result:
case h.e_6.h.h.pointIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
a✝ : Fin (n + 2 + 1)
⊢ ↑(n + 2 + 1) / ↑(n + 1) * (↑(n + 2 + 1))⁻¹ = (↑(n + 1))⁻¹

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter)
      ((↑(n + 2 + 1) / ↑(n + 2 - 1)) •
          (centroidWeightsWithCircumcenter univ - circumcenterWeightsWithCircumcenter (n + 2)) +
        circumcenterWeightsWithCircumcenter (n + 2)) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (mongePointWeightsWithCircumcenter n)

Tactic:
congr with i

Result:
case h.e_6.h.h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i : PointsWithCircumcenterIndex (n + 2)
⊢ ((↑(n + 2 + 1) / ↑(n + 2 - 1)) •
          (centroidWeightsWithCircumcenter univ - circumcenterWeightsWithCircumcenter (n + 2)) +
        circumcenterWeightsWithCircumcenter (n + 2))
      i =
    mongePointWeightsWithCircumcenter n i

Proof state:
case h.e_6.h.h.circumcenterIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
⊢ -1 + (-2 + -↑n) + (↑n + 1) = -2

Tactic:
ring

Result:
no goals

Proof state:
case h.e_6.h.h.pointIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
a✝ : Fin (n + 2 + 1)
⊢ ↑(n + 2 + 1) / ↑(n + 1) * (↑(n + 2 + 1))⁻¹ = (↑(n + 1))⁻¹

Tactic:
have hn3 : (n + 2 + 1 : ℝ) ≠ 0 := by norm_cast

Result:
case h.e_6.h.h.pointIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
a✝ : Fin (n + 2 + 1)
hn3 : ↑n + 2 + 1 ≠ 0
⊢ ↑(n + 2 + 1) / ↑(n + 1) * (↑(n + 2 + 1))⁻¹ = (↑(n + 1))⁻¹

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
a✝ : Fin (n + 2 + 1)
⊢ ↑n + 2 + 1 ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
case h.e_6.h.h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i : PointsWithCircumcenterIndex (n + 2)
hn1 : ↑n + 1 ≠ 0
⊢ ↑(n + 2 + 1) / ↑(n + 2 - 1) *
        (centroidWeightsWithCircumcenter univ i - circumcenterWeightsWithCircumcenter (n + 2) i) +
      circumcenterWeightsWithCircumcenter (n + 2) i =
    mongePointWeightsWithCircumcenter n i

Tactic:
cases i <;>
    simp_rw [centroidWeightsWithCircumcenter, circumcenterWeightsWithCircumcenter,
      mongePointWeightsWithCircumcenter] <;>
  rw [add_tsub_assoc_of_le (by decide : 1 ≤ 2), (by decide : 2 - 1 = 1)]

Result:
case h.e_6.h.h.pointIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
a✝ : Fin (n + 2 + 1)
⊢ ↑(n + 2 + 1) / ↑(n + 1) * ((if a✝ ∈ univ then (↑(#univ))⁻¹ else 0) - 0) + 0 = (↑(n + 1))⁻¹

case h.e_6.h.h.circumcenterIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
⊢ ↑(n + 2 + 1) / ↑(n + 1) * (0 - 1) + 1 = -2 / ↑(n + 1)

Proof state:
case h.e_6.h.h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i : PointsWithCircumcenterIndex (n + 2)
⊢ ↑(n + 2 + 1) / ↑(n + 2 - 1) *
        (centroidWeightsWithCircumcenter univ i - circumcenterWeightsWithCircumcenter (n + 2) i) +
      circumcenterWeightsWithCircumcenter (n + 2) i =
    mongePointWeightsWithCircumcenter n i

Tactic:
have hn1 : (n + 1 : ℝ) ≠ 0 := n.cast_add_one_ne_zero

Result:
case h.e_6.h.h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i : PointsWithCircumcenterIndex (n + 2)
hn1 : ↑n + 1 ≠ 0
⊢ ↑(n + 2 + 1) / ↑(n + 2 - 1) *
        (centroidWeightsWithCircumcenter univ i - circumcenterWeightsWithCircumcenter (n + 2) i) +
      circumcenterWeightsWithCircumcenter (n + 2) i =
    mongePointWeightsWithCircumcenter n i

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
⊢ 1 ≤ 2

Tactic:
decide

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
⊢ 2 - 1 = 1

Tactic:
decide

Result:
no goals

Proof state:
case h.e_6.h.h.circumcenterIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
⊢ ↑(n + 2 + 1) / ↑(n + 1) * (0 - 1) + 1 = -2 / ↑(n + 1)

Tactic:
simp (disch := field_simp_discharge) only
  [Nat.cast_add, Nat.cast_ofNat, Nat.cast_one, zero_sub, mul_neg, mul_one, neg_div',
  neg_add_rev, div_add', one_mul, eq_div_iff, div_mul_cancel₀]

Result:
case h.e_6.h.h.circumcenterIndex
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
hn1 : ↑n + 1 ≠ 0
⊢ -1 + (-2 + -↑n) + (↑n + 1) = -2