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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
intro :
  ∀ (x : ℕ) (hn : Fintype.card ι = x),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius

Tactic:
induction hn : Fintype.card ι generalizing ι with
  | zero =>
    exfalso
    have h := Fintype.card_pos_iff.2 hne
    lia
  | succ m hm =>
    rcases m with - | m
    · rw [Fintype.card_eq_one_iff] at hn
      obtain ⟨i, hi⟩ := hn
      haveI : Unique ι := ⟨⟨i⟩, hi⟩
      use ⟨p i, 0⟩
      simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton]
      constructor
      · simp_rw [hi default, Set.singleton_subset_iff]
        exact ⟨⟨⟩, by simp only [Metric.sphere_zero, Set.mem_singleton_iff]⟩
      · rintro ⟨cc, cr⟩
        rintro ⟨rfl, hdist⟩
        replace hdist : 0 = cr := by simpa using hdist
        rw [hi default, hdist]
    · have i := hne.some
      let ι2 := { x // x ≠ i }
      classical
      have hc : Fintype.card ι2 = m + 1 := by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
          simp
        · simp
      haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) := by
        change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert! ha.notMem_affineSpan_diff i Set.univ
      change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      simp

Premises used: Set.singleton_subset_iff, Set.range_unique, Fintype.card, Set.image_eq_range, AffineSubspace.mem_affineSpan_singleton, Fintype.card_eq_one_iff, affineSpan_insert_affineSpan, rfl
-- 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
⊢ (Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumsphere.center ∧
      Set.range s.points ⊆ Metric.sphere s.circumsphere.center s.circumsphere.radius) ∧
    ∀ (cs : Sphere P),
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) cs.center ∧
          Set.range s.points ⊆ Metric.sphere cs.center cs.radius →
        cs = s.circumsphere

Tactic:
s.independent.existsUnique_dist_eq.choose_spec

Premises used: Exists.choose_spec, Set.Mem, Affine.Simplex.circumsphere, Affine.Simplex.independent, AffineIndependent.existsUnique_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
⊢ s.circumsphere.center = s.circumcenter

Tactic:
rfl

Premises used: Affine.Simplex.circumcenter, rfl
-- 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
⊢ s.circumsphere.radius = s.circumradius

Tactic:
rfl

Premises used: Affine.Simplex.circumradius, rfl
-- 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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter

Tactic:
s.circumsphere_unique_dist_eq.1.1

Premises used: Set.Mem, Affine.Simplex.circumcenter, Affine.Simplex.circumsphere_unique_dist_eq, And.left
-- 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
i : Fin (n + 1)
⊢ dist (s.points i) s.circumcenter = s.circumradius

Tactic:
dist_of_mem_subset_sphere (Set.mem_range_self _) s.circumsphere_unique_dist_eq.1.2

Premises used: Set.mem_range_self, EuclideanGeometry.dist_of_mem_subset_sphere, Affine.Simplex.circumcenter, Affine.Simplex.circumsphere_unique_dist_eq, And.right, And.left, 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
i : Fin (n + 1)
⊢ s.points i ∈ s.circumsphere

Tactic:
s.dist_circumcenter_eq_circumradius i

Premises used: Set.Mem, setOf, Affine.Simplex.circumcenter, Affine.Simplex.dist_circumcenter_eq_circumradius, Affine.Simplex.circumradius, Metric.sphere
-- 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
i : Fin (n + 1)
rw : dist (s.points i) s.circumcenter = s.circumradius
⊢ dist s.circumcenter (s.points i) = s.circumradius

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- 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
i : Fin (n + 1)
⊢ dist (s.points i) s.circumcenter = s.circumradius

Tactic:
dist_circumcenter_eq_circumradius _ _

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 : Simplex ℝ P n
i : Fin (n + 1)
⊢ dist (s.points i) s.circumcenter = s.circumradius

Tactic:
exact dist_circumcenter_eq_circumradius _ _

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 : Simplex ℝ P n
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
        (Sphere.center { center := p, radius := r : Sphere P }) ∧
      Set.range s.points ⊆
        Metric.sphere (Sphere.center { center := p, radius := r }) (Sphere.radius { center := p, radius := r }) →
    { center := p, radius := r } = s.circumsphere

Tactic:
have h := s.circumsphere_unique_dist_eq.2 ⟨p, 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
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
        (Sphere.center { center := p, radius := r : Sphere P }) ∧
      Set.range s.points ⊆
        Metric.sphere (Sphere.center { center := p, radius := r }) (Sphere.radius { center := p, radius := r }) →
    { center := p, radius := r } = s.circumsphere
⊢ p = s.circumsphere.center ∧ r = s.circumsphere.radius

Tactic:
simp only [hp, hr, forall_const, subset_sphere (s := ⟨p, r⟩), Sphere.ext_iff,
    Set.forall_mem_range, mem_sphere, true_and] at h

Premises used: EuclideanGeometry.subset_sphere, Set.forall_mem_range, EuclideanGeometry.mem_sphere, forall_const, true_and, EuclideanGeometry.Sphere.ext_iff
-- 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
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h : p = s.circumsphere.center ∧ r = s.circumsphere.radius
⊢ p = s.circumcenter

Tactic:
h.1

Premises used: Affine.Simplex.circumcenter, And.left
-- 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
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h : p = s.circumsphere.center ∧ r = s.circumsphere.radius
⊢ p = s.circumcenter

Tactic:
exact h.1

Premises used: And.left
-- 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
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h : p = s.circumsphere.center ∧ r = s.circumsphere.radius
⊢ r = s.circumradius

Tactic:
h.2

Premises used: And.right, 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
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h : p = s.circumsphere.center ∧ r = s.circumsphere.radius
⊢ r = s.circumradius

Tactic:
exact h.2

Premises used: And.right
-- 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
⊢ 0 ≤ s.circumradius

Tactic:
s.dist_circumcenter_eq_circumradius 0 ▸ dist_nonneg

Premises used: dist_nonneg, Eq.rec, Affine.Simplex.dist_circumcenter_eq_circumradius, OfNat.ofNat
-- 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 + 1)
⊢ 0 < s.circumradius

Tactic:
lt_of_le_of_ne s.circumradius_nonneg ?_

Premises used: Affine.Simplex.circumradius_nonneg, lt_of_le_of_ne
-- 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 + 1)
refine : 0 ≠ s.circumradius
⊢ 0 < s.circumradius

Tactic:
refine lt_of_le_of_ne s.circumradius_nonneg ?_

Premises used: Affine.Simplex.circumradius_nonneg, lt_of_le_of_ne
-- 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 + 1)
h : 0 = s.circumradius
⊢ ∀ (i : Fin (n + 1 + 1)), dist (s.points i) s.circumcenter = s.circumradius

Tactic:
have hr := s.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 : Simplex ℝ P (n + 1)
h : 0 = s.circumradius
hr : ∀ (i : Fin (n + 1 + 1)), dist (s.points i) s.circumcenter = s.circumradius
⊢ ∀ (i : Fin (n + 1 + 1)), s.points i = s.circumcenter

Tactic:
simp_rw [← h, dist_eq_zero] at hr

Premises used: dist_eq_zero
-- 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 + 1)
h : 0 = s.circumradius
hr : ∀ (i : Fin (n + 1 + 1)), s.points i = s.circumcenter
⊢ Ne (α := Fin (n + 2)) 0 1

Tactic:
simp
-- 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 + 1)
h : 0 = s.circumradius
hr : ∀ (i : Fin (n + 1 + 1)), s.points i = s.circumcenter
⊢ s.points 0 ≠ s.points 1

Tactic:
have h01 := s.independent.injective.ne (by simp : (0 : Fin (n + 2)) ≠ 1)
-- 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 + 1)
h : 0 = s.circumradius
hr : ∀ (i : Fin (n + 1 + 1)), s.points i = s.circumcenter
h01 : s.points 0 ≠ s.points 1
⊢ False

Tactic:
simp [hr] at h01
-- 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
s : Simplex ℝ P 0
i : Fin 1
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter

Tactic:
have 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
s : Simplex ℝ P 0
i : Fin 1
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter
⊢ LT.lt (α := ℕ) 0 1

Tactic:
decide
-- 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
s : Simplex ℝ P 0
i : Fin 1
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter
a : Fin 1
⊢ a = default

Tactic:
simp only [Fin.eq_zero]

Premises used: Fin.eq_zero
-- 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
s : Simplex ℝ P 0
i : Fin 1
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter
have : ∀ (this : Unique (Fin 1)), s.circumcenter = s.points i
⊢ s.circumcenter = s.points i

Tactic:
have : Unique (Fin 1) := ⟨⟨0, by decide⟩, fun a => by simp only [Fin.eq_zero]⟩
-- 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
s : Simplex ℝ P 0
i : Fin 1
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter
this : Unique (Fin 1)
⊢ s.circumcenter = s.points default

Tactic:
simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton] at h

Premises used: Set.range_unique, AffineSubspace.mem_affineSpan_singleton
-- 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
s : Simplex ℝ P 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
rw : s.points default = s.points i
⊢ s.circumcenter = s.points i

Tactic:
rw [h]
-- 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
s : Simplex ℝ P 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
e_a : default = i
⊢ s.points default = s.points i

Tactic:
congr
-- 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
s : Simplex ℝ P 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ default = i

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- 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 + 1)
i : Fin (n + 2)
rw : s.circumradius ≠ 0
⊢ s.circumcenter ≠ s.points i

Tactic:
rw [← dist_ne_zero, dist_circumcenter_eq_circumradius']

Premises used: dist_ne_zero, 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 : Simplex ℝ P (n + 1)
i : Fin (n + 2)
⊢ s.circumradius ≠ 0

Tactic:
s.circumradius_pos.ne'

Premises used: LT.lt.ne', Affine.Simplex.circumradius_pos
-- 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 + 1)
i : Fin (n + 2)
⊢ s.circumradius ≠ 0

Tactic:
exact s.circumradius_pos.ne'

Premises used: LT.lt.ne', Affine.Simplex.circumradius_pos
-- 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
s : Simplex ℝ P 1
i : Fin 2
hi : Membership.mem (γ := Set (Fin 2)) Set.univ i
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hij : i ≠ j
rw :
  ‖HSMul.hSMul (α := ℝ) 1 (s.points i -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
⊢ dist (s.points i) (Finset.centroid ℝ univ s.points) = dist (s.points j) (Finset.centroid ℝ univ s.points)

Tactic:
rw [Finset.centroid_pair_fin, dist_eq_norm_vsub V (s.points i),
      dist_eq_norm_vsub V (s.points j), vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, ←
      one_smul ℝ (s.points i -ᵥ s.points 0), ← one_smul ℝ (s.points j -ᵥ s.points 0)]

Premises used: Affine.Simplex.points, Real, vsub_vadd_eq_vsub_sub, VSub.vsub, one_smul, dist_eq_norm_vsub, Finset.centroid_pair_fin, OfNat.ofNat
-- 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
s : Simplex ℝ P 1
i : Fin 2
hi : Membership.mem (γ := Set (Fin 2)) Set.univ i
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hij : i ≠ j
0 :
  ∀ (hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
    (hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j),
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
      ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
1 :
  ∀ (hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
    (hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j),
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
      ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points i -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖

Tactic:
fin_cases i
-- 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
s : Simplex ℝ P 1
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
0 :
  ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
    (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
      ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
h :
  ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
    (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
      ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖

Tactic:
fin_cases 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
s : Simplex ℝ P 1
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
    (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
      ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
h :
  ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
    (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
      ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖

Tactic:
fin_cases j