internlm/Lean-Github huggingface dataset:
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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]
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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]
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₀
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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]
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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⟩
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₀
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₁]
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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]
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₁
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₁
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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]
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₂
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₂
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₂
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₁
Proof 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