ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c : P<VAR>R : ℝ<VAR>x : P<GOAL>EuclideanGeometry.inversion c R x -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ 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>c : P<VAR>R : ℝ<GOAL>EuclideanGeometry.inversion c R c = 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>c x : P<GOAL>EuclideanGeometry.inversion c 0 x = 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>c : P<VAR>a R : ℝ<VAR>x : P<GOAL>EuclideanGeometry.inversion c (a * R) x = (AffineMap.homothety c (a ^ 2)) (EuclideanGeometry.inversion c R x)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x : P<GOAL>EuclideanGeometry.inversion c (dist x c) x = x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x : P<GOAL>EuclideanGeometry.inversion c (dist c x) x = x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x : P<VAR>R : ℝ<VAR>h : x ∈ Metric.sphere c R<GOAL>EuclideanGeometry.inversion c R x = x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x : P<VAR>R : ℝ<GOAL>dist (EuclideanGeometry.inversion c R x) c = R ^ 2 / dist x 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>c x : P<VAR>R : ℝ<GOAL>dist c (EuclideanGeometry.inversion c R x) = R ^ 2 / dist c x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>x : P<GOAL>EuclideanGeometry.inversion c R (EuclideanGeometry.inversion c R x) = x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c : P<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>Function.Involutive (EuclideanGeometry.inversion c 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>c : P<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>Function.Surjective (EuclideanGeometry.inversion c 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>c : P<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>Function.Injective (EuclideanGeometry.inversion c 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>c : P<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>Function.Bijective (EuclideanGeometry.inversion c 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>c x : P<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>EuclideanGeometry.inversion c R x = c ↔ x = 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>c x : P<VAR>R : ℝ<GOAL>EuclideanGeometry.inversion c R x = c ↔ x = c ∨ R = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x : P<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>c = EuclideanGeometry.inversion c R x ↔ x = 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>c x : P<VAR>R : ℝ<GOAL>c = EuclideanGeometry.inversion c R x ↔ x = c ∨ R = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x y : P<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>R : ℝ<GOAL>dist (EuclideanGeometry.inversion c R x) (EuclideanGeometry.inversion c R y) = R ^ 2 / (dist x c * dist y c) * dist x y
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<GOAL>dist (EuclideanGeometry.inversion c R x) y * dist x c = dist x (EuclideanGeometry.inversion c R y) * dist y 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>a b c d : P<GOAL>dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
<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>x c : P<VAR>R : ℝ<VAR>l : Filter α<VAR>fc fx : α → P<VAR>fR : α → ℝ<VAR>hc : Filter.Tendsto fc l (𝓝 c)<VAR>hR : Filter.Tendsto fR l (𝓝 R)<VAR>hx : Filter.Tendsto fx l (𝓝 x)<VAR>hne : x ≠ c<GOAL>Filter.Tendsto (fun a => EuclideanGeometry.inversion (fc a) (fR a) (fx a)) l (𝓝 (EuclideanGeometry.inversion c R x))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>c x : X → P<VAR>R : X → ℝ<VAR>a₀ : X<VAR>s : Set X<VAR>hc : ContinuousWithinAt c s a₀<VAR>hR : ContinuousWithinAt R s a₀<VAR>hx : ContinuousWithinAt x s a₀<VAR>hne : x a₀ ≠ c a₀<GOAL>ContinuousWithinAt (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s a₀
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>c x : X → P<VAR>R : X → ℝ<VAR>a₀ : X<VAR>hc : ContinuousAt c a₀<VAR>hR : ContinuousAt R a₀<VAR>hx : ContinuousAt x a₀<VAR>hne : x a₀ ≠ c a₀<GOAL>ContinuousAt (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) a₀
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>c x : X → P<VAR>R : X → ℝ<VAR>s : Set X<VAR>hc : ContinuousOn c s<VAR>hR : ContinuousOn R s<VAR>hx : ContinuousOn x s<VAR>hne : ∀ a ∈ s, x a ≠ c a<GOAL>ContinuousOn (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>c x : X → P<VAR>R : X → ℝ<VAR>hc : Continuous c<VAR>hR : Continuous R<VAR>hx : Continuous x<VAR>hne : ∀ (a : X), x a ≠ c a<GOAL>Continuous fun a => EuclideanGeometry.inversion (c a) (R a) (x a)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>P : Type u_2<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>a b c d p : P<VAR>h : EuclideanGeometry.Cospherical {a, b, c, d}<VAR>hapc : ∠ a p c = π<VAR>hbpd : ∠ b p d = π<GOAL>dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>carrier : TopCat<VAR>presheaf : TopCat.Presheaf C carrier<GOAL>↑{ carrier := carrier, presheaf := presheaf } = carrier
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α β : X.Hom Y<VAR>w : α.base = β.base<VAR>h : α.c ≫ CategoryTheory.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf = β.c<GOAL>α = β
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α β : X.Hom Y<VAR>w : α.base = β.base<VAR>h : HEq α.c β.c<GOAL>α = β
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>α : X.Hom Y<VAR>β : Y.Hom Z<GOAL>(AlgebraicGeometry.PresheafedSpace.comp α β).c = β.c ≫ (TopCat.Presheaf.pushforward C β.base).map α.c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α β : X ⟶ Y<VAR>w : α.base = β.base<VAR>h : α.c ≫ CategoryTheory.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf = β.c<GOAL>α = β
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>(𝟙 X).base = 𝟙 ↑X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>(𝟙 X).c = 𝟙 X.presheaf
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>U : (TopologicalSpace.Opens ↑↑X)ᵒᵖ<GOAL>(𝟙 X).c.app U = X.presheaf.map (𝟙 U)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).base = f.base ≫ g.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y Z : AlgebraicGeometry.PresheafedSpace C<VAR>α : X ⟶ Y<VAR>β : Y ⟶ Z<VAR>U : (TopologicalSpace.Opens ↑↑Z)ᵒᵖ<GOAL>(α ≫ β).c.app U = β.c.app U ≫ α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj (Opposite.unop U)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>α β : X ⟶ Y<VAR>h : α = β<VAR>U : (TopologicalSpace.Opens ↑↑Y)ᵒᵖ<GOAL>α.c.app U = β.c.app U ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>∀ {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y), (AlgebraicGeometry.PresheafedSpace.forget C).map f = f.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>(AlgebraicGeometry.PresheafedSpace.forget C).obj X = ↑X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>H : ↑X ≅ ↑Y<VAR>α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf<GOAL>(AlgebraicGeometry.PresheafedSpace.isoOfComponents H α).inv = { base := H.inv, c := TopCat.Presheaf.toPushforwardOfIso H α.hom }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>H : ↑X ≅ ↑Y<VAR>α : (TopCat.Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf<GOAL>(AlgebraicGeometry.PresheafedSpace.isoOfComponents H α).hom = { base := H.hom, c := α.inv }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>H : X ≅ Y<GOAL>(AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso H).hom = H.hom.c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>H : X ≅ Y<GOAL>(AlgebraicGeometry.PresheafedSpace.sheafIsoOfIso H).inv = TopCat.Presheaf.pushforwardToOfIso ((AlgebraicGeometry.PresheafedSpace.forget C).mapIso H).symm H.inv.c
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f.base<VAR>CategoryTheory.IsIso f.c<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<GOAL>↑(X.restrict h) = U
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<GOAL>(X.restrict h).presheaf = ⋯.functor.op ⋙ X.presheaf
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<VAR>V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ<GOAL>(X.ofRestrict h).c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.PresheafedSpace C<VAR>f : U ⟶ ↑X<VAR>h : OpenEmbedding ⇑f<GOAL>(X.ofRestrict h).base = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>(X.restrict ⋯).presheaf = (TopCat.Presheaf.pushforward C (TopologicalSpace.Opens.inclusionTopIso ↑X).inv).obj X.presheaf
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>(X.ofRestrict ⋯).c = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>X.toRestrictTop.c = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>X.toRestrictTop.base = (TopologicalSpace.Opens.inclusionTopIso ↑X).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>X.restrictTopIso.inv = X.toRestrictTop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>X.restrictTopIso.hom = X.ofRestrict ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>∀ {X Y : (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ} (f : X ⟶ Y), AlgebraicGeometry.PresheafedSpace.Γ.map f = f.unop.c.app (Opposite.op ⊤)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : (AlgebraicGeometry.PresheafedSpace C)ᵒᵖ<GOAL>AlgebraicGeometry.PresheafedSpace.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>AlgebraicGeometry.PresheafedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.PresheafedSpace.Γ.map f.op = f.c.app (Opposite.op ⊤)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>↑(F.mapPresheaf.obj X) = ↑X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>X : AlgebraicGeometry.PresheafedSpace C<GOAL>(F.mapPresheaf.obj X).presheaf = X.presheaf ⋙ F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<GOAL>(F.mapPresheaf.map f).base = f.base
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : C ⥤ D<VAR>X Y : AlgebraicGeometry.PresheafedSpace C<VAR>f : X ⟶ Y<GOAL>(F.mapPresheaf.map f).c = CategoryTheory.whiskerRight f.c F
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>s : Set E<VAR>a : E<VAR>n : ℕ∞<VAR>hc : ContDiffWithinAt ℝ n c s a<VAR>hR : ContDiffWithinAt ℝ n R s a<VAR>hx : ContDiffWithinAt ℝ n x s a<VAR>hne : x a ≠ c a<GOAL>ContDiffWithinAt ℝ n (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s a
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hc : ContDiffOn ℝ n c s<VAR>hR : ContDiffOn ℝ n R s<VAR>hx : ContDiffOn ℝ n x s<VAR>hne : ∀ a ∈ s, x a ≠ c a<GOAL>ContDiffOn ℝ n (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>a : E<VAR>n : ℕ∞<VAR>hc : ContDiffAt ℝ n c a<VAR>hR : ContDiffAt ℝ n R a<VAR>hx : ContDiffAt ℝ n x a<VAR>hne : x a ≠ c a<GOAL>ContDiffAt ℝ n (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) a
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>n : ℕ∞<VAR>hc : ContDiff ℝ n c<VAR>hR : ContDiff ℝ n R<VAR>hx : ContDiff ℝ n x<VAR>hne : ∀ (a : E), x a ≠ c a<GOAL>ContDiff ℝ n fun a => EuclideanGeometry.inversion (c a) (R a) (x a)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>s : Set E<VAR>a : E<VAR>hc : DifferentiableWithinAt ℝ c s a<VAR>hR : DifferentiableWithinAt ℝ R s a<VAR>hx : DifferentiableWithinAt ℝ x s a<VAR>hne : x a ≠ c a<GOAL>DifferentiableWithinAt ℝ (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s a
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>s : Set E<VAR>hc : DifferentiableOn ℝ c s<VAR>hR : DifferentiableOn ℝ R s<VAR>hx : DifferentiableOn ℝ x s<VAR>hne : ∀ a ∈ s, x a ≠ c a<GOAL>DifferentiableOn ℝ (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>a : E<VAR>hc : DifferentiableAt ℝ c a<VAR>hR : DifferentiableAt ℝ R a<VAR>hx : DifferentiableAt ℝ x a<VAR>hne : x a ≠ c a<GOAL>DifferentiableAt ℝ (fun a => EuclideanGeometry.inversion (c a) (R a) (x a)) a
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>hc : Differentiable ℝ c<VAR>hR : Differentiable ℝ R<VAR>hx : Differentiable ℝ x<VAR>hne : ∀ (a : E), x a ≠ c a<GOAL>Differentiable ℝ fun a => EuclideanGeometry.inversion (c a) (R a) (x a)
<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>c x : F<VAR>R : ℝ<VAR>hx : x ≠ c<GOAL>HasFDerivAt (EuclideanGeometry.inversion c R) ((R / dist x c) ^ 2 • ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {x - c})ᗮ).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>c : P<VAR>r : ℝ<GOAL>{ center := c, radius := r }.center = c
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>c : P<VAR>r : ℝ<GOAL>{ center := c, radius := r }.radius = r
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>s : EuclideanGeometry.Sphere P<GOAL>{ center := s.center, radius := s.radius } = s
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>c : P<VAR>r : ℝ<GOAL>Metric.sphere { center := c, radius := r }.center { center := c, radius := r }.radius = Metric.sphere c r
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p : P<VAR>s : EuclideanGeometry.Sphere P<GOAL>p ∈ Metric.sphere s.center s.radius ↔ p ∈ s
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p : P<VAR>s : EuclideanGeometry.Sphere P<GOAL>dist p s.center = s.radius ↔ p ∈ s
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p : P<VAR>s : EuclideanGeometry.Sphere P<GOAL>p ∈ s ↔ dist p s.center = s.radius
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p : P<VAR>s : EuclideanGeometry.Sphere P<GOAL>p ∈ s ↔ dist s.center p = s.radius
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>ps : Set P<VAR>s : EuclideanGeometry.Sphere P<GOAL>ps ⊆ Metric.sphere s.center s.radius ↔ ∀ p ∈ ps, p ∈ s
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p : P<VAR>ps : Set P<VAR>s : EuclideanGeometry.Sphere P<VAR>hp : p ∈ ps<VAR>hps : ps ⊆ Metric.sphere s.center s.radius<GOAL>dist p s.center = s.radius
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p c : P<VAR>ps : Set P<VAR>r : ℝ<VAR>hp : p ∈ ps<VAR>hps : ps ⊆ Metric.sphere { center := c, radius := r }.center { center := c, radius := r }.radius<GOAL>dist p c = r
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>s₁ s₂ : EuclideanGeometry.Sphere P<GOAL>s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>s₁ s₂ : EuclideanGeometry.Sphere P<VAR>p : P<VAR>hs₁ : p ∈ s₁<VAR>hs₂ : p ∈ s₂<GOAL>s₁.center = s₂.center ↔ s₁ = s₂
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>s₁ s₂ : EuclideanGeometry.Sphere P<VAR>p : P<VAR>hs₁ : p ∈ s₁<VAR>hs₂ : p ∈ s₂<GOAL>s₁.center ≠ s₂.center ↔ s₁ ≠ s₂
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p₁ p₂ : P<VAR>s : EuclideanGeometry.Sphere P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>dist p₁ s.center = dist p₂ s.center
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p₁ p₂ : P<VAR>s : EuclideanGeometry.Sphere P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>dist s.center p₁ = dist s.center p₂
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>ps : Set P<GOAL>EuclideanGeometry.Cospherical ps ↔ ∃ center radius, ∀ p ∈ ps, dist p center = radius
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>ps : Set P<GOAL>EuclideanGeometry.Cospherical ps ↔ ∃ s, ps ⊆ Metric.sphere s.center s.radius
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>s : EuclideanGeometry.Sphere P<GOAL>EuclideanGeometry.Cospherical (Metric.sphere s.center s.radius)
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>ps₁ ps₂ : Set P<VAR>hs : ps₁ ⊆ ps₂<VAR>hc : EuclideanGeometry.Cospherical ps₂<GOAL>EuclideanGeometry.Cospherical ps₁
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>Nonempty P<GOAL>EuclideanGeometry.Cospherical ∅
<VAR>P : Type u_2<VAR>MetricSpace P<VAR>p : P<GOAL>EuclideanGeometry.Cospherical {p}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>EuclideanGeometry.Cospherical {p₁, p₂}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps : Set P<VAR>self : EuclideanGeometry.Concyclic ps<GOAL>Coplanar ℝ ps
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps : Set P<VAR>self : EuclideanGeometry.Concyclic ps<GOAL>EuclideanGeometry.Cospherical ps
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>ps₁ ps₂ : Set P<VAR>hs : ps₁ ⊆ ps₂<VAR>h : EuclideanGeometry.Concyclic ps₂<GOAL>EuclideanGeometry.Concyclic ps₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<GOAL>EuclideanGeometry.Concyclic ∅
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p : P<GOAL>EuclideanGeometry.Concyclic {p}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>p₁ p₂ : P<GOAL>EuclideanGeometry.Concyclic {p₁, 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 : Set P<VAR>hs : EuclideanGeometry.Cospherical s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<GOAL>AffineIndependent ℝ 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 : Set P<VAR>hs : EuclideanGeometry.Cospherical s<VAR>p₁ p₂ p₃ : P<VAR>h₁ : p₁ ∈ s<VAR>h₂ : p₂ ∈ s<VAR>h₃ : p₃ ∈ s<VAR>h₁₂ : p₁ ≠ p₂<VAR>h₁₃ : p₁ ≠ p₃<VAR>h₂₃ : p₂ ≠ p₃<GOAL>AffineIndependent ℝ ![p₁, p₂, 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>p₁ p₂ p₃ : P<VAR>hs : EuclideanGeometry.Cospherical {p₁, p₂, p₃}<VAR>h₁₂ : p₁ ≠ p₂<VAR>h₁₃ : p₁ ≠ p₃<VAR>h₂₃ : p₂ ≠ p₃<GOAL>AffineIndependent ℝ ![p₁, p₂, 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>p₁ p₂ : P<VAR>s₁ s₂ : EuclideanGeometry.Sphere P<VAR>hp₁s₁ : p₁ ∈ s₁<VAR>hp₂s₁ : p₂ ∈ s₁<VAR>hp₁s₂ : p₁ ∈ s₂<VAR>hp₂s₂ : p₂ ∈ s₂<GOAL>⟪s₂.center -ᵥ s₁.center, p₂ -ᵥ p₁⟫_ℝ = 0
<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>FiniteDimensional ℝ ↥s.direction<VAR>hd : FiniteDimensional.finrank ℝ ↥s.direction = 2<VAR>s₁ s₂ : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p : P<VAR>hs₁ : s₁.center ∈ s<VAR>hs₂ : s₂.center ∈ s<VAR>hp₁s : p₁ ∈ s<VAR>hp₂s : p₂ ∈ s<VAR>hps : p ∈ s<VAR>hs : s₁ ≠ s₂<VAR>hp : p₁ ≠ p₂<VAR>hp₁s₁ : p₁ ∈ s₁<VAR>hp₂s₁ : p₂ ∈ s₁<VAR>hps₁ : p ∈ s₁<VAR>hp₁s₂ : p₁ ∈ s₂<VAR>hp₂s₂ : p₂ ∈ s₂<VAR>hps₂ : p ∈ s₂<GOAL>p = p₁ ∨ p = p₂