MAT3253 Complex Variables

5. Chapter 2.7 Stereographic projection🔗

In Section 2.7 we define the stereographic projection. The main theorem is

Theorem 2.7.1. Define the stereographic projection

P :\mathbb{R}^2 \rightarrow S\setminus \{(0,0,2r)\}

by

P(x,y) = \Big( \frac{4r^2x}{4r^2+x^2+y^2},\ \frac{4r^2y}{4r^2+x^2+y^2},\ \frac{2r(x^2+y^2)}{4r^2+x^2+y^2} \Big).

This gives a bijection between the complex plane \mathbb{R}^2 and the punctured sphere S\setminus \{(0,0,2r)\}.

The point (0,0,2r) is called the point at infinity.

We want to show that this bijection maps circle/line on the complex plane to circles on the Riemann sphere. Straight lines on the complex plane correspond to circles that passes through the north pole.

The formalization below is done with the help of Harmonics Aristotle.

import Mathlib.Data.Complex.Basic
import Mathlib.Tactic

This section is noncomputable.

noncomputable section stereograph_projection

Open the name space Complex, Real and Set.

open Complex Real Set variable (r : ℝ) -- r is the radius of the sphere

Definitions of the Riemann sphere S r with radius r. The point in S r satisfies

x^2 + y^2+ (z-r)^2 = r^2

In the definition below, p.1 is the x-coordinate, p.2.1 is the y-coordinate and p.2.2 is the z-coordinate.

def S : Set (ℝ × ℝ × ℝ) := { p | p.1^2 + p.2.1^2 + (p.2.2 - r)^2 = r^2 }

The north pole / point at infinity N is the point (0,0,2r).

def N : ℝ × ℝ × ℝ := (0, 0, 2 * r)

The stereographic projection is represented by P r A point p is mapped to P r p.

def P (p : ℝ × ℝ) : ℝ × ℝ × ℝ := let x := p.1 let y := p.2 let den := 4 * r^2 + x^2 + y^2 (4 * r^2 * x / den, 4 * r^2 * y / den, 2 * r * (x^2 + y^2) / den)

Define the inverse of the stereographic projection by Q

def Q (p : ℝ × ℝ × ℝ) : ℝ × ℝ := let α := p.1 let β := p.2.1 let γ := p.2.2 let den := 2 * r - γ (2 * r * α / den, 2 * r * β / den)

Show tha the image of the stereographic projection P lies in the punctured Riemann sphere S r\ {N r}.

theorem P_range (h_r : r > 0) -- asume r is positive (p : ℝ × ℝ) : P r p ∈ S r \ {N r} := r:ℝh_r:r > 0p:ℝ × ℝ⊢ P r p ∈ S r \ {N r} -- Substitute the coordinates of `P(p)` -- into the equation of the sphere $S$. have h_sphere : (4 * r^2 * p.1 / (4 * r^2 + p.1^2 + p.2^2))^2 + (4 * r^2 * p.2 / (4 * r^2 + p.1^2 + p.2^2))^2 + (2 * r * (p.1^2 + p.2^2) / (4 * r^2 + p.1^2 + p.2^2) - r)^2 = r^2 := r:ℝh_r:r > 0p:ℝ × ℝ⊢ P r p ∈ S r \ {N r} All goals completed! 🐙 r:ℝh_r:r > 0p:ℝ × ℝh_sphere:(4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ^ 2 + (4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ^ 2 + (2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) - r) ^ 2 = r ^ 2⊢ (have x := p.1; have y := p.2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)) ∈ {p | p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2} \ {(0, 0, 2 * r)} All goals completed! 🐙

Next, show that P and Q are inverse of each other.

/-- The composition P ∘ Q is the identity function on the punctured sphere S \ {N}. -/ theorem P_left_inv (h_r : r > 0) (p : ℝ × ℝ × ℝ) (hp : p ∈ S r \ {N r}) : P r (Q r p) = p := r:ℝh_r:r > 0p:ℝ × ℝ × ℝhp:p ∈ S r \ {N r}⊢ P r (Q r p) = p r:ℝh_r:r > 0p:ℝ × ℝ × ℝhp:p ∈ {p | p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2} \ {N r}⊢ (have x := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).1; have y := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)) = p r:ℝh_r:r > 0p:ℝ × ℝ × ℝhp:p ∈ {p | p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2} \ {N r}h:2 * r - p.2.2 = 0⊢ (have x := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).1; have y := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)) = pr:ℝh_r:r > 0p:ℝ × ℝ × ℝhp:p ∈ {p | p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2} \ {N r}h:¬2 * r - p.2.2 = 0⊢ (have x := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).1; have y := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)) = p r:ℝh_r:r > 0p:ℝ × ℝ × ℝhp:p ∈ {p | p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2} \ {N r}h:2 * r - p.2.2 = 0⊢ (have x := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).1; have y := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)) = pr:ℝh_r:r > 0p:ℝ × ℝ × ℝhp:p ∈ {p | p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2} \ {N r}h:¬2 * r - p.2.2 = 0⊢ (have x := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).1; have y := (have α := p.1; have β := p.2.1; have γ := p.2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)).2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)) = p r:ℝp:ℝ × ℝ × ℝh_r:0 < rhp:p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2 ∧ ¬p = N rh:¬2 * r = p.2.2⊢ (4 * r ^ 2 * (2 * r * p.1 / (2 * r - p.2.2)) / (4 * r ^ 2 + (2 * r * p.1 / (2 * r - p.2.2)) ^ 2 + (2 * r * p.2.1 / (2 * r - p.2.2)) ^ 2), 4 * r ^ 2 * (2 * r * p.2.1 / (2 * r - p.2.2)) / (4 * r ^ 2 + (2 * r * p.1 / (2 * r - p.2.2)) ^ 2 + (2 * r * p.2.1 / (2 * r - p.2.2)) ^ 2), 2 * r * ((2 * r * p.1 / (2 * r - p.2.2)) ^ 2 + (2 * r * p.2.1 / (2 * r - p.2.2)) ^ 2) / (4 * r ^ 2 + (2 * r * p.1 / (2 * r - p.2.2)) ^ 2 + (2 * r * p.2.1 / (2 * r - p.2.2)) ^ 2)) = p r:ℝp:ℝ × ℝ × ℝh_r:0 < rhp:p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2 ∧ ¬p = N rh:2 * r = p.2.2⊢ (0, 0, 0) = p exact False.elim <| hp.2 <| Prod.mk_inj.mpr ⟨ r:ℝp:ℝ × ℝ × ℝh_r:0 < rhp:p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2 ∧ ¬p = N rh:2 * r = p.2.2⊢ p.1 = 0 All goals completed! 🐙, Prod.mk_inj.mpr ⟨ r:ℝp:ℝ × ℝ × ℝh_r:0 < rhp:p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2 ∧ ¬p = N rh:2 * r = p.2.2⊢ p.2.1 = 0 All goals completed! 🐙, r:ℝp:ℝ × ℝ × ℝh_r:0 < rhp:p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2 ∧ ¬p = N rh:2 * r = p.2.2⊢ p.2.2 = 2 * r All goals completed! 🐙 ⟩ ⟩ r:ℝp:ℝ × ℝ × ℝh_r:0 < rhp:p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2 ∧ ¬p = N rh:¬2 * r = p.2.2⊢ (4 * r ^ 2 * (2 * r * p.1 / (2 * r - p.2.2)) / (4 * r ^ 2 + (2 * r * p.1 / (2 * r - p.2.2)) ^ 2 + (2 * r * p.2.1 / (2 * r - p.2.2)) ^ 2), 4 * r ^ 2 * (2 * r * p.2.1 / (2 * r - p.2.2)) / (4 * r ^ 2 + (2 * r * p.1 / (2 * r - p.2.2)) ^ 2 + (2 * r * p.2.1 / (2 * r - p.2.2)) ^ 2), 2 * r * ((2 * r * p.1 / (2 * r - p.2.2)) ^ 2 + (2 * r * p.2.1 / (2 * r - p.2.2)) ^ 2) / (4 * r ^ 2 + (2 * r * p.1 / (2 * r - p.2.2)) ^ 2 + (2 * r * p.2.1 / (2 * r - p.2.2)) ^ 2)) = p r:ℝp:ℝ × ℝ × ℝh_r:0 < rhp:p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2 ∧ ¬p = N rh:¬2 * r = p.2.2⊢ (4 * r * 2 * p.1 / ((r * 2 - p.2.2) * (4 + 2 ^ 2 * p.1 ^ 2 / (r * 2 - p.2.2) ^ 2 + 2 ^ 2 * p.2.1 ^ 2 / (r * 2 - p.2.2) ^ 2)), 4 * r * 2 * p.2.1 / ((r * 2 - p.2.2) * (4 + 2 ^ 2 * p.1 ^ 2 / (r * 2 - p.2.2) ^ 2 + 2 ^ 2 * p.2.1 ^ 2 / (r * 2 - p.2.2) ^ 2)), r * 2 ^ 3 * (p.1 ^ 2 + p.2.1 ^ 2) / ((r * 2 - p.2.2) ^ 2 * (4 + 2 ^ 2 * p.1 ^ 2 / (r * 2 - p.2.2) ^ 2 + 2 ^ 2 * p.2.1 ^ 2 / (r * 2 - p.2.2) ^ 2))) = p All goals completed! 🐙 /- The composition Q ∘ P is the identity on the complex plane. -/ theorem P_right_inv (h_r : r > 0) (p : ℝ × ℝ) : Q r (P r p) = p := r:ℝh_r:r > 0p:ℝ × ℝ⊢ Q r (P r p) = p r:ℝh_r:r > 0p:ℝ × ℝ⊢ (have α := (have x := p.1; have y := p.2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)).1; have β := (have x := p.1; have y := p.2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)).2.1; have γ := (have x := p.1; have y := p.2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den)).2.2; have den := 2 * r - γ; (2 * r * α / den, 2 * r * β / den)) = p r:ℝh_r:r > 0p:ℝ × ℝ⊢ (r ^ 2 * 4 * p.1 / (r ^ 2 * 4 + p.1 ^ 2 + p.2 ^ 2 - (p.1 ^ 2 + p.2 ^ 2)), r ^ 2 * 4 * p.2 / (r ^ 2 * 4 + p.1 ^ 2 + p.2 ^ 2 - (p.1 ^ 2 + p.2 ^ 2))) = p All goals completed! 🐙 def S_minus_N (r : ℝ) : Set (ℝ × ℝ × ℝ) := S r \ {N r} def P_to_S (h_r : r > 0) (p : ℝ × ℝ) : S_minus_N r := ⟨P r p, P_range r h_r p⟩ theorem P_bijective (h_r : r > 0) : Function.Bijective (P_to_S r h_r) := r:ℝh_r:r > 0⊢ Function.Bijective (P_to_S r h_r) r:ℝh_r:r > 0⊢ Function.Injective (P_to_S r h_r)r:ℝh_r:r > 0⊢ Function.Surjective (P_to_S r h_r); r:ℝh_r:r > 0⊢ Function.Injective (P_to_S r h_r) intro p r:ℝh_r:r > 0p:ℝ × ℝq:ℝ × ℝ⊢ P_to_S r h_r p = P_to_S r h_r q → p = q r:ℝh_r:r > 0p:ℝ × ℝq:ℝ × ℝh_eq:P_to_S r h_r p = P_to_S r h_r q⊢ p = q r:ℝh_r:r > 0p:ℝ × ℝq:ℝ × ℝh_eq:⟨P r p, ⋯⟩ = ⟨P r q, ⋯⟩⊢ p = q r:ℝh_r:r > 0p:ℝ × ℝq:ℝ × ℝh_eq:⟨P r p, ⋯⟩ = ⟨P r q, ⋯⟩this:Q r (P r p) = p⊢ p = q r:ℝh_r:r > 0p:ℝ × ℝq:ℝ × ℝh_eq:⟨P r p, ⋯⟩ = ⟨P r q, ⋯⟩this✝:Q r (P r p) = pthis:Q r (P r q) = q⊢ p = q All goals completed! 🐙 r:ℝh_r:r > 0⊢ Function.Surjective (P_to_S r h_r) r:ℝh_r:r > 0p:↑(S_minus_N r)⊢ ∃ a, P_to_S r h_r a = p; r:ℝh_r:r > 0p:↑(S_minus_N r)this:↑p ∈ S r \ {N r} → P r (Q r ↑p) = ↑p⊢ ∃ a, P_to_S r h_r a = p r:ℝh_r:r > 0p:↑(S_minus_N r)this:↑p ∈ S r \ {N r} → P r (Q r ↑p) = ↑p⊢ ∃ a, ⟨P r a, ⋯⟩ = p All goals completed! 🐙 /- The complex definition of stereographic projection is equivalent to the real definition. -/ def P_complex (z : ℂ) : ℝ × ℝ × ℝ := let den := 4 * r^2 + ‖z‖^2 (4 * r^2 * z.re / den, 4 * r^2 * z.im / den, 2 * r * ‖z‖^2 / den) theorem P_complex_eq_P (z : ℂ) : P_complex r z = P r (z.re, z.im) := r:ℝz:ℂ⊢ P_complex r z = P r (z.re, z.im) r:ℝz:ℂ⊢ (have den := 4 * r ^ 2 + ‖z‖ ^ 2; (4 * r ^ 2 * z.re / den, 4 * r ^ 2 * z.im / den, 2 * r * ‖z‖ ^ 2 / den)) = have x := (z.re, z.im).1; have y := (z.re, z.im).2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den) r:ℝz:ℂ⊢ 4 * r ^ 2 * z.re / (4 * r ^ 2 + (z.re * z.re + z.im * z.im)) = 4 * r ^ 2 * z.re / (4 * r ^ 2 + z.re ^ 2 + z.im ^ 2) ∧ 4 * r ^ 2 * z.im / (4 * r ^ 2 + (z.re * z.re + z.im * z.im)) = 4 * r ^ 2 * z.im / (4 * r ^ 2 + z.re ^ 2 + z.im ^ 2) ∧ 2 * r * (z.re * z.re + z.im * z.im) / (4 * r ^ 2 + (z.re * z.re + z.im * z.im)) = 2 * r * (z.re ^ 2 + z.im ^ 2) / (4 * r ^ 2 + z.re ^ 2 + z.im ^ 2) r:ℝz:ℂ⊢ True ∧ True ∧ True All goals completed! 🐙

A set s is a circle or line if the points (x,y)$ in s satisfy the equation

A(x^2+y^2)+Bx+Cy +D = 0

for some constants A, B, C and D are real numbers that arenot all equal to 0. When A is nonzero, this equation represents a circle. When A is zero, it is a straight line.

def IsCircleOrLine (s : Set (ℝ × ℝ)) : Prop := ∃ A B C D : ℝ, (A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0) ∧ s = {p | A * (p.1^2 + p.2^2) + B * p.1 + C * p.2 + D = 0}

A set of points (x,y,z) on the Riemann sphere S r lie on a plane section if tehre are real constants a, b, c, not all zero, such that

a x + b y + c = d

for some real constant d.

def IsPlaneSection (r : ℝ) (s : Set (ℝ × ℝ × ℝ)) : Prop := ∃ a b c d : ℝ, (a ≠ 0 ∨ b ≠ 0 ∨ c ≠ 0) ∧ s = S r ∩ { p | a * p.1 + b * p.2.1 + c * p.2.2 = d }

We will show at the end of this section that the locus of this equation is mapped to a circle on the Riemann sphere. We first establish a correspondence between a point p ont the plane and its stereographic projection q on the Riemann sphere S r with radius r.

lemma stereographic_equation_iff (r : ℝ) (hr : r ≠ 0) (A B C D : ℝ) : let a := -B let b := -C let c := (D - 4 * r^2 * A) / (2 * r) let d := D ∀ p : ℝ × ℝ, A * (p.1^2 + p.2^2) + B * p.1 + C * p.2 + D = 0 ↔ let q := P r p a * q.1 + b * q.2.1 + c * q.2.2 = d := r:ℝhr:r ≠ 0A:ℝB:ℝC:ℝD:ℝ⊢ let a := -B; let b := -C; let c := (D - 4 * r ^ 2 * A) / (2 * r); let d := D; ∀ (p : ℝ × ℝ), A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0 ↔ let q := P r p; a * q.1 + b * q.2.1 + c * q.2.2 = d r:ℝhr:r ≠ 0A:ℝB:ℝC:ℝD:ℝ⊢ let a := -B; let b := -C; let c := (D - 4 * r ^ 2 * A) / (2 * r); let d := D; ∀ (p : ℝ × ℝ), A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0 ↔ let q := have x := p.1; have y := p.2; have den := 4 * r ^ 2 + x ^ 2 + y ^ 2; (4 * r ^ 2 * x / den, 4 * r ^ 2 * y / den, 2 * r * (x ^ 2 + y ^ 2) / den); a * q.1 + b * q.2.1 + c * q.2.2 = d r:ℝhr:r ≠ 0A:ℝB:ℝC:ℝD:ℝ⊢ ∀ (p : ℝ × ℝ), A * (p.1 ^ 2 + p.2 ^ 2) + p.1 * B + p.2 * C + D = 0 ↔ 4 * r ^ 2 * (-(p.1 * B) + -(p.2 * C)) + (p.1 ^ 2 + p.2 ^ 2) * (D - A * 4 * r ^ 2) = D * (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) All goals completed! 🐙

Finally, we prove that if s is a circle or a line, then we can find a plane section s' on the Riemann sphere, such that the image of s through the stereographic projection is the plane section s', possibly except the point at infinity.

/-- The stereographic projection P maps circles and lines in the complex plane to plane sections of the sphere S. -/ theorem stereographic_preserves_circle_line (r : ℝ) (hr : r > 0) -- assume radius r is positive (s : Set (ℝ × ℝ)) -- s is a set on the plane (h : IsCircleOrLine s) -- assume s is a circle or line : ∃ s', IsPlaneSection r s' --there is a plane section s' ∧ P r '' s = s' \ {N r} --image of s lies in s` \ {N r} := r:ℝhr:r > 0s:Set (ℝ × ℝ)h:IsCircleOrLine s⊢ ∃ s', IsPlaneSection r s' ∧ P r '' s = s' \ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}⊢ ∃ s', IsPlaneSection r s' ∧ P r '' s = s' \ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0⊢ ∃ s', IsPlaneSection r s' ∧ P r '' s = s' \ {N r}r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)⊢ ∃ s', IsPlaneSection r s' ∧ P r '' s = s' \ {N r}; r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0⊢ ∃ s', IsPlaneSection r s' ∧ P r '' s = s' \ {N r} r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + D = 0}h:B = 0 ∧ C = 0 ∧ D - 4 * r ^ 2 * A = 0⊢ ∃ s', IsPlaneSection r s' ∧ P r '' {p | A * (p.1 ^ 2 + p.2 ^ 2) + D = 0} = s' \ {N r} -- Since $A \neq 0$, we can divide -- both sides of the equation -- $A * (p.1^2 + p.2^2) + 4 * r^2 * A = 0$ -- by $A$ to get $p.1^2 + p.2^2 + 4 * r^2 = 0$. have h_eq : {p : ℝ × ℝ | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅ := r:ℝhr:r > 0s:Set (ℝ × ℝ)h:IsCircleOrLine s⊢ ∃ s', IsPlaneSection r s' ∧ P r '' s = s' \ {N r} exact Set.eq_empty_of_forall_notMem fun p hp => hD <| r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + D = 0}h:B = 0 ∧ C = 0 ∧ D - 4 * r ^ 2 * A = 0p:ℝ × ℝhp:p ∈ {p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0}⊢ A = 0 All goals completed! 🐙 ; r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = ∅h:B = 0 ∧ C = 0 ∧ D = 4 * r ^ 2 * Ah_eq:{p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅⊢ ∃ s', IsPlaneSection r s' ∧ ∅ = s' \ {N r} r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = ∅h:B = 0 ∧ C = 0 ∧ D = 4 * r ^ 2 * Ah_eq:{p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅⊢ IsPlaneSection r ∅r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = ∅h:B = 0 ∧ C = 0 ∧ D = 4 * r ^ 2 * Ah_eq:{p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅⊢ ∅ = ∅ \ {N r} r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = ∅h:B = 0 ∧ C = 0 ∧ D = 4 * r ^ 2 * Ah_eq:{p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅⊢ IsPlaneSection r ∅r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = ∅h:B = 0 ∧ C = 0 ∧ D = 4 * r ^ 2 * Ah_eq:{p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅⊢ ∅ = ∅ \ {N r} All goals completed! 🐙 r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = ∅h:B = 0 ∧ C = 0 ∧ D = 4 * r ^ 2 * Ah_eq:{p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅⊢ (0 ≠ 0 ∨ 0 ≠ 0 ∨ 1 ≠ 0) ∧ ∅ = S r ∩ {p | 0 * p.1 + 0 * p.2.1 + 1 * p.2.2 = 3 * r} r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = ∅h:B = 0 ∧ C = 0 ∧ D = 4 * r ^ 2 * Ah_eq:{p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅⊢ ∅ = {p | p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2} ∩ {p | p.2.2 = 3 * r}; exact Eq.symm ( Set.eq_empty_of_forall_notMem fun p hp => r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhr:0 < rhD:¬A = 0hs:s = ∅h:B = 0 ∧ C = 0 ∧ D = 4 * r ^ 2 * Ah_eq:{p | A * (p.1 ^ 2 + p.2 ^ 2) + 4 * r ^ 2 * A = 0} = ∅p:ℝ × ℝ × ℝhp:p ∈ {p | p.1 ^ 2 + p.2.1 ^ 2 + (p.2.2 - r) ^ 2 = r ^ 2} ∩ {p | p.2.2 = 3 * r}⊢ False All goals completed! 🐙 ) r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)⊢ ∃ s', IsPlaneSection r s' ∧ P r '' s = s' \ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)⊢ IsPlaneSection r (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D})r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)⊢ P r '' s = (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)⊢ IsPlaneSection r (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)⊢ (-B ≠ 0 ∨ -C ≠ 0 ∨ (D - 4 * r ^ 2 * A) / (2 * r) ≠ 0) ∧ S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D} = S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}; All goals completed! 🐙 r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)⊢ P r '' s = (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)x:ℝy:ℝz:ℝ⊢ (x, y, z) ∈ P r '' s ↔ (x, y, z) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)x:ℝy:ℝz:ℝ⊢ (x, y, z) ∈ P r '' s → (x, y, z) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r}r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)x:ℝy:ℝz:ℝ⊢ (x, y, z) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r} → (x, y, z) ∈ P r '' s r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)x:ℝy:ℝz:ℝ⊢ (x, y, z) ∈ P r '' s → (x, y, z) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)p:ℝ × ℝhp:p ∈ s⊢ (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)p:ℝ × ℝhp:p ∈ s⊢ (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ∈ S rr:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)p:ℝ × ℝhp:p ∈ s⊢ (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ∈ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)p:ℝ × ℝhp:p ∈ s⊢ (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ∉ {N r} r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)p:ℝ × ℝhp:p ∈ s⊢ (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ∈ S rr:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)p:ℝ × ℝhp:p ∈ s⊢ (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ∈ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)p:ℝ × ℝhp:p ∈ s⊢ (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2), 2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ∉ {N r} r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0⊢ (r = 0 ∨ p.1 = 0) ∨ 4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2 = 0 → (r = 0 ∨ p.2 = 0) ∨ 4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2 = 0 → ¬2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) = 2 * r r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0⊢ (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ^ 2 + (4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ^ 2 + (2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) - r) ^ 2 = r ^ 2 -- Combine like terms and simplify the expression. r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0⊢ 4 ^ 2 * r ^ 2 * (p.1 ^ 2 + p.2 ^ 2) + ((p.1 ^ 2 + p.2 ^ 2) * 2 - (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) ^ 2 = (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) ^ 2 All goals completed! 🐙 r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0⊢ -(B * (4 * r ^ 2 * p.1 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2))) + -(C * (4 * r ^ 2 * p.2 / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2))) + (D - 4 * r ^ 2 * A) / (2 * r) * (2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2)) = D r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0⊢ 4 * r ^ 2 * (-(B * p.1) + -(p.2 * C)) + (D - 4 * r ^ 2 * A) * (p.1 ^ 2 + p.2 ^ 2) = (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) * D r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0h✝:D < 0⊢ 4 * r ^ 2 * (-(B * p.1) + -(p.2 * C)) + (D - 4 * r ^ 2 * A) * (p.1 ^ 2 + p.2 ^ 2) = (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) * Dr:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0h✝:0 ≤ D⊢ 4 * r ^ 2 * (-(B * p.1) + -(p.2 * C)) + (D - 4 * r ^ 2 * A) * (p.1 ^ 2 + p.2 ^ 2) = (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) * D r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0h✝:D < 0⊢ 4 * r ^ 2 * (-(B * p.1) + -(p.2 * C)) + (D - 4 * r ^ 2 * A) * (p.1 ^ 2 + p.2 ^ 2) = (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) * Dr:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0h✝:0 ≤ D⊢ 4 * r ^ 2 * (-(B * p.1) + -(p.2 * C)) + (D - 4 * r ^ 2 * A) * (p.1 ^ 2 + p.2 ^ 2) = (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) * D All goals completed! 🐙 r:ℝs:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝp:ℝ × ℝhr:0 < rhD:¬A = 0 ∨ ¬B = 0 ∨ ¬C = 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:B = 0 → C = 0 → ¬D - 4 * r ^ 2 * A = 0 ∧ ¬r = 0hp:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0⊢ (r = 0 ∨ p.1 = 0) ∨ 4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2 = 0 → (r = 0 ∨ p.2 = 0) ∨ 4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2 = 0 → ¬2 * r * (p.1 ^ 2 + p.2 ^ 2) / (4 * r ^ 2 + p.1 ^ 2 + p.2 ^ 2) = 2 * r All goals completed! 🐙 r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)x:ℝy:ℝz:ℝ⊢ (x, y, z) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r} → (x, y, z) ∈ P r '' s r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)x:ℝy:ℝz:ℝhxyz:(x, y, z) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r}⊢ (x, y, z) ∈ P r '' s obtain ⟨p, hp⟩ : ∃ p : ℝ × ℝ, P r p = (x, y, z) := r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)x:ℝy:ℝz:ℝhxyz:(x, y, z) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r}⊢ ∃ p, P r p = (x, y, z) -- Use the inverse Q and `P_left_inv` -- to show surjectivity. All goals completed! 🐙 r:ℝhr:r > 0s:Set (ℝ × ℝ)A:ℝB:ℝC:ℝD:ℝhD:A ≠ 0 ∨ B ≠ 0 ∨ C ≠ 0hs:s = {p | A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0}h:¬(-B = 0 ∧ -C = 0 ∧ (D - 4 * r ^ 2 * A) / (2 * r) = 0)x:ℝy:ℝz:ℝhxyz:(x, y, z) ∈ (S r ∩ {p | -B * p.1 + -C * p.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * p.2.2 = D}) \ {N r}p:ℝ × ℝhp:P r p = (x, y, z)this:A * (p.1 ^ 2 + p.2 ^ 2) + B * p.1 + C * p.2 + D = 0 ↔ have q := P r p; -B * q.1 + -C * q.2.1 + (D - 4 * r ^ 2 * A) / (2 * r) * q.2.2 = D⊢ (x, y, z) ∈ P r '' s All goals completed! 🐙 end stereograph_projection