internlm/Lean-Github huggingface dataset:
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₁
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
h₂ : (fun x₀ => x₀ - r + 1) (-1 + r) = (fun x₀ => x₀ - r + 1) (r ^ 2) := congrArg (fun x₀ => x₀ - r + 1) h₁
⊢ False
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₂
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
h₂ : -1 + r - r + 1 = r ^ 2 - r + 1 := congrArg (fun x₀ => x₀ - r + 1) h₁
⊢ False
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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)
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
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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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₀
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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⟩
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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⟩
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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]
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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]
Proof 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)
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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)
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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)
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof 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)
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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]
Proof 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)
Theorem: EqualSetsSoqqtstqm1₀AndSoqqtstqm1₁
Proof 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
Proof state after:
no goals
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
⊢ Soqqtstqm1₁ = Soqqtstqm1₂
Tactic:
ext ⟨r, x, y, z⟩
Proof 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₂
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof 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₂]
Proof state after:
case h.mk
r x y 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) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 1 / 2
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk
r x y 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) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 1 / 2
Tactic:
simp only [one_div, ext_iff]
Proof state after:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4) ↔
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
constructor
Proof state after:
case h.mk.mp
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4) →
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹

case h.mk.mpr
r x y z : ℝ
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹ →
    ∃ 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.mp
r x y z : ℝ
⊢ (∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4) →
    ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
intros h₀
Proof state after:
case h.mk.mp
r x y z : ℝ
h₀ : ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp
r x y z : ℝ
h₀ : ∃ rx ry rz, (r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz) ∧ rx * rx + ry * ry + rz * rz = 3 / 4
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
rcases h₀ with ⟨rx, ry, rz, hx, hSphere⟩
Proof state after:
case h.mk.mp.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hx : r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hx : r = 2⁻¹ ∧ x = rx ∧ y = ry ∧ z = rz
hSphere : rx * rx + ry * ry + rz * rz = 3 / 4
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
rcases hx with ⟨hr, hx, hy, hz⟩
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
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
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
rw [←hx, ←hy, ←hz] at hSphere
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
have hrSquare := congrArg (λ (x₀ : ℝ) => x₀ ^ 2) hr
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : (fun x₀ => x₀ ^ 2) r = (fun x₀ => x₀ ^ 2) 2⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : (fun x₀ => x₀ ^ 2) r = (fun x₀ => x₀ ^ 2) 2⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
simp only [inv_pow] at hrSquare
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
have hNormSq := congrArg (λ (x₀ : ℝ) => x₀ + r ^ 2) hSphere
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : (fun x₀ => x₀ + r ^ 2) (x * x + y * y + z * z) = (fun x₀ => x₀ + r ^ 2) (3 / 4)
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : (fun x₀ => x₀ + r ^ 2) (x * x + y * y + z * z) = (fun x₀ => x₀ + r ^ 2) (3 / 4)
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
nth_rewrite 2 [hrSquare] at hNormSq
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : (fun x₀ => x₀ + r ^ 2) (x * x + y * y + z * z) = (fun x₀ => x₀ + (2 ^ 2)⁻¹) (3 / 4)
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : (fun x₀ => x₀ + r ^ 2) (x * x + y * y + z * z) = (fun x₀ => x₀ + (2 ^ 2)⁻¹) (3 / 4)
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
simp only at hNormSq
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x * x + y * y + z * z + r ^ 2 = 3 / 4 + (2 ^ 2)⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x * x + y * y + z * z + r ^ 2 = 3 / 4 + (2 ^ 2)⁻¹
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
ring_nf at hNormSq
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
let hSqrtNormSquare := congrArg Real.sqrt (Quaternion.normSq_eq_norm_mul_self (@QuaternionAlgebra.mk ℝ (-1) (-1) r x y z))
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) =
  √(‖{ re := r, imI := x, imJ := y, imK := z }‖ * ‖{ re := r, imI := x, imJ := y, imK := z }‖) :=
  congrArg Real.sqrt (normSq_eq_norm_mul_self { re := r, imI := x, imJ := y, imK := z })
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) =
  √(‖{ re := r, imI := x, imJ := y, imK := z }‖ * ‖{ re := r, imI := x, imJ := y, imK := z }‖) :=
  congrArg Real.sqrt (normSq_eq_norm_mul_self { re := r, imI := x, imJ := y, imK := z })
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
simp only [norm_nonneg, Real.sqrt_mul_self] at hSqrtNormSquare
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ ‖{ re := r, imI := x, imJ := y, imK := z }‖ = 1 ∧ r = 2⁻¹
Tactic:
rw [←hSqrtNormSquare, Quaternion.normSq_def']
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ √({ re := r, imI := x, imJ := y, imK := z }.re ^ 2 + { re := r, imI := x, imJ := y, imK := z }.imI ^ 2 +
            { re := r, imI := x, imJ := y, imK := z }.imJ ^ 2 +
          { re := r, imI := x, imJ := y, imK := z }.imK ^ 2) =
      1 ∧
    r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ √({ re := r, imI := x, imJ := y, imK := z }.re ^ 2 + { re := r, imI := x, imJ := y, imK := z }.imI ^ 2 +
            { re := r, imI := x, imJ := y, imK := z }.imJ ^ 2 +
          { re := r, imI := x, imJ := y, imK := z }.imK ^ 2) =
      1 ∧
    r = 2⁻¹
Tactic:
simp only [Real.sqrt_eq_one]
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ r ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1 ∧ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ r ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1 ∧ r = 2⁻¹
Tactic:
constructor
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro.left
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ r ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1

case h.mk.mp.intro.intro.intro.intro.intro.intro.intro.right
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ r = 2⁻¹
Theorem: EqualSetsSoqqtstqm1₁AndSoqqtstqm1₂
Proof state before:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro.left
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ r ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1
Tactic:
rw [←hNormSq]
Proof state after:
case h.mk.mp.intro.intro.intro.intro.intro.intro.intro.left
r x y z rx ry rz : ℝ
hSphere : x * x + y * y + z * z = 3 / 4
hr : r = 2⁻¹
hx : x = rx
hy : y = ry
hz : z = rz
hrSquare : r ^ 2 = (2 ^ 2)⁻¹
hNormSq : x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2 = 1
hSqrtNormSquare : √(normSq { re := r, imI := x, imJ := y, imK := z }) = ‖{ re := r, imI := x, imJ := y, imK := z }‖
⊢ r ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = x ^ 2 + y ^ 2 + z ^ 2 + r ^ 2