Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃ (NazgandLean4/quaternionLemma.lean)

State before:
⊢ Soqqtstqm1₁ = Soqqtstqm1₃
Tactic:
ext ⟨r, x, y, z⟩
State after:
case h.mk
r x y z : ℝ
⊢ { re := r, imI := x, imJ := y, imK := z } ∈ Soqqtstqm1₁ ↔ { re := r, imI := x, imJ := y, imK := z } ∈ Soqqtstqm1₃

State before:
case h.mk
r x y z : ℝ
⊢ { re := r, imI := x, imJ := y, imK := z } ∈ Soqqtstqm1₁ ↔ { re := r, imI := x, imJ := y, imK := z } ∈ Soqqtstqm1₃
Tactic:
dsimp [Soqqtstqm1₁, Soqqtstqm1₃, Soqtstn1₁]
State after:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz,
      { re := r, imI := x, imJ := y, imK := z } = { re := 1 / 2, imI := rx, imJ := ry, imK := rz } ∧
        rx * rx + ry * ry + rz * rz = 3 / 4) ↔
    ∃ qim,
      (∃ rx ry rz, qim = { re := 0, imI := rx, imJ := ry, imK := rz } ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        { re := r, imI := x, imJ := y, imK := z } = 1 / 2 + qim * ↑√3 / 2

State before:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz,
      { re := r, imI := x, imJ := y, imK := z } = { re := 1 / 2, imI := rx, imJ := ry, imK := rz } ∧
        rx * rx + ry * ry + rz * rz = 3 / 4) ↔
    ∃ qim,
      (∃ rx ry rz, qim = { re := 0, imI := rx, imJ := ry, imK := rz } ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        { re := r, imI := x, imJ := y, imK := z } = 1 / 2 + qim * ↑√3 / 2
Tactic:
simp only [one_div, ext_iff, add_re, add_imI, add_imJ, add_imK]
State after:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4) ↔
    ∃ qim,
      (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
          x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK

State before:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4) ↔
    ∃ qim,
      (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
          x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
Tactic:
constructor
State after:
case h.mk.mp
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4) →
    ∃ qim,
      (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
          x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK

case h.mk.mpr
r x y z : ℝ
⊢ (∃ qim,
      (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
          x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK) →
    ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4

State before:
case h.mk.mp
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4) →
    ∃ qim,
      (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
          x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
Tactic:
intros h₀
State after:
case h.mk.mp
r x y z : ℝ
h₀ : ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
⊢ ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK

State before:
case h.mk.mp
r x y z : ℝ
h₀ : ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
⊢ ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
Tactic:
rcases h₀ with ⟨rx, ry, rz, hx, hSphere⟩
State after:
case h.mk.mp.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hx : r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
⊢ ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK

State before:
case h.mk.mp.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hx : r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
⊢ ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
Tactic:
rcases hx with ⟨hr, hx, hy, hz⟩
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
Tactic:
use (@QuaternionAlgebra.mk ℝ (-1) (-1) 0 (rx * 2 / Real.sqrt 3) (ry * 2 / Real.sqrt 3) (rz * 2 / Real.sqrt 3))
State after:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ (∃ rx_1 ry_1 rz_1,
      ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 }.re = 0 ∧
          { re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 }.imI = rx_1 ∧
            { re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 }.imJ = ry_1 ∧
              { re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 }.imK = rz_1) ∧
        rx_1 * rx_1 + ry_1 * ry_1 + rz_1 * rz_1 = 1) ∧
    r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re ∧
      x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
        y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
          z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK

State before:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ (∃ rx_1 ry_1 rz_1,
      ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 }.re = 0 ∧
          { re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 }.imI = rx_1 ∧
            { re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 }.imJ = ry_1 ∧
              { re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 }.imK = rz_1) ∧
        rx_1 * rx_1 + ry_1 * ry_1 + rz_1 * rz_1 = 1) ∧
    r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re ∧
      x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
        y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
          z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
simp only [true_and]
State after:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ (∃ rx_1 ry_1 rz_1,
      (rx * 2 / √3 = rx_1 ∧ ry * 2 / √3 = ry_1 ∧ rz * 2 / √3 = rz_1) ∧ rx_1 * rx_1 + ry_1 * ry_1 + rz_1 * rz_1 = 1) ∧
    r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re ∧
      x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
        y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
          z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK

State before:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ (∃ rx_1 ry_1 rz_1,
      (rx * 2 / √3 = rx_1 ∧ ry * 2 / √3 = ry_1 ∧ rz * 2 / √3 = rz_1) ∧ rx_1 * rx_1 + ry_1 * ry_1 + rz_1 * rz_1 = 1) ∧
    r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re ∧
      x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
        y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
          z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
constructor
State after:
case h.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ∃ rx_1 ry_1 rz_1,
    (rx * 2 / √3 = rx_1 ∧ ry * 2 / √3 = ry_1 ∧ rz * 2 / √3 = rz_1) ∧ rx_1 * rx_1 + ry_1 * ry_1 + rz_1 * rz_1 = 1

case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
      y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
        z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK

State before:
case h.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ∃ rx_1 ry_1 rz_1,
    (rx * 2 / √3 = rx_1 ∧ ry * 2 / √3 = ry_1 ∧ rz * 2 / √3 = rz_1) ∧ rx_1 * rx_1 + ry_1 * ry_1 + rz_1 * rz_1 = 1
Tactic:
use rx * 2 / Real.sqrt 3
State after:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ∃ ry_1 rz_1,
    (rx * 2 / √3 = rx * 2 / √3 ∧ ry * 2 / √3 = ry_1 ∧ rz * 2 / √3 = rz_1) ∧
      rx * 2 / √3 * (rx * 2 / √3) + ry_1 * ry_1 + rz_1 * rz_1 = 1

State before:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ∃ ry_1 rz_1,
    (rx * 2 / √3 = rx * 2 / √3 ∧ ry * 2 / √3 = ry_1 ∧ rz * 2 / √3 = rz_1) ∧
      rx * 2 / √3 * (rx * 2 / √3) + ry_1 * ry_1 + rz_1 * rz_1 = 1
Tactic:
use ry * 2 / Real.sqrt 3
State after:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ∃ rz_1,
    (rx * 2 / √3 = rx * 2 / √3 ∧ ry * 2 / √3 = ry * 2 / √3 ∧ rz * 2 / √3 = rz_1) ∧
      rx * 2 / √3 * (rx * 2 / √3) + ry * 2 / √3 * (ry * 2 / √3) + rz_1 * rz_1 = 1

State before:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ∃ rz_1,
    (rx * 2 / √3 = rx * 2 / √3 ∧ ry * 2 / √3 = ry * 2 / √3 ∧ rz * 2 / √3 = rz_1) ∧
      rx * 2 / √3 * (rx * 2 / √3) + ry * 2 / √3 * (ry * 2 / √3) + rz_1 * rz_1 = 1
Tactic:
use rz * 2 / Real.sqrt 3
State after:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ (rx * 2 / √3 = rx * 2 / √3 ∧ ry * 2 / √3 = ry * 2 / √3 ∧ rz * 2 / √3 = rz * 2 / √3) ∧
    rx * 2 / √3 * (rx * 2 / √3) + ry * 2 / √3 * (ry * 2 / √3) + rz * 2 / √3 * (rz * 2 / √3) = 1

State before:
case h
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ (rx * 2 / √3 = rx * 2 / √3 ∧ ry * 2 / √3 = ry * 2 / √3 ∧ rz * 2 / √3 = rz * 2 / √3) ∧
    rx * 2 / √3 * (rx * 2 / √3) + ry * 2 / √3 * (ry * 2 / √3) + rz * 2 / √3 * (rz * 2 / √3) = 1
Tactic:
constructor
State after:
case h.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ rx * 2 / √3 = rx * 2 / √3 ∧ ry * 2 / √3 = ry * 2 / √3 ∧ rz * 2 / √3 = rz * 2 / √3

case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ rx * 2 / √3 * (rx * 2 / √3) + ry * 2 / √3 * (ry * 2 / √3) + rz * 2 / √3 * (rz * 2 / √3) = 1

State before:
case h.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ rx * 2 / √3 = rx * 2 / √3 ∧ ry * 2 / √3 = ry * 2 / √3 ∧ rz * 2 / √3 = rz * 2 / √3
Tactic:
simp only [and_self]
State after:
no goals

State before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ rx * 2 / √3 * (rx * 2 / √3) + ry * 2 / √3 * (ry * 2 / √3) + rz * 2 / √3 * (rz * 2 / √3) = 1
Tactic:
ring_nf
State after:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ rx ^ 2 * (√3)⁻¹ ^ 2 * 4 + (√3)⁻¹ ^ 2 * ry ^ 2 * 4 + (√3)⁻¹ ^ 2 * rz ^ 2 * 4 = 1

State before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ rx ^ 2 * (√3)⁻¹ ^ 2 * 4 + (√3)⁻¹ ^ 2 * ry ^ 2 * 4 + (√3)⁻¹ ^ 2 * rz ^ 2 * 4 = 1
Tactic:
have h3g0 : (0 : ℝ) ≤ 3 := by linarith
State after:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
⊢ rx ^ 2 * (√3)⁻¹ ^ 2 * 4 + (√3)⁻¹ ^ 2 * ry ^ 2 * 4 + (√3)⁻¹ ^ 2 * rz ^ 2 * 4 = 1

State before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
⊢ rx ^ 2 * (√3)⁻¹ ^ 2 * 4 + (√3)⁻¹ ^ 2 * ry ^ 2 * 4 + (√3)⁻¹ ^ 2 * rz ^ 2 * 4 = 1
Tactic:
simp only [inv_pow, Real.sq_sqrt h3g0]
State after:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = 1

State before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = 1
Tactic:
have hSphere₂ := congrArg (λ (x₀ : ℝ) => x₀ * 4 / 3) hSphere
State after:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (fun x₀ => x₀ * 4 / 3) (rx * rx + ry * ry + rz * rz) = (fun x₀ => x₀ * 4 / 3) (3 / 4)
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = 1

State before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (fun x₀ => x₀ * 4 / 3) (rx * rx + ry * ry + rz * rz) = (fun x₀ => x₀ * 4 / 3) (3 / 4)
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = 1
Tactic:
simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
  IsUnit.div_mul_cancel, div_self] at hSphere₂
State after:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (rx * rx + ry * ry + rz * rz) * 4 / 3 = 1
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = 1

State before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (rx * rx + ry * ry + rz * rz) * 4 / 3 = 1
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = 1
Tactic:
rw [←hSphere₂]
State after:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (rx * rx + ry * ry + rz * rz) * 4 / 3 = 1
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = (rx * rx + ry * ry + rz * rz) * 4 / 3

State before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (rx * rx + ry * ry + rz * rz) * 4 / 3 = 1
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = (rx * rx + ry * ry + rz * rz) * 4 / 3
Tactic:
ring
State after:
no goals

State before:
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ 0 ≤ 3
Tactic:
linarith
State after:
no goals

State before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
      y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
        z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
constructor
State after:
case h.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re

case h.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
    y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
      z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK

State before:
case h.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re
Tactic:
sorry
State after:
no goals

State before:
case h.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
    y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
      z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
constructor
State after:
case h.right.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI

case h.right.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
    z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK

State before:
case h.right.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI
Tactic:
sorry
State after:
no goals

State before:
case h.right.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
    z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
constructor
State after:
case h.right.right.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ

case h.right.right.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK

State before:
case h.right.right.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ
Tactic:
sorry
State after:
no goals

State before:
case h.right.right.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
sorry
State after:
no goals

State before:
case h.mk.mpr
r x y z : ℝ
⊢ (∃ qim,
      (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
          x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK) →
    ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
intros h₀
State after:
case h.mk.mpr
r x y z : ℝ
h₀ :
  ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4

State before:
case h.mk.mpr
r x y z : ℝ
h₀ :
  ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
rcases h₀ with ⟨qim, hx₁, hx₂⟩
State after:
case h.mk.mpr.intro.intro
r x y z : ℝ
qim : ℍ
hx₁ : ∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1
hx₂ :
  r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4

State before:
case h.mk.mpr.intro.intro
r x y z : ℝ
qim : ℍ
hx₁ : ∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1
hx₂ :
  r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
rcases hx₁ with ⟨rx, ry, rz, hQim, hSphere⟩
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
hx₂ :
  r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
rx ry rz : ℝ
hQim : qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4

State before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
hx₂ :
  r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
rx ry rz : ℝ
hQim : qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
rcases hx₂ with ⟨hr, hx, hy, hz⟩
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hQim : qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4

State before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hQim : qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
rcases hQim with ⟨hQimR, hQimI, hQimJ, hQimK⟩
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4

State before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
use x
State after:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ ry rz, (r = 2⁻¹ ∧ x = x ∧ y = ry ∧ z = rz) ∧ x * x + ry * ry + rz * rz = 3 / 4

State before:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ ry rz, (r = 2⁻¹ ∧ x = x ∧ y = ry ∧ z = rz) ∧ x * x + ry * ry + rz * rz = 3 / 4
Tactic:
use y
State after:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ rz, (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 3 / 4

State before:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ rz, (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 3 / 4
Tactic:
use z
State after:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 3 / 4

State before:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 3 / 4
Tactic:
simp only [and_self, and_true]
State after:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ r = 2⁻¹ ∧ x * x + y * y + z * z = 3 / 4

State before:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ r = 2⁻¹ ∧ x * x + y * y + z * z = 3 / 4
Tactic:
constructor
State after:
case h.left
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ r = 2⁻¹

case h.right
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ x * x + y * y + z * z = 3 / 4

State before:
case h.left
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ r = 2⁻¹
Tactic:
sorry
State after:
no goals

State before:
case h.right
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ x * x + y * y + z * z = 3 / 4
Tactic:
sorry
State after:
no goals