Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂ (NazgandLean4/quaternionLemma.lean)

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

State before:
case h.mk
r x y z : ℝ
⊢ { re := r, imI := x, imJ := y, imK := z } ∈ Soqtstn1₁ ↔ { re := r, imI := x, imJ := y, imK := z } ∈ Soqtstn1₂
Tactic:
dsimp [Soqtstn1₁, Soqtstn1₂]
State after:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz,
      { re := r, imI := x, imJ := y, imK := z } = { re := 0, imI := rx, imJ := ry, imK := rz } ∧
        rx * rx + ry * ry + rz * rz = 1) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0

State before:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz,
      { re := r, imI := x, imJ := y, imK := z } = { re := 0, imI := rx, imJ := ry, imK := rz } ∧
        rx * rx + ry * ry + rz * rz = 1) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
Tactic:
simp only [ext_iff]
State after:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0

State before:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
Tactic:
constructor
State after:
case h.mk.mp
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1) →
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0

case h.mk.mpr
r x y z : ℝ
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0 →
    ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1

State before:
case h.mk.mp
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1) →
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
Tactic:
intros h
State after:
case h.mk.mp
r x y z : ℝ
h : ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0

State before:
case h.mk.mp
r x y z : ℝ
h : ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
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 = 0 ∧ x = rx ∧ y = ry ∧ z = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0

State before:
case h.mk.mp.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hx : r = 0 ∧ x = rx ∧ y = ry ∧ z = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
Tactic:
rcases hx with ⟨hr0, hxrx, hyry, hzrz⟩
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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0

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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
Tactic:
simp_rw [hr0]
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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1 ∧ True

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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1 ∧ True
Tactic:
simp only [and_true]
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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1

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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1
Tactic:
simp_rw [←hxrx, ←hyry, ←hzrz] at hSphere
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1
Tactic:
let hNorm1 := congrArg Real.sqrt hSphere
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = √1 := congrArg Real.sqrt hSphere
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = √1 := congrArg Real.sqrt hSphere
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1
Tactic:
simp only [Real.sqrt_one] at hNorm1
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1
Tactic:
simp_rw [←hNorm1]
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = √(x * x + y * y + z * z)

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = √(x * x + y * y + z * z)
Tactic:
let hSqrtNormSquare := congrArg Real.sqrt (Quaternion.normSq_eq_norm_mul_self (@QuaternionAlgebra.mk ℝ (-1) (-1) 0 x y z))
State after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
hSqrtNormSquare : √(normSq { re := 0, imI := x, imJ := y, imK := z }) =
  √(‖{ re := 0, imI := x, imJ := y, imK := z }‖ * ‖{ re := 0, imI := x, imJ := y, imK := z }‖) :=
  congrArg Real.sqrt (normSq_eq_norm_mul_self { re := 0, imI := x, imJ := y, imK := z })
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = √(x * x + y * y + z * z)

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
hSqrtNormSquare : √(normSq { re := 0, imI := x, imJ := y, imK := z }) =
  √(‖{ re := 0, imI := x, imJ := y, imK := z }‖ * ‖{ re := 0, imI := x, imJ := y, imK := z }‖) :=
  congrArg Real.sqrt (normSq_eq_norm_mul_self { re := 0, imI := x, imJ := y, imK := z })
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = √(x * x + y * y + z * z)
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 : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
hSqrtNormSquare : √(normSq { re := 0, imI := x, imJ := y, imK := z }) = ‖{ re := 0, imI := x, imJ := y, imK := z }‖
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = √(x * x + y * y + z * z)

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
hSqrtNormSquare : √(normSq { re := 0, imI := x, imJ := y, imK := z }) = ‖{ re := 0, imI := x, imJ := y, imK := z }‖
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = √(x * x + y * y + z * z)
Tactic:
simp_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 : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
hSqrtNormSquare : √(normSq { re := 0, imI := x, imJ := y, imK := z }) = ‖{ re := 0, imI := x, imJ := y, imK := z }‖
⊢ √(0 ^ 2 + x ^ 2 + y ^ 2 + z ^ 2) = √(x * x + y * y + z * z)

State before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
hSphere : x * x + y * y + z * z = 1
hNorm1 : √(x * x + y * y + z * z) = 1
hSqrtNormSquare : √(normSq { re := 0, imI := x, imJ := y, imK := z }) = ‖{ re := 0, imI := x, imJ := y, imK := z }‖
⊢ √(0 ^ 2 + x ^ 2 + y ^ 2 + z ^ 2) = √(x * x + y * y + z * z)
Tactic:
ring_nf
State after:
no goals

State before:
case h.mk.mpr
r x y z : ℝ
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0 →
    ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
Tactic:
intros h₀
State after:
case h.mk.mpr
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
⊢ ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1

State before:
case h.mk.mpr
r x y z : ℝ
h₀ : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
⊢ ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
Tactic:
rcases h₀ with ⟨hNorm1, hr0⟩
State after:
case h.mk.mpr.intro
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1

State before:
case h.mk.mpr.intro
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
Tactic:
use x
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ ∃ ry rz, (r = 0 ∧ x = x ∧ y = ry ∧ z = rz) ∧ x * x + ry * ry + rz * rz = 1

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ ∃ ry rz, (r = 0 ∧ x = x ∧ y = ry ∧ z = rz) ∧ x * x + ry * ry + rz * rz = 1
Tactic:
use y
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ ∃ rz, (r = 0 ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 1

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ ∃ rz, (r = 0 ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 1
Tactic:
use z
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ (r = 0 ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 1

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ (r = 0 ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 1
Tactic:
simp only [hr0, and_self, true_and]
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ x * x + y * y + z * z = 1

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
⊢ x * x + y * y + z * z = 1
Tactic:
let hNormSquare1 := congrArg (λ (r₀ : ℝ) => r₀ * r₀) hNorm1
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 : (fun r₀ => r₀ * r₀) ‖{ re := r, imI := x, imJ := y, imK := z }‖ = (fun r₀ => r₀ * r₀) 1 :=
  congrArg (fun r₀ => r₀ * r₀) hNorm1
⊢ x * x + y * y + z * z = 1

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 : (fun r₀ => r₀ * r₀) ‖{ re := r, imI := x, imJ := y, imK := z }‖ = (fun r₀ => r₀ * r₀) 1 :=
  congrArg (fun r₀ => r₀ * r₀) hNorm1
⊢ x * x + y * y + z * z = 1
Tactic:
simp only [mul_one] at hNormSquare1
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ * ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
⊢ x * x + y * y + z * z = 1

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ * ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
⊢ x * x + y * y + z * z = 1
Tactic:
rw [←Quaternion.normSq_eq_norm_mul_self, hr0, Quaternion.normSq_def'] at hNormSquare1
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 :
  { re := 0, imI := x, imJ := y, imK := z }.re ^ 2 + { re := 0, imI := x, imJ := y, imK := z }.imI ^ 2 +
        { re := 0, imI := x, imJ := y, imK := z }.imJ ^ 2 +
      { re := 0, imI := x, imJ := y, imK := z }.imK ^ 2 =
    1
⊢ x * x + y * y + z * z = 1

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 :
  { re := 0, imI := x, imJ := y, imK := z }.re ^ 2 + { re := 0, imI := x, imJ := y, imK := z }.imI ^ 2 +
        { re := 0, imI := x, imJ := y, imK := z }.imJ ^ 2 +
      { re := 0, imI := x, imJ := y, imK := z }.imK ^ 2 =
    1
⊢ x * x + y * y + z * z = 1
Tactic:
rw [←hNormSquare1]
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 :
  { re := 0, imI := x, imJ := y, imK := z }.re ^ 2 + { re := 0, imI := x, imJ := y, imK := z }.imI ^ 2 +
        { re := 0, imI := x, imJ := y, imK := z }.imJ ^ 2 +
      { re := 0, imI := x, imJ := y, imK := z }.imK ^ 2 =
    1
⊢ x * x + y * y + z * z =
    { re := 0, imI := x, imJ := y, imK := z }.re ^ 2 + { re := 0, imI := x, imJ := y, imK := z }.imI ^ 2 +
        { re := 0, imI := x, imJ := y, imK := z }.imJ ^ 2 +
      { re := 0, imI := x, imJ := y, imK := z }.imK ^ 2

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 :
  { re := 0, imI := x, imJ := y, imK := z }.re ^ 2 + { re := 0, imI := x, imJ := y, imK := z }.imI ^ 2 +
        { re := 0, imI := x, imJ := y, imK := z }.imJ ^ 2 +
      { re := 0, imI := x, imJ := y, imK := z }.imK ^ 2 =
    1
⊢ x * x + y * y + z * z =
    { re := 0, imI := x, imJ := y, imK := z }.re ^ 2 + { re := 0, imI := x, imJ := y, imK := z }.imI ^ 2 +
        { re := 0, imI := x, imJ := y, imK := z }.imJ ^ 2 +
      { re := 0, imI := x, imJ := y, imK := z }.imK ^ 2
Tactic:
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_add]
State after:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 :
  { re := 0, imI := x, imJ := y, imK := z }.re ^ 2 + { re := 0, imI := x, imJ := y, imK := z }.imI ^ 2 +
        { re := 0, imI := x, imJ := y, imK := z }.imJ ^ 2 +
      { re := 0, imI := x, imJ := y, imK := z }.imK ^ 2 =
    1
⊢ x * x + y * y + z * z = x ^ 2 + y ^ 2 + z ^ 2

State before:
case h
r x y z : ℝ
hNorm1 : ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1
hr0 : r = 0
hNormSquare1 :
  { re := 0, imI := x, imJ := y, imK := z }.re ^ 2 + { re := 0, imI := x, imJ := y, imK := z }.imI ^ 2 +
        { re := 0, imI := x, imJ := y, imK := z }.imJ ^ 2 +
      { re := 0, imI := x, imJ := y, imK := z }.imK ^ 2 =
    1
⊢ x * x + y * y + z * z = x ^ 2 + y ^ 2 + z ^ 2
Tactic:
ring_nf
State after:
no goals