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₂]
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) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 1 / 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) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 1 / 2
Tactic:
simp only [one_div, ext_iff]
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) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

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) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
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) →
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

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

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) →
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
rw [←hx, ←hy, ←hz] at hSphere
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
have hrSquare := congrArg (λ (x₀ : ℝ) => x₀ ^ 2) hr
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 : (fun x₀ => x₀ ^ 2) r = (fun x₀ => x₀ ^ 2) 2⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 : (fun x₀ => x₀ ^ 2) r = (fun x₀ => x₀ ^ 2) 2⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
simp only [inv_pow] at hrSquare
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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)⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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)⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
have hNormSq := congrArg (λ (x₀ : ℝ) => x₀ + r ^ 2) hSphere
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 : (fun x₀ => x₀ + r ^ 2) (x * x + y * y + z * z) = (fun x₀ => x₀ + r ^ 2) (3 / 4)
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 : (fun x₀ => x₀ + r ^ 2) (x * x + y * y + z * z) = (fun x₀ => x₀ + r ^ 2) (3 / 4)
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
nth_rewrite 2 [hrSquare] at hNormSq
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 : (fun x₀ => x₀ + r ^ 2) (x * x + y * y + z * z) = (fun x₀ => x₀ + (2 ^ 2)⁻¹) (3 / 4)
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 : (fun x₀ => x₀ + r ^ 2) (x * x + y * y + z * z) = (fun x₀ => x₀ + (2 ^ 2)⁻¹) (3 / 4)
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
simp only at hNormSq
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 * x + y * y + z * z + r ^ 2 = 3 / 4 + (2 ^ 2)⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 * x + y * y + z * z + r ^ 2 = 3 / 4 + (2 ^ 2)⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
ring_nf at hNormSq
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
let hSqrtNormSquare := congrArg Real.sqrt (Quaternion.normSq_eq_norm_mul_self (@QuaternionAlgebra.mk ℝ (-1) (-1) r x y z))
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 }‖ * ‖{ re := r, imI := x, imJ := y, imK := z }‖) :=
  congrArg Real.sqrt (normSq_eq_norm_mul_self { re := r, imI := x, imJ := y, imK := z })
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 }‖ * ‖{ re := r, imI := x, imJ := y, imK := z }‖) :=
  congrArg Real.sqrt (normSq_eq_norm_mul_self { re := r, imI := x, imJ := y, imK := z })
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
simp only [norm_nonneg, Real.sqrt_mul_self] at hSqrtNormSquare
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 }‖
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 }‖
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
rw [←hSqrtNormSquare, Quaternion.normSq_def']
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 }‖
⊢ √({ re := r, imI := x, imJ := y, imK := z }.re ^ 2 + { re := r, imI := x, imJ := y, imK := z }.imI ^ 2 +
            { re := r, imI := x, imJ := y, imK := z }.imJ ^ 2 +
          { re := r, imI := x, imJ := y, imK := z }.imK ^ 2) =
      1 ∧
    r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 }‖
⊢ √({ re := r, imI := x, imJ := y, imK := z }.re ^ 2 + { re := r, imI := x, imJ := y, imK := z }.imI ^ 2 +
            { re := r, imI := x, imJ := y, imK := z }.imJ ^ 2 +
          { re := r, imI := x, imJ := y, imK := z }.imK ^ 2) =
      1 ∧
    r = 2⁻¹
Tactic:
simp only [Real.sqrt_eq_one]
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 = 1 ∧ r = 2⁻¹

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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 = 1 ∧ r = 2⁻¹
Tactic:
constructor
State after:
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 = 1

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⁻¹

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 = 1
Tactic:
rw [←hNormSq]
State after:
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

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
State after:
no goals

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
State after:
no goals

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₀
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

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
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

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
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

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
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

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⟩
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

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]
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

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
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

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
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

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
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

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
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

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
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

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]
State after:
no goals