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 : ℝ
⊢ -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 := 0, imI := rx, imJ := ry, imK := rz } ∧
        rx * rx + ry * ry + rz * rz = 1

State before:
case h.mk
r x y 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 := 0, imI := rx, imJ := ry, imK := rz } ∧
        rx * rx + ry * ry + rz * rz = 1
Tactic:
simp only [ext_iff, neg_re, QuaternionAlgebra.one_re, mul_re, neg_imI, QuaternionAlgebra.one_imI,
  neg_zero, mul_imI, neg_imJ, QuaternionAlgebra.one_imJ, mul_imJ, neg_imK,
  QuaternionAlgebra.one_imK, mul_imK]
State after:
case h.mk
r x y z : ℝ
⊢ -1 = r * r - x * x - y * y - z * z ∧
      0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r ↔
    ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1

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

case h.mk.mpr
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1) →
    -1 = r * r - x * x - y * y - z * z ∧
      0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r

State before:
case h.mk.mp
r x y z : ℝ
⊢ -1 = r * r - x * x - y * y - z * z ∧
      0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r →
    ∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1
Tactic:
intros ha
State after:
case h.mk.mp
r x y z : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ ∃ 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 : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ ∃ 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 : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ ∃ 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 : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ ∃ 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 : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ ∃ rz, (r = 0 ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 1

State before:
case h
r x y z : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ ∃ 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 : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ (r = 0 ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 1

State before:
case h
r x y z : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ (r = 0 ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 1
Tactic:
simp only [and_self, and_true]
State after:
case h
r x y z : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h
r x y z : ℝ
ha :
  -1 = r * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
rcases ha with ⟨hSphere3, h0x, h0y, h0z⟩
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : 0 = r * x + x * r + y * z - z * y
h0y : 0 = r * y - x * z + y * r + z * x
h0z : 0 = r * z + x * y - y * x + z * r
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : 0 = r * x + x * r + y * z - z * y
h0y : 0 = r * y - x * z + y * r + z * x
h0z : 0 = r * z + x * y - y * x + z * r
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
ring_nf at h0x
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0y : 0 = r * y - x * z + y * r + z * x
h0z : 0 = r * z + x * y - y * x + z * r
h0x : 0 = r * x * 2
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0y : 0 = r * y - x * z + y * r + z * x
h0z : 0 = r * z + x * y - y * x + z * r
h0x : 0 = r * x * 2
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
ring_nf at h0y
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0z : 0 = r * z + x * y - y * x + z * r
h0x : 0 = r * x * 2
h0y : 0 = r * y * 2
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0z : 0 = r * z + x * y - y * x + z * r
h0x : 0 = r * x * 2
h0y : 0 = r * y * 2
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
ring_nf at h0z
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : 0 = r * x * 2
h0y : 0 = r * y * 2
h0z : 0 = r * z * 2
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : 0 = r * x * 2
h0y : 0 = r * y * 2
h0z : 0 = r * z * 2
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
simp only [zero_eq_mul, mul_eq_zero, OfNat.ofNat_ne_zero, or_false] at h0x
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0y : 0 = r * y * 2
h0z : 0 = r * z * 2
h0x : r = 0 ∨ x = 0
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0y : 0 = r * y * 2
h0z : 0 = r * z * 2
h0x : r = 0 ∨ x = 0
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
simp only [zero_eq_mul, mul_eq_zero, OfNat.ofNat_ne_zero, or_false] at h0y
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0z : 0 = r * z * 2
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0z : 0 = r * z * 2
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
simp only [zero_eq_mul, mul_eq_zero, OfNat.ofNat_ne_zero, or_false] at h0z
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
have hr₀ : (¬ r = 0) → False := by
  intros hrn0
  let hrn0₂ := Iff.mpr iff_false_iff hrn0
  simp only [hrn0₂, false_or] at h0x
  simp only [hrn0₂, false_or] at h0y
  simp only [hrn0₂, false_or] at h0z
  simp_rw [h0x, h0y, h0z] at hSphere3
  simp only [mul_zero, sub_zero] at hSphere3
  have hrnn := mul_self_nonneg r
  rw [←hSphere3] at hrnn
  linarith
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
have hr : r = 0 := by_contra hr₀
State after:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
⊢ r = 0 ∧ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
⊢ r = 0 ∧ x * x + y * y + z * z = 1
Tactic:
constructor
State after:
case h.intro.intro.intro.left
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
⊢ r = 0

case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
⊢ x * x + y * y + z * z = 1

State before:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
⊢ ¬r = 0 → False
Tactic:
intros hrn0
State after:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hrn0 : ¬r = 0
⊢ False

State before:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hrn0 : ¬r = 0
⊢ False
Tactic:
let hrn0₂ := Iff.mpr iff_false_iff hrn0
State after:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
⊢ False

State before:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
⊢ False
Tactic:
simp only [hrn0₂, false_or] at h0x
State after:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
⊢ False

State before:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
⊢ False
Tactic:
simp only [hrn0₂, false_or] at h0y
State after:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0z : r = 0 ∨ z = 0
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
⊢ False

State before:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0z : r = 0 ∨ z = 0
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
⊢ False
Tactic:
simp only [hrn0₂, false_or] at h0z
State after:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
⊢ False

State before:
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
⊢ False
Tactic:
simp_rw [h0x, h0y, h0z] at hSphere3
State after:
r x y z : ℝ
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
hSphere3 : -1 = r * r - 0 * 0 - 0 * 0 - 0 * 0
⊢ False

State before:
r x y z : ℝ
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
hSphere3 : -1 = r * r - 0 * 0 - 0 * 0 - 0 * 0
⊢ False
Tactic:
simp only [mul_zero, sub_zero] at hSphere3
State after:
r x y z : ℝ
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
hSphere3 : -1 = r * r
⊢ False

State before:
r x y z : ℝ
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
hSphere3 : -1 = r * r
⊢ False
Tactic:
have hrnn := mul_self_nonneg r
State after:
r x y z : ℝ
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
hSphere3 : -1 = r * r
hrnn : 0 ≤ r * r
⊢ False

State before:
r x y z : ℝ
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
hSphere3 : -1 = r * r
hrnn : 0 ≤ r * r
⊢ False
Tactic:
rw [←hSphere3] at hrnn
State after:
r x y z : ℝ
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
hSphere3 : -1 = r * r
hrnn : 0 ≤ -1
⊢ False

State before:
r x y z : ℝ
hrn0 : ¬r = 0
hrn0₂ : r = 0 ↔ False := iff_false_iff.mpr hrn0
h0x : x = 0
h0y : y = 0
h0z : z = 0
hSphere3 : -1 = r * r
hrnn : 0 ≤ -1
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case h.intro.intro.intro.left
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
⊢ r = 0
Tactic:
exact hr
State after:
no goals

State before:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = r * r - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
⊢ x * x + y * y + z * z = 1
Tactic:
rw [hr] at hSphere3
State after:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = 0 * 0 - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
⊢ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = 0 * 0 - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
⊢ x * x + y * y + z * z = 1
Tactic:
let hSphere4 := congrArg (λ (xk : ℝ) => -xk) hSphere3
State after:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = 0 * 0 - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
hSphere4 : (fun xk => -xk) (-1) = (fun xk => -xk) (0 * 0 - x * x - y * y - z * z) := congrArg (fun xk => -xk) hSphere3
⊢ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = 0 * 0 - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
hSphere4 : (fun xk => -xk) (-1) = (fun xk => -xk) (0 * 0 - x * x - y * y - z * z) := congrArg (fun xk => -xk) hSphere3
⊢ x * x + y * y + z * z = 1
Tactic:
simp only [neg_neg, mul_zero, zero_sub, neg_sub] at hSphere4
State after:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = 0 * 0 - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
hSphere4 : 1 = z * z - (-(x * x) - y * y)
⊢ x * x + y * y + z * z = 1

State before:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = 0 * 0 - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
hSphere4 : 1 = z * z - (-(x * x) - y * y)
⊢ x * x + y * y + z * z = 1
Tactic:
rw [hSphere4]
State after:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = 0 * 0 - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
hSphere4 : 1 = z * z - (-(x * x) - y * y)
⊢ x * x + y * y + z * z = z * z - (-(x * x) - y * y)

State before:
case h.intro.intro.intro.right
r x y z : ℝ
hSphere3 : -1 = 0 * 0 - x * x - y * y - z * z
h0x : r = 0 ∨ x = 0
h0y : r = 0 ∨ y = 0
h0z : r = 0 ∨ z = 0
hr₀ : ¬r = 0 → False
hr : r = 0
hSphere4 : 1 = z * z - (-(x * x) - y * y)
⊢ x * x + y * y + z * z = z * z - (-(x * x) - y * y)
Tactic:
ring_nf
State after:
no goals

State before:
case h.mk.mpr
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 0 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 1) →
    -1 = r * r - x * x - y * y - z * z ∧
      0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
Tactic:
intros h₀
State after:
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 * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r

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 * r - x * x - y * y - z * z ∧
    0 = r * x + x * r + y * z - z * y ∧ 0 = r * y - x * z + y * r + z * x ∧ 0 = r * z + x * y - y * x + z * r
Tactic:
ring_nf
State after:
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

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

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

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

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

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

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

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

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

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

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