awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
hr : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)

Tactic:
change ∃ r : ℝ, ∀ i, (fun x => dist x p = r) (s.points i) at hr
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
hr : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
obtain :
  ∀ (r : ℝ) (hr : ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)),
    ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
⊢ ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r

Tactic:
obtain ⟨r, hr⟩ := hr
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
h : ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
⊢ ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r

Tactic:
use r
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
⊢ ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r

Tactic:
Set.forall_mem_range.mpr ?_

Premises used: Iff.mpr, Set.forall_mem_range
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
h : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r

Tactic:
refine Set.forall_mem_range.mpr ?_

Premises used: Iff.mpr, Set.forall_mem_range
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
⊢ ∀ (i : Fin (n + 1)), dist (s.points i) p = r

Tactic:
hr
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
⊢ ∀ (i : Fin (n + 1)), dist (s.points i) p = r

Tactic:
exact hr
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
hr : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
⊢ ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r

Tactic:
have hr : ∃ (r : ℝ), ∀ (a : P),
      a ∈ Set.range (fun (i : Fin (n + 1)) => s.points i) → dist a p = r := by
    obtain ⟨r, hr⟩ := hr
    use r
    refine Set.forall_mem_range.mpr ?_
    exact hr
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
hr_1 : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
hr : ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
⊢ ∃ (r : ℝ),
    ∀ (p₁ : P),
      Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) p₁ →
        dist p₁
            (↑((orthogonalProjection (affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)))
                  p) :
              P) =
          r

Tactic:
rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq (subset_affineSpan ℝ _) p] at hr

Premises used: Real, subset_affineSpan, EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
hr_1 : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
hr :
  ∃ (r : ℝ),
    ∀ (p₁ : P),
      Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) p₁ →
        dist p₁
            (↑((orthogonalProjection (affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)))
                  p) :
              P) =
          r
obtain :
  ∀ (r : ℝ)
    (hr :
      ∀ (p₁ : P),
        Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) p₁ →
          dist p₁
              (↑((orthogonalProjection (affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)))
                    p) :
                P) =
            r),
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter

Tactic:
obtain ⟨r, hr⟩ := hr
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
hr_1 : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
r : ℝ
hr :
  ∀ (p₁ : P),
    Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) p₁ →
      dist p₁
          (↑((orthogonalProjection (affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)) :
                  (a : P) → ↥(affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)))
                p) :
            P) =
        r
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter

Tactic:
s.eq_circumcenter_of_dist_eq (orthogonalProjection_mem p) fun i => hr _ (Set.mem_range_self i)

Premises used: Set.mem_range_self, Affine.Simplex.points, EuclideanGeometry.orthogonalProjection_mem, Affine.Simplex.eq_circumcenter_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
hr_1 : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
r : ℝ
hr :
  ∀ (p₁ : P),
    Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) p₁ →
      dist p₁
          (↑((orthogonalProjection (affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)) :
                  (a : P) → ↥(affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)))
                p) :
            P) =
        r
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter

Tactic:
exact
    s.eq_circumcenter_of_dist_eq (orthogonalProjection_mem p) fun i => hr _ (Set.mem_range_self i)

Premises used: Set.mem_range_self, Affine.Simplex.points, EuclideanGeometry.orthogonalProjection_mem, Affine.Simplex.eq_circumcenter_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
p : P
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter

Tactic:
s.orthogonalProjection_eq_circumcenter_of_exists_dist_eq ⟨r, hr⟩

Premises used: Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, Exists.intro
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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))
m : ℕ
h : #fs = m + 1
h₁ : ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = s.circumradius
⊢ ∃ (r : ℝ), ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = r

Tactic:
use s.circumradius

Premises used: Affine.Simplex.circumradius
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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))
m : ℕ
h : #fs = m + 1
⊢ ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = s.circumradius

Tactic:
simp [face_points]

Premises used: Affine.Simplex.face_points
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
⊢ 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
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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)
⊢ s₂.points i ∈ Set.range s₂.points

Tactic:
have hi : s₂.points i ∈ Set.range s₂.points := Set.mem_range_self _
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
⊢ ∃ (y : Fin (n + 1)), s₁.points y = s₂.points i

Tactic:
rw [← h, Set.mem_range] at hi

Premises used: Set.mem_range
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
rcases : ∀ (j : Fin (n + 1)) (hj : s₁.points j = s₂.points i), dist (s₂.points i) s₁.circumcenter = s₁.circumradius
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius

Tactic:
rcases hi with ⟨j, hj⟩
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
rw₁ rw₂ : s₁.circumradius = s₁.circumradius
⊢ dist (s₂.points i) s₁.circumcenter = s₁.circumradius

Tactic:
rw [← hj, s₁.dist_circumcenter_eq_circumradius j]

Premises used: Affine.Simplex.dist_circumcenter_eq_circumradius
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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

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]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
hr : ∀ (i : Fin (n + 1)), dist (s₂.points i) s₁.circumcenter = s₁.circumradius
⊢ s₁.circumcenter = s₂.circumcenter

Tactic:
s₂.eq_circumcenter_of_dist_eq hs hr

Premises used: Affine.Simplex.eq_circumcenter_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
hr : ∀ (i : Fin (n + 1)), dist (s₂.points i) s₁.circumcenter = s₁.circumradius
⊢ s₁.circumcenter = s₂.circumcenter

Tactic:
exact s₂.eq_circumcenter_of_dist_eq hs hr

Premises used: Affine.Simplex.eq_circumcenter_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ℕ
x x_1 : Fin (n + 1)
h :
  Eq (α := PointsWithCircumcenterIndex n) ((fun (i : Fin (n + 1)) ↦ pointIndex i) x)
    ((fun (i : Fin (n + 1)) ↦ pointIndex i) x_1)
⊢ x = x_1

Tactic:
injection h
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h :
  ∀ (x : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ x ↔
      x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
ext x
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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)

Tactic:
⟨fun h => ?_, fun _ => mem_univ _⟩

Premises used: Finset.mem_univ, Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
h :
  ∀ (h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ x),
    x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ x ↔
    x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
refine ⟨fun h => ?_, fun _ => mem_univ _⟩
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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)
h₂ :
  ∀ (h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex),
    circumcenterIndex ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
obtain i | - := x
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
i : Fin (n + 1)
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i)
⊢ pointIndex i ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))

Premises used: Finset.mem_univ, Finset.mem_insert_of_mem, Finset.mem_map_of_mem
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
i : Fin (n + 1)
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i)
⊢ pointIndex i ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))

Premises used: Finset.mem_univ, Finset.mem_insert_of_mem, Finset.mem_map_of_mem
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex
⊢ circumcenterIndex ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
mem_insert_self _ _

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex
⊢ circumcenterIndex ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
exact mem_insert_self _ _

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
⊢ 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 _ _
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
change :
  ∑ 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

Tactic:
change _ = (∑ i, f (pointIndexEmbedding n i)) + _

Premises used: Finset.univ, Affine.Simplex.pointIndexEmbedding, DFunLike.coe, Finset.sum
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
rw : 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:
rw [add_comm, h, ← sum_map, sum_insert]

Premises used: Finset.sum_map, add_comm, Finset.sum_insert
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
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))
⊢ circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ

Tactic:
simp_rw [Finset.mem_map, not_exists]

Premises used: not_exists, Finset.mem_map
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h_1 : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
x : Fin (n + 1)
left : 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:
injection h