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
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex
hn : Ne (α := PointsWithCircumcenterIndex n) circumcenterIndex circumcenterIndex
⊢ circumcenterWeightsWithCircumcenter n circumcenterIndex = 0

Tactic:
tauto
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
simp_rw :
  HSMul.hSMul (β := ℝ)
          (card (α := Fin (n + 1))
            ((if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) ∪
              if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
          1 +
        HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
      -1 =
    1
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i) 1

Tactic:
simp_rw [sum_pointsWithCircumcenter, reflectionCircumcenterWeightsWithCircumcenter, sum_ite,
    sum_const, filter_or, filter_eq']

Premises used: Finset.filter_eq', Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter, Finset.filter_or, Affine.Simplex.sum_pointsWithCircumcenter, Finset.sum_ite, Finset.sum_const
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
rw :
  HSMul.hSMul (β := ℝ)
          (card (α := Fin (n + 1)) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) +
            card (α := Fin (n + 1)) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
          1 +
        HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
      -1 =
    1
rw₁ :
  Disjoint (α := Finset (Fin (n + 1))) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅)
    (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅)
⊢ HSMul.hSMul (β := ℝ)
          (card (α := Fin (n + 1))
            ((if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) ∪
              if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
          1 +
        HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
      -1 =
    1

Tactic:
rw [card_union_of_disjoint]

Premises used: Finset.card_union_of_disjoint
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ HSMul.hSMul (β := ℝ)
          (card (α := Fin (n + 1)) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅) +
            card (α := Fin (n + 1)) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅))
          1 +
        HSMul.hSMul (β := ℝ) (card (α := Fin (n + 1)) {x : Fin (n + 1) | ¬(x = i₁ ∨ x = i₂)}) 0 +
      -1 =
    1

Tactic:
norm_num
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ Disjoint (α := Finset (Fin (n + 1))) (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₁ then {i₁} else ∅)
    (if Membership.mem (γ := Finset (Fin (n + 1))) univ i₂ then {i₂} else ∅)

Tactic:
simpa only [if_true, mem_univ, disjoint_singleton] using h

Premises used: Finset.mem_univ, if_true, Finset.disjoint_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
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ card (α := Fin (n + 1)) {i₁, i₂} = 2

Tactic:
simp [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
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ card (α := Fin (n + 1)) {i₁, i₂} = 2

Tactic:
have hc : #{i₁, i₂} = 2 := by simp [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
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h₁ : W = affineSpan ℝ (Set.range (s.face hc).points)
⊢ Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)

Tactic:
apply eq_orthogonalProjection_of_eq_subspace

Premises used: EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace
-- 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₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
⊢ W = affineSpan ℝ (Set.range (s.face hc).points)

Tactic:
simp [W]
-- 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₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
⊢ Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)

Tactic:
have h_faces :
    (orthogonalProjection W s.circumcenter : P) =
      ↑((s.face hc).orthogonalProjectionSpan s.circumcenter) := by
    apply eq_orthogonalProjection_of_eq_subspace
    simp [W]
-- 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₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
rw :
  ∑ i : Fin (n + 1),
        (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
                centroidWeightsWithCircumcenter {i₁, i₂} -
              reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
            (pointIndex i) •
          (s.pointsWithCircumcenter (pointIndex i) -ᵥ Classical.choice ⋯) +
      (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
              centroidWeightsWithCircumcenter {i₁, i₂} -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
          circumcenterIndex •
        (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) =
    0
⊢ Eq (α := P) ((reflection (affineSpan ℝ (s.points '' {i₁, i₂})) : (a : P) → P) s.circumcenter : P)
    ((affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
        (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) :
      P)

Tactic:
rw [reflection_apply', h_faces, s.orthogonalProjection_circumcenter hc,
    circumcenter_eq_centroid, s.face_centroid_eq_centroid hc,
    centroid_eq_affineCombination_of_pointsWithCircumcenter,
    circumcenter_eq_affineCombination_of_pointsWithCircumcenter, ← @vsub_eq_zero_iff_eq V,
    affineCombination_vsub, weightedVSub_vadd_affineCombination, affineCombination_vsub,
    weightedVSub_apply, sum_pointsWithCircumcenter]

Premises used: Finset.affineCombination_vsub, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, vsub_eq_zero_iff_eq, Affine.Simplex.face_centroid_eq_centroid, Affine.Simplex.orthogonalProjection_circumcenter, Finset.weightedVSub_vadd_affineCombination, Finset.weightedVSub_apply, EuclideanGeometry.reflection_apply', Affine.Simplex.sum_pointsWithCircumcenter, Affine.Simplex.circumcenter_eq_centroid, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter
-- 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₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
simp_rw :
  Eq.{u_1 + 1} (α := V)
    (∑ x : Fin (n + 1),
      ((if Membership.mem (γ := Finset (Fin (n + 1))) {i₁, i₂} x then
          HAdd.hAdd (α := ℝ) (↑2 : ℝ)⁻¹ (↑2 : ℝ)⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
        else 0) -
        if x = i₁ ∨ x = i₂ then HSMul.hSMul (α := ℝ) 1 (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
        else 0))
    0
⊢ ∑ i : Fin (n + 1),
        (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
                centroidWeightsWithCircumcenter {i₁, i₂} -
              reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
            (pointIndex i) •
          (s.pointsWithCircumcenter (pointIndex i) -ᵥ Classical.choice ⋯) +
      (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
              centroidWeightsWithCircumcenter {i₁, i₂} -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
          circumcenterIndex •
        (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) =
    0

Tactic:
simp_rw [Pi.sub_apply, Pi.add_apply, Pi.sub_apply, sub_smul, add_smul, sub_smul,
    centroidWeightsWithCircumcenter, circumcenterWeightsWithCircumcenter,
    reflectionCircumcenterWeightsWithCircumcenter, ite_smul, zero_smul, sub_zero,
    apply_ite₂ (· + ·), add_zero, ← add_smul, hc, zero_sub, neg_smul, sub_self, add_zero]

Premises used: apply_ite₂, neg_smul, sub_self, sub_zero, sub_smul, Affine.Simplex.centroidWeightsWithCircumcenter, Pi.add_apply, zero_smul, add_smul, HAdd.hAdd, Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter, Affine.Simplex.circumcenterWeightsWithCircumcenter, ite_smul, add_zero, zero_sub, Pi.sub_apply
-- 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₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
⊢ Eq.{u_1 + 1} (α := V) (∑ _x : Fin (n + 1), 0) 0

Tactic:
sum_const_zero

Premises used: Finset.sum_const_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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
h₁ :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) univ x →
      ((if Membership.mem (γ := Finset (Fin (n + 1))) {i₁, i₂} x then
            HAdd.hAdd (α := ℝ) (↑2 : ℝ)⁻¹ (↑2 : ℝ)⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0) -
          if x = i₁ ∨ x = i₂ then HSMul.hSMul (α := ℝ) 1 (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0) =
        0
⊢ Eq.{u_1 + 1} (α := V)
    (∑ x : Fin (n + 1),
      ((if Membership.mem (γ := Finset (Fin (n + 1))) {i₁, i₂} x then
          HAdd.hAdd (α := ℝ) (↑2 : ℝ)⁻¹ (↑2 : ℝ)⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
        else 0) -
        if x = i₁ ∨ x = i₂ then HSMul.hSMul (α := ℝ) 1 (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
        else 0))
    0

Tactic:
convert! sum_const_zero

Premises used: Finset.sum_const_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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : card (α := Fin (n + 1)) {i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces :
  Eq.{u_2 + 1} (α := P) (↑((orthogonalProjection W : (a : P) → ↥W) s.circumcenter) : P)
    (↑(((s.face hc).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.face hc).points)))
          s.circumcenter) :
      P)
x : Fin (n + 1)
h_1 : Membership.mem (γ := Finset (Fin (n + 1))) univ x
⊢ ((if Membership.mem (γ := Finset (Fin (n + 1))) {i₁, i₂} x then
        HAdd.hAdd (α := ℝ) (↑2 : ℝ)⁻¹ (↑2 : ℝ)⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
      else 0) -
      if x = i₁ ∨ x = i₂ then HSMul.hSMul (α := ℝ) 1 (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
      else 0) =
    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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
mp : Cospherical ps → ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
mpr : (∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius) → Cospherical ps
⊢ Cospherical ps ↔ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius

Tactic:
constructor
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
c : P
hcr : ∃ (radius : ℝ), ∀ p ∈ ps, dist p c = radius
⊢ ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) c) : P) = r

Tactic:
rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq h c] at hcr

Premises used: 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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
c : P
hcr : ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) c) : P) = r
⊢ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius

Tactic:
⟨orthogonalProjection s c, orthogonalProjection_mem _, hcr⟩

Premises used: EuclideanGeometry.orthogonalProjection_mem, And.intro, Exists.intro, EuclideanGeometry.orthogonalProjection, Subtype.val, DFunLike.coe
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
c : P
hcr : ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) c) : P) = r
⊢ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius

Tactic:
exact ⟨orthogonalProjection s c, orthogonalProjection_mem _, hcr⟩
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
⊢ (∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius) → Cospherical ps

Tactic:
fun ⟨c, _, hd⟩ => ⟨c, hd⟩

Premises used: EuclideanGeometry.Cospherical, _private.0.EuclideanGeometry.cospherical_iff_exists_mem_of_complete.match_1, 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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : s.direction.HasOrthogonalProjection
⊢ (∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius) → Cospherical ps

Tactic:
exact fun ⟨c, _, hd⟩ => ⟨c, hd⟩
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
⊢ Cospherical ps ↔ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius

Tactic:
cospherical_iff_exists_mem_of_complete h

Premises used: EuclideanGeometry.cospherical_iff_exists_mem_of_complete
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
⊢ ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius

Tactic:
rw [cospherical_iff_exists_mem_of_finiteDimensional h] at hc

Premises used: EuclideanGeometry.cospherical_iff_exists_mem_of_finiteDimensional
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
rcases :
  ∀ (c : P) (hc : c ∈ s) (r : ℝ) (hcr : ∀ p ∈ ps, dist p c = r),
    ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r

Tactic:
rcases hc with ⟨c, hc, r, hcr⟩
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
h₁ : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = 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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ affineSpan ℝ (Set.range sx.points) = s

Tactic:
sx.independent.affineSpan_eq_of_le_of_card_eq_finrank_add_one
        (affineSpan_le_of_subset_coe (hsxps.trans h)) ?_

Premises used: HasSubset.Subset.trans, AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one, affineSpan_le_of_subset_coe, Affine.Simplex.independent
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
this : Fintype.card (Fin (n + 1)) = finrank.{0, u_1} ℝ ↥s.direction + 1
⊢ affineSpan ℝ (Set.range sx.points) = s

Tactic:
refine
      sx.independent.affineSpan_eq_of_le_of_card_eq_finrank_add_one
        (affineSpan_le_of_subset_coe (hsxps.trans h)) ?_

Premises used: HasSubset.Subset.trans, AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one, affineSpan_le_of_subset_coe, Affine.Simplex.independent
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ Fintype.card (Fin (n + 1)) = finrank.{0, u_1} ℝ ↥s.direction + 1

Tactic:
simp [hd]
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ affineSpan ℝ (Set.range sx.points) = s

Tactic:
have hsx : affineSpan ℝ (Set.range sx.points) = s := by
    refine
      sx.independent.affineSpan_eq_of_le_of_card_eq_finrank_add_one
        (affineSpan_le_of_subset_coe (hsxps.trans h)) ?_
    simp [hd]
-- 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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range sx.points)) c

Tactic:
have hc : c ∈ affineSpan ℝ (Set.range sx.points) := hsx.symm ▸ hc