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 : ℝ
⊢ { 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

State before:
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
Tactic:
simp only [ext_iff, sub_re, QuaternionAlgebra.one_re, mul_re, sub_imI, QuaternionAlgebra.one_imI,
  sub_zero, mul_imI, sub_imJ, QuaternionAlgebra.one_imJ, mul_imJ, sub_imK,
  QuaternionAlgebra.one_imK, mul_imK, one_div]
State after:
case h.mk
r x y z : ℝ
⊢ r - 1 = r * r - x * x - y * y - z * z ∧
      x = r * x + x * r + y * z - z * y ∧ y = r * y - x * z + y * r + z * x ∧ z = r * z + x * y - y * x + z * r ↔
    ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4

State before:
case h.mk
r x y z : ℝ
⊢ r - 1 = r * r - x * x - y * y - z * z ∧
      x = r * x + x * r + y * z - z * y ∧ y = r * y - x * z + y * r + z * x ∧ z = r * z + x * y - y * x + z * r ↔
    ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
ring_nf
State after:
case h.mk
r x y z : ℝ
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2 ↔
    ∃ rx ry rz, (r = 1 / 2 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4

State before:
case h.mk
r x y z : ℝ
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2 ↔
    ∃ rx ry rz, (r = 1 / 2 ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
Tactic:
simp only [one_div]
State after:
case h.mk
r x y z : ℝ
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2 ↔
    ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4

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

case h.mk.mpr
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4) →
    -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2

State before:
case h.mk.mp
r x y z : ℝ
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2 →
    ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
Tactic:
intros h₀
State after:
case h.mk.mp
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4

State before:
case h.mk.mp
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
Tactic:
use x
State after:
case h
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ ∃ ry rz, (r = 2⁻¹ ∧ x = x ∧ y = ry ∧ z = rz) ∧ x ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4

State before:
case h
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ ∃ ry rz, (r = 2⁻¹ ∧ x = x ∧ y = ry ∧ z = rz) ∧ x ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
Tactic:
use y
State after:
case h
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ ∃ rz, (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = rz) ∧ x ^ 2 + y ^ 2 + rz ^ 2 = 3 / 4

State before:
case h
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ ∃ rz, (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = rz) ∧ x ^ 2 + y ^ 2 + rz ^ 2 = 3 / 4
Tactic:
use z
State after:
case h
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
simp only [and_self, and_true]
State after:
case h
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h
r x y z : ℝ
h₀ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
rcases h₀ with ⟨h₁, hx, hy, hz⟩
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
have EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → (x₀ = 0 ∨ r = 1 / 2) := by
  intro x₀ h
  have hFactored : x₀ * (1 - r * 2) = 0 := by linarith
  simp at hFactored
  apply hFactored.imp_right
  intro h
  field_simp
  linarith
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
let hx₂ := EqSplit x hx
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
let hy₂ := EqSplit y hy
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
let hz₂ := EqSplit z hz
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
have hr₀ : (¬ r = 1/2) → False := by
  intros hrn0
  simp only [one_div] at hrn0
  simp only [one_div, hrn0, or_false] at hx₂
  simp only [one_div, hrn0, or_false] at hy₂
  simp only [one_div, hrn0, or_false] at hz₂
  simp [hx₂, hy₂, hz₂] at h₁
  let h₂ := congrArg (λ (x₀ : ℝ) => x₀ - r + 1) h₁
  simp only [add_sub_cancel, add_left_neg] at h₂
  have hSquareNn := mul_self_nonneg (r - 1 / 2)
  linarith
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
have hr₁ : r = 1/2 := by_contra hr₀
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
⊢ r = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
rw [hr₁]
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
⊢ 1 / 2 = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
⊢ 1 / 2 = 2⁻¹ ∧ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
simp only [one_div, true_and]
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
rw [hr₁] at h₁
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + 1 / 2 = (1 / 2) ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + 1 / 2 = (1 / 2) ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
let hSphere := congrArg (λ (x₀ : ℝ) => 1 / 4 - x₀) h₁
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + 1 / 2 = (1 / 2) ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
hSphere : (fun x₀ => 1 / 4 - x₀) (-1 + 1 / 2) = (fun x₀ => 1 / 4 - x₀) ((1 / 2) ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)) :=
  congrArg (fun x₀ => 1 / 4 - x₀) h₁
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + 1 / 2 = (1 / 2) ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
hSphere : (fun x₀ => 1 / 4 - x₀) (-1 + 1 / 2) = (fun x₀ => 1 / 4 - x₀) ((1 / 2) ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)) :=
  congrArg (fun x₀ => 1 / 4 - x₀) h₁
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
ring_nf at hSphere
State after:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + 1 / 2 = (1 / 2) ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
hSphere : 3 / 4 = x ^ 2 + y ^ 2 + z ^ 2
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4

State before:
case h.intro.intro.intro
r x y z : ℝ
h₁ : -1 + 1 / 2 = (1 / 2) ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hr₀ : ¬r = 1 / 2 → False
hr₁ : r = 1 / 2
hSphere : 3 / 4 = x ^ 2 + y ^ 2 + z ^ 2
⊢ x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
Tactic:
rw [←hSphere]
State after:
no goals

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
⊢ ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
Tactic:
intro x₀ h
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
⊢ x₀ = 0 ∨ r = 1 / 2

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
⊢ x₀ = 0 ∨ r = 1 / 2
Tactic:
have hFactored : x₀ * (1 - r * 2) = 0 := by linarith
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
hFactored : x₀ * (1 - r * 2) = 0
⊢ x₀ = 0 ∨ r = 1 / 2

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
hFactored : x₀ * (1 - r * 2) = 0
⊢ x₀ = 0 ∨ r = 1 / 2
Tactic:
simp at hFactored
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
hFactored : x₀ = 0 ∨ 1 - r * 2 = 0
⊢ x₀ = 0 ∨ r = 1 / 2

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
hFactored : x₀ = 0 ∨ 1 - r * 2 = 0
⊢ x₀ = 0 ∨ r = 1 / 2
Tactic:
apply hFactored.imp_right
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
hFactored : x₀ = 0 ∨ 1 - r * 2 = 0
⊢ 1 - r * 2 = 0 → r = 1 / 2

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
hFactored : x₀ = 0 ∨ 1 - r * 2 = 0
⊢ 1 - r * 2 = 0 → r = 1 / 2
Tactic:
intro h
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h✝ : x₀ = r * x₀ * 2
hFactored : x₀ = 0 ∨ 1 - r * 2 = 0
h : 1 - r * 2 = 0
⊢ r = 1 / 2

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h✝ : x₀ = r * x₀ * 2
hFactored : x₀ = 0 ∨ 1 - r * 2 = 0
h : 1 - r * 2 = 0
⊢ r = 1 / 2
Tactic:
field_simp
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h✝ : x₀ = r * x₀ * 2
hFactored : x₀ = 0 ∨ 1 - r * 2 = 0
h : 1 - r * 2 = 0
⊢ r * 2 = 1

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h✝ : x₀ = r * x₀ * 2
hFactored : x₀ = 0 ∨ 1 - r * 2 = 0
h : 1 - r * 2 = 0
⊢ r * 2 = 1
Tactic:
linarith
State after:
no goals

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
x₀ : ℝ
h : x₀ = r * x₀ * 2
⊢ x₀ * (1 - r * 2) = 0
Tactic:
linarith
State after:
no goals

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
⊢ ¬r = 1 / 2 → False
Tactic:
intros hrn0
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hrn0 : ¬r = 1 / 2
⊢ False

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hrn0 : ¬r = 1 / 2
⊢ False
Tactic:
simp only [one_div] at hrn0
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hrn0 : ¬r = 2⁻¹
⊢ False

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hx₂ : x = 0 ∨ r = 1 / 2 := EqSplit x hx
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hrn0 : ¬r = 2⁻¹
⊢ False
Tactic:
simp only [one_div, hrn0, or_false] at hx₂
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
⊢ False

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hy₂ : y = 0 ∨ r = 1 / 2 := EqSplit y hy
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
⊢ False
Tactic:
simp only [one_div, hrn0, or_false] at hy₂
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
⊢ False

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hz₂ : z = 0 ∨ r = 1 / 2 := EqSplit z hz
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
⊢ False
Tactic:
simp only [one_div, hrn0, or_false] at hz₂
State after:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
⊢ False

State before:
r x y z : ℝ
h₁ : -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2)
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
⊢ False
Tactic:
simp [hx₂, hy₂, hz₂] at h₁
State after:
r x y z : ℝ
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
h₁ : -1 + r = r ^ 2
⊢ False

State before:
r x y z : ℝ
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
h₁ : -1 + r = r ^ 2
⊢ False
Tactic:
let h₂ := congrArg (λ (x₀ : ℝ) => x₀ - r + 1) h₁
State after:
r x y z : ℝ
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
h₁ : -1 + r = r ^ 2
h₂ : (fun x₀ => x₀ - r + 1) (-1 + r) = (fun x₀ => x₀ - r + 1) (r ^ 2) := congrArg (fun x₀ => x₀ - r + 1) h₁
⊢ False

State before:
r x y z : ℝ
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
h₁ : -1 + r = r ^ 2
h₂ : (fun x₀ => x₀ - r + 1) (-1 + r) = (fun x₀ => x₀ - r + 1) (r ^ 2) := congrArg (fun x₀ => x₀ - r + 1) h₁
⊢ False
Tactic:
simp only [add_sub_cancel, add_left_neg] at h₂
State after:
r x y z : ℝ
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
h₁ : -1 + r = r ^ 2
h₂ : -1 + r - r + 1 = r ^ 2 - r + 1 := congrArg (fun x₀ => x₀ - r + 1) h₁
⊢ False

State before:
r x y z : ℝ
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
h₁ : -1 + r = r ^ 2
h₂ : -1 + r - r + 1 = r ^ 2 - r + 1 := congrArg (fun x₀ => x₀ - r + 1) h₁
⊢ False
Tactic:
have hSquareNn := mul_self_nonneg (r - 1 / 2)
State after:
r x y z : ℝ
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
h₁ : -1 + r = r ^ 2
h₂ : -1 + r - r + 1 = r ^ 2 - r + 1 := congrArg (fun x₀ => x₀ - r + 1) h₁
hSquareNn : 0 ≤ (r - 1 / 2) * (r - 1 / 2)
⊢ False

State before:
r x y z : ℝ
hx : x = r * x * 2
hy : y = r * y * 2
hz : z = r * z * 2
EqSplit : ∀ (x₀ : ℝ), x₀ = r * x₀ * 2 → x₀ = 0 ∨ r = 1 / 2
hrn0 : ¬r = 2⁻¹
hx₂ : x = 0
hy₂ : y = 0
hz₂ : z = 0
h₁ : -1 + r = r ^ 2
h₂ : -1 + r - r + 1 = r ^ 2 - r + 1 := congrArg (fun x₀ => x₀ - r + 1) h₁
hSquareNn : 0 ≤ (r - 1 / 2) * (r - 1 / 2)
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case h.mk.mpr
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4) →
    -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
Tactic:
intros h₀
State after:
case h.mk.mpr
r x y z : ℝ
h₀ : ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2

State before:
case h.mk.mpr
r x y z : ℝ
h₀ : ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
Tactic:
rcases h₀ with ⟨rx, ry, rz, hx, hSphere⟩
State after:
case h.mk.mpr.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hx : r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz
hSphere : rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2

State before:
case h.mk.mpr.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hx : r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz
hSphere : rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = r * z * 2
Tactic:
rcases hx with ⟨hr, hx, hy, hz⟩
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = 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 ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 + r = r ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = r * x * 2 ∧ y = r * y * 2 ∧ z = 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 ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 + 2⁻¹ = 2⁻¹ ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = 2⁻¹ * x * 2 ∧ y = 2⁻¹ * y * 2 ∧ z = 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 ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 + 2⁻¹ = 2⁻¹ ^ 2 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ x = 2⁻¹ * x * 2 ∧ y = 2⁻¹ * y * 2 ∧ z = 2⁻¹ * z * 2
Tactic:
ring_nf
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 / 2 = 1 / 4 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ True ∧ True ∧ True

State before:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : rx ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 / 2 = 1 / 4 - x ^ 2 + (-y ^ 2 - z ^ 2) ∧ True ∧ True ∧ True
Tactic:
simp only [Int.cast_negOfNat, Nat.cast_one, Int.ofNat_eq_coe, Int.cast_one, Nat.cast_ofNat,
  one_div, neg_mul, one_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 ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 / 2 = 4⁻¹ - 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 ^ 2 + ry ^ 2 + rz ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 / 2 = 4⁻¹ - x ^ 2 + (-y ^ 2 - z ^ 2)
Tactic:
rw [←hx, ←hy, ←hz] at hSphere
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 / 2 = 4⁻¹ - 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 : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ -1 / 2 = 4⁻¹ - x ^ 2 + (-y ^ 2 - z ^ 2)
Tactic:
let hXSquare := congrArg (λ (x₀ : ℝ) => x₀ - y ^ 2 - z ^ 2) hSphere
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hXSquare : (fun x₀ => x₀ - y ^ 2 - z ^ 2) (x ^ 2 + y ^ 2 + z ^ 2) = (fun x₀ => x₀ - y ^ 2 - z ^ 2) (3 / 4) :=
  congrArg (fun x₀ => x₀ - y ^ 2 - z ^ 2) hSphere
⊢ -1 / 2 = 4⁻¹ - 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 : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hXSquare : (fun x₀ => x₀ - y ^ 2 - z ^ 2) (x ^ 2 + y ^ 2 + z ^ 2) = (fun x₀ => x₀ - y ^ 2 - z ^ 2) (3 / 4) :=
  congrArg (fun x₀ => x₀ - y ^ 2 - z ^ 2) hSphere
⊢ -1 / 2 = 4⁻¹ - x ^ 2 + (-y ^ 2 - z ^ 2)
Tactic:
ring_nf at hXSquare
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hXSquare : x ^ 2 = 3 / 4 + (-y ^ 2 - z ^ 2)
⊢ -1 / 2 = 4⁻¹ - 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 : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hXSquare : x ^ 2 = 3 / 4 + (-y ^ 2 - z ^ 2)
⊢ -1 / 2 = 4⁻¹ - x ^ 2 + (-y ^ 2 - z ^ 2)
Tactic:
rw [hXSquare]
State after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hXSquare : x ^ 2 = 3 / 4 + (-y ^ 2 - z ^ 2)
⊢ -1 / 2 = 4⁻¹ - (3 / 4 + (-y ^ 2 - z ^ 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 : x ^ 2 + y ^ 2 + z ^ 2 = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hXSquare : x ^ 2 = 3 / 4 + (-y ^ 2 - z ^ 2)
⊢ -1 / 2 = 4⁻¹ - (3 / 4 + (-y ^ 2 - z ^ 2)) + (-y ^ 2 - z ^ 2)
Tactic:
ring
State after:
no goals