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 + 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
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
⊢ -(∑ 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

Tactic:
rw [← sum_subset fs.subset_univ _]

Premises used: Finset.sum_subset, Finset.subset_univ
-- 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₁ 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 : 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
⊢ -(∑ 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:
simp_rw [fs, sum_insert (notMem_singleton.2 h), sum_singleton]

Premises used: Finset.notMem_singleton, Iff.mpr, Finset.sum_singleton, Finset.sum_insert
-- 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₁ 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₂
⊢ -((if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if True then 1 else 0) (if i₁ = i₂ then 1 else 0) *
                  (dist (s.points i₁) (s.points i₁) * dist (s.points i₁) (s.points i₁)) +
                (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if i₂ = i₁ then 1 else 0) (if True then 1 else 0) *
                  (dist (s.points i₁) (s.points i₂) * dist (s.points i₁) (s.points i₂)) +
              (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) +
            ((if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if True then 1 else 0) (if i₁ = i₂ then 1 else 0) *
                  (dist (s.points i₂) (s.points i₁) * dist (s.points i₂) (s.points i₁)) +
                (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if i₂ = i₁ then 1 else 0) (if True then 1 else 0) *
                  (dist (s.points i₂) (s.points i₂) * dist (s.points i₂) (s.points i₂)) +
              (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 [h, Ne.symm h, dist_comm (s.points i₁)]

Premises used: Affine.Simplex.points, Ne.symm, dist_comm
-- 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₁ 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₂
i : Fin (n + 3)
_ :
  Membership.mem (γ := Finset (Fin (n + 3))) univ i →
    i ∉ fs →
      (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) *
            HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
          (dist (s.points i₂) (s.points i) * dist (s.points i₂) (s.points i)) =
        0
⊢ Membership.mem (γ := Finset (Fin (n + 3))) univ i →
    i ∉ fs →
      (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) *
            HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
          (dist (s.points i₂) (s.points i) * dist (s.points i₂) (s.points i)) =
        0

Tactic:
_
-- 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₁ 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₂
i : Fin (n + 3)
h_1 : Membership.mem (γ := Finset (Fin (n + 3))) univ i
hi : i ∉ fs
⊢ (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) *
        HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
      (dist (s.points i₂) (s.points i) * dist (s.points i₂) (s.points i)) =
    0

Tactic:
simp [hfs i hi]
-- 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₁ 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₂
i : Fin (n + 3)
_ :
  Membership.mem (γ := Finset (Fin (n + 3))) univ i →
    i ∉ fs →
      (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
            HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
          (dist (s.points i₁) (s.points i) * dist (s.points i₁) (s.points i)) =
        0
⊢ Membership.mem (γ := Finset (Fin (n + 3))) univ i →
    i ∉ fs →
      (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
            HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
          (dist (s.points i₁) (s.points i) * dist (s.points i₁) (s.points i)) =
        0

Tactic:
_
-- 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₁ 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₂
i : Fin (n + 3)
h_1 : Membership.mem (γ := Finset (Fin (n + 3))) univ i
hi : i ∉ fs
⊢ (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
        HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
      (dist (s.points i₁) (s.points i) * dist (s.points i₁) (s.points i)) =
    0

Tactic:
simp [hfs i hi]
-- 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₁ 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₂
i : Fin (n + 3)
_ :
  Membership.mem (γ := Finset (Fin (n + 3))) univ i →
    i ∉ fs →
      HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points i) * dist s.circumcenter (s.points i)) =
        0
⊢ Membership.mem (γ := Finset (Fin (n + 3))) univ i →
    i ∉ fs →
      HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points i) * dist s.circumcenter (s.points i)) =
        0

Tactic:
_
-- 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₁ 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₂
i : Fin (n + 3)
h_1 : Membership.mem (γ := Finset (Fin (n + 3))) univ i
hi : i ∉ fs
⊢ HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) (if i = i₁ then 1 else 0) (if i = i₂ then 1 else 0) *
      (dist s.circumcenter (s.points i) * dist s.circumcenter (s.points i)) =
    0

Tactic:
simp [hfs i hi]
-- 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₁ 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₂
i : Fin (n + 3)
_ :
  Membership.mem (γ := Finset (Fin (n + 3))) univ i →
    i ∉ fs →
      Eq (α := ℝ)
        (∑ x : PointsWithCircumcenterIndex (n + 2),
          (if i = i₁ ∨ i = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
              (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x *
            (dist (s.points i) (s.pointsWithCircumcenter x) * dist (s.points i) (s.pointsWithCircumcenter x)))
        0
⊢ Membership.mem (γ := Finset (Fin (n + 3))) univ i →
    i ∉ fs →
      Eq (α := ℝ)
        (∑ x : PointsWithCircumcenterIndex (n + 2),
          (if i = i₁ ∨ i = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
              (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x *
            (dist (s.points i) (s.pointsWithCircumcenter x) * dist (s.points i) (s.pointsWithCircumcenter x)))
        0

Tactic:
_
-- 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₁ 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₂
i : Fin (n + 3)
h_1 : Membership.mem (γ := Finset (Fin (n + 3))) univ i
hi : i ∉ fs
⊢ Eq (α := ℝ)
    (∑ x : PointsWithCircumcenterIndex (n + 2),
      (if i = i₁ ∨ i = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
          (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x *
        (dist (s.points i) (s.pointsWithCircumcenter x) * dist (s.points i) (s.pointsWithCircumcenter x)))
    0

Tactic:
simp [hfs i hi]
-- 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₁ i₂ : Fin (n + 3)
⊢ s.mongePlane i₁ i₂ =
    mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ affineSpan ℝ (Set.range s.points)

Tactic:
rfl

Premises used: Affine.Simplex.mongePlane, rfl
-- 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
m n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (m + 3)
i₁ i₂ : Fin (m + 3)
⊢ n = m

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

Premises used: Iff.mpr, Fintype.card_eq, Nonempty.intro
-- 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
m n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (m + 3)
i₁ i₂ : Fin (m + 3)
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₂)
⊢ (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₂)

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

Premises used: rfl
-- 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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
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)
⊢ (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:
simp_rw [mongePlane, reindex_points, reindex_range_points, Function.comp_apply, centroid_def,
    reindex]

Premises used: Affine.Simplex.reindex, Affine.Simplex.mongePlane, Affine.Simplex.reindex_points, Function.comp_apply, Affine.Simplex.reindex_range_points, Finset.centroid_def
-- 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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
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)
⊢ 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:
congr 2
-- 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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ Eq.{u_2 + 1} (α := P)
    ((affineCombination ℝ
            (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))))ᶜ)
            (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))))ᶜ
            (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))) :
          (a : Fin (n + 3) → ℝ) → P)
        (Function.comp (β := Fin (n + 3)) (centroidWeights ℝ {i₁, i₂}ᶜ)
          (⇑e.toEmbedding : (a : Fin (n + 3)) → Fin (n + 3))) :
      P)

Tactic:
Finset.affineCombination_map {e.symm i₁, e.symm i₂}ᶜ e.toEmbedding _ _

Premises used: Compl.compl, Insert.insert, Finset.affineCombination_map, Equiv.toEmbedding, Equiv.symm, Singleton.singleton, DFunLike.coe