internlm/Lean-Github huggingface dataset:
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ -1 / 2 * (rt3 / 2) + rt3 / 2 * (-1 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).im
Tactic:
ring_nf
Proof state after:
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).im
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).im
Tactic:
dsimp
Proof state after:
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑1 / 2) = -0 - rt3 * (↑1 / 2)
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ rt3 * ↑(negOfNat 1) * (↑1 / 2) = -0 - rt3 * (↑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 : ℤω
x✝ y✝ : ℤ
⊢ toℂ (mul { x := x✝, y := y✝ } b) = toℂ { x := x✝, y := y✝ } * toℂ b
Theorem: ℤω.my_map_mul
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ toℂ (mul { x := x✝, y := y✝ } b) = toℂ { x := x✝, y := y✝ } * toℂ b
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ toℂ (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) = toℂ { x := x✝¹, y := y✝¹ } * toℂ { x := x✝, y := y✝ }
Theorem: ℤω.my_map_mul
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ toℂ (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) = toℂ { x := x✝¹, y := y✝¹ } * toℂ { x := x✝, y := y✝ }
Tactic:
simp only [mul, toℂ]
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑(x✝¹ * x✝ - y✝¹ * y✝) + ↑(x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) * complexω =
    (↑x✝¹ + ↑y✝¹ * complexω) * (↑x✝ + ↑y✝ * complexω)
Theorem: ℤω.my_map_mul
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑(x✝¹ * x✝ - y✝¹ * y✝) + ↑(x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) * complexω =
    (↑x✝¹ + ↑y✝¹ * complexω) * (↑x✝ + ↑y✝ * complexω)
Tactic:
norm_num
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑x✝¹ * ↑x✝ - ↑y✝¹ * ↑y✝ + (↑x✝¹ * ↑y✝ + ↑y✝¹ * ↑x✝ - ↑y✝¹ * ↑y✝) * complexω =
    (↑x✝¹ + ↑y✝¹ * complexω) * (↑x✝ + ↑y✝ * complexω)
Theorem: ℤω.my_map_mul
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑x✝¹ * ↑x✝ - ↑y✝¹ * ↑y✝ + (↑x✝¹ * ↑y✝ + ↑y✝¹ * ↑x✝ - ↑y✝¹ * ↑y✝) * complexω =
    (↑x✝¹ + ↑y✝¹ * complexω) * (↑x✝ + ↑y✝ * complexω)
Tactic:
ring_nf
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑x✝¹ * ↑x✝ + ↑x✝¹ * ↑y✝ * complexω + ↑x✝ * ↑y✝¹ * complexω + (-(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω) =
    ↑x✝¹ * ↑x✝ + ↑x✝¹ * ↑y✝ * complexω + ↑x✝ * ↑y✝¹ * complexω + ↑y✝¹ * ↑y✝ * complexω ^ 2
Theorem: ℤω.my_map_mul
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑x✝¹ * ↑x✝ + ↑x✝¹ * ↑y✝ * complexω + ↑x✝ * ↑y✝¹ * complexω + (-(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω) =
    ↑x✝¹ * ↑x✝ + ↑x✝¹ * ↑y✝ * complexω + ↑x✝ * ↑y✝¹ * complexω + ↑y✝¹ * ↑y✝ * complexω ^ 2
Tactic:
congr
Proof state after:
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * complexω ^ 2
Theorem: ℤω.my_map_mul
Proof state before:
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * complexω ^ 2
Tactic:
rw [complexω_sq]
Proof state after:
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * (-complexω - 1)
Theorem: ℤω.my_map_mul
Proof state before:
case mk.mk.e_a
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ -(↑y✝¹ * ↑y✝) - ↑y✝¹ * ↑y✝ * complexω = ↑y✝¹ * ↑y✝ * (-complexω - 1)
Tactic:
sorry
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 : ℤω
x✝ y✝ : ℤ
⊢ toℂ (add { x := x✝, y := y✝ } b) = toℂ { x := x✝, y := y✝ } + toℂ b
Theorem: ℤω.my_map_add
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ toℂ (add { x := x✝, y := y✝ } b) = toℂ { x := x✝, y := y✝ } + toℂ b
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ toℂ (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) = toℂ { x := x✝¹, y := y✝¹ } + toℂ { x := x✝, y := y✝ }
Theorem: ℤω.my_map_add
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ toℂ (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) = toℂ { x := x✝¹, y := y✝¹ } + toℂ { x := x✝, y := y✝ }
Tactic:
simp only [add, toℂ, complexω]
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑(x✝¹ + x✝) + ↑(y✝¹ + y✝) * { re := -1 / 2, im := rt3 / 2 } =
    ↑x✝¹ + ↑y✝¹ * { re := -1 / 2, im := rt3 / 2 } + (↑x✝ + ↑y✝ * { re := -1 / 2, im := rt3 / 2 })
Theorem: ℤω.my_map_add
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑(x✝¹ + x✝) + ↑(y✝¹ + y✝) * { re := -1 / 2, im := rt3 / 2 } =
    ↑x✝¹ + ↑y✝¹ * { re := -1 / 2, im := rt3 / 2 } + (↑x✝ + ↑y✝ * { re := -1 / 2, im := rt3 / 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 { x := x, y := y } = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Tactic:
change toℂ ⟨x, y⟩ = ⟨x - y / 2, y * rt3 / 2⟩
Proof state after:
a b c : ℤω
x y : ℤ
⊢ toℂ { x := x, y := y } = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Theorem: ℤω.coe_of_mk
Proof state before:
a b c : ℤω
x y : ℤ
⊢ toℂ { x := x, y := y } = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Tactic:
unfold toℂ
Proof state after:
a b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x + ↑{ x := x, y := y }.y * complexω = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Theorem: ℤω.coe_of_mk
Proof state before:
a b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x + ↑{ x := x, y := y }.y * complexω = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Tactic:
dsimp
Proof state after:
a b c : ℤω
x y : ℤ
⊢ ↑x + ↑y * complexω = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Theorem: ℤω.coe_of_mk
Proof state before:
a b c : ℤω
x y : ℤ
⊢ ↑x + ↑y * complexω = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Tactic:
unfold complexω
Proof state after:
a b c : ℤω
x y : ℤ
⊢ ↑x + ↑y * { re := -1 / 2, im := rt3 / 2 } = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Theorem: ℤω.coe_of_mk
Proof state before:
a b c : ℤω
x y : ℤ
⊢ ↑x + ↑y * { re := -1 / 2, im := rt3 / 2 } = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
Tactic:
ext
Proof state after:
case a
a b c : ℤω
x y : ℤ
⊢ (↑x + ↑y * { re := -1 / 2, im := rt3 / 2 }).re = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }.re

case a
a b c : ℤω
x y : ℤ
⊢ (↑x + ↑y * { re := -1 / 2, im := rt3 / 2 }).im = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }.im
Theorem: ℤω.coe_of_mk
Proof state before:
case a
a b c : ℤω
x y : ℤ
⊢ (↑x + ↑y * { re := -1 / 2, im := rt3 / 2 }).re = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 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 := rt3 / 2 }).im = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 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 * (rt3 / 2) = ↑y * rt3 / 2
Theorem: ℤω.coe_of_mk
Proof state before:
case a
a b c : ℤω
x y : ℤ
⊢ ↑y * (rt3 / 2) = ↑y * rt3 / 2
Tactic:
ring
Proof state after:
no goals
Theorem: ℤω.re_of_coe
Proof state before:
a b c : ℤω
⊢ (OneHom.toFun (↑↑inclusion) a).re = ↑a.x - ↑a.y / 2
Tactic:
change (toℂ a).re = a.x - a.y / 2
Proof state after:
a b c : ℤω
⊢ (toℂ a).re = ↑a.x - ↑a.y / 2
Theorem: ℤω.re_of_coe
Proof state before:
a b c : ℤω
⊢ (toℂ a).re = ↑a.x - ↑a.y / 2
Tactic:
unfold toℂ
Proof state after:
a b c : ℤω
⊢ (↑a.x + ↑a.y * complexω).re = ↑a.x - ↑a.y / 2
Theorem: ℤω.re_of_coe
Proof state before:
a b c : ℤω
⊢ (↑a.x + ↑a.y * complexω).re = ↑a.x - ↑a.y / 2
Tactic:
unfold complexω
Proof state after:
a b c : ℤω
⊢ (↑a.x + ↑a.y * { re := -1 / 2, im := rt3 / 2 }).re = ↑a.x - ↑a.y / 2
Theorem: ℤω.re_of_coe
Proof state before:
a b c : ℤω
⊢ (↑a.x + ↑a.y * { re := -1 / 2, im := rt3 / 2 }).re = ↑a.x - ↑a.y / 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.x + ↑a.y * (-1 / 2) = ↑a.x - ↑a.y / 2
Theorem: ℤω.re_of_coe
Proof state before:
a b c : ℤω
⊢ ↑a.x + ↑a.y * (-1 / 2) = ↑a.x - ↑a.y / 2
Tactic:
ring
Proof state after:
no goals
Theorem: ℤω.im_of_coe
Proof state before:
a b c : ℤω
⊢ (OneHom.toFun (↑↑inclusion) a).im = ↑a.y * rt3 / 2
Tactic:
change (toℂ a).im = a.y * rt3 / 2
Proof state after:
a b c : ℤω
⊢ (toℂ a).im = ↑a.y * rt3 / 2
Theorem: ℤω.im_of_coe
Proof state before:
a b c : ℤω
⊢ (toℂ a).im = ↑a.y * rt3 / 2
Tactic:
unfold toℂ
Proof state after:
a b c : ℤω
⊢ (↑a.x + ↑a.y * complexω).im = ↑a.y * rt3 / 2
Theorem: ℤω.im_of_coe
Proof state before:
a b c : ℤω
⊢ (↑a.x + ↑a.y * complexω).im = ↑a.y * rt3 / 2
Tactic:
unfold complexω
Proof state after:
a b c : ℤω
⊢ (↑a.x + ↑a.y * { re := -1 / 2, im := rt3 / 2 }).im = ↑a.y * rt3 / 2
Theorem: ℤω.im_of_coe
Proof state before:
a b c : ℤω
⊢ (↑a.x + ↑a.y * { re := -1 / 2, im := rt3 / 2 }).im = ↑a.y * rt3 / 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.y * (rt3 / 2) = ↑a.y * rt3 / 2
Theorem: ℤω.im_of_coe
Proof state before:
a b c : ℤω
⊢ ↑a.y * (rt3 / 2) = ↑a.y * rt3 / 2
Tactic:
ring
Proof state after:
no goals
Theorem: ℤω.y_from_coe
Proof state before:
a b c : ℤω
⊢ ↑a.y = 2 * rt3⁻¹ * (OneHom.toFun (↑↑inclusion) a).im
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.y = 2 * rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im
Theorem: ℤω.y_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.y = 2 * rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im
Tactic:
simp only [coe_of_mk]
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = 2 * rt3⁻¹ * (↑y * rt3 / 2)
Theorem: ℤω.y_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = 2 * rt3⁻¹ * (↑y * rt3 / 2)
Tactic:
ring_nf
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = rt3 * rt3⁻¹ * ↑y
Theorem: ℤω.y_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = rt3 * rt3⁻¹ * ↑y
Tactic:
rw [mul_comm rt3]
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = rt3⁻¹ * rt3 * ↑y
Theorem: ℤω.y_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑y = rt3⁻¹ * rt3 * ↑y
Tactic:
simp only [sqrt3_inv_hMul_self, _root_.one_mul, Int.cast_inj, eq_self_iff_true]
Proof state after:
no goals
Theorem: ℤω.x_from_coe
Proof state before:
a b c : ℤω
⊢ ↑a.x = (OneHom.toFun (↑↑inclusion) a).re + rt3⁻¹ * (OneHom.toFun (↑↑inclusion) a).im
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x =
    (OneHom.toFun ↑↑inclusion { x := x, y := y }).re + rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im
Theorem: ℤω.x_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x =
    (OneHom.toFun ↑↑inclusion { x := x, y := y }).re + rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im
Tactic:
simp only [coe_of_mk]
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x - ↑y / 2 + rt3⁻¹ * (↑y * rt3 / 2)
Theorem: ℤω.x_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x - ↑y / 2 + rt3⁻¹ * (↑y * rt3 / 2)
Tactic:
ring_nf
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * rt3 * rt3⁻¹ * (↑(ofNat 1) / ↑2) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
Theorem: ℤω.x_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * rt3 * rt3⁻¹ * (↑(ofNat 1) / ↑2) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
Tactic:
rw [mul_assoc,mul_assoc,mul_comm rt3]
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * (↑(ofNat 1) / ↑2) * rt3) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
Theorem: ℤω.x_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * (↑(ofNat 1) / ↑2) * rt3) + ↑y * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)
Tactic:
simp only [ofNat_eq_coe, Nat.cast_one, cast_one, Nat.cast_ofNat, one_div, cast_negOfNat, mul_neg,
  mul_one, neg_mul]
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * 2⁻¹ * rt3) + -(↑y * 2⁻¹)
Theorem: ℤω.x_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (rt3⁻¹ * 2⁻¹ * rt3) + -(↑y * 2⁻¹)
Tactic:
rw [mul_comm ((rt3)⁻¹),mul_assoc]
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (2⁻¹ * (rt3⁻¹ * rt3)) + -(↑y * 2⁻¹)
Theorem: ℤω.x_from_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x + ↑y * (2⁻¹ * (rt3⁻¹ * rt3)) + -(↑y * 2⁻¹)
Tactic:
simp only [ne_eq, sqrt3_inv_hMul_self, mul_one, add_neg_cancel_right]
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.x
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ z.x = 0.x

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

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

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

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

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

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

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

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

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y
Tactic:
norm_num
Proof state after:
case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y
Theorem: ℤω.coe_eq_zero
Proof state before:
case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y
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.x) + ↑(-a.y) * complexω = -(↑a.x + ↑a.y * complexω)
Theorem: ℤω.coe_neg
Proof state before:
a b c : ℤω
⊢ ↑(-a.x) + ↑(-a.y) * complexω = -(↑a.x + ↑a.y * complexω)
Tactic:
norm_num
Proof state after:
a b c : ℤω
⊢ -↑a.x + -(↑a.y * complexω) = -(↑a.y * complexω) + -↑a.x
Theorem: ℤω.coe_neg
Proof state before:
a b c : ℤω
⊢ -↑a.x + -(↑a.y * complexω) = -(↑a.y * complexω) + -↑a.x
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 { x := x, y := y }) = ↑(norm { x := x, y := y })
Theorem: ℤω.normSq_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { x := x, y := y }) = ↑(norm { x := x, y := y })
Tactic:
simp [normSq, Norm]
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ (↑inclusion { x := x, y := y }).re * (↑inclusion { x := x, y := y }).re +
      (↑inclusion { x := x, y := y }).im * (↑inclusion { x := x, y := y }).im =
    ↑(norm { x := x, y := y })
Theorem: ℤω.normSq_coe
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ (↑inclusion { x := x, y := y }).re * (↑inclusion { x := x, y := y }).re +
      (↑inclusion { x := x, y := y }).im * (↑inclusion { x := x, y := y }).im =
    ↑(norm { x := x, y := y })
Tactic:
ring_nf
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ (↑inclusion { x := x, y := y }).re ^ 2 + (↑inclusion { x := x, y := y }).im ^ 2 = ↑(norm { x := x, y := y })
Theorem: ℤω.natNorm_coe
Proof state before:
a b c : ℤω
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natNorm a)
Tactic:
unfold natNorm
Proof state after:
a b c : ℤω
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natAbs (norm a))
Theorem: ℤω.natNorm_coe
Proof state before:
a b c : ℤω
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natAbs (norm a))
Tactic:
rw [normSq_coe]
Proof state after:
a b c : ℤω
⊢ ↑(norm a) = ↑(natAbs (norm a))
Theorem: ℤω.natNorm_coe
Proof state before:
a b c : ℤω
⊢ ↑(norm a) = ↑(natAbs (norm a))
Tactic:
suffices : a.norm = a.norm.natAbs
Proof state after:
a b c : ℤω
this : norm a = ↑(natAbs (norm a))
⊢ ↑(norm a) = ↑(natAbs (norm a))

case this
a b c : ℤω
⊢ norm a = ↑(natAbs (norm a))
Theorem: ℤω.natNorm_coe
Proof state before:
a b c : ℤω
this : norm a = ↑(natAbs (norm a))
⊢ ↑(norm a) = ↑(natAbs (norm a))

case this
a b c : ℤω
⊢ norm a = ↑(natAbs (norm a))
Tactic:
congr
Proof state after:
case this
a b c : ℤω
⊢ norm a = ↑(natAbs (norm a))
Theorem: ℤω.natNorm_coe
Proof state before:
case this
a b c : ℤω
⊢ norm a = ↑(natAbs (norm a))
Tactic:
exact this
Proof state after:
no goals
Theorem: ℤω.norm_hMul
Proof state before:
a b c : ℤω
⊢ norm (a * b) = norm a * norm b
Tactic:
have := normSq_mul a b
Proof state after:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ norm (a * b) = norm a * norm b
Theorem: ℤω.norm_hMul
Proof state before:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ norm (a * b) = norm a * norm b
Tactic:
rw [← coe_hMul] at this
Proof state after:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ norm (a * b) = norm a * norm b
Theorem: ℤω.norm_hMul
Proof state before:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ norm (a * b) = norm a * norm b
Tactic:
simp only [normSq_coe] at this
Proof state after:
a b c : ℤω
this : ↑(norm (a * b)) = ↑(norm a) * ↑(norm b)
⊢ norm (a * b) = norm a * norm b
Theorem: ℤω.norm_hMul
Proof state before:
a b c : ℤω
this : ↑(norm (a * b)) = ↑(norm a) * ↑(norm b)
⊢ norm (a * b) = norm a * norm b
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: ℤω.natNorm_hMul
Proof state before:
a b c : ℤω
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
have := normSq_mul a b
Proof state after:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Theorem: ℤω.natNorm_hMul
Proof state before:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
rw [← coe_hMul] at this
Proof state after:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Theorem: ℤω.natNorm_hMul
Proof state before:
a b c : ℤω
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
simp only [natNorm_coe] at this
Proof state after:
a b c : ℤω
this : ↑(natNorm (a * b)) = ↑(natNorm a) * ↑(natNorm b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Theorem: ℤω.natNorm_hMul
Proof state before:
a b c : ℤω
this : ↑(natNorm (a * b)) = ↑(natNorm a) * ↑(natNorm b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
a b c : ℤω
⊢ natNorm a = 0 ↔ a = 0
Tactic:
constructor
Proof state after:
case mp
a b c : ℤω
⊢ natNorm a = 0 → a = 0

case mpr
a b c : ℤω
⊢ a = 0 → natNorm a = 0
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
case mp
a b c : ℤω
⊢ natNorm a = 0 → a = 0
Tactic:
intro h
Proof state after:
case mp
a b c : ℤω
h : natNorm a = 0
⊢ a = 0
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
case mp
a b c : ℤω
h : natNorm a = 0
⊢ a = 0
Tactic:
have : (a.natNorm : ℝ) = 0 := by exact_mod_cast h
Proof state after:
case mp
a b c : ℤω
h : natNorm a = 0
this : ↑(natNorm a) = 0
⊢ a = 0