-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub {n : ℕ} {i₁ i₂ : Fin (n + 3)}
    (h : i₁ ≠ i₂) :
    mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ =
      mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ

Proof state:
case h.pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ (pointIndex i) =
    (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) (pointIndex i)

Tactic:
rw [Pi.sub_apply, mongePointWeightsWithCircumcenter, centroidWeightsWithCircumcenter,
  mongePointVSubFaceCentroidWeightsWithCircumcenter]

Result:
case h.pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) = (↑(n + 1))⁻¹ - if i ∈ {i₁, i₂}ᶜ then (↑(#{i₁, i₂}ᶜ))⁻¹ else 0

Proof state:
case h.pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
hu : #{i₁, i₂}ᶜ = n + 1
⊢ (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) = (↑(n + 1))⁻¹ - if i ∈ {i₁, i₂}ᶜ then (↑(#{i₁, i₂}ᶜ))⁻¹ else 0

Tactic:
rw [hu]

Result:
case h.pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
hu : #{i₁, i₂}ᶜ = n + 1
⊢ (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) = (↑(n + 1))⁻¹ - if i ∈ {i₁, i₂}ᶜ then (↑(n + 1))⁻¹ else 0

Proof state:
case h.pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
hu : #{i₁, i₂}ᶜ = n + 1
⊢ (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) = (↑(n + 1))⁻¹ - if i ∈ {i₁, i₂}ᶜ then (↑(n + 1))⁻¹ else 0

Tactic:
by_cases hi : i = i₁ ∨ i = i₂ <;> simp [compl_eq_univ_sdiff, hi]

Result:
no goals

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ =
    mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ

Tactic:
ext i

Result:
case h
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : PointsWithCircumcenterIndex (n + 2)
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i =
    (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i

Proof state:
case h
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : PointsWithCircumcenterIndex (n + 2)
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i =
    (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i

Tactic:
obtain i | i := i

Result:
case h.pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ (pointIndex i) =
    (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) (pointIndex i)

case h.circumcenterIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ circumcenterIndex =
    (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) circumcenterIndex

Proof state:
case h.pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) = (↑(n + 1))⁻¹ - if i ∈ {i₁, i₂}ᶜ then (↑(#{i₁, i₂}ᶜ))⁻¹ else 0

Tactic:
have hu : #{i₁, i₂}ᶜ = n + 1 := by
  simp [card_compl, Fintype.card_fin, h]

Result:
case h.pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
hu : #{i₁, i₂}ᶜ = n + 1
⊢ (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) = (↑(n + 1))⁻¹ - if i ∈ {i₁, i₂}ᶜ then (↑(#{i₁, i₂}ᶜ))⁻¹ else 0

Proof state:
case h.circumcenterIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ circumcenterIndex =
    (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) circumcenterIndex

Tactic:
simp [mongePointWeightsWithCircumcenter, centroidWeightsWithCircumcenter,
  mongePointVSubFaceCentroidWeightsWithCircumcenter]

Result:
no goals

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ #{i₁, i₂}ᶜ = n + 1

Tactic:
simp [card_compl, Fintype.card_fin, h]

Result:
no goals