internlm/Lean-Github huggingface dataset:
Theorem: SetSpiroRelated2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : f₀ ∈ SetSpiro k m₀
⊢ (fun t => cexp (I * t * (↑m₁ - ↑m₀)) * f₀ t) ∈ SetSpiro k m₁
Tactic:
simp [SetSpiro] at *
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
⊢ ∀ (t : ℂ),
    cexp (I * (t + 2 * ↑π / ↑↑k) * (↑m₁ - ↑m₀)) * f₀ (t + 2 * ↑π / ↑↑k) =
      cexp (I * 2 * ↑m₁ * ↑π / ↑↑k) * (cexp (I * t * (↑m₁ - ↑m₀)) * f₀ t)
Theorem: SetSpiroRelated2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
⊢ ∀ (t : ℂ),
    cexp (I * (t + 2 * ↑π / ↑↑k) * (↑m₁ - ↑m₀)) * f₀ (t + 2 * ↑π / ↑↑k) =
      cexp (I * 2 * ↑m₁ * ↑π / ↑↑k) * (cexp (I * t * (↑m₁ - ↑m₀)) * f₀ t)
Tactic:
intros t
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * (↑m₁ - ↑m₀)) * f₀ (t + 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑π / ↑↑k) * (cexp (I * t * (↑m₁ - ↑m₀)) * f₀ t)
Theorem: SetSpiroRelated2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * (↑m₁ - ↑m₀)) * f₀ (t + 2 * ↑π / ↑↑k) =
    cexp (I * 2 * ↑m₁ * ↑π / ↑↑k) * (cexp (I * t * (↑m₁ - ↑m₀)) * f₀ t)
Tactic:
rw [h₀]
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * (↑m₁ - ↑m₀)) * (cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t) =
    cexp (I * 2 * ↑m₁ * ↑π / ↑↑k) * (cexp (I * t * (↑m₁ - ↑m₀)) * f₀ t)
Theorem: SetSpiroRelated2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * (t + 2 * ↑π / ↑↑k) * (↑m₁ - ↑m₀)) * (cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t) =
    cexp (I * 2 * ↑m₁ * ↑π / ↑↑k) * (cexp (I * t * (↑m₁ - ↑m₀)) * f₀ t)
Tactic:
ring_nf
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * t * ↑m₁ - I * t * ↑m₀ + (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 - I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2)) *
        cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) *
      f₀ t =
    f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2) * cexp (I * t * ↑m₁ - I * t * ↑m₀)
Theorem: SetSpiroRelated2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp (I * t * ↑m₁ - I * t * ↑m₀ + (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 - I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2)) *
        cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) *
      f₀ t =
    f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2) * cexp (I * t * ↑m₁ - I * t * ↑m₀)
Tactic:
rw [←Complex.exp_add, (show f₀ t * (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2).exp * (I * t * ↑m₁ - I * t * ↑m₀).exp =
  f₀ t * ((I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2).exp * (I * t * ↑m₁ - I * t * ↑m₀).exp) by ring), ←Complex.exp_add]
Proof state after:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp
        (I * t * ↑m₁ - I * t * ↑m₀ + (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 - I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) +
          I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) *
      f₀ t =
    f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 + (I * t * ↑m₁ - I * t * ↑m₀))
Theorem: SetSpiroRelated2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ cexp
        (I * t * ↑m₁ - I * t * ↑m₀ + (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 - I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) +
          I * ↑π * (↑↑k)⁻¹ * ↑m₀ * 2) *
      f₀ t =
    f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2 + (I * t * ↑m₁ - I * t * ↑m₀))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SetSpiroRelated2
Proof state before:
f₀ : ℂ → ℂ
k : ℕ+
m₀ m₁ : ℤ
h₀ : ∀ (t : ℂ), f₀ (t + 2 * ↑π / ↑↑k) = cexp (I * 2 * ↑m₀ * ↑π / ↑↑k) * f₀ t
t : ℂ
⊢ f₀ t * cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2) * cexp (I * t * ↑m₁ - I * t * ↑m₀) =
    f₀ t * (cexp (I * ↑π * (↑↑k)⁻¹ * ↑m₁ * 2) * cexp (I * t * ↑m₁ - I * t * ↑m₀))
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 : ℝ
⊢ -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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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]
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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]
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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⟩
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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₀
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof state after:
no goals
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof state after:
no goals
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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]
Proof 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)
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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
Proof state after:
no goals
Theorem: EqualSetsSoqtstn1₀AndSoqtstn1₁
Proof 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₀
Proof 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
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 * 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
Proof 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