awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
i : Fin (n + 1)
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (pointWeightsWithCircumcenter i) =
    s.pointsWithCircumcenter (pointIndex i)
have affineCombination_of_eq_one_of_eq_zero : ∀ (i2 : PointsWithCircumcenterIndex n),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ i2 →
    i2 ≠ pointIndex i → pointWeightsWithCircumcenter i i2 = 0
Tactic: refine
    affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_univ _)
      (by simp [pointWeightsWithCircumcenter]) ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
i_1 : Fin (n + 1)
i : PointsWithCircumcenterIndex n
hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ i
hn : i ≠ pointIndex i_1
⊢ pointWeightsWithCircumcenter i_1 i = 0
have pointIndex : ∀ (a : Fin (n + 1)) (hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a))
  (hn : pointIndex a ≠ pointIndex i_1), pointWeightsWithCircumcenter i_1 (pointIndex a) = 0
Tactic: cases i
Cleared hypotheses: i, hi, hn
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
i_1 : Fin (n + 1)
i : PointsWithCircumcenterIndex n
hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ i
hn : i ≠ PointsWithCircumcenterIndex.pointIndex i_1
pointIndex :
  ∀ (a : Fin (n + 1))
    (hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (PointsWithCircumcenterIndex.pointIndex a))
    (hn : PointsWithCircumcenterIndex.pointIndex a ≠ PointsWithCircumcenterIndex.pointIndex i_1),
    pointWeightsWithCircumcenter i_1 (PointsWithCircumcenterIndex.pointIndex a) = 0
⊢ pointWeightsWithCircumcenter i_1 i = 0
have circumcenterIndex : ∀ (hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex)
  (hn : circumcenterIndex ≠ PointsWithCircumcenterIndex.pointIndex i_1),
  pointWeightsWithCircumcenter i_1 circumcenterIndex = 0
Tactic: cases i
Cleared hypotheses: i, hi, hn
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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
i a : Fin (n + 1)
hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a)
hn : pointIndex a ≠ pointIndex i
⊢ pointWeightsWithCircumcenter i (pointIndex a) = 0
have h : a ≠ i
Tactic: have h : _ ≠ i := fun h => hn (h ▸ rfl)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, centroidWeightsWithCircumcenter fs i) 1
have simp_rw : Eq (α := ℝ) (∑ x : Fin (n + 1), if x ∈ fs then (↑(#fs) : ℝ)⁻¹ else 0)
  (∑ i : Fin (n + 1), (↑fs : Set (Fin (n + 1))).indicator (centroidWeights ℝ fs) i)
Tactic: simp_rw [sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter, add_zero, ←
    fs.sum_centroidWeights_eq_one_of_nonempty ℝ h, ← sum_indicator_subset _ fs.subset_univ]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
fs : Finset (Fin (n + 1))
⊢ Finset.centroid ℝ fs s.points =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (centroidWeightsWithCircumcenter fs)
have simp_rw : HVAdd.hVAdd.{u_1, u_2, u_2} (α := V) (β := P)
    (∑ x : Fin (n + 1),
      HSMul.hSMul (α := ℝ) (if x ∈ (↑fs : Set (Fin (n + 1))) then Function.const (Fin (n + 1)) (↑(#fs) : ℝ)⁻¹ x else 0)
        (s.points x -ᵥ Classical.choice sorry))
    (Classical.choice sorry) =
  HVAdd.hVAdd.{u_1, u_2, u_2} (α := V) (β := P)
    (∑ x : Fin (n + 1), HSMul.hSMul (α := ℝ) (if x ∈ fs then (↑(#fs) : ℝ)⁻¹ else 0) (s.points x -ᵥ Classical.choice sorry))
    (Classical.choice sorry)
Tactic: simp_rw [centroid_def, affineCombination_apply, weightedVSubOfPoint_apply,
    sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter,
    pointsWithCircumcenter_point, zero_smul, add_zero, centroidWeights,
    ← sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (#fs : ℝ)⁻¹)
      (fun i wi => wi • (s.points i -ᵥ Classical.choice AddTorsor.nonempty)) fs.subset_univ fun _ =>
      zero_smul ℝ _,
    Set.indicator_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, circumcenterWeightsWithCircumcenter n i) 1
have h : ∀ (j : PointsWithCircumcenterIndex n),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
    circumcenterWeightsWithCircumcenter n j =
      if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
Tactic: convert! sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
h :
  ∀ (j : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
      circumcenterWeightsWithCircumcenter n j =
        if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, circumcenterWeightsWithCircumcenter n i) 1
have h₁ : Eq (α := ℝ) 1
  (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex then
    Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
  else 0)
Tactic: convert! sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
j : PointsWithCircumcenterIndex n
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j
⊢ circumcenterWeightsWithCircumcenter n j =
    if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
have h : ∀ (a : Fin (n + 1)),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a) →
    circumcenterWeightsWithCircumcenter n (pointIndex a) =
      if pointIndex a = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex a) else 0
Tactic: cases j
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
j : PointsWithCircumcenterIndex n
h_1 : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j
h :
  ∀ (a : Fin (n + 1)),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a) →
      circumcenterWeightsWithCircumcenter n (pointIndex a) =
        if pointIndex a = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex a) else 0
⊢ circumcenterWeightsWithCircumcenter n j =
    if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
have h₁ : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex →
  circumcenterWeightsWithCircumcenter n circumcenterIndex =
    if Eq (α := PointsWithCircumcenterIndex n) circumcenterIndex circumcenterIndex then
      Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
    else 0
Tactic: cases j
Cleared hypotheses: j, h_1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, circumcenterWeightsWithCircumcenter n i) 1
have h : ∀ (j : PointsWithCircumcenterIndex n),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
    circumcenterWeightsWithCircumcenter n j =
      if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
Tactic: classical
  convert! sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [circumcenterWeightsWithCircumcenter]
  · simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
h :
  ∀ (j : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
      circumcenterWeightsWithCircumcenter n j =
        if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, circumcenterWeightsWithCircumcenter n i) 1
have h₁ : Eq (α := ℝ) 1
  (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex then
    Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
  else 0)
Tactic: classical
  convert! sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [circumcenterWeightsWithCircumcenter]
  · simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
⊢ s.circumcenter =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n)
have rw : s.pointsWithCircumcenter circumcenterIndex =
  (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
    (circumcenterWeightsWithCircumcenter n)
Tactic: rw [← pointsWithCircumcenter_eq_circumcenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
⊢ s.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n)
have symm : (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
    (circumcenterWeightsWithCircumcenter n) =
  s.pointsWithCircumcenter circumcenterIndex
Tactic: symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n) =
    s.pointsWithCircumcenter circumcenterIndex
have refine : ∀ (i2 : PointsWithCircumcenterIndex n),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ i2 →
    i2 ≠ circumcenterIndex → circumcenterWeightsWithCircumcenter n i2 = 0
Tactic: refine affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_univ _) rfl ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i) 1
have simp_rw : HSMul.hSMul (β := ℝ)
        (card (α := Fin (n + 1))
          ((if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) ∪
            if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
        1 +
      HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
    -1 =
  1
Tactic: simp_rw [sum_pointsWithCircumcenter, reflectionCircumcenterWeightsWithCircumcenter, sum_ite,
    sum_const, filter_or, filter_eq']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ HSMul.hSMul (β := ℝ)
          (card (α := Fin (n + 1))
            ((if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) ∪
              if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
          1 +
        HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
      -1 =
    1
have rw : HSMul.hSMul (β := ℝ)
        (card (α := Fin (n + 1)) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) +
          card (α := Fin (n + 1)) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
        1 +
      HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
    -1 =
  1
Tactic: rw [card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
rw :
  HSMul.hSMul (β := ℝ)
          (card (α := Fin (n + 1)) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) +
            card (α := Fin (n + 1)) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
          1 +
        HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
      -1 =
    1
⊢ HSMul.hSMul (β := ℝ)
          (card (α := Fin (n + 1))
            ((if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) ∪
              if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
          1 +
        HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
      -1 =
    1
have rw₁ : Disjoint (α := Finset (Fin (n + 1))) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅)
  (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅)
Tactic: rw [card_union_of_disjoint]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ Eq (α := P) ((reflection (affineSpan ℝ (s.points '' {i₁, i₂})) : (a : P) → P) s.circumcenter : P)
    ((affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
        (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) :
      P)
have hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
Tactic: have hc : #{i₁, i₂} = 2 := by simp [h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
⊢ Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
have h₁ : W = affineSpan ℝ (Set.range (s.face hc).points)
Tactic: apply eq_orthogonalProjection_of_eq_subspace
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
⊢ Eq (α := P) ((reflection (affineSpan ℝ (s.points '' {i₁, i₂})) : (a : P) → P) s.circumcenter : P)
    ((affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
        (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) :
      P)
have h_faces : Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
  (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points))) s.circumcenter) :
    P)
Tactic: have h_faces :
    (orthogonalProjection W s.circumcenter : P) =
      ↑((s.face hc).orthogonalProjectionSpan s.circumcenter) := by
    apply eq_orthogonalProjection_of_eq_subspace
    simp [W]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
⊢ Eq (α := P) ((reflection (affineSpan ℝ (s.points '' {i₁, i₂})) : (a : P) → P) s.circumcenter : P)
    ((affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
        (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) :
      P)
have rw : ∑ i : Fin (n + 1),
      (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
              centroidWeightsWithCircumcenter {i₁, i₂} -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
          (pointIndex i) •
        (s.pointsWithCircumcenter (pointIndex i) -ᵥ Classical.choice sorry) +
    (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
            centroidWeightsWithCircumcenter {i₁, i₂} -
          reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
        circumcenterIndex •
      (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice sorry) =
  0
Tactic: rw [reflection_apply', h_faces, s.orthogonalProjection_circumcenter hc,
    circumcenter_eq_centroid, s.face_centroid_eq_centroid hc,
    centroid_eq_affineCombination_of_pointsWithCircumcenter,
    circumcenter_eq_affineCombination_of_pointsWithCircumcenter, ← @vsub_eq_zero_iff_eq V,
    affineCombination_vsub, weightedVSub_vadd_affineCombination, affineCombination_vsub,
    weightedVSub_apply, sum_pointsWithCircumcenter]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
⊢ ∑ i : Fin (n + 1),
        (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
                centroidWeightsWithCircumcenter {i₁, i₂} -
              reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
            (pointIndex i) •
          (s.pointsWithCircumcenter (pointIndex i) -ᵥ Classical.choice ⋯) +
      (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
              centroidWeightsWithCircumcenter {i₁, i₂} -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
          circumcenterIndex •
        (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) =
    0
have simp_rw : Eq.{u_1 + 1} (α := V)
  (∑ x : Fin (n + 1),
    ((if Membership.mem (γ := Finset (Fin (n + 1))) {i₁, i₂} x then
        HAdd.hAdd (α := ℝ) (↑2 : ℝ)⁻¹ (↑2 : ℝ)⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice sorry)
      else 0) -
      if x = i₁ ∨ x = i₂ then HSMul.hSMul (α := ℝ) 1 (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice sorry)
      else 0))
  0
Tactic: simp_rw [Pi.sub_apply, Pi.add_apply, Pi.sub_apply, sub_smul, add_smul, sub_smul,
    centroidWeightsWithCircumcenter, circumcenterWeightsWithCircumcenter,
    reflectionCircumcenterWeightsWithCircumcenter, ite_smul, zero_smul, sub_zero,
    apply_ite₂ (· + ·), add_zero, ← add_smul, hc, zero_sub, neg_smul, sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
⊢ Eq.{u_1 + 1} (α := V)
    (∑ x : Fin (n + 1),
      ((if Membership.mem (γ := Finset (Fin (n + 1))) {i₁, i₂} x then
          HAdd.hAdd (α := ℝ) (↑2 : ℝ)⁻¹ (↑2 : ℝ)⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
        else 0) -
        if x = i₁ ∨ x = i₂ then HSMul.hSMul (α := ℝ) 1 (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
        else 0))
    0
have h₁ : ∀ (x : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) univ x →
    ((if Membership.mem (γ := Finset (Fin (n + 1))) {i₁, i₂} x then
          HAdd.hAdd (α := ℝ) (↑2 : ℝ)⁻¹ (↑2 : ℝ)⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice sorry)
        else 0) -
        if x = i₁ ∨ x = i₂ then HSMul.hSMul (α := ℝ) 1 (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice sorry)
        else 0) =
      0
Tactic: convert! sum_const_zero
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
⊢ Cospherical ps ↔ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
have mp : Cospherical ps → ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
mp : Cospherical ps → ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
⊢ Cospherical ps ↔ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
have mpr : (∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius) → Cospherical ps
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
c : P
hcr : ∃ (radius : ℝ), ∀ p ∈ ps, dist p c = radius
⊢ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
have hcr₁ : ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) c) : P) = r
Tactic: rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq h c] at hcr
Cleared hypotheses: hcr