internlm/Lean-Github huggingface dataset:
Theorem: ℤα.rt7_sq
Proof state before:
a b c : ℤα
⊢ rt7 ^ 2 = 7
Tactic:
have : (0 : ℝ) ≤ 7 := by norm_num
Proof state after:
a b c : ℤα
this : 0 ≤ 7
⊢ rt7 ^ 2 = 7
Theorem: ℤα.rt7_sq
Proof state before:
a b c : ℤα
this : 0 ≤ 7
⊢ rt7 ^ 2 = 7
Tactic:
rw [pow_two]
Proof state after:
a b c : ℤα
this : 0 ≤ 7
⊢ rt7 * rt7 = 7
Theorem: ℤα.rt7_sq
Proof state before:
a b c : ℤα
this : 0 ≤ 7
⊢ rt7 * rt7 = 7
Tactic:
rw [← Real.sqrt_mul this 7]
Proof state after:
a b c : ℤα
this : 0 ≤ 7
⊢ Real.sqrt (7 * 7) = 7
Theorem: ℤα.rt7_sq
Proof state before:
a b c : ℤα
this : 0 ≤ 7
⊢ Real.sqrt (7 * 7) = 7
Tactic:
rw [Real.sqrt_mul_self this]
Proof state after:
no goals
Theorem: ℤα.rt7_sq
Proof state before:
a b c : ℤα
⊢ 0 ≤ 7
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤα.sqrt7_inv_hMul_self
Proof state before:
a b c : ℤα
⊢ rt7⁻¹ * rt7 = 1
Tactic:
apply inv_mul_cancel
Proof state after:
case h
a b c : ℤα
⊢ rt7 ≠ 0
Theorem: ℤα.sqrt7_inv_hMul_self
Proof state before:
case h
a b c : ℤα
⊢ rt7 ≠ 0
Tactic:
intro h
Proof state after:
case h
a b c : ℤα
h : rt7 = 0
⊢ False
Theorem: ℤα.sqrt7_inv_hMul_self
Proof state before:
case h
a b c : ℤα
h : rt7 = 0
⊢ False
Tactic:
norm_num at h
Proof state after:
no goals
Theorem: ℤα.complexα_sq
Proof state before:
a b c : ℤα
⊢ complexα ^ 2 = complexα - 2
Tactic:
rw [pow_two]
Proof state after:
a b c : ℤα
⊢ complexα * complexα = complexα - 2
Theorem: ℤα.complexα_sq
Proof state before:
a b c : ℤα
⊢ complexα * complexα = complexα - 2
Tactic:
ext
Proof state after:
case a
a b c : ℤα
⊢ (complexα * complexα).re = (complexα - 2).re

case a
a b c : ℤα
⊢ (complexα * complexα).im = (complexα - 2).im
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ (complexα * complexα).re = (complexα - 2).re
Tactic:
simp only [Complex.mul_re]
Proof state after:
case a
a b c : ℤα
⊢ complexα.re * complexα.re - complexα.im * complexα.im = (complexα - 2).re
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ complexα.re * complexα.re - complexα.im * complexα.im = (complexα - 2).re
Tactic:
simp only [complexα]
Proof state after:
case a
a b c : ℤα
⊢ 1 / 2 * (1 / 2) - rt7 / 2 * (rt7 / 2) = ({ re := 1 / 2, im := rt7 / 2 } - 2).re
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ 1 / 2 * (1 / 2) - rt7 / 2 * (rt7 / 2) = ({ re := 1 / 2, im := rt7 / 2 } - 2).re
Tactic:
ring_nf
Proof state after:
case a
a b c : ℤα
⊢ ↑(ofNat 1) / ↑4 + rt7 ^ 2 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-2 + { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).re
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ ↑(ofNat 1) / ↑4 + rt7 ^ 2 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-2 + { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).re
Tactic:
rw [rt7_sq]
Proof state after:
case a
a b c : ℤα
⊢ ↑(ofNat 1) / ↑4 + 7 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-2 + { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).re
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ ↑(ofNat 1) / ↑4 + 7 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-2 + { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).re
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ (complexα * complexα).im = (complexα - 2).im
Tactic:
rw [Complex.mul_im]
Proof state after:
case a
a b c : ℤα
⊢ complexα.re * complexα.im + complexα.im * complexα.re = (complexα - 2).im
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ complexα.re * complexα.im + complexα.im * complexα.re = (complexα - 2).im
Tactic:
simp only [complexα]
Proof state after:
case a
a b c : ℤα
⊢ 1 / 2 * (rt7 / 2) + rt7 / 2 * (1 / 2) = ({ re := 1 / 2, im := rt7 / 2 } - 2).im
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ 1 / 2 * (rt7 / 2) + rt7 / 2 * (1 / 2) = ({ re := 1 / 2, im := rt7 / 2 } - 2).im
Tactic:
ring_nf
Proof state after:
case a
a b c : ℤα
⊢ rt7 * (↑(ofNat 1) / ↑2) = (-2 + { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).im
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ rt7 * (↑(ofNat 1) / ↑2) = (-2 + { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).im
Tactic:
dsimp
Proof state after:
case a
a b c : ℤα
⊢ rt7 * (↑1 / 2) = -0 + rt7 * (↑1 / 2)
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ rt7 * (↑1 / 2) = -0 + rt7 * (↑1 / 2)
Tactic:
norm_cast
Proof state after:
case a
a b c : ℤα
⊢ rt7 * ↑(Rat.divInt 1 2) = ↑(-0) + rt7 * ↑(Rat.divInt 1 2)
Theorem: ℤα.complexα_sq
Proof state before:
case a
a b c : ℤα
⊢ rt7 * ↑(Rat.divInt 1 2) = ↑(-0) + rt7 * ↑(Rat.divInt 1 2)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ℤα.my_map_one
Proof state before:
a b c : ℤα
⊢ toℂ one = 1
Tactic:
simp only [toℂ, one]
Proof state after:
a b c : ℤα
⊢ ↑1 + ↑0 * complexα = 1
Theorem: ℤα.my_map_one
Proof state before:
a b c : ℤα
⊢ ↑1 + ↑0 * complexα = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤα.my_map_mul
Proof state before:
a b c : ℤα
⊢ toℂ (mul a b) = toℂ a * toℂ b
Tactic:
cases a
Proof state after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ toℂ (mul { z := z✝, w := w✝ } b) = toℂ { z := z✝, w := w✝ } * toℂ b
Theorem: ℤα.my_map_mul
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ toℂ (mul { z := z✝, w := w✝ } b) = toℂ { z := z✝, w := w✝ } * toℂ b
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ toℂ (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) = toℂ { z := z✝¹, w := w✝¹ } * toℂ { z := z✝, w := w✝ }
Theorem: ℤα.my_map_mul
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ toℂ (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) = toℂ { z := z✝¹, w := w✝¹ } * toℂ { z := z✝, w := w✝ }
Tactic:
simp only [mul, toℂ]
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑(z✝¹ * z✝ - 2 * w✝¹ * w✝) + ↑(z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)
Theorem: ℤα.my_map_mul
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑(z✝¹ * z✝ - 2 * w✝¹ * w✝) + ↑(z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)
Tactic:
norm_num
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ - 2 * ↑w✝¹ * ↑w✝ + (↑z✝¹ * ↑w✝ + ↑w✝¹ * ↑z✝ + ↑w✝¹ * ↑w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)
Theorem: ℤα.my_map_mul
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ - 2 * ↑w✝¹ * ↑w✝ + (↑z✝¹ * ↑w✝ + ↑w✝¹ * ↑z✝ + ↑w✝¹ * ↑w✝) * complexα =
    (↑z✝¹ + ↑w✝¹ * complexα) * (↑z✝ + ↑w✝ * complexα)
Tactic:
ring_nf
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + (↑z✝ * ↑w✝¹ * complexα - ↑w✝¹ * ↑w✝ * 2) + ↑w✝¹ * ↑w✝ * complexα =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * ↑w✝¹ * complexα + ↑w✝¹ * ↑w✝ * complexα ^ 2
Theorem: ℤα.my_map_mul
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + (↑z✝ * ↑w✝¹ * complexα - ↑w✝¹ * ↑w✝ * 2) + ↑w✝¹ * ↑w✝ * complexα =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * ↑w✝¹ * complexα + ↑w✝¹ * ↑w✝ * complexα ^ 2
Tactic:
ring
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + (↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2) =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + ↑w✝ * complexα ^ 2 * ↑w✝¹
Theorem: ℤα.my_map_mul
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + (↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2) =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + ↑w✝ * complexα ^ 2 * ↑w✝¹
Tactic:
rw [complexα_sq]
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + (↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2) =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + ↑w✝ * (complexα - 2) * ↑w✝¹
Theorem: ℤα.my_map_mul
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + (↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2) =
    ↑z✝¹ * ↑z✝ + ↑z✝¹ * ↑w✝ * complexα + ↑z✝ * complexα * ↑w✝¹ + ↑w✝ * (complexα - 2) * ↑w✝¹
Tactic:
congr
Proof state after:
case mk.mk.e_a
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2 = ↑w✝ * (complexα - 2) * ↑w✝¹
Theorem: ℤα.my_map_mul
Proof state before:
case mk.mk.e_a
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑w✝ * complexα * ↑w✝¹ - ↑w✝ * ↑w✝¹ * 2 = ↑w✝ * (complexα - 2) * ↑w✝¹
Tactic:
ring
Proof state after:
no goals
Theorem: ℤα.my_map_zero
Proof state before:
a b c : ℤα
⊢ toℂ zero = 0
Tactic:
simp [toℂ, zero]
Proof state after:
no goals
Theorem: ℤα.my_map_add
Proof state before:
a b c : ℤα
⊢ toℂ (add a b) = toℂ a + toℂ b
Tactic:
cases a
Proof state after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ toℂ (add { z := z✝, w := w✝ } b) = toℂ { z := z✝, w := w✝ } + toℂ b
Theorem: ℤα.my_map_add
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ toℂ (add { z := z✝, w := w✝ } b) = toℂ { z := z✝, w := w✝ } + toℂ b
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ toℂ (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) = toℂ { z := z✝¹, w := w✝¹ } + toℂ { z := z✝, w := w✝ }
Theorem: ℤα.my_map_add
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ toℂ (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) = toℂ { z := z✝¹, w := w✝¹ } + toℂ { z := z✝, w := w✝ }
Tactic:
simp only [add, toℂ, complexα]
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑(z✝¹ + z✝) + ↑(w✝¹ + w✝) * { re := 1 / 2, im := rt7 / 2 } =
    ↑z✝¹ + ↑w✝¹ * { re := 1 / 2, im := rt7 / 2 } + (↑z✝ + ↑w✝ * { re := 1 / 2, im := rt7 / 2 })
Theorem: ℤα.my_map_add
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ ↑(z✝¹ + z✝) + ↑(w✝¹ + w✝) * { re := 1 / 2, im := rt7 / 2 } =
    ↑z✝¹ + ↑w✝¹ * { re := 1 / 2, im := rt7 / 2 } + (↑z✝ + ↑w✝ * { re := 1 / 2, im := rt7 / 2 })
Tactic:
ext <;> dsimp <;> norm_num <;> ring
Proof state after:
no goals
Theorem: ℤα.coe_of_mk
Proof state before:
a b c : ℤα
x y : ℤ
⊢ OneHom.toFun ↑↑inclusion { z := x, w := y } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
change toℂ ⟨x, y⟩ = ⟨x + y / 2, y * rt7 / 2⟩
Proof state after:
a b c : ℤα
x y : ℤ
⊢ toℂ { z := x, w := y } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Theorem: ℤα.coe_of_mk
Proof state before:
a b c : ℤα
x y : ℤ
⊢ toℂ { z := x, w := y } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
unfold toℂ
Proof state after:
a b c : ℤα
x y : ℤ
⊢ ↑{ z := x, w := y }.z + ↑{ z := x, w := y }.w * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Theorem: ℤα.coe_of_mk
Proof state before:
a b c : ℤα
x y : ℤ
⊢ ↑{ z := x, w := y }.z + ↑{ z := x, w := y }.w * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
dsimp
Proof state after:
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Theorem: ℤα.coe_of_mk
Proof state before:
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
unfold complexα
Proof state after:
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * { re := 1 / 2, im := rt7 / 2 } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Theorem: ℤα.coe_of_mk
Proof state before:
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * { re := 1 / 2, im := rt7 / 2 } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
Tactic:
ext
Proof state after:
case a
a b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).re = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }.re

case a
a b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).im = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }.im
Theorem: ℤα.coe_of_mk
Proof state before:
case a
a b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).re = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }.re
Tactic:
simp only [add_re, int_cast_re, mul_re, int_cast_im, MulZeroClass.zero_mul, tsub_zero]
Proof state after:
case a
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * (1 / 2) = ↑x + ↑y / 2
Theorem: ℤα.coe_of_mk
Proof state before:
case a
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * (1 / 2) = ↑x + ↑y / 2
Tactic:
ring
Proof state after:
no goals
Theorem: ℤα.coe_of_mk
Proof state before:
case a
a b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).im = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }.im
Tactic:
simp only [add_im, int_cast_im, mul_im, int_cast_re, MulZeroClass.zero_mul, add_zero, zero_add,
  mul_eq_mul_left_iff, cast_eq_zero]
Proof state after:
case a
a b c : ℤα
x y : ℤ
⊢ ↑y * (rt7 / 2) = ↑y * rt7 / 2
Theorem: ℤα.coe_of_mk
Proof state before:
case a
a b c : ℤα
x y : ℤ
⊢ ↑y * (rt7 / 2) = ↑y * rt7 / 2
Tactic:
ring
Proof state after:
no goals
Theorem: ℤα.re_of_coe
Proof state before:
a b c : ℤα
⊢ (OneHom.toFun (↑↑inclusion) a).re = ↑a.z + ↑a.w / 2
Tactic:
change (toℂ a).re = a.z + a.w / 2
Proof state after:
a b c : ℤα
⊢ (toℂ a).re = ↑a.z + ↑a.w / 2
Theorem: ℤα.re_of_coe
Proof state before:
a b c : ℤα
⊢ (toℂ a).re = ↑a.z + ↑a.w / 2
Tactic:
unfold toℂ
Proof state after:
a b c : ℤα
⊢ (↑a.z + ↑a.w * complexα).re = ↑a.z + ↑a.w / 2
Theorem: ℤα.re_of_coe
Proof state before:
a b c : ℤα
⊢ (↑a.z + ↑a.w * complexα).re = ↑a.z + ↑a.w / 2
Tactic:
unfold complexα
Proof state after:
a b c : ℤα
⊢ (↑a.z + ↑a.w * { re := 1 / 2, im := rt7 / 2 }).re = ↑a.z + ↑a.w / 2
Theorem: ℤα.re_of_coe
Proof state before:
a b c : ℤα
⊢ (↑a.z + ↑a.w * { re := 1 / 2, im := rt7 / 2 }).re = ↑a.z + ↑a.w / 2
Tactic:
simp only [add_re, int_cast_re, mul_re, int_cast_im, MulZeroClass.zero_mul, tsub_zero]
Proof state after:
a b c : ℤα
⊢ ↑a.z + ↑a.w * (1 / 2) = ↑a.z + ↑a.w / 2
Theorem: ℤα.re_of_coe
Proof state before:
a b c : ℤα
⊢ ↑a.z + ↑a.w * (1 / 2) = ↑a.z + ↑a.w / 2
Tactic:
ring
Proof state after:
no goals
Theorem: ℤα.im_of_coe
Proof state before:
a b c : ℤα
⊢ (OneHom.toFun (↑↑inclusion) a).im = ↑a.w * rt7 / 2
Tactic:
change (toℂ a).im = a.w * rt7 / 2
Proof state after:
a b c : ℤα
⊢ (toℂ a).im = ↑a.w * rt7 / 2
Theorem: ℤα.im_of_coe
Proof state before:
a b c : ℤα
⊢ (toℂ a).im = ↑a.w * rt7 / 2
Tactic:
unfold toℂ
Proof state after:
a b c : ℤα
⊢ (↑a.z + ↑a.w * complexα).im = ↑a.w * rt7 / 2
Theorem: ℤα.im_of_coe
Proof state before:
a b c : ℤα
⊢ (↑a.z + ↑a.w * complexα).im = ↑a.w * rt7 / 2
Tactic:
unfold complexα
Proof state after:
a b c : ℤα
⊢ (↑a.z + ↑a.w * { re := 1 / 2, im := rt7 / 2 }).im = ↑a.w * rt7 / 2
Theorem: ℤα.im_of_coe
Proof state before:
a b c : ℤα
⊢ (↑a.z + ↑a.w * { re := 1 / 2, im := rt7 / 2 }).im = ↑a.w * rt7 / 2
Tactic:
simp only [add_im, int_cast_im, mul_im, int_cast_re, MulZeroClass.zero_mul, add_zero, zero_add]
Proof state after:
a b c : ℤα
⊢ ↑a.w * (rt7 / 2) = ↑a.w * rt7 / 2
Theorem: ℤα.im_of_coe
Proof state before:
a b c : ℤα
⊢ ↑a.w * (rt7 / 2) = ↑a.w * rt7 / 2
Tactic:
ring
Proof state after:
no goals
Theorem: ℤα.y_from_coe
Proof state before:
a b c : ℤα
⊢ ↑a.w = 2 * rt7⁻¹ * (OneHom.toFun (↑↑inclusion) a).im
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑{ z := x, w := y }.w = 2 * rt7⁻¹ * (OneHom.toFun ↑↑inclusion { z := x, w := y }).im
Theorem: ℤα.y_from_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑{ z := x, w := y }.w = 2 * rt7⁻¹ * (OneHom.toFun ↑↑inclusion { z := x, w := y }).im
Tactic:
simp only [coe_of_mk]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = 2 * rt7⁻¹ * (↑y * rt7 / 2)
Theorem: ℤα.y_from_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = 2 * rt7⁻¹ * (↑y * rt7 / 2)
Tactic:
ring_nf
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = rt7 * rt7⁻¹ * ↑y
Theorem: ℤα.y_from_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = rt7 * rt7⁻¹ * ↑y
Tactic:
rw [mul_comm]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = ↑y * (rt7 * rt7⁻¹)
Theorem: ℤα.y_from_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑y = ↑y * (rt7 * rt7⁻¹)
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤα.x_from_coe
Proof state before:
a b c : ℤα
⊢ ↑a.z = (OneHom.toFun (↑↑inclusion) a).re - rt7⁻¹ * (OneHom.toFun (↑↑inclusion) a).im
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑{ z := x, w := y }.z =
    (OneHom.toFun ↑↑inclusion { z := x, w := y }).re - rt7⁻¹ * (OneHom.toFun ↑↑inclusion { z := x, w := y }).im
Theorem: ℤα.x_from_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑{ z := x, w := y }.z =
    (OneHom.toFun ↑↑inclusion { z := x, w := y }).re - rt7⁻¹ * (OneHom.toFun ↑↑inclusion { z := x, w := y }).im
Tactic:
simp only [coe_of_mk]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x = ↑x + ↑y / 2 - rt7⁻¹ * (↑y * rt7 / 2)
Theorem: ℤα.x_from_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x = ↑x + ↑y / 2 - rt7⁻¹ * (↑y * rt7 / 2)
Tactic:
ring_nf
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x = ↑x + ↑y * (↑(ofNat 1) / ↑2) + ↑y * rt7 * rt7⁻¹ * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
Theorem: ℤα.x_from_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x = ↑x + ↑y * (↑(ofNat 1) / ↑2) + ↑y * rt7 * rt7⁻¹ * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤα.coe_eq_zero
Proof state before:
a b c z : ℤα
⊢ OneHom.toFun (↑↑inclusion) z = 0 ↔ z = 0
Tactic:
constructor
Proof state after:
case mp
a b c z : ℤα
⊢ OneHom.toFun (↑↑inclusion) z = 0 → z = 0

case mpr
a b c z : ℤα
⊢ z = 0 → OneHom.toFun (↑↑inclusion) z = 0
Theorem: ℤα.coe_eq_zero
Proof state before:
case mp
a b c z : ℤα
⊢ OneHom.toFun (↑↑inclusion) z = 0 → z = 0
Tactic:
intro h
Proof state after:
case mp
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z = 0
Theorem: ℤα.coe_eq_zero
Proof state before:
case mp
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z = 0
Tactic:
ext
Proof state after:
case mp.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.z = 0.z

case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.w = 0.w
Theorem: ℤα.coe_eq_zero
Proof state before:
case mp.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.z = 0.z
Tactic:
have : (z.z : ℝ) = 0
Proof state after:
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.z = 0

case mp.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.z = 0
⊢ z.z = 0.z
Theorem: ℤα.coe_eq_zero
Proof state before:
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.z = 0

case mp.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.z = 0
⊢ z.z = 0.z
Tactic:
rw [x_from_coe, h]
Proof state after:
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 0.re - rt7⁻¹ * 0.im = 0

case mp.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.z = 0
⊢ z.z = 0.z
Theorem: ℤα.coe_eq_zero
Proof state before:
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 0.re - rt7⁻¹ * 0.im = 0

case mp.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.z = 0
⊢ z.z = 0.z
Tactic:
norm_num
Proof state after:
case mp.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.z = 0
⊢ z.z = 0.z
Theorem: ℤα.coe_eq_zero
Proof state before:
case mp.z
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.z = 0
⊢ z.z = 0.z
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: ℤα.coe_eq_zero
Proof state before:
case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.w = 0.w
Tactic:
have : (z.w : ℝ) = 0
Proof state after:
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.w = 0

case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.w = 0
⊢ z.w = 0.w
Theorem: ℤα.coe_eq_zero
Proof state before:
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.w = 0

case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.w = 0
⊢ z.w = 0.w
Tactic:
rw [y_from_coe, h]
Proof state after:
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 2 * rt7⁻¹ * 0.im = 0

case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.w = 0
⊢ z.w = 0.w
Theorem: ℤα.coe_eq_zero
Proof state before:
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 2 * rt7⁻¹ * 0.im = 0

case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.w = 0
⊢ z.w = 0.w
Tactic:
norm_num
Proof state after:
case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.w = 0
⊢ z.w = 0.w
Theorem: ℤα.coe_eq_zero
Proof state before:
case mp.w
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.w = 0
⊢ z.w = 0.w
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: ℤα.coe_eq_zero
Proof state before:
case mpr
a b c z : ℤα
⊢ z = 0 → OneHom.toFun (↑↑inclusion) z = 0
Tactic:
intro h
Proof state after:
case mpr
a b c z : ℤα
h : z = 0
⊢ OneHom.toFun (↑↑inclusion) z = 0
Theorem: ℤα.coe_eq_zero
Proof state before:
case mpr
a b c z : ℤα
h : z = 0
⊢ OneHom.toFun (↑↑inclusion) z = 0
Tactic:
rw [h]
Proof state after:
case mpr
a b c z : ℤα
h : z = 0
⊢ OneHom.toFun (↑↑inclusion) 0 = 0
Theorem: ℤα.coe_eq_zero
Proof state before:
case mpr
a b c z : ℤα
h : z = 0
⊢ OneHom.toFun (↑↑inclusion) 0 = 0
Tactic:
exact my_map_zero
Proof state after:
no goals
Theorem: ℤα.coe_neg
Proof state before:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (-a) = -OneHom.toFun (↑↑inclusion) a
Tactic:
change toℂ (neg a) = -toℂ a
Proof state after:
a b c : ℤα
⊢ toℂ (neg a) = -toℂ a
Theorem: ℤα.coe_neg
Proof state before:
a b c : ℤα
⊢ toℂ (neg a) = -toℂ a
Tactic:
simp only [neg, toℂ]
Proof state after:
a b c : ℤα
⊢ ↑(-a.z) + ↑(-a.w) * complexα = -(↑a.z + ↑a.w * complexα)
Theorem: ℤα.coe_neg
Proof state before:
a b c : ℤα
⊢ ↑(-a.z) + ↑(-a.w) * complexα = -(↑a.z + ↑a.w * complexα)
Tactic:
norm_num
Proof state after:
a b c : ℤα
⊢ -↑a.z + -(↑a.w * complexα) = -(↑a.w * complexα) + -↑a.z
Theorem: ℤα.coe_neg
Proof state before:
a b c : ℤα
⊢ -↑a.z + -(↑a.w * complexα) = -(↑a.w * complexα) + -↑a.z
Tactic:
ring
Proof state after:
no goals
Theorem: ℤα.coe_sub
Proof state before:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a - b) = OneHom.toFun (↑↑inclusion) a - OneHom.toFun (↑↑inclusion) b
Tactic:
change ((a + -b : ℤα) : ℂ) = a + -(b : ℂ)
Proof state after:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + -OneHom.toFun (↑↑inclusion) b
Theorem: ℤα.coe_sub
Proof state before:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + -OneHom.toFun (↑↑inclusion) b
Tactic:
rw [← coe_neg]
Proof state after:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + OneHom.toFun (↑↑inclusion) (-b)
Theorem: ℤα.coe_sub
Proof state before:
a b c : ℤα
⊢ OneHom.toFun (↑↑inclusion) (a + -b) = OneHom.toFun (↑↑inclusion) a + OneHom.toFun (↑↑inclusion) (-b)
Tactic:
exact my_map_add a (-b)
Proof state after:
no goals
Theorem: ℤα.normSq_coe
Proof state before:
a b c : ℤα
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(norm a)
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { z := x, w := y }) = ↑(norm { z := x, w := y })
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { z := x, w := y }) = ↑(norm { z := x, w := y })
Tactic:
simp [normSq, norm]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re * (↑inclusion { z := x, w := y }).re +
      (↑inclusion { z := x, w := y }).im * (↑inclusion { z := x, w := y }).im =
    ↑x ^ 2 + ↑x * ↑y + 2 * ↑y ^ 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re * (↑inclusion { z := x, w := y }).re +
      (↑inclusion { z := x, w := y }).im * (↑inclusion { z := x, w := y }).im =
    ↑x ^ 2 + ↑x * ↑y + 2 * ↑y ^ 2
Tactic:
ring_nf
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re ^ 2 + (↑inclusion { z := x, w := y }).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re ^ 2 + (↑inclusion { z := x, w := y }).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
norm_cast
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re ^ 2 + (↑inclusion { z := x, w := y }).im ^ 2 = ↑(x * y + x ^ 2 + y ^ 2 * 2)
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re ^ 2 + (↑inclusion { z := x, w := y }).im ^ 2 = ↑(x * y + x ^ 2 + y ^ 2 * 2)
Tactic:
rw [inclusion]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := x, w := y }).re ^
        2 +
      (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := x, w := y }).im ^
        2 =
    ↑(x * y + x ^ 2 + y ^ 2 * 2)