internlm/Lean-Github huggingface dataset:
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro.left
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ r ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro.right
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ r = 2⁻¹
Tactic:
exact hr
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mpr
r x y z : ℝ
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹ →
    ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
intros h₀
Proof state after:
case h.mk.mpr
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mpr
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
use x
Proof state after:
case h
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
⊢ ∃ ry rz, (r = 2⁻¹ ∧ x = x ∧ y = ry ∧ z = rz) ∧ x * x + ry * ry + rz * rz = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
⊢ ∃ ry rz, (r = 2⁻¹ ∧ x = x ∧ y = ry ∧ z = rz) ∧ x * x + ry * ry + rz * rz = 3 / 4
Tactic:
use y
Proof state after:
case h
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
⊢ ∃ rz, (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
⊢ ∃ rz, (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 3 / 4
Tactic:
use z
Proof state after:
case h
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 3 / 4
Tactic:
rcases h₀ with ⟨hNorm, hr⟩
Proof state after:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 3 / 4
Tactic:
simp only [hr, and_self, true_and]
Proof state after:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
⊢ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
⊢ x * x + y * y + z * z = 3 / 4
Tactic:
have hNormSqMr := congrArg (λ (x₀ : ℝ) => x₀ * x₀ - 1 / 4) hNorm
Proof state after:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : (fun x₀ => x₀ * x₀ - 1 / 4) ‖{ re := r, imI := x, imJ := y, imK := z }‖ = (fun x₀ => x₀ * x₀ - 1 / 4) 1
⊢ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : (fun x₀ => x₀ * x₀ - 1 / 4) ‖{ re := r, imI := x, imJ := y, imK := z }‖ = (fun x₀ => x₀ * x₀ - 1 / 4) 1
⊢ x * x + y * y + z * z = 3 / 4
Tactic:
simp only [one_div, mul_one, ←Quaternion.normSq_eq_norm_mul_self, Quaternion.normSq_def'] at hNormSqMr
Proof state after:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : r ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 - 4⁻¹ = 1 - 4⁻¹
⊢ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : r ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 - 4⁻¹ = 1 - 4⁻¹
⊢ x * x + y * y + z * z = 3 / 4
Tactic:
simp only [hr, inv_pow] at hNormSqMr
Proof state after:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : (2 ^ 2)⁻¹ + x ^ 2 + y ^ 2 + z ^ 2 - 4⁻¹ = 1 - 4⁻¹
⊢ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : (2 ^ 2)⁻¹ + x ^ 2 + y ^ 2 + z ^ 2 - 4⁻¹ = 1 - 4⁻¹
⊢ x * x + y * y + z * z = 3 / 4
Tactic:
ring_nf at hNormSqMr
Proof state after:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
⊢ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
⊢ x * x + y * y + z * z = 3 / 4
Tactic:
ring_nf
Proof state after:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.intro
r x y z : ℝ
hNorm : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr : r = 2⁻¹
hNormSqMr : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
rw [hNormSqMr]
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
⊢ Soqqtstqm1₁ = Soqqtstqm1₃
Tactic:
ext ⟨r, x, y, z⟩
Proof 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₃
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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₁]
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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]
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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₀
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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⟩
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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⟩
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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))
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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]
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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]
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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]
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof 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₂
Proof 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