internlm/Lean-Github huggingface dataset:
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (rx * rx + ry * ry + rz * rz) * 4 / 3 = 1
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = 1
Tactic:
rw [←hSphere₂]
Proof state after:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (rx * rx + ry * ry + rz * rz) * 4 / 3 = 1
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = (rx * rx + ry * ry + rz * rz) * 4 / 3
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
h3g0 : 0 ≤ 3
hSphere₂ : (rx * rx + ry * ry + rz * rz) * 4 / 3 = 1
⊢ rx ^ 2 * 3⁻¹ * 4 + 3⁻¹ * ry ^ 2 * 4 + 3⁻¹ * rz ^ 2 * 4 = (rx * rx + ry * ry + rz * rz) * 4 / 3
Tactic:
ring
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ 0 ≤ 3
Tactic:
linarith
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
      y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
        z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
constructor
Proof state after:
case h.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re

case h.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
    y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
      z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ r = 2⁻¹.re + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).re
Tactic:
sorry
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI ∧
    y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
      z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
constructor
Proof state after:
case h.right.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI

case h.right.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
    z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ x = 2⁻¹.imI + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imI
Tactic:
sorry
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ ∧
    z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
constructor
Proof state after:
case h.right.right.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ

case h.right.right.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right.right.right.left
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ y = 2⁻¹.imJ + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imJ
Tactic:
sorry
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right.right.right.right
r x y z rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ z = 2⁻¹.imK + ({ re := 0, imI := rx * 2 / √3, imJ := ry * 2 / √3, imK := rz * 2 / √3 } * ↑√3 / 2).imK
Tactic:
sorry
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.mk.mpr
r x y z : ℝ
⊢ (∃ qim,
      (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
        r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
          x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK) →
    ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
intros h₀
Proof state after:
case h.mk.mpr
r x y z : ℝ
h₀ :
  ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ 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.mpr
r x y z : ℝ
h₀ :
  ∃ qim,
    (∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1) ∧
      r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
        x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
rcases h₀ with ⟨qim, hx₁, hx₂⟩
Proof state after:
case h.mk.mpr.intro.intro
r x y z : ℝ
qim : ℍ
hx₁ : ∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1
hx₂ :
  r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ 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.mpr.intro.intro
r x y z : ℝ
qim : ℍ
hx₁ : ∃ rx ry rz, (qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz) ∧ rx * rx + ry * ry + rz * rz = 1
hx₂ :
  r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
rcases hx₁ with ⟨rx, ry, rz, hQim, hSphere⟩
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
hx₂ :
  r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
rx ry rz : ℝ
hQim : qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
⊢ ∃ 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.mpr.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
hx₂ :
  r = 2⁻¹.re + (qim * ↑√3 / 2).re ∧
    x = 2⁻¹.imI + (qim * ↑√3 / 2).imI ∧ y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ ∧ z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
rx ry rz : ℝ
hQim : qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
rcases hx₂ with ⟨hr, hx, hy, hz⟩
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hQim : qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ 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.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hQim : qim.re = 0 ∧ qim.imI = rx ∧ qim.imJ = ry ∧ qim.imK = rz
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
rcases hQim with ⟨hQimR, hQimI, hQimJ, hQimK⟩
Proof state after:
case h.mk.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ 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.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
Tactic:
use x
Proof state after:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ ry rz, (r = 2⁻¹ ∧ x = x ∧ y = ry ∧ z = rz) ∧ x * x + ry * ry + rz * rz = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ ry rz, (r = 2⁻¹ ∧ x = x ∧ y = ry ∧ z = rz) ∧ x * x + ry * ry + rz * rz = 3 / 4
Tactic:
use y
Proof state after:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ rz, (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ ∃ rz, (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = rz) ∧ x * x + y * y + rz * rz = 3 / 4
Tactic:
use z
Proof state after:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ (r = 2⁻¹ ∧ x = x ∧ y = y ∧ z = z) ∧ x * x + y * y + z * z = 3 / 4
Tactic:
simp only [and_self, and_true]
Proof state after:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ r = 2⁻¹ ∧ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ r = 2⁻¹ ∧ x * x + y * y + z * z = 3 / 4
Tactic:
constructor
Proof state after:
case h.left
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ r = 2⁻¹

case h.right
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ x * x + y * y + z * z = 3 / 4
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.left
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ r = 2⁻¹
Tactic:
sorry
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₃
Proof state before:
case h.right
r x y z : ℝ
qim : ℍ
rx ry rz : ℝ
hSphere : rx * rx + ry * ry + rz * rz = 1
hr : r = 2⁻¹.re + (qim * ↑√3 / 2).re
hx : x = 2⁻¹.imI + (qim * ↑√3 / 2).imI
hy : y = 2⁻¹.imJ + (qim * ↑√3 / 2).imJ
hz : z = 2⁻¹.imK + (qim * ↑√3 / 2).imK
hQimR : qim.re = 0
hQimI : qim.imI = rx
hQimJ : qim.imJ = ry
hQimK : qim.imK = rz
⊢ x * x + y * y + z * z = 3 / 4
Tactic:
sorry
Proof state after:
no goals
Theorem: impliesOr
Proof state before:
p q r : Prop
⊢ p → q ∨ r ↔ (p → q) ∨ (p → r)
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesAnd
Proof state before:
p q r : Prop
⊢ p → q ∧ r ↔ (p → q) ∧ (p → r)
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesImplies
Proof state before:
p q r : Prop
⊢ p → q → r ↔ (p → q) → p → r
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesIff
Proof state before:
p q r : Prop
⊢ p → (q ↔ r) ↔ (p → q ↔ p → r)
Tactic:
tauto
Proof state after:
no goals
Theorem: trueImpliesOnlyTrue
Proof state before:
p r : Prop
⊢ p → (p → r ↔ r)
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesReorder
Proof state before:
p q r : Prop
⊢ p → q → r ↔ q → p → r
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesAndImplies
Proof state before:
p q r : Prop
⊢ p → q → r ↔ q ∧ p → r
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesOrImplies
Proof state before:
p₀ p₁ r : Prop
⊢ (p₀ → r) ∧ (p₁ → r) ↔ p₀ ∨ p₁ → r
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesOrImplies3
Proof state before:
p₀ p₁ p₂ r : Prop
⊢ (p₀ → r) ∧ (p₁ → r) ∧ (p₂ → r) ↔ p₀ ∨ p₁ ∨ p₂ → r
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesOrImplies4
Proof state before:
p₀ p₁ p₂ p₃ r : Prop
⊢ (p₀ → r) ∧ (p₁ → r) ∧ (p₂ → r) ∧ (p₃ → r) ↔ p₀ ∨ p₁ ∨ p₂ ∨ p₃ → r
Tactic:
tauto
Proof state after:
no goals
Theorem: impliesOrImpliesGeneralized
Proof state before:
k : ℕ+
p : ℕ → Prop
r : Prop
⊢ (∀ k₀ ∈ range ↑k, p k₀ → r) ↔ (∃ k₀ ∈ range ↑k, p k₀) → r
Tactic:
aesop
Proof state after:
no goals
Theorem: combineCases
Proof state before:
q r : Prop
⊢ (q → r) ∧ (¬q → r) ↔ r
Tactic:
tauto
Proof state after:
no goals
Theorem: combineCasesGeneralized
Proof state before:
k : ℕ+
p : ℕ → Prop
r : Prop
⊢ (∃ k₀ ∈ range ↑k, p k₀) → (r ↔ ∀ k₀ ∈ range ↑k, p k₀ → r)
Tactic:
tauto
Proof state after:
no goals
Theorem: squashImplies
Proof state before:
q r : Prop
⊢ q → q → r ↔ q → r
Tactic:
tauto
Proof state after:
no goals
Theorem: insightFromGeneralization
Proof state before:
p₀ p₁ p₂ : Prop
⊢ (p₀ ↔ p₁ → p₂) → p₁ → (p₀ ↔ p₂)
Tactic:
tauto
Proof state after:
no goals
Theorem: ExpTsumForm
Proof state before:
z : ℂ
⊢ cexp z = ∑' (k : ℕ), z ^ k / ↑k.factorial
Tactic:
rw [exp_eq_exp_ℂ, exp_eq_tsum_div]
Proof state after:
no goals
Theorem: ExpTaylorSeriesSummable
Proof state before:
z : ℂ
⊢ Summable fun k => z ^ k / ↑k.factorial
Tactic:
exact expSeries_div_summable ℂ z
Proof state after:
no goals
Theorem: RuesRealToReal
Proof state before:
n : ℕ+
x : ℝ
⊢ (Rues n ↑x).im = 0
Tactic:
rw [Rues]
Proof state after:
n : ℕ+
x : ℝ
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Theorem: RuesRealToReal
Proof state before:
n : ℕ+
x : ℝ
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Tactic:
let h₀ := ContinuousLinearMap.map_tsum Complex.imCLM (RuesSummable n x)
Proof state after:
n : ℕ+
x : ℝ
h₀ : imCLM (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial) =
  ∑' (z : ℕ), imCLM (↑x ^ (↑n * z) / ↑(↑n * z).factorial) :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Theorem: RuesRealToReal
Proof state before:
n : ℕ+
x : ℝ
h₀ : imCLM (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial) =
  ∑' (z : ℕ), imCLM (↑x ^ (↑n * z) / ↑(↑n * z).factorial) :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Tactic:
simp only [imCLM_apply] at h₀
Proof state after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Theorem: RuesRealToReal
Proof state before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Tactic:
rw [h₀]
Proof state after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0
Theorem: RuesRealToReal
Proof state before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0
Tactic:
suffices h₁ : ∑' (z : ℕ), (x ^ (n * z) : ℂ).im / ↑(Nat.factorial (n * z)) = ∑' (z : ℕ), 0
Proof state after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = ∑' (z : ℕ), 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0

case h₁
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = ∑' (z : ℕ), 0
Theorem: RuesRealToReal
Proof state before:
case h₁
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = ∑' (z : ℕ), 0
Tactic:
congr
Proof state after:
case h₁.e_f
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (fun z => (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial) = fun z => 0
Theorem: RuesRealToReal
Proof state before:
case h₁.e_f
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (fun z => (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial) = fun z => 0
Tactic:
ext1 k
Proof state after:
case h₁.e_f.h
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
k : ℕ
⊢ (↑x ^ (↑n * k)).im / ↑(↑n * k).factorial = 0
Theorem: RuesRealToReal
Proof state before:
case h₁.e_f.h
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
k : ℕ
⊢ (↑x ^ (↑n * k)).im / ↑(↑n * k).factorial = 0
Tactic:
norm_cast at *
Proof state after:
case h₁.e_f.h
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
k : ℕ
⊢ 0 / ↑(↑n * k).factorial = 0
Theorem: RuesRealToReal
Proof state before:
case h₁.e_f.h
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
k : ℕ
⊢ 0 / ↑(↑n * k).factorial = 0
Tactic:
simp only [zero_div]
Proof state after:
no goals