awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
⊢ s₁.circumcenter = s₂.circumcenter
have hs : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s₂.points)) s₁.circumcenter
Tactic: have hs : s₁.circumcenter ∈ affineSpan ℝ (Set.range s₂.points) :=
    h ▸ s₁.circumcenter_mem_affineSpan
-- 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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
hs : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s₂.points)) s₁.circumcenter
i : Fin (n + 1)
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius
have hi : s₂.points i ∈ Set.range s₂.points
Tactic: have hi : s₂.points i ∈ Set.range s₂.points := Set.mem_range_self _
-- 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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
hs : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s₂.points)) s₁.circumcenter
i : Fin (n + 1)
hi : s₂.points i ∈ Set.range s₂.points
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius
have hi₁ : ∃ (y : Fin (n + 1)), s₁.points y = s₂.points i
Tactic: rw [← h, Set.mem_range] at hi
Cleared hypotheses: hi
-- 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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
hs : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s₂.points)) s₁.circumcenter
i : Fin (n + 1)
hi : ∃ (y : Fin (n + 1)), s₁.points y = s₂.points i
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius
have rcases : ∀ (j : Fin (n + 1)) (hj : s₁.points j = s₂.points i), dist (s₂.points i) s₁.circumcenter = s₁.circumradius
Tactic: rcases hi with ⟨j, hj⟩
Cleared hypotheses: hi
-- 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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
hs : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s₂.points)) s₁.circumcenter
i j : Fin (n + 1)
hj : s₁.points j = s₂.points i
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius
have rw : dist (s₁.points j) s₁.circumcenter = s₁.circumradius
Tactic: rw [← hj, s₁.dist_circumcenter_eq_circumradius j]
-- 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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
hs : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s₂.points)) s₁.circumcenter
i j : Fin (n + 1)
hj : s₁.points j = s₂.points i
rw : dist (s₁.points j) s₁.circumcenter = s₁.circumradius
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius
have rw₁ : s₁.circumradius = s₁.circumradius
Tactic: rw [← hj, s₁.dist_circumcenter_eq_circumradius j]
-- 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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
hs : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s₂.points)) s₁.circumcenter
⊢ s₁.circumcenter = s₂.circumcenter
have hr : ∀ (i : Fin (n + 1)), dist (s₂.points i) s₁.circumcenter = s₁.circumradius
Tactic: have hr : ∀ i, dist (s₂.points i) s₁.circumcenter = s₁.circumradius := by
    intro i
    have hi : s₂.points i ∈ Set.range s₂.points := Set.mem_range_self _
    rw [← h, Set.mem_range] at hi
    rcases hi with ⟨j, hj⟩
    rw [← hj, s₁.dist_circumcenter_eq_circumradius j]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
⊢ univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have h : ∀ (x : PointsWithCircumcenterIndex n),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ x ↔
    x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
⊢ Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ x ↔
    x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have h : ∀ (h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ x),
  x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
Tactic: refine ⟨fun h => ?_, fun _ => mem_univ _⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ x
⊢ x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have h₁ : ∀ (i : Fin (n + 1)) (h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i)),
  pointIndex i ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
Tactic: obtain i | - := x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ x
h₁ :
  ∀ (i : Fin (n + 1)) (h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i)),
    pointIndex i ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have h₂ : ∀ (h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex),
  circumcenterIndex ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
Tactic: obtain i | - := x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
Tactic: have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have change : ∑ i : PointsWithCircumcenterIndex n, f i =
  ∑ i : Fin (n + 1), f ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) i) +
    f circumcenterIndex
Tactic: change _ = (∑ i, f (pointIndexEmbedding n i)) + _
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i : PointsWithCircumcenterIndex n, f i =
    ∑ i : Fin (n + 1), f ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) i) +
      f circumcenterIndex
have rw : circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ
Tactic: rw [add_comm, h, ← sum_map, sum_insert]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ
have simp_rw : ∀ (x : Fin (n + 1)),
  ¬(Membership.mem (γ := Finset (Fin (n + 1))) univ x ∧
      Eq (α := PointsWithCircumcenterIndex n)
        ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) x : PointsWithCircumcenterIndex n)
        (circumcenterIndex : PointsWithCircumcenterIndex n))
Tactic: simp_rw [Finset.mem_map, not_exists]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have have : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
Tactic: classical
  have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
  change _ = (∑ i, f (pointIndexEmbedding n i)) + _
  rw [add_comm, h, ← sum_map, sum_insert]
  simp_rw [Finset.mem_map, not_exists]
  rintro x ⟨_, h⟩
  injection h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
have : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have have₁ : ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
  ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
Tactic: classical
  have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
  change _ = (∑ i, f (pointIndexEmbedding n i)) + _
  rw [add_comm, h, ← sum_map, sum_insert]
  simp_rw [Finset.mem_map, not_exists]
  rintro x ⟨_, h⟩
  injection h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
have : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₁ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₂ : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₃ have₄ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have have₅ : ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
  ∑ i : PointsWithCircumcenterIndex n, f i =
    ∑ i : Fin (n + 1), f ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) i) +
      f circumcenterIndex
Tactic: classical
  have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
  change _ = (∑ i, f (pointIndexEmbedding n i)) + _
  rw [add_comm, h, ← sum_map, sum_insert]
  simp_rw [Finset.mem_map, not_exists]
  rintro x ⟨_, h⟩
  injection h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
have : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₁ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₂ : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₃ have₄ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₅ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i =
      ∑ i : Fin (n + 1), f ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) i) +
        f circumcenterIndex
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have have₆ : ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
  circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ
Tactic: classical
  have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
  change _ = (∑ i, f (pointIndexEmbedding n i)) + _
  rw [add_comm, h, ← sum_map, sum_insert]
  simp_rw [Finset.mem_map, not_exists]
  rintro x ⟨_, h⟩
  injection h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
have : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₁ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₂ : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₃ have₄ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₅ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i =
      ∑ i : Fin (n + 1), f ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) i) +
        f circumcenterIndex
have₆ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have have₇ : ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)) (x : Fin (n + 1)),
  ¬(Membership.mem (γ := Finset (Fin (n + 1))) univ x ∧
      Eq (α := PointsWithCircumcenterIndex n)
        ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) x : PointsWithCircumcenterIndex n)
        (circumcenterIndex : PointsWithCircumcenterIndex n))
Tactic: classical
  have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
  change _ = (∑ i, f (pointIndexEmbedding n i)) + _
  rw [add_comm, h, ← sum_map, sum_insert]
  simp_rw [Finset.mem_map, not_exists]
  rintro x ⟨_, h⟩
  injection h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
have : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₁ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₂ : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₃ have₄ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₅ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i =
      ∑ i : Fin (n + 1), f ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) i) +
        f circumcenterIndex
have₆ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ
have₇ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)) (x : Fin (n + 1)),
    ¬(Membership.mem (γ := Finset (Fin (n + 1))) univ x ∧
        Eq (α := PointsWithCircumcenterIndex n)
          ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) x :
            PointsWithCircumcenterIndex n)
          (circumcenterIndex : PointsWithCircumcenterIndex n))
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have have₈ : ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)) (x : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) univ x →
    ∀
      (h :
        Eq (α := PointsWithCircumcenterIndex n)
          ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) x :
            PointsWithCircumcenterIndex n)
          (circumcenterIndex : PointsWithCircumcenterIndex n)),
      False
Tactic: classical
  have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
  change _ = (∑ i, f (pointIndexEmbedding n i)) + _
  rw [add_comm, h, ← sum_map, sum_insert]
  simp_rw [Finset.mem_map, not_exists]
  rintro x ⟨_, h⟩
  injection h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := ℝ) (∑ j : PointsWithCircumcenterIndex n, pointWeightsWithCircumcenter i j) 1
have h : ∀ (j : PointsWithCircumcenterIndex n),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
    pointWeightsWithCircumcenter i j =
      if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
Tactic: convert! sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h :
  ∀ (j : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
      pointWeightsWithCircumcenter i j =
        if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
⊢ Eq (α := ℝ) (∑ j : PointsWithCircumcenterIndex n, pointWeightsWithCircumcenter i j) 1
have h₁ : Eq (α := ℝ) 1
  (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i) then
    Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i)
  else 0)
Tactic: convert! sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : PointsWithCircumcenterIndex n
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j
⊢ pointWeightsWithCircumcenter i j = if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
have h : ∀ (a : Fin (n + 1)),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a) →
    pointWeightsWithCircumcenter i (pointIndex a) =
      if pointIndex a = pointIndex i 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 : ℕ
i : Fin (n + 1)
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) →
      pointWeightsWithCircumcenter i (pointIndex a) =
        if pointIndex a = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex a) else 0
⊢ pointWeightsWithCircumcenter i j = if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
have h₁ : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex →
  pointWeightsWithCircumcenter i circumcenterIndex =
    if circumcenterIndex = pointIndex i 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 : ℕ
i : Fin (n + 1)
⊢ Eq (α := ℝ) (∑ j : PointsWithCircumcenterIndex n, pointWeightsWithCircumcenter i j) 1
have h : ∀ (j : PointsWithCircumcenterIndex n),
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
    pointWeightsWithCircumcenter i j =
      if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
Tactic: classical
  convert! sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [pointWeightsWithCircumcenter]
  · simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h :
  ∀ (j : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
      pointWeightsWithCircumcenter i j =
        if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
⊢ Eq (α := ℝ) (∑ j : PointsWithCircumcenterIndex n, pointWeightsWithCircumcenter i j) 1
have h₁ : Eq (α := ℝ) 1
  (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i) then
    Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i)
  else 0)
Tactic: classical
  convert! sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [pointWeightsWithCircumcenter]
  · 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
i : Fin (n + 1)
⊢ s.points i =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (pointWeightsWithCircumcenter i)
have rw : s.pointsWithCircumcenter (pointIndex i) =
  (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
    (pointWeightsWithCircumcenter i)
Tactic: rw [← pointsWithCircumcenter_point]
-- 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)
⊢ s.pointsWithCircumcenter (pointIndex i) =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (pointWeightsWithCircumcenter i)
have symm : (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
    (pointWeightsWithCircumcenter i) =
  s.pointsWithCircumcenter (pointIndex i)
Tactic: symm