awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs :
  Eq (α := ℝ)
    (∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i) 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            (∑ x_1 : Fin (n + 2 + 1),
                (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if x_1 = i₁ then 1 else 0) (if x_1 = i₂ then 1 else 0) *
                  (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x : Fin (n + 2 + 1),
              HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                  HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 0 *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0
have neg : -(∑ x ∈ fs,
          (∑ x_1 : Fin (n + 2 + 1),
              (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                  HSub.hSub (α := ℝ) (if x_1 = i₁ then 1 else 0) (if x_1 = i₂ then 1 else 0) *
                (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
            (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
              (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
        (∑ x ∈ fs,
            HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
              (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
          HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 0 *
            (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
    2 =
  0
Tactic: rw [← sum_subset fs.subset_univ _]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs :
  Eq (α := ℝ)
    (∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i) 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
neg :
  -(∑ x ∈ fs,
            (∑ x_1 : Fin (n + 2 + 1),
                (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if x_1 = i₁ then 1 else 0) (if x_1 = i₂ then 1 else 0) *
                  (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x ∈ fs,
              HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                  HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 0 *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0
⊢ -(∑ x ∈ fs,
            (∑ x_1 : Fin (n + 2 + 1),
                (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if x_1 = i₁ then 1 else 0) (if x_1 = i₂ then 1 else 0) *
                  (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x : Fin (n + 2 + 1),
              HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                  HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 0 *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0
have rw : ∀ (x : Fin (n + 3)),
  Membership.mem (γ := Finset (Fin (n + 3))) univ x →
    x ∉ fs →
      HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) =
        0
Tactic: rw [← sum_subset fs.subset_univ _]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs :
  Eq (α := ℝ)
    (∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i) 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            (∑ x_1 : Fin (n + 2 + 1),
                (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if x_1 = i₁ then 1 else 0) (if x_1 = i₂ then 1 else 0) *
                  (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x ∈ fs,
              HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                  HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 0 *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0
have neg : -(∑ x : Fin (n + 2 + 1),
              (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                  HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                (dist (s.points i₁) (s.points x) * dist (s.points i₁) (s.points x)) +
            (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
              (dist (s.points i₁) s.circumcenter * dist (s.points i₁) s.circumcenter) +
          (∑ x : Fin (n + 2 + 1),
              (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) *
                  HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                (dist (s.points i₂) (s.points x) * dist (s.points i₂) (s.points x)) +
            (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
              (dist (s.points i₂) s.circumcenter * dist (s.points i₂) s.circumcenter)) +
        (HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                HSub.hSub (α := ℝ) (if True then 1 else 0) (if i₁ = i₂ then 1 else 0) *
              (dist s.circumcenter (s.points i₁) * dist s.circumcenter (s.points i₁)) +
            HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                HSub.hSub (α := ℝ) (if i₂ = i₁ then 1 else 0) (if True then 1 else 0) *
              (dist s.circumcenter (s.points i₂) * dist s.circumcenter (s.points i₂)) +
          HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 0 *
            (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
    2 =
  0
Tactic: simp_rw [fs, sum_insert (notMem_singleton.2 h), sum_singleton]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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
m n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (m + 3)
i₁ i₂ : Fin (m + 3)
⊢ (s.reindex e).mongePlane i₁ i₂ =
    s.mongePlane ((e.symm : (a : Fin (m + 3)) → Fin (n + 3)) i₁) ((e.symm : (a : Fin (m + 3)) → Fin (n + 3)) i₂)
have obtain : ∀ (e : Fin (n + 3) ≃ Fin (n + 3)) (i₁ i₂ : Fin (n + 3)),
  (s.reindex e).mongePlane i₁ i₂ =
    s.mongePlane ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂)
Tactic: obtain rfl : n = m := by simpa using Fintype.card_eq.2 ⟨e⟩
Cleared hypotheses: m, e, i₁, i₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ (s.reindex e).mongePlane i₁ i₂ =
    s.mongePlane ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂)
have simp_rw : Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
  (mk'
        ((affineCombination ℝ {i₁, i₂}ᶜ (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1))) :
            (a : Fin (n + 3) → ℝ) → P)
          (centroidWeights ℝ {i₁, i₂}ᶜ))
        (ℝ ∙
            (s.points ((e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1)) i₁) -ᵥ
              s.points ((e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1)) i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points) :
    AffineSubspace ℝ P)
  (mk'
        ((affineCombination ℝ
              (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                  (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
              s.points :
            (a : Fin (n + 3) → ℝ) → P)
          (centroidWeights ℝ
            (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ))
        (ℝ ∙
            (s.points ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁) -ᵥ
              s.points ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points) :
    AffineSubspace ℝ P)
Tactic: simp_rw [mongePlane, reindex_points, reindex_range_points, Function.comp_apply, centroid_def,
    reindex]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ Eq.{u_2 + 1} (α := AffineSubspace ℝ P)
    (mk'
          ((affineCombination ℝ {i₁, i₂}ᶜ (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1))) :
              (a : Fin (n + 3) → ℝ) → P)
            (centroidWeights ℝ {i₁, i₂}ᶜ))
          (ℝ ∙
              (s.points ((e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1)) i₁) -ᵥ
                s.points ((e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1)) i₂)))ᗮ ⊓
        affineSpan ℝ (Set.range s.points) :
      AffineSubspace ℝ P)
    (mk'
          ((affineCombination ℝ
                (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                    (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
                s.points :
              (a : Fin (n + 3) → ℝ) → P)
            (centroidWeights ℝ
              (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                  (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ))
          (ℝ ∙
              (s.points ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁) -ᵥ
                s.points ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂)))ᗮ ⊓
        affineSpan ℝ (Set.range s.points) :
      AffineSubspace ℝ P)
have e_a : Eq.{u_2 + 1} (α := P)
  ((affineCombination ℝ {i₁, i₂}ᶜ (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1))) :
        (a : Fin (n + 3) → ℝ) → P)
      (centroidWeights ℝ {i₁, i₂}ᶜ) :
    P)
  ((affineCombination ℝ
          (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
              (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
          s.points :
        (a : Fin (n + 3) → ℝ) → P)
      (centroidWeights ℝ
        (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
            (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ) :
    P)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ {i₁, i₂}ᶜ (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1))) :
          (a : Fin (n + 3) → ℝ) → P)
        (centroidWeights ℝ {i₁, i₂}ᶜ) :
      P)
    ((affineCombination ℝ
            (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
            s.points :
          (a : Fin (n + 3) → ℝ) → P)
        (centroidWeights ℝ
          (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
              (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ) :
      P)
have h : {i₁, i₂}ᶜ =
  Finset.map e.toEmbedding
    (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
Tactic: convert! Finset.affineCombination_map {e.symm i₁, e.symm i₂}ᶜ e.toEmbedding _ _ using 3
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
h :
  {i₁, i₂}ᶜ =
    Finset.map e.toEmbedding
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
⊢ Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ {i₁, i₂}ᶜ (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1))) :
          (a : Fin (n + 3) → ℝ) → P)
        (centroidWeights ℝ {i₁, i₂}ᶜ) :
      P)
    ((affineCombination ℝ
            (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
            s.points :
          (a : Fin (n + 3) → ℝ) → P)
        (centroidWeights ℝ
          (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
              (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ) :
      P)
have h₁ : s.points =
  Function.comp (β := Fin (n + 3)) (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1)))
    (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3))
Tactic: convert! Finset.affineCombination_map {e.symm i₁, e.symm i₂}ᶜ e.toEmbedding _ _ using 3
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
h :
  {i₁, i₂}ᶜ =
    Finset.map e.toEmbedding
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
h₁ :
  s.points =
    Function.comp (β := Fin (n + 3)) (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1)))
      (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3))
⊢ Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ {i₁, i₂}ᶜ (s.points ∘ (⇑e.symm : (a : Fin (n + 2 + 1)) → Fin (n + 2 + 1))) :
          (a : Fin (n + 3) → ℝ) → P)
        (centroidWeights ℝ {i₁, i₂}ᶜ) :
      P)
    ((affineCombination ℝ
            (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
            s.points :
          (a : Fin (n + 3) → ℝ) → P)
        (centroidWeights ℝ
          (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
              (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ) :
      P)
have h₂ : Eq (α := Fin (n + 3) → ℝ)
  (centroidWeights ℝ
    (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ)
  (Function.comp (β := Fin (n + 3)) (centroidWeights ℝ {i₁, i₂}ᶜ) (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3)))
Tactic: convert! Finset.affineCombination_map {e.symm i₁, e.symm i₂}ᶜ e.toEmbedding _ _ using 3
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ {i₁, i₂}ᶜ =
    Finset.map e.toEmbedding
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
have h : ∀ (i : Fin (n + 3)),
  Membership.mem (γ := Finset (Fin (n + 3))) {i₁, i₂}ᶜ i ↔
    i ∈
      Finset.map e.toEmbedding
        (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
            (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ Eq (α := Fin (n + 3) → ℝ)
    (centroidWeights ℝ
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))ᶜ)
    (Function.comp (β := Fin (n + 3)) (centroidWeights ℝ {i₁, i₂}ᶜ) (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3)))
have h : Eq (α := Fin (n + 3) → ℝ)
  (Function.const (Fin (n + 3))
    (↑(Fintype.card (Fin (n + 3)) -
            card (α := Fin (n + 3))
              (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))) :
        ℝ)⁻¹)
  (Function.const (Fin (n + 3)) (↑(Fintype.card (Fin (n + 3)) - card (α := Fin (n + 3)) {i₁, i₂}) : ℝ)⁻¹)
Tactic: simp_rw [centroidWeights, Function.const_comp, Finset.card_compl]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ Eq (α := Fin (n + 3) → ℝ)
    (Function.const (Fin (n + 3))
      (↑(Fintype.card (Fin (n + 3)) -
              card (α := Fin (n + 3))
                (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
                  (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3))))) :
          ℝ)⁻¹)
    (Function.const (Fin (n + 3)) (↑(Fintype.card (Fin (n + 3)) - card (α := Fin (n + 3)) {i₁, i₂}) : ℝ)⁻¹)
have h : card (α := Fin (n + 3))
    (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
      (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
  card (α := Fin (n + 3)) {i₁, i₂}
Tactic: congr 4
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ card (α := Fin (n + 3))
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
    card (α := Fin (n + 3)) {i₁, i₂}
have pos : ∀ (h : i₁ = i₂),
  card (α := Fin (n + 3))
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
    card (α := Fin (n + 3)) {i₁, i₂}
Tactic: by_cases h : i₁ = i₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
pos :
  ∀ (h : i₁ = i₂),
    card (α := Fin (n + 3))
        (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
          (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
      card (α := Fin (n + 3)) {i₁, i₂}
⊢ card (α := Fin (n + 3))
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
    card (α := Fin (n + 3)) {i₁, i₂}
have neg : ∀ (h : ¬i₁ = i₂),
  card (α := Fin (n + 3))
      (insert (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₁ : Fin (n + 3))
        (singleton (α := Fin (n + 3)) ((e.symm : (a : Fin (n + 3)) → Fin (n + 3)) i₂ : Fin (n + 3)))) =
    card (α := Fin (n + 3)) {i₁, i₂}
Tactic: by_cases h : i₁ = i₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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₁ i₂ : Fin (n + 3)
⊢ Eq (α := AffineSubspace ℝ P)
    (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ affineSpan ℝ (Set.range s.points))
    (mk' (Finset.centroid ℝ {i₂, i₁}ᶜ s.points) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁))ᗮ ⊓ affineSpan ℝ (Set.range s.points))
have e_a : Eq (α := Finset (Fin (n + 3))) {i₁, i₂}ᶜ {i₂, i₁}ᶜ
Tactic: congr 3