internlm/Lean-Github huggingface dataset:
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr
r x y z : ℝ
h₀ : ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
⊢ -1 = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = r * x * 2 ∧ 0 = r * y * 2 ∧ 0 = r * z * 2
Tactic:
rcases h₀ with ⟨rx, ry, rz, hx⟩
Proof state after:
case h.mk.mpr.intro.intro.intro
r x y z rx ry rz : ℝ
hx : (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
⊢ -1 = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = r * x * 2 ∧ 0 = r * y * 2 ∧ 0 = r * z * 2
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.intro.intro.intro
r x y z rx ry rz : ℝ
hx : (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
⊢ -1 = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = r * x * 2 ∧ 0 = r * y * 2 ∧ 0 = r * z * 2
Tactic:
rcases hx with ⟨hx₀, hSphere⟩
Proof state after:
case h.mk.mpr.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
⊢ -1 = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = r * x * 2 ∧ 0 = r * y * 2 ∧ 0 = r * z * 2
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.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
⊢ -1 = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = r * x * 2 ∧ 0 = r * y * 2 ∧ 0 = r * z * 2
Tactic:
rcases hx₀ with ⟨hr, hrx, hry, hrz⟩
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
⊢ -1 = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = r * x * 2 ∧ 0 = r * y * 2 ∧ 0 = r * z * 2
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
⊢ -1 = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = r * x * 2 ∧ 0 = r * y * 2 ∧ 0 = r * z * 2
Tactic:
simp_rw [hr]
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
⊢ -1 = 0 ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = 0 * x * 2 ∧ 0 = 0 * y * 2 ∧ 0 = 0 * z * 2
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
⊢ -1 = 0 ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ 0 = 0 * x * 2 ∧ 0 = 0 * y * 2 ∧ 0 = 0 * z * 2
Tactic:
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_sub, zero_mul,
  and_self, and_true]
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
⊢ -1 = -x ^ 2 + (-y ^ 2 - z ^ 2)
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
⊢ -1 = -x ^ 2 + (-y ^ 2 - z ^ 2)
Tactic:
simp_rw [hrx,hry,hrz]
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
⊢ -1 = -rx ^ 2 + (-ry ^ 2 - rz ^ 2)
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
⊢ -1 = -rx ^ 2 + (-ry ^ 2 - rz ^ 2)
Tactic:
let hSphere2 := congrArg (λ (xk : ℝ) => -xk) hSphere
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
hSphere2 : (fun xk => -xk) (rx * rx + ry * ry + rz * rz) = (fun xk => -xk) 1 := congrArg (fun xk => -xk) hSphere
⊢ -1 = -rx ^ 2 + (-ry ^ 2 - rz ^ 2)
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
hSphere2 : (fun xk => -xk) (rx * rx + ry * ry + rz * rz) = (fun xk => -xk) 1 := congrArg (fun xk => -xk) hSphere
⊢ -1 = -rx ^ 2 + (-ry ^ 2 - rz ^ 2)
Tactic:
simp only [neg_add_rev] at hSphere2
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
hSphere2 : -(rz * rz) + (-(ry * ry) + -(rx * rx)) = -1
⊢ -1 = -rx ^ 2 + (-ry ^ 2 - rz ^ 2)
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
hSphere2 : -(rz * rz) + (-(ry * ry) + -(rx * rx)) = -1
⊢ -1 = -rx ^ 2 + (-ry ^ 2 - rz ^ 2)
Tactic:
rw [←hSphere2]
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
hSphere2 : -(rz * rz) + (-(ry * ry) + -(rx * rx)) = -1
⊢ -(rz * rz) + (-(ry * ry) + -(rx * rx)) = -rx ^ 2 + (-ry ^ 2 - rz ^ 2)
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof state before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 0
hrx : x = rx
hry : y = ry
hrz : z = rz
hSphere2 : -(rz * rz) + (-(ry * ry) + -(rx * rx)) = -1
⊢ -(rz * rz) + (-(ry * ry) + -(rx * rx)) = -rx ^ 2 + (-ry ^ 2 - rz ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof state before:
⊢ Soqtstn1₁ = Soqtstn1₂
Tactic:
ext ⟨r, x, y, z⟩
Proof 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₂
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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₂]
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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]
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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⟩
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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⟩
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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 0
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
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 = 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]
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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1 ∧ True
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
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 = 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]
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 = 1
hr0 : r = 0
hxrx : x = rx
hyry : y = ry
hzrz : z = rz
⊢ ‖{ re := 0, imI := x, imJ := y, imK := z }‖ = 1
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
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 = 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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]
Proof 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)
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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))
Proof 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)
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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)
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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']
Proof 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)
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof state after:
no goals
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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₀
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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⟩
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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]
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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]
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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]
Proof 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
Theorem: EqualSetsSoqtstn1₁AndSoqtstn1₂
Proof 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
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₁]
Proof state after:
case h.mk
r x y z : ℝ
⊢ { re := r, imI := x, imJ := y, imK := z } - 1 =
      { re := r, imI := x, imJ := y, imK := z } * { re := r, imI := x, imJ := y, imK := 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