ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace Ω<VAR>mΩ : MeasurableSpace Ω<VAR>StandardBorelSpace Ω<VAR>Nonempty Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>NormedAddCommGroup F<VAR>f : Ω → F<VAR>NormedSpace ℝ F<VAR>CompleteSpace F<VAR>hm : m ≤ mΩ<VAR>hf_int : MeasureTheory.Integrable f μ<GOAL>μ[f|m] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condexpKernel μ m) ω
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>p1 p2 : P<VAR>p3 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<GOAL>dist p1 p3 = dist p2 p3 ↔ dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p3) = dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p3)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hps : ps ⊆ ↑s<VAR>p : P<GOAL>(ps.Pairwise fun p1 p2 => dist p1 p = dist p2 p) ↔ ps.Pairwise fun p1 p2 => dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p) = dist p2 ↑((EuclideanGeometry.orthogonalProjection s) p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hps : ps ⊆ ↑s<VAR>p : P<GOAL>(∃ r, ∀ p1 ∈ ps, dist p1 p = r) ↔ ∃ r, ∀ p1 ∈ ps, dist p1 ↑((EuclideanGeometry.orthogonalProjection s) p) = r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>HasOrthogonalProjection s.direction<VAR>ps : Set P<VAR>hnps : ps.Nonempty<VAR>p : P<VAR>hps : ps ⊆ ↑s<VAR>hp : p ∉ s<VAR>hu : ∃! cs, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius<GOAL>∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ι : Type u_3<VAR>hne : Nonempty ι<VAR>Finite ι<VAR>p : ι → P<VAR>ha : AffineIndependent ℝ p<GOAL>∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>(s.circumsphere.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ Metric.sphere s.circumsphere.center s.circumsphere.radius) ∧ ∀ (cs : EuclideanGeometry.Sphere P), cs.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ Metric.sphere cs.center cs.radius → cs = s.circumsphere
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>s.circumsphere.center = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>s.circumsphere.radius = s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>dist (s.points i) s.circumcenter = s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>s.points i ∈ s.circumsphere
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>dist s.circumcenter (s.points i) = s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<GOAL>p = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<GOAL>r = s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>0 ≤ s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 1)<GOAL>0 < s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Affine.Simplex ℝ P 0<VAR>i : Fin 1<GOAL>s.circumcenter = s.points i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Affine.Simplex ℝ P 1<GOAL>s.circumcenter = Finset.centroid ℝ Finset.univ s.points
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>m n : ℕ<VAR>s : Affine.Simplex ℝ P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>(s.reindex e).circumsphere = s.circumsphere
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>m n : ℕ<VAR>s : Affine.Simplex ℝ P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>(s.reindex e).circumcenter = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>m n : ℕ<VAR>s : Affine.Simplex ℝ P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>(s.reindex e).circumradius = s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>p1 : P<VAR>p2 : P<VAR>r : ℝ<VAR>hp : p1 ∈ affineSpan ℝ (Set.range s.points)<GOAL>s.orthogonalProjectionSpan (r • (p2 -ᵥ ↑(s.orthogonalProjectionSpan p2)) +ᵥ p1) = ⟨p1, hp⟩
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>r₁ : ℝ<VAR>s : Affine.Simplex ℝ P n<VAR>p p₁o : P<VAR>hp₁o : p₁o ∈ affineSpan ℝ (Set.range s.points)<GOAL>↑(s.orthogonalProjectionSpan (r₁ • (p -ᵥ ↑(s.orthogonalProjectionSpan p)) +ᵥ p₁o)) = p₁o
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>p1 : P<VAR>p2 : P<VAR>hp1 : p1 ∈ affineSpan ℝ (Set.range s.points)<GOAL>dist p1 p2 * dist p1 p2 = dist p1 ↑(s.orthogonalProjectionSpan p2) * dist p1 ↑(s.orthogonalProjectionSpan p2) + dist p2 ↑(s.orthogonalProjectionSpan p2) * dist p2 ↑(s.orthogonalProjectionSpan p2)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>r : ℝ<VAR>s : Affine.Simplex ℝ P n<VAR>p₁ : P<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter<VAR>h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)<GOAL>dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>p : P<VAR>hr : ∃ r, ∀ (i : Fin (n + 1)), dist (s.points i) p = r<GOAL>↑(s.orthogonalProjectionSpan p) = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>p : P<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<GOAL>↑(s.orthogonalProjectionSpan p) = s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>fs : Finset (Fin (n + 1))<VAR>m : ℕ<VAR>h : fs.card = m + 1<GOAL>↑((s.face h).orthogonalProjectionSpan s.circumcenter) = (s.face h).circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s₁ s₂ : Affine.Simplex ℝ P n<VAR>h : Set.range s₁.points = Set.range s₂.points<GOAL>s₁.circumcenter = s₂.circumcenter
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>f : Affine.Simplex.PointsWithCircumcenterIndex n → α<GOAL>∑ i : Affine.Simplex.PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i) + f Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>s.pointsWithCircumcenter (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i) = s.points i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>s.pointsWithCircumcenter Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex = s.circumcenter
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>∑ j : Affine.Simplex.PointsWithCircumcenterIndex n, Affine.Simplex.pointWeightsWithCircumcenter i j = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>i : Fin (n + 1)<GOAL>s.points i = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.pointWeightsWithCircumcenter i)
<VAR>n : ℕ<VAR>fs : Finset (Fin (n + 1))<VAR>h : fs.Nonempty<GOAL>∑ i : Affine.Simplex.PointsWithCircumcenterIndex n, Affine.Simplex.centroidWeightsWithCircumcenter fs i = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>fs : Finset (Fin (n + 1))<GOAL>Finset.centroid ℝ fs s.points = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.centroidWeightsWithCircumcenter fs)
<VAR>n : ℕ<GOAL>∑ i : Affine.Simplex.PointsWithCircumcenterIndex n, Affine.Simplex.circumcenterWeightsWithCircumcenter n i = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>s.circumcenter = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.circumcenterWeightsWithCircumcenter n)
<VAR>n : ℕ<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<GOAL>∑ i : Affine.Simplex.PointsWithCircumcenterIndex n, Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>i₁ i₂ : Fin (n + 1)<VAR>h : i₁ ≠ i₂<GOAL>(EuclideanGeometry.reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>Nonempty ↥s<VAR>HasOrthogonalProjection s.direction<GOAL>EuclideanGeometry.Cospherical ps ↔ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>Nonempty ↥s<VAR>FiniteDimensional ℝ ↥s.direction<GOAL>EuclideanGeometry.Cospherical ps ↔ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>Nonempty ↥s<VAR>n : ℕ<VAR>FiniteDimensional ℝ ↥s.direction<VAR>hd : FiniteDimensional.finrank ℝ ↥s.direction = n<VAR>hc : EuclideanGeometry.Cospherical ps<GOAL>∃ r, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>Nonempty ↥s<VAR>n : ℕ<VAR>FiniteDimensional ℝ ↥s.direction<VAR>hd : FiniteDimensional.finrank ℝ ↥s.direction = n<VAR>hc : EuclideanGeometry.Cospherical ps<VAR>sx₁ sx₂ : Affine.Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumradius = sx₂.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>FiniteDimensional ℝ V<VAR>hd : FiniteDimensional.finrank ℝ V = n<VAR>hc : EuclideanGeometry.Cospherical ps<GOAL>∃ r, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>FiniteDimensional ℝ V<VAR>hd : FiniteDimensional.finrank ℝ V = n<VAR>hc : EuclideanGeometry.Cospherical ps<VAR>sx₁ sx₂ : Affine.Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumradius = sx₂.circumradius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>Nonempty ↥s<VAR>n : ℕ<VAR>FiniteDimensional ℝ ↥s.direction<VAR>hd : FiniteDimensional.finrank ℝ ↥s.direction = n<VAR>hc : EuclideanGeometry.Cospherical ps<GOAL>∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>Nonempty ↥s<VAR>n : ℕ<VAR>FiniteDimensional ℝ ↥s.direction<VAR>hd : FiniteDimensional.finrank ℝ ↥s.direction = n<VAR>hc : EuclideanGeometry.Cospherical ps<VAR>sx₁ sx₂ : Affine.Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumcenter = sx₂.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>FiniteDimensional ℝ V<VAR>hd : FiniteDimensional.finrank ℝ V = n<VAR>hc : EuclideanGeometry.Cospherical ps<GOAL>∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>FiniteDimensional ℝ V<VAR>hd : FiniteDimensional.finrank ℝ V = n<VAR>hc : EuclideanGeometry.Cospherical ps<VAR>sx₁ sx₂ : Affine.Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumcenter = sx₂.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>Nonempty ↥s<VAR>n : ℕ<VAR>FiniteDimensional ℝ ↥s.direction<VAR>hd : FiniteDimensional.finrank ℝ ↥s.direction = n<VAR>hc : EuclideanGeometry.Cospherical ps<GOAL>∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>Nonempty ↥s<VAR>n : ℕ<VAR>FiniteDimensional ℝ ↥s.direction<VAR>hd : FiniteDimensional.finrank ℝ ↥s.direction = n<VAR>hc : EuclideanGeometry.Cospherical ps<VAR>sx₁ sx₂ : Affine.Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumsphere = sx₂.circumsphere
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>FiniteDimensional ℝ V<VAR>hd : FiniteDimensional.finrank ℝ V = n<VAR>hc : EuclideanGeometry.Cospherical ps<GOAL>∃ c, ∀ (sx : Affine.Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps : Set P<VAR>n : ℕ<VAR>FiniteDimensional ℝ V<VAR>hd : FiniteDimensional.finrank ℝ V = n<VAR>hc : EuclideanGeometry.Cospherical ps<VAR>sx₁ sx₂ : Affine.Simplex ℝ P n<VAR>hsx₁ : Set.range sx₁.points ⊆ ps<VAR>hsx₂ : Set.range sx₂.points ⊆ ps<GOAL>sx₁.circumsphere = sx₂.circumsphere
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<VAR>p p₁ p₂ : P<VAR>r : ℝ<VAR>hp₁ : p₁ ∈ affineSpan ℝ (insert p (Set.range s.points))<VAR>hp₂ : p₂ ∈ affineSpan ℝ (insert p (Set.range s.points))<VAR>h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r<VAR>h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r<GOAL>p₁ = p₂ ∨ p₁ = (EuclideanGeometry.reflection (affineSpan ℝ (Set.range s.points))) p₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>OpenEmbedding ⇑f.base
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑X<GOAL>CategoryTheory.IsIso (f.c.app (Opposite.op (⋯.functor.obj U)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑↑(Y.restrict ⋯))ᵒᵖ), (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f).hom.c.app X_1 = f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj (Opposite.unop X_1))) ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f).inv ≫ f = Y.ofRestrict ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>V : TopologicalSpace.Opens ↑↑Y<VAR>U : TopologicalSpace.Opens ↑↑X<VAR>h : V = (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U<GOAL>CategoryTheory.IsIso (f.c.app (Opposite.op V))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>U V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ<VAR>i : U ⟶ V<GOAL>X.presheaf.map i ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f (Opposite.unop V) = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f (Opposite.unop U) ≫ Y.presheaf.map ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).op.map i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑X<GOAL>CategoryTheory.inv (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U) = f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U)) ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑X<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U ≫ f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U)) = X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑Y<GOAL>f.c.app (Opposite.op U) ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U) = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>U : TopologicalSpace.Opens ↑↑Y<VAR>hU : ↑U ⊆ Set.range ⇑f.base<GOAL>f.c.app (Opposite.op U) ≫ AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U) = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>Y : TopCat<VAR>f : Y ⟶ TopCat.of ↑↑X<VAR>h : OpenEmbedding ⇑f<VAR>U : TopologicalSpace.Opens ↑↑(X.restrict h)<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U = 𝟙 ((X.restrict h).presheaf.obj (Opposite.op U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>h' : CategoryTheory.Epi f.base<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>g : Y ⟶ Z<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f g ≫ f = Y.ofRestrict ⋯ ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : CategoryTheory.Limits.PullbackCone f g<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f g s ≫ (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g).fst = s.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : CategoryTheory.Limits.PullbackCone f g<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f g s ≫ (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeft f g).snd = s.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)