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
s : Simplex ℝ P 1
hi 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)‖

Tactic:
simp [-one_smul, ← sub_smul]

Premises used: sub_smul, one_smul
-- 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
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
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, ⋯⟩)
0 : ‖HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ = ‖HSub.hSub (α := ℝ) 1 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 ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖

Tactic:
simp [-one_smul, ← sub_smul]

Premises used: sub_smul, one_smul
-- 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
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨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, ⋯⟩)
1 : ‖HSub.hSub (α := ℝ) 1 2⁻¹ • (s.points 1 -ᵥ 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)‖

Tactic:
simp [-one_smul, ← sub_smul]

Premises used: sub_smul, one_smul
-- 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
hi 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)‖

Tactic:
simp [-one_smul, ← sub_smul]

Premises used: sub_smul, one_smul
-- 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
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
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 (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ = ‖HSub.hSub (α := ℝ) 1 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

Tactic:
norm_num
-- 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
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨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, ⋯⟩)
⊢ ‖HSub.hSub (α := ℝ) 1 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ = ‖HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖

Tactic:
norm_num
-- 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
⊢ Set.Pairwise Set.univ fun (i j : Fin 2) ↦
    dist (s.points i) (Finset.centroid ℝ univ s.points) = dist (s.points j) (Finset.centroid ℝ univ s.points)

Tactic:
have hr :
    Set.Pairwise Set.univ fun i j : Fin 2 =>
      dist (s.points i) (Finset.univ.centroid ℝ s.points) =
        dist (s.points j) (Finset.univ.centroid ℝ s.points) := by
    intro i hi j hj hij
    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)]
    fin_cases i <;> fin_cases j <;> simp [-one_smul, ← sub_smul] <;> norm_num
-- 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
hr :
  Set.Pairwise Set.univ fun (i j : Fin 2) ↦
    dist (s.points i) (Finset.centroid ℝ univ s.points) = dist (s.points j) (Finset.centroid ℝ univ s.points)
⊢ ∃ (z : ℝ),
    ∀ (x : Fin 2),
      Membership.mem (γ := Set (Fin 2)) Set.univ x → dist (s.points x) (Finset.centroid ℝ univ s.points) = z

Tactic:
rw [Set.pairwise_eq_iff_exists_eq] at hr

Premises used: Set.pairwise_eq_iff_exists_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
s : Simplex ℝ P 1
hr :
  ∃ (z : ℝ),
    ∀ (x : Fin 2),
      Membership.mem (γ := Set (Fin 2)) Set.univ x → dist (s.points x) (Finset.centroid ℝ univ s.points) = z
obtain :
  ∀ (r : ℝ)
    (hr :
      ∀ (x : Fin 2),
        Membership.mem (γ := Set (Fin 2)) Set.univ x → dist (s.points x) (Finset.centroid ℝ univ s.points) = r),
    s.circumcenter = Finset.centroid ℝ univ s.points
⊢ s.circumcenter = Finset.centroid ℝ univ s.points

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
s : Simplex ℝ P 1
r : ℝ
hr :
  ∀ (x : Fin 2), Membership.mem (γ := Set (Fin 2)) Set.univ x → dist (s.points x) (Finset.centroid ℝ univ s.points) = r
⊢ s.circumcenter = Finset.centroid ℝ univ s.points

Tactic:
(s.eq_circumcenter_of_dist_eq
        (centroid_mem_affineSpan_of_card_eq_add_one ℝ _ (Finset.card_fin 2)) fun i =>
        hr i (Set.mem_univ _)).symm

Premises used: Real, Finset.card_fin, Set.mem_univ, centroid_mem_affineSpan_of_card_eq_add_one, OfNat.ofNat, Eq.symm, 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
s : Simplex ℝ P 1
r : ℝ
hr :
  ∀ (x : Fin 2), Membership.mem (γ := Set (Fin 2)) Set.univ x → dist (s.points x) (Finset.centroid ℝ univ s.points) = r
⊢ s.circumcenter = Finset.centroid ℝ univ s.points

Tactic:
exact
    (s.eq_circumcenter_of_dist_eq
        (centroid_mem_affineSpan_of_card_eq_add_one ℝ _ (Finset.card_fin 2)) fun i =>
        hr i (Set.mem_univ _)).symm

Premises used: Real, Finset.card_fin, Set.mem_univ, centroid_mem_affineSpan_of_card_eq_add_one, OfNat.ofNat, Eq.symm, 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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumsphere = s.circumsphere

Tactic:
s.circumsphere_unique_dist_eq.2 _ ⟨?_, ?_⟩

Premises used: Affine.Simplex.circumsphere_unique_dist_eq, And.right, And.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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
refine_1 :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.reindex e).circumsphere.center
refine_2 : Set.range s.points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius
⊢ (s.reindex e).circumsphere = s.circumsphere

Tactic:
refine s.circumsphere_unique_dist_eq.2 _ ⟨?_, ?_⟩

Premises used: Affine.Simplex.circumsphere_unique_dist_eq, And.right, And.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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
refine_1 :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.reindex e).points))
    (s.reindex e).circumsphere.center
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.reindex e).circumsphere.center

Tactic:
rw [← s.reindex_range_points e]

Premises used: Affine.Simplex.reindex_range_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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
refine_2 :
  Set.range (s.reindex e).points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius
⊢ Set.range s.points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius

Tactic:
rw [← s.reindex_range_points e]

Premises used: Affine.Simplex.reindex_range_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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.reindex e).points))
    (s.reindex e).circumsphere.center

Tactic:
(s.reindex e).circumsphere_unique_dist_eq.1.1

Premises used: Affine.Simplex.reindex, 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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.reindex e).points))
    (s.reindex e).circumsphere.center

Tactic:
exact (s.reindex e).circumsphere_unique_dist_eq.1.1

Premises used: Affine.Simplex.reindex, 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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range (s.reindex e).points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius

Tactic:
(s.reindex e).circumsphere_unique_dist_eq.1.2

Premises used: Affine.Simplex.reindex, Affine.Simplex.circumsphere_unique_dist_eq, And.right, 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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range (s.reindex e).points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius

Tactic:
exact (s.reindex e).circumsphere_unique_dist_eq.1.2

Premises used: Affine.Simplex.reindex, Affine.Simplex.circumsphere_unique_dist_eq, And.right, 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
rw : (f : (a : P) → P₂) s.circumcenter = (s.map f.toAffineMap ⋯).circumcenter
⊢ (s.map f.toAffineMap ⋯).circumcenter = (f : (a : P) → P₂) s.circumcenter

Tactic:
rw [eq_comm]

Premises used: eq_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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ dist ((s.map f.toAffineMap ⋯).points i) ((f : (a : P) → P₂) s.circumcenter) = s.circumradius

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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
refine :
  Membership.mem (α := P₂) (γ := AffineSubspace ℝ P₂) (affineSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points))
    ((f : (a : P) → P₂) s.circumcenter : P₂)
⊢ (f : (a : P) → P₂) s.circumcenter = (s.map f.toAffineMap ⋯).circumcenter

Tactic:
refine (s.map f.toAffineMap f.injective).eq_circumcenter_of_dist_eq (r := s.circumradius) ?_
    fun i ↦ by simp

Premises used: Affine.Simplex.map, AffineIsometry.toAffineMap, AffineIsometry.injective, 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
rw :
  Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (affineSpan ℝ (Set.range s.points)))
    ((f : (a : P) → P₂) s.circumcenter : P₂)
⊢ Membership.mem (α := P₂) (γ := AffineSubspace ℝ P₂) (affineSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points))
    ((f : (a : P) → P₂) s.circumcenter : P₂)

Tactic:
rw [map_points, Set.range_comp, ← AffineSubspace.map_span]

Premises used: Set.range_comp, AffineSubspace.map_span, Affine.Simplex.map_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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (affineSpan ℝ (Set.range s.points)))
    ((f : (a : P) → P₂) s.circumcenter : P₂)

Tactic:
AffineSubspace.mem_map_of_mem _ s.circumcenter_mem_affineSpan

Premises used: Affine.Simplex.circumcenter_mem_affineSpan, Set.Mem, AffineSubspace.mem_map_of_mem
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (affineSpan ℝ (Set.range s.points)))
    ((f : (a : P) → P₂) s.circumcenter : P₂)

Tactic:
exact AffineSubspace.mem_map_of_mem _ s.circumcenter_mem_affineSpan

Premises used: Affine.Simplex.circumcenter_mem_affineSpan, AffineSubspace.mem_map_of_mem
-- 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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
rw : s.circumradius = (s.map f.toAffineMap ⋯).circumradius
⊢ (s.map f.toAffineMap ⋯).circumradius = s.circumradius

Tactic:
rw [eq_comm]

Premises used: eq_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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
refine :
  Membership.mem (α := P₂) (γ := AffineSubspace ℝ P₂) (affineSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points))
    ((f : (a : P) → P₂) s.circumcenter : P₂)
⊢ s.circumradius = (s.map f.toAffineMap ⋯).circumradius

Tactic:
refine (s.map f.toAffineMap f.injective).eq_circumradius_of_dist_eq (p := f s.circumcenter) ?_
    fun i ↦ by simp

Premises used: Affine.Simplex.map, AffineIsometry.toAffineMap, Affine.Simplex.eq_circumradius_of_dist_eq, AffineIsometry.injective
-- 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 : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
rw : s.circumcenter = (↑((s.restrict S hS).circumcenter (n := n)) : P)
⊢ (↑((s.restrict S hS).circumcenter (n := n)) : P) = s.circumcenter

Tactic:
rw [eq_comm]

Premises used: eq_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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ Nonempty.{u_2 + 1} ↥S

Tactic:
have : Nonempty S := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- 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 : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty.{u_2 + 1} ↥S
⊢ s.circumcenter = (↑((s.restrict S hS).circumcenter (n := n)) : P)

Tactic:
(s.restrict S hS).circumcenter_map S.subtypeₐᵢ

Premises used: Affine.Simplex.circumcenter_map, Affine.Simplex.map, AffineSubspace.subtypeₐᵢ, Affine.Simplex.restrict
-- 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 : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty.{u_2 + 1} ↥S
⊢ s.circumcenter = (↑((s.restrict S hS).circumcenter (n := n)) : P)

Tactic:
exact (s.restrict S hS).circumcenter_map S.subtypeₐᵢ

Premises used: Affine.Simplex.circumcenter_map, AffineSubspace.subtypeₐᵢ, Affine.Simplex.restrict
-- 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 : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
rw : s.circumradius = circumradius.{u_1, u_2} (P := ↥S) (n := n) (s.restrict S hS)
⊢ circumradius.{u_1, u_2} (P := ↥S) (n := n) (s.restrict S hS) = s.circumradius

Tactic:
rw [eq_comm]

Premises used: eq_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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty.{u_2 + 1} ↥S
⊢ s.circumradius = circumradius.{u_1, u_2} (P := ↥S) (n := n) (s.restrict S hS)

Tactic:
(s.restrict S hS).circumradius_map S.subtypeₐᵢ

Premises used: Affine.Simplex.map, AffineSubspace.subtypeₐᵢ, Affine.Simplex.restrict, Affine.Simplex.circumradius_map
-- 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 : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty.{u_2 + 1} ↥S
⊢ s.circumradius = circumradius.{u_1, u_2} (P := ↥S) (n := n) (s.restrict S hS)

Tactic:
exact (s.restrict S hS).circumradius_map S.subtypeₐᵢ

Premises used: AffineSubspace.subtypeₐᵢ, Affine.Simplex.restrict, Affine.Simplex.circumradius_map
-- 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 : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.points 0)
rw :
  dist s.circumcenter p₁ * dist s.circumcenter p₁ =
    dist (s.points 0) (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) *
          dist (s.points 0) (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) +
        dist p₁ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) *
          dist p₁ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) -
      s.circumradius * s.circumradius
⊢ dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius

Tactic:
rw [dist_comm, ← h₁ 0,
    s.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₁ h]

Premises used: Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, dist_comm, 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 : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.points 0)
⊢ dist s.circumcenter p₁ * dist s.circumcenter p₁ =
    dist (s.points 0) (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) *
          dist (s.points 0) (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) +
        dist p₁ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) *
          dist p₁ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) -
      s.circumradius * s.circumradius

Tactic:
simp only [h₁', dist_comm p₁, add_sub_cancel_left, Simplex.dist_circumcenter_eq_circumradius]

Premises used: add_sub_cancel_left, dist_comm, Affine.Simplex.dist_circumcenter_eq_circumradius