internlm/Lean-Github huggingface dataset:
Theorem: ℤα.normSq_mod_lt
Proof state before:
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true
Tactic:
congr
Proof state after:
case e_a.e_a
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ (OneHom.toFun (↑↑inclusion) b)⁻¹ = sorryAx ℂ true

case e_a
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) b *
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
      sorryAx ℂ true
Theorem: ℤα.normSq_mod_lt
Proof state before:
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
Tactic:
apply mul_inv_cancel
Proof state after:
case h
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b ≠ 0
Theorem: ℤα.normSq_mod_lt
Proof state before:
case h
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b ≠ 0
Tactic:
norm_cast
Proof state after:
case h
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ ¬OneHom.toFun (↑↑inclusion) b = 0
Theorem: ℤα.normSq_mod_lt
Proof state before:
case h
a b c : ℤα
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ ¬OneHom.toFun (↑↑inclusion) b = 0
Tactic:
simpa [coe_eq_zero] using h
Proof state after:
no goals
Theorem: ℤα.my_quotient_zero
Proof state before:
a b c : ℤα
⊢ div a 0 = 0
Tactic:
unfold div
Proof state after:
a b c : ℤα
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Theorem: ℤα.my_quotient_zero
Proof state before:
a b c : ℤα
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Tactic:
have : ((0 : ℤα) : ℂ) = 0 := my_map_zero
Proof state after:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Theorem: ℤα.my_quotient_zero
Proof state before:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) 0) = 0
Tactic:
rw [this]
Proof state after:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / 0) = 0
Theorem: ℤα.my_quotient_zero
Proof state before:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα (OneHom.toFun (↑↑inclusion) a / 0) = 0
Tactic:
rw [div_zero]
Proof state after:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα 0 = 0
Theorem: ℤα.my_quotient_zero
Proof state before:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ nearestℤα 0 = 0
Tactic:
unfold nearestℤα
Proof state after:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ (let y := round (2 * rt7⁻¹ * 0.im);
    { z := round (0.re - 2⁻¹ * ↑y), w := y }) =
    0
Theorem: ℤα.my_quotient_zero
Proof state before:
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ (let y := round (2 * rt7⁻¹ * 0.im);
    { z := round (0.re - 2⁻¹ * ↑y), w := y }) =
    0
Tactic:
ext <;> dsimp <;> simp only [MulZeroClass.mul_zero, round_zero, algebraMap.coe_zero, sub_zero] <;>
norm_num
Proof state after:
no goals
Theorem: ℤα.my_hMul_left_not_lt
Proof state before:
a b c : ℤα
hb : b ≠ 0
⊢ ¬natNorm (a * b) < natNorm a
Tactic:
rw [natNorm_hMul]
Proof state after:
a b c : ℤα
hb : b ≠ 0
⊢ ¬natNorm a * natNorm b < natNorm a
Theorem: ℤα.my_hMul_left_not_lt
Proof state before:
a b c : ℤα
hb : b ≠ 0
⊢ ¬natNorm a * natNorm b < natNorm a
Tactic:
intro h
Proof state after:
a b c : ℤα
hb : b ≠ 0
h : natNorm a * natNorm b < natNorm a
⊢ False
Theorem: ℤα.my_hMul_left_not_lt
Proof state before:
a b c : ℤα
hb : b ≠ 0
h : natNorm a * natNorm b < natNorm a
⊢ False
Tactic:
apply hb
Proof state after:
a b c : ℤα
hb : b ≠ 0
h : natNorm a * natNorm b < natNorm a
⊢ b = 0
Theorem: ℤα.my_hMul_left_not_lt
Proof state before:
a b c : ℤα
hb : b ≠ 0
h : natNorm a * natNorm b < natNorm a
⊢ b = 0
Tactic:
clear hb
Proof state after:
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ b = 0
Theorem: ℤα.my_hMul_left_not_lt
Proof state before:
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ b = 0
Tactic:
rw [← natNorm_eq_zero_iff]
Proof state after:
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ natNorm b = 0
Theorem: ℤα.my_hMul_left_not_lt
Proof state before:
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ natNorm b = 0
Tactic:
cases b.natNorm
Proof state after:
case zero
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ Nat.zero = 0

case succ
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
n✝ : ℕ
⊢ Nat.succ n✝ = 0
Theorem: ℤα.my_hMul_left_not_lt
Proof state before:
case zero
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
⊢ Nat.zero = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤα.my_hMul_left_not_lt
Proof state before:
case succ
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
n✝ : ℕ
⊢ Nat.succ n✝ = 0
Tactic:
exfalso
Proof state after:
case succ.h
a b c : ℤα
h : natNorm a * natNorm b < natNorm a
n✝ : ℕ
⊢ False
Theorem: ℤω.my_add_assoc
Proof state before:
a b c : ℤω
⊢ add (add a b) c = add a (add b c)
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ add (add { x := x✝, y := y✝ } b) c = add { x := x✝, y := y✝ } (add b c)
Theorem: ℤω.my_add_assoc
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ add (add { x := x✝, y := y✝ } b) c = add { x := x✝, y := y✝ } (add b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ add (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) c = add { x := x✝¹, y := y✝¹ } (add { x := x✝, y := y✝ } c)
Theorem: ℤω.my_add_assoc
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ add (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) c = add { x := x✝¹, y := y✝¹ } (add { x := x✝, y := y✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ add (add { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    add { x := x✝², y := y✝² } (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ })
Theorem: ℤω.my_add_assoc
Proof state before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ add (add { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    add { x := x✝², y := y✝² } (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ })
Tactic:
simp only [add, add_assoc]
Proof state after:
no goals
Theorem: ℤω.my_zero_add
Proof state before:
a b c : ℤω
⊢ add zero a = a
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ add zero { x := x, y := y } = { x := x, y := y }
Theorem: ℤω.my_zero_add
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ add zero { x := x, y := y } = { x := x, y := y }
Tactic:
simp only [add, zero, zero_add]
Proof state after:
no goals
Theorem: ℤω.my_add_zero
Proof state before:
a b c : ℤω
⊢ add a zero = a
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤω
x y : ℤ
⊢ add { x := x, y := y } zero = { x := x, y := y }
Theorem: ℤω.my_add_zero
Proof state before:
case mk
b c : ℤω
x y : ℤ
⊢ add { x := x, y := y } zero = { x := x, y := y }
Tactic:
simp only [add, zero, add_zero]
Proof state after:
no goals
Theorem: ℤω.my_add_left_neg
Proof state before:
a b c : ℤω
⊢ add (neg a) a = zero
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ add (neg { x := x✝, y := y✝ }) { x := x✝, y := y✝ } = zero
Theorem: ℤω.my_add_left_neg
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ add (neg { x := x✝, y := y✝ }) { x := x✝, y := y✝ } = zero
Tactic:
simp only [neg, add]
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ { x := -x✝ + x✝, y := -y✝ + y✝ } = zero
Theorem: ℤω.my_add_left_neg
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ { x := -x✝ + x✝, y := -y✝ + y✝ } = zero
Tactic:
simp only [add_left_neg]
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ { x := 0, y := 0 } = zero
Theorem: ℤω.my_add_left_neg
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ { x := 0, y := 0 } = zero
Tactic:
tauto
Proof state after:
no goals
Theorem: ℤω.my_add_comm
Proof state before:
a b c : ℤω
⊢ add a b = add b a
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ add { x := x✝, y := y✝ } b = add b { x := x✝, y := y✝ }
Theorem: ℤω.my_add_comm
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ add { x := x✝, y := y✝ } b = add b { x := x✝, y := y✝ }
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ } = add { x := x✝, y := y✝ } { x := x✝¹, y := y✝¹ }
Theorem: ℤω.my_add_comm
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ } = add { x := x✝, y := y✝ } { x := x✝¹, y := y✝¹ }
Tactic:
simp only [add, add_comm]
Proof state after:
no goals
Theorem: ℤω.my_mul_assoc
Proof state before:
a b c : ℤω
⊢ mul (mul a b) c = mul a (mul b c)
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul (mul { x := x✝, y := y✝ } b) c = mul { x := x✝, y := y✝ } (mul b c)
Theorem: ℤω.my_mul_assoc
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul (mul { x := x✝, y := y✝ } b) c = mul { x := x✝, y := y✝ } (mul b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) c = mul { x := x✝¹, y := y✝¹ } (mul { x := x✝, y := y✝ } c)
Theorem: ℤω.my_mul_assoc
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) c = mul { x := x✝¹, y := y✝¹ } (mul { x := x✝, y := y✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    mul { x := x✝², y := y✝² } (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ })
Theorem: ℤω.my_mul_assoc
Proof state before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    mul { x := x✝², y := y✝² } (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ })
Tactic:
simp only [mul]
Proof state after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := (x✝² * x✝¹ - y✝² * y✝¹) * x✝ - (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝,
      y :=
        (x✝² * x✝¹ - y✝² * y✝¹) * y✝ + (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * x✝ -
          (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝ } =
    { x := x✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝),
      y :=
        x✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) + y✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) }
Theorem: ℤω.my_mul_assoc
Proof state before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := (x✝² * x✝¹ - y✝² * y✝¹) * x✝ - (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝,
      y :=
        (x✝² * x✝¹ - y✝² * y✝¹) * y✝ + (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * x✝ -
          (x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹) * y✝ } =
    { x := x✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝),
      y :=
        x✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) + y✝² * (x✝¹ * x✝ - y✝¹ * y✝) - y✝² * (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) }
Tactic:
ring
Proof state after:
no goals
Theorem: ℤω.my_zero_mul
Proof state before:
a b c : ℤω
⊢ mul zero a = zero
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul zero { x := x✝, y := y✝ } = zero
Theorem: ℤω.my_zero_mul
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul zero { x := x✝, y := y✝ } = zero
Tactic:
simp [zero,mul]
Proof state after:
no goals
Theorem: ℤω.my_mul_zero
Proof state before:
a b c : ℤω
⊢ mul a zero = zero
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul { x := x✝, y := y✝ } zero = zero
Theorem: ℤω.my_mul_zero
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul { x := x✝, y := y✝ } zero = zero
Tactic:
simp [mul, zero]
Proof state after:
no goals
Theorem: ℤω.my_one_mul
Proof state before:
a b c : ℤω
⊢ mul one a = a
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul one { x := x✝, y := y✝ } = { x := x✝, y := y✝ }
Theorem: ℤω.my_one_mul
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul one { x := x✝, y := y✝ } = { x := x✝, y := y✝ }
Tactic:
simp [mul, one]
Proof state after:
no goals
Theorem: ℤω.my_mul_one
Proof state before:
a b c : ℤω
⊢ mul a one = a
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul { x := x✝, y := y✝ } one = { x := x✝, y := y✝ }
Theorem: ℤω.my_mul_one
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul { x := x✝, y := y✝ } one = { x := x✝, y := y✝ }
Tactic:
simp [mul, one]
Proof state after:
no goals
Theorem: ℤω.my_left_distrib
Proof state before:
a b c : ℤω
⊢ mul a (add b c) = add (mul a b) (mul a c)
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul { x := x✝, y := y✝ } (add b c) = add (mul { x := x✝, y := y✝ } b) (mul { x := x✝, y := y✝ } c)
Theorem: ℤω.my_left_distrib
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul { x := x✝, y := y✝ } (add b c) = add (mul { x := x✝, y := y✝ } b) (mul { x := x✝, y := y✝ } c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝¹, y := y✝¹ } (add { x := x✝, y := y✝ } c) =
    add (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) (mul { x := x✝¹, y := y✝¹ } c)
Theorem: ℤω.my_left_distrib
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝¹, y := y✝¹ } (add { x := x✝, y := y✝ } c) =
    add (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) (mul { x := x✝¹, y := y✝¹ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝², y := y✝² } (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) =
    add (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) (mul { x := x✝², y := y✝² } { x := x✝, y := y✝ })
Theorem: ℤω.my_left_distrib
Proof state before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝², y := y✝² } (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) =
    add (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) (mul { x := x✝², y := y✝² } { x := x✝, y := y✝ })
Tactic:
simp only [mul, add]
Proof state after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := x✝² * (x✝¹ + x✝) - y✝² * (y✝¹ + y✝), y := x✝² * (y✝¹ + y✝) + y✝² * (x✝¹ + x✝) - y✝² * (y✝¹ + y✝) } =
    { x := x✝² * x✝¹ - y✝² * y✝¹ + (x✝² * x✝ - y✝² * y✝),
      y := x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹ + (x✝² * y✝ + y✝² * x✝ - y✝² * y✝) }
Theorem: ℤω.my_left_distrib
Proof state before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := x✝² * (x✝¹ + x✝) - y✝² * (y✝¹ + y✝), y := x✝² * (y✝¹ + y✝) + y✝² * (x✝¹ + x✝) - y✝² * (y✝¹ + y✝) } =
    { x := x✝² * x✝¹ - y✝² * y✝¹ + (x✝² * x✝ - y✝² * y✝),
      y := x✝² * y✝¹ + y✝² * x✝¹ - y✝² * y✝¹ + (x✝² * y✝ + y✝² * x✝ - y✝² * y✝) }
Tactic:
ring
Proof state after:
no goals
Theorem: ℤω.my_right_distrib
Proof state before:
a b c : ℤω
⊢ mul (add a b) c = add (mul a c) (mul b c)
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul (add { x := x✝, y := y✝ } b) c = add (mul { x := x✝, y := y✝ } c) (mul b c)
Theorem: ℤω.my_right_distrib
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul (add { x := x✝, y := y✝ } b) c = add (mul { x := x✝, y := y✝ } c) (mul b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) c =
    add (mul { x := x✝¹, y := y✝¹ } c) (mul { x := x✝, y := y✝ } c)
Theorem: ℤω.my_right_distrib
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) c =
    add (mul { x := x✝¹, y := y✝¹ } c) (mul { x := x✝, y := y✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (add { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    add (mul { x := x✝², y := y✝² } { x := x✝, y := y✝ }) (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ })
Theorem: ℤω.my_right_distrib
Proof state before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul (add { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) { x := x✝, y := y✝ } =
    add (mul { x := x✝², y := y✝² } { x := x✝, y := y✝ }) (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ })
Tactic:
simp only [mul, add]
Proof state after:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := (x✝² + x✝¹) * x✝ - (y✝² + y✝¹) * y✝, y := (x✝² + x✝¹) * y✝ + (y✝² + y✝¹) * x✝ - (y✝² + y✝¹) * y✝ } =
    { x := x✝² * x✝ - y✝² * y✝ + (x✝¹ * x✝ - y✝¹ * y✝),
      y := x✝² * y✝ + y✝² * x✝ - y✝² * y✝ + (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) }
Theorem: ℤω.my_right_distrib
Proof state before:
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := (x✝² + x✝¹) * x✝ - (y✝² + y✝¹) * y✝, y := (x✝² + x✝¹) * y✝ + (y✝² + y✝¹) * x✝ - (y✝² + y✝¹) * y✝ } =
    { x := x✝² * x✝ - y✝² * y✝ + (x✝¹ * x✝ - y✝¹ * y✝),
      y := x✝² * y✝ + y✝² * x✝ - y✝² * y✝ + (x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝) }
Tactic:
ring
Proof state after:
no goals
Theorem: ℤω.my_mul_comm
Proof state before:
a b c : ℤω
⊢ mul a b = mul b a
Tactic:
cases a
Proof state after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul { x := x✝, y := y✝ } b = mul b { x := x✝, y := y✝ }
Theorem: ℤω.my_mul_comm
Proof state before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul { x := x✝, y := y✝ } b = mul b { x := x✝, y := y✝ }
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ } = mul { x := x✝, y := y✝ } { x := x✝¹, y := y✝¹ }
Theorem: ℤω.my_mul_comm
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ } = mul { x := x✝, y := y✝ } { x := x✝¹, y := y✝¹ }
Tactic:
simp only [mul]
Proof state after:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := x✝¹ * x✝ - y✝¹ * y✝, y := x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝ } =
    { x := x✝ * x✝¹ - y✝ * y✝¹, y := x✝ * y✝¹ + y✝ * x✝¹ - y✝ * y✝¹ }
Theorem: ℤω.my_mul_comm
Proof state before:
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ { x := x✝¹ * x✝ - y✝¹ * y✝, y := x✝¹ * y✝ + y✝¹ * x✝ - y✝¹ * y✝ } =
    { x := x✝ * x✝¹ - y✝ * y✝¹, y := x✝ * y✝¹ + y✝ * x✝¹ - y✝ * y✝¹ }
Tactic:
ring
Proof state after:
no goals
Theorem: ℤω.rt3_sq
Proof state before:
a b c : ℤω
⊢ rt3 ^ 2 = 3
Tactic:
have : (0 : ℝ) ≤ 3 := by norm_num
Proof state after:
a b c : ℤω
this : 0 ≤ 3
⊢ rt3 ^ 2 = 3
Theorem: ℤω.rt3_sq
Proof state before:
a b c : ℤω
this : 0 ≤ 3
⊢ rt3 ^ 2 = 3
Tactic:
rw [pow_two]
Proof state after:
a b c : ℤω
this : 0 ≤ 3
⊢ rt3 * rt3 = 3
Theorem: ℤω.rt3_sq
Proof state before:
a b c : ℤω
this : 0 ≤ 3
⊢ rt3 * rt3 = 3
Tactic:
rw [← Real.sqrt_mul this 3]
Proof state after:
a b c : ℤω
this : 0 ≤ 3
⊢ Real.sqrt (3 * 3) = 3
Theorem: ℤω.rt3_sq
Proof state before:
a b c : ℤω
this : 0 ≤ 3
⊢ Real.sqrt (3 * 3) = 3
Tactic:
rw [Real.sqrt_mul_self this]
Proof state after:
no goals
Theorem: ℤω.rt3_sq
Proof state before:
a b c : ℤω
⊢ 0 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤω.sqrt3_inv_hMul_self
Proof state before:
a b c : ℤω
⊢ rt3⁻¹ * rt3 = 1
Tactic:
apply inv_mul_cancel
Proof state after:
case h
a b c : ℤω
⊢ rt3 ≠ 0
Theorem: ℤω.sqrt3_inv_hMul_self
Proof state before:
case h
a b c : ℤω
⊢ rt3 ≠ 0
Tactic:
intro h
Proof state after:
case h
a b c : ℤω
h : rt3 = 0
⊢ False
Theorem: ℤω.sqrt3_inv_hMul_self
Proof state before:
case h
a b c : ℤω
h : rt3 = 0
⊢ False
Tactic:
have := Real.sqrt_eq_iff_mul_self_eq (by norm_num : (0:ℝ) ≤ 3) (by norm_num : (0:ℝ) ≤ 0)
Proof state after:
case h
a b c : ℤω
h : rt3 = 0
this : Real.sqrt 3 = 0 ↔ 0 * 0 = 3
⊢ False
Theorem: ℤω.sqrt3_inv_hMul_self
Proof state before:
case h
a b c : ℤω
h : rt3 = 0
this : Real.sqrt 3 = 0 ↔ 0 * 0 = 3
⊢ False
Tactic:
rw [this] at h
Proof state after:
case h
a b c : ℤω
h : 0 * 0 = 3
this : Real.sqrt 3 = 0 ↔ 0 * 0 = 3
⊢ False
Theorem: ℤω.sqrt3_inv_hMul_self
Proof state before:
case h
a b c : ℤω
h : 0 * 0 = 3
this : Real.sqrt 3 = 0 ↔ 0 * 0 = 3
⊢ False
Tactic:
norm_num at h
Proof state after:
no goals
Theorem: ℤω.sqrt3_inv_hMul_self
Proof state before:
a b c : ℤω
h : rt3 = 0
⊢ 0 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤω.sqrt3_inv_hMul_self
Proof state before:
a b c : ℤω
h : rt3 = 0
⊢ 0 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤω.complexω_sq
Proof state before:
a b c : ℤω
⊢ complexω ^ 2 = -complexω - 1
Tactic:
rw [pow_two]
Proof state after:
a b c : ℤω
⊢ complexω * complexω = -complexω - 1
Theorem: ℤω.complexω_sq
Proof state before:
a b c : ℤω
⊢ complexω * complexω = -complexω - 1
Tactic:
ext
Proof state after:
case a
a b c : ℤω
⊢ (complexω * complexω).re = (-complexω - 1).re

case a
a b c : ℤω
⊢ (complexω * complexω).im = (-complexω - 1).im
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ (complexω * complexω).re = (-complexω - 1).re
Tactic:
simp only [Complex.mul_re]
Proof state after:
case a
a b c : ℤω
⊢ complexω.re * complexω.re - complexω.im * complexω.im = (-complexω - 1).re
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ complexω.re * complexω.re - complexω.im * complexω.im = (-complexω - 1).re
Tactic:
simp only [complexω]
Proof state after:
case a
a b c : ℤω
⊢ -1 / 2 * (-1 / 2) - rt3 / 2 * (rt3 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).re
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ -1 / 2 * (-1 / 2) - rt3 / 2 * (rt3 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).re
Tactic:
ring_nf
Proof state after:
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re
Tactic:
rw [rt3_sq]
Proof state after:
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + 3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(ofNat 1) / ↑2) }).re
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ ↑(ofNat 1) / ↑4 + 3 * ↑(negOfNat 1) * (↑(ofNat 1) / ↑4) =
    (-1 - { re := ↑(negOfNat 1) * (↑(ofNat 1) / ↑2), im := rt3 * (↑(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ω - 1).im
Tactic:
rw [Complex.mul_im]
Proof state after:
case a
a b c : ℤω
⊢ complexω.re * complexω.im + complexω.im * complexω.re = (-complexω - 1).im
Theorem: ℤω.complexω_sq
Proof state before:
case a
a b c : ℤω
⊢ complexω.re * complexω.im + complexω.im * complexω.re = (-complexω - 1).im
Tactic:
simp only [complexω]
Proof state after:
case a
a b c : ℤω
⊢ -1 / 2 * (rt3 / 2) + rt3 / 2 * (-1 / 2) = (-{ re := -1 / 2, im := rt3 / 2 } - 1).im