internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.my_left_distrib
Proof state before:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝², g := g✝², h := h✝² } (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) =
    add (mul { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ })
      (mul { f := f✝², g := g✝², h := h✝² } { f := f✝, g := g✝, h := h✝ })
Tactic:
simp only [mul, add]
Proof state after:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := f✝² * (f✝¹ + f✝) + 6 * h✝² * (h✝¹ + h✝) - 2 * g✝² * (h✝¹ + h✝) - 2 * h✝² * (g✝¹ + g✝),
      g := f✝² * (g✝¹ + g✝) + g✝² * (f✝¹ + f✝) + 16 * h✝² * (h✝¹ + h✝) - 6 * g✝² * (h✝¹ + h✝) - 6 * h✝² * (g✝¹ + g✝),
      h :=
        f✝² * (h✝¹ + h✝) + h✝² * (f✝¹ + f✝) + g✝² * (g✝¹ + g✝) + 3 * h✝² * (h✝¹ + h✝) - 3 * g✝² * (h✝¹ + h✝) -
          3 * h✝² * (g✝¹ + g✝) } =
    {
      f :=
        f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹ +
          (f✝² * f✝ + 6 * h✝² * h✝ - 2 * g✝² * h✝ - 2 * h✝² * g✝),
      g :=
        f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹ +
          (f✝² * g✝ + g✝² * f✝ + 16 * h✝² * h✝ - 6 * g✝² * h✝ - 6 * h✝² * g✝),
      h :=
        f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹ +
          (f✝² * h✝ + h✝² * f✝ + g✝² * g✝ + 3 * h✝² * h✝ - 3 * g✝² * h✝ - 3 * h✝² * g✝) }
Theorem: ℤθ.my_left_distrib
Proof state before:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := f✝² * (f✝¹ + f✝) + 6 * h✝² * (h✝¹ + h✝) - 2 * g✝² * (h✝¹ + h✝) - 2 * h✝² * (g✝¹ + g✝),
      g := f✝² * (g✝¹ + g✝) + g✝² * (f✝¹ + f✝) + 16 * h✝² * (h✝¹ + h✝) - 6 * g✝² * (h✝¹ + h✝) - 6 * h✝² * (g✝¹ + g✝),
      h :=
        f✝² * (h✝¹ + h✝) + h✝² * (f✝¹ + f✝) + g✝² * (g✝¹ + g✝) + 3 * h✝² * (h✝¹ + h✝) - 3 * g✝² * (h✝¹ + h✝) -
          3 * h✝² * (g✝¹ + g✝) } =
    {
      f :=
        f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹ +
          (f✝² * f✝ + 6 * h✝² * h✝ - 2 * g✝² * h✝ - 2 * h✝² * g✝),
      g :=
        f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹ +
          (f✝² * g✝ + g✝² * f✝ + 16 * h✝² * h✝ - 6 * g✝² * h✝ - 6 * h✝² * g✝),
      h :=
        f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹ +
          (f✝² * h✝ + h✝² * f✝ + g✝² * g✝ + 3 * h✝² * h✝ - 3 * g✝² * h✝ - 3 * h✝² * g✝) }
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 : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul (add { f := f✝, g := g✝, h := h✝ } b) c = add (mul { f := f✝, g := g✝, h := h✝ } c) (mul b c)
Theorem: ℤθ.my_right_distrib
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul (add { f := f✝, g := g✝, h := h✝ } b) c = add (mul { f := f✝, g := g✝, h := h✝ } c) (mul b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    add (mul { f := f✝¹, g := g✝¹, h := h✝¹ } c) (mul { f := f✝, g := g✝, h := h✝ } c)
Theorem: ℤθ.my_right_distrib
Proof state before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    add (mul { f := f✝¹, g := g✝¹, h := h✝¹ } c) (mul { f := f✝, g := g✝, h := h✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul (add { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ }) { f := f✝, g := g✝, h := h✝ } =
    add (mul { f := f✝², g := g✝², h := h✝² } { f := f✝, g := g✝, h := h✝ })
      (mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ })
Theorem: ℤθ.my_right_distrib
Proof state before:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul (add { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ }) { f := f✝, g := g✝, h := h✝ } =
    add (mul { f := f✝², g := g✝², h := h✝² } { f := f✝, g := g✝, h := h✝ })
      (mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ })
Tactic:
simp only [mul, add]
Proof state after:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := (f✝² + f✝¹) * f✝ + 6 * (h✝² + h✝¹) * h✝ - 2 * (g✝² + g✝¹) * h✝ - 2 * (h✝² + h✝¹) * g✝,
      g := (f✝² + f✝¹) * g✝ + (g✝² + g✝¹) * f✝ + 16 * (h✝² + h✝¹) * h✝ - 6 * (g✝² + g✝¹) * h✝ - 6 * (h✝² + h✝¹) * g✝,
      h :=
        (f✝² + f✝¹) * h✝ + (h✝² + h✝¹) * f✝ + (g✝² + g✝¹) * g✝ + 3 * (h✝² + h✝¹) * h✝ - 3 * (g✝² + g✝¹) * h✝ -
          3 * (h✝² + h✝¹) * g✝ } =
    {
      f :=
        f✝² * f✝ + 6 * h✝² * h✝ - 2 * g✝² * h✝ - 2 * h✝² * g✝ + (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝),
      g :=
        f✝² * g✝ + g✝² * f✝ + 16 * h✝² * h✝ - 6 * g✝² * h✝ - 6 * h✝² * g✝ +
          (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝),
      h :=
        f✝² * h✝ + h✝² * f✝ + g✝² * g✝ + 3 * h✝² * h✝ - 3 * g✝² * h✝ - 3 * h✝² * g✝ +
          (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) }
Theorem: ℤθ.my_right_distrib
Proof state before:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := (f✝² + f✝¹) * f✝ + 6 * (h✝² + h✝¹) * h✝ - 2 * (g✝² + g✝¹) * h✝ - 2 * (h✝² + h✝¹) * g✝,
      g := (f✝² + f✝¹) * g✝ + (g✝² + g✝¹) * f✝ + 16 * (h✝² + h✝¹) * h✝ - 6 * (g✝² + g✝¹) * h✝ - 6 * (h✝² + h✝¹) * g✝,
      h :=
        (f✝² + f✝¹) * h✝ + (h✝² + h✝¹) * f✝ + (g✝² + g✝¹) * g✝ + 3 * (h✝² + h✝¹) * h✝ - 3 * (g✝² + g✝¹) * h✝ -
          3 * (h✝² + h✝¹) * g✝ } =
    {
      f :=
        f✝² * f✝ + 6 * h✝² * h✝ - 2 * g✝² * h✝ - 2 * h✝² * g✝ + (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝),
      g :=
        f✝² * g✝ + g✝² * f✝ + 16 * h✝² * h✝ - 6 * g✝² * h✝ - 6 * h✝² * g✝ +
          (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝),
      h :=
        f✝² * h✝ + h✝² * f✝ + g✝² * g✝ + 3 * h✝² * h✝ - 3 * g✝² * h✝ - 3 * h✝² * g✝ +
          (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) }
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 : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } b = mul b { f := f✝, g := g✝, h := h✝ }
Theorem: ℤθ.my_mul_comm
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } b = mul b { f := f✝, g := g✝, h := h✝ }
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ } =
    mul { f := f✝, g := g✝, h := h✝ } { f := f✝¹, g := g✝¹, h := h✝¹ }
Theorem: ℤθ.my_mul_comm
Proof state before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ } =
    mul { f := f✝, g := g✝, h := h✝ } { f := f✝¹, g := g✝¹, h := h✝¹ }
Tactic:
simp only [mul]
Proof state after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝,
      g := f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝,
      h := f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝ } =
    { f := f✝ * f✝¹ + 6 * h✝ * h✝¹ - 2 * g✝ * h✝¹ - 2 * h✝ * g✝¹,
      g := f✝ * g✝¹ + g✝ * f✝¹ + 16 * h✝ * h✝¹ - 6 * g✝ * h✝¹ - 6 * h✝ * g✝¹,
      h := f✝ * h✝¹ + h✝ * f✝¹ + g✝ * g✝¹ + 3 * h✝ * h✝¹ - 3 * g✝ * h✝¹ - 3 * h✝ * g✝¹ }
Theorem: ℤθ.my_mul_comm
Proof state before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ { f := f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝,
      g := f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝,
      h := f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝ } =
    { f := f✝ * f✝¹ + 6 * h✝ * h✝¹ - 2 * g✝ * h✝¹ - 2 * h✝ * g✝¹,
      g := f✝ * g✝¹ + g✝ * f✝¹ + 16 * h✝ * h✝¹ - 6 * g✝ * h✝¹ - 6 * h✝ * g✝¹,
      h := f✝ * h✝¹ + h✝ * f✝¹ + g✝ * g✝¹ + 3 * h✝ * h✝¹ - 3 * g✝ * h✝¹ - 3 * h✝ * g✝¹ }
Tactic:
ring
Proof state after:
no goals
Theorem: ℤθ.my_zsmul_zero'
Proof state before:
a b c : ℤθ
⊢ ∀ (a : ℤθ), zsmul 0 a = zero
Tactic:
intro a
Proof state after:
a✝ b c a : ℤθ
⊢ zsmul 0 a = zero
Theorem: ℤθ.my_zsmul_zero'
Proof state before:
a✝ b c a : ℤθ
⊢ zsmul 0 a = zero
Tactic:
unfold zsmul
Proof state after:
a✝ b c a : ℤθ
⊢ { f := 0 * a.f, g := 0 * a.g, h := 0 * a.h } = zero
Theorem: ℤθ.my_zsmul_zero'
Proof state before:
a✝ b c a : ℤθ
⊢ { f := 0 * a.f, g := 0 * a.g, h := 0 * a.h } = zero
Tactic:
rw [MulZeroClass.zero_mul]
Proof state after:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0 * a.g, h := 0 * a.h } = zero
Theorem: ℤθ.my_zsmul_zero'
Proof state before:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0 * a.g, h := 0 * a.h } = zero
Tactic:
rw [MulZeroClass.zero_mul]
Proof state after:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0, h := 0 * a.h } = zero
Theorem: ℤθ.my_zsmul_zero'
Proof state before:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0, h := 0 * a.h } = zero
Tactic:
rw [MulZeroClass.zero_mul]
Proof state after:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0, h := 0 } = zero
Theorem: ℤθ.my_zsmul_zero'
Proof state before:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0, h := 0 } = zero
Tactic:
rw [← zero]
Proof state after:
no goals
Theorem: ℤθ.my_zsmul_succ'
Proof state before:
a b c : ℤθ
⊢ ∀ (n : ℕ) (a : ℤθ), zsmul (Int.ofNat (Nat.succ n)) a = add a (zsmul (Int.ofNat n) a)
Tactic:
intro n a
Proof state after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.ofNat (Nat.succ n)) a = add a (zsmul (Int.ofNat n) a)
Theorem: ℤθ.my_zsmul_succ'
Proof state before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.ofNat (Nat.succ n)) a = add a (zsmul (Int.ofNat n) a)
Tactic:
change
  (⟨Int.ofNat n.succ * a.f, Int.ofNat n.succ * a.g, Int.ofNat n.succ * a.h⟩ : ℤθ) =
    (⟨a.f + Int.ofNat n * a.f, a.g + Int.ofNat n * a.g, a.h + Int.ofNat n * a.h⟩ : ℤθ)
Proof state after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ { f := Int.ofNat (Nat.succ n) * a.f, g := Int.ofNat (Nat.succ n) * a.g, h := Int.ofNat (Nat.succ n) * a.h } =
    { f := a.f + Int.ofNat n * a.f, g := a.g + Int.ofNat n * a.g, h := a.h + Int.ofNat n * a.h }
Theorem: ℤθ.my_zsmul_succ'
Proof state before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ { f := Int.ofNat (Nat.succ n) * a.f, g := Int.ofNat (Nat.succ n) * a.g, h := Int.ofNat (Nat.succ n) * a.h } =
    { f := a.f + Int.ofNat n * a.f, g := a.g + Int.ofNat n * a.g, h := a.h + Int.ofNat n * a.h }
Tactic:
norm_num
Proof state after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.f = a.f + ↑n * a.f ∧ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Theorem: ℤθ.my_zsmul_succ'
Proof state before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.f = a.f + ↑n * a.f ∧ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
constructor
Proof state after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.f = a.f + ↑n * a.f

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Theorem: ℤθ.my_zsmul_succ'
Proof state before:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.f = a.f + ↑n * a.f

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
linarith
Proof state after:
case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Theorem: ℤθ.my_zsmul_succ'
Proof state before:
case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g ∧ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
constructor
Proof state after:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.h = a.h + ↑n * a.h
Theorem: ℤθ.my_zsmul_succ'
Proof state before:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.g = a.g + ↑n * a.g

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
linarith
Proof state after:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.h = a.h + ↑n * a.h
Theorem: ℤθ.my_zsmul_succ'
Proof state before:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ (↑n + 1) * a.h = a.h + ↑n * a.h
Tactic:
linarith
Proof state after:
no goals
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
a b c : ℤθ
⊢ ∀ (n : ℕ) (a : ℤθ), zsmul (Int.negSucc n) a = neg (zsmul (↑(Nat.succ n)) a)
Tactic:
intro n a
Proof state after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑(Nat.succ n)) a)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑(Nat.succ n)) a)
Tactic:
simp
Proof state after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑n + 1) a)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑n + 1) a)
Tactic:
change
  (⟨Int.negSucc n * a.f, Int.negSucc n * a.g, Int.negSucc n * a.h⟩ : ℤθ) =
    (⟨-(Int.ofNat n.succ * a.f), -(Int.ofNat n.succ * a.g), -(Int.ofNat n.succ * a.h)⟩ : ℤθ)
Proof state after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ { f := Int.negSucc n * a.f, g := Int.negSucc n * a.g, h := Int.negSucc n * a.h } =
    { f := -(Int.ofNat (Nat.succ n) * a.f), g := -(Int.ofNat (Nat.succ n) * a.g), h := -(Int.ofNat (Nat.succ n) * a.h) }
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ { f := Int.negSucc n * a.f, g := Int.negSucc n * a.g, h := Int.negSucc n * a.h } =
    { f := -(Int.ofNat (Nat.succ n) * a.f), g := -(Int.ofNat (Nat.succ n) * a.g), h := -(Int.ofNat (Nat.succ n) * a.h) }
Tactic:
simp
Proof state after:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.f = -((↑n + 1) * a.f) ∧
    Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.f = -((↑n + 1) * a.f) ∧
    Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
constructor
Proof state after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.f = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.f = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.negSucc_coe]
Proof state after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -↑(n + 1) * a.f = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -↑(n + 1) * a.f = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.neg_mul_eq_neg_mul_symm]
Proof state after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -(↑(n + 1) * a.f) = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -(↑(n + 1) * a.f) = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.ofNat_add]
Proof state after:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -((↑n + ↑1) * a.f) = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -((↑n + ↑1) * a.f) = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.ofNat_one]
Proof state after:
case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
constructor
Proof state after:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g)

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g)

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.negSucc_coe]
Proof state after:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -↑(n + 1) * a.g = -((↑n + 1) * a.g)

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -↑(n + 1) * a.g = -((↑n + 1) * a.g)

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.neg_mul_eq_neg_mul_symm]
Proof state after:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -(↑(n + 1) * a.g) = -((↑n + 1) * a.g)

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -(↑(n + 1) * a.g) = -((↑n + 1) * a.g)

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.ofNat_add]
Proof state after:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -((↑n + ↑1) * a.g) = -((↑n + 1) * a.g)

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -((↑n + ↑1) * a.g) = -((↑n + 1) * a.g)

case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.ofNat_one]
Proof state after:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.negSucc_coe]
Proof state after:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -↑(n + 1) * a.h = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -↑(n + 1) * a.h = -((↑n + 1) * a.h)
Tactic:
rw [Int.neg_mul_eq_neg_mul_symm]
Proof state after:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -(↑(n + 1) * a.h) = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -(↑(n + 1) * a.h) = -((↑n + 1) * a.h)
Tactic:
rw [Int.ofNat_add]
Proof state after:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -((↑n + ↑1) * a.h) = -((↑n + 1) * a.h)
Theorem: ℤθ.my_zsmul_neg'
Proof state before:
case right.right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -((↑n + ↑1) * a.h) = -((↑n + 1) * a.h)
Tactic:
rw [Int.ofNat_one]
Proof state after:
no goals
Theorem: ℤθ.my_natCast_zero
Proof state before:
a b c : ℤθ
⊢ natCast 0 = zero
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤθ.my_natCast_succ
Proof state before:
a b c : ℤθ
⊢ ∀ (n : ℕ), natCast (n + 1) = add (natCast n) one
Tactic:
intro n
Proof state after:
a b c : ℤθ
n : ℕ
⊢ natCast (n + 1) = add (natCast n) one
Theorem: ℤθ.my_natCast_succ
Proof state before:
a b c : ℤθ
n : ℕ
⊢ natCast (n + 1) = add (natCast n) one
Tactic:
change (⟨Int.ofNat (n + 1), 0, 0⟩ : ℤθ) = (⟨Int.ofNat n + 1, 0, 0⟩ : ℤθ)
Proof state after:
a b c : ℤθ
n : ℕ
⊢ { f := Int.ofNat (n + 1), g := 0, h := 0 } = { f := Int.ofNat n + 1, g := 0, h := 0 }
Theorem: ℤθ.my_natCast_succ
Proof state before:
a b c : ℤθ
n : ℕ
⊢ { f := Int.ofNat (n + 1), g := 0, h := 0 } = { f := Int.ofNat n + 1, g := 0, h := 0 }
Tactic:
simp
Proof state after:
no goals
Theorem: ℤθ.my_intCast_of_nat
Proof state before:
a b c : ℤθ
⊢ ∀ (n : ℕ), intCast ↑n = natCast n
Tactic:
intro n
Proof state after:
a b c : ℤθ
n : ℕ
⊢ intCast ↑n = natCast n
Theorem: ℤθ.my_intCast_of_nat
Proof state before:
a b c : ℤθ
n : ℕ
⊢ intCast ↑n = natCast n
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤθ.my_intCast_neg_succ_of_nat
Proof state before:
a b c : ℤθ
⊢ ∀ (n : ℕ), intCast (-↑(n + 1)) = neg (natCast (n + 1))
Tactic:
intro n
Proof state after:
a b c : ℤθ
n : ℕ
⊢ intCast (-↑(n + 1)) = neg (natCast (n + 1))
Theorem: ℤθ.my_intCast_neg_succ_of_nat
Proof state before:
a b c : ℤθ
n : ℕ
⊢ intCast (-↑(n + 1)) = neg (natCast (n + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤθ.unit_l
Proof state before:
a b c : ℤθ
⊢ ↑unit = { f := -1, g := -3, h := -1 }
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤθ.unit_neg_1
Proof state before:
a b c : ℤθ
⊢ ↑(unit ^ (-1)) = { f := 25, g := 13, h := 5 }
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤθ.simp_norm
Proof state before:
a✝ b✝ c : ℤθ
a b : ℤ
⊢ norm { f := a, g := -b, h := 0 } = |a ^ 3 + 3 * a ^ 2 * b + 6 * a * b ^ 2 + 2 * b ^ 3|
Tactic:
unfold norm
Proof state after:
a✝ b✝ c : ℤθ
a b : ℤ
⊢ |{ f := a, g := -b, h := 0 }.f ^ 3 - 2 * { f := a, g := -b, h := 0 }.g ^ 3 + 4 * { f := a, g := -b, h := 0 }.h ^ 3 -
                    3 * { f := a, g := -b, h := 0 }.f ^ 2 * { f := a, g := -b, h := 0 }.g -
                  3 * { f := a, g := -b, h := 0 }.f ^ 2 * { f := a, g := -b, h := 0 }.h +
                6 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.g ^ 2 +
              6 * { f := a, g := -b, h := 0 }.g ^ 2 * { f := a, g := -b, h := 0 }.h +
            24 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.h ^ 2 -
          12 * { f := a, g := -b, h := 0 }.g * { f := a, g := -b, h := 0 }.h ^ 2 -
        12 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.g * { f := a, g := -b, h := 0 }.h| =
    |a ^ 3 + 3 * a ^ 2 * b + 6 * a * b ^ 2 + 2 * b ^ 3|
Theorem: ℤθ.simp_norm
Proof state before:
a✝ b✝ c : ℤθ
a b : ℤ
⊢ |{ f := a, g := -b, h := 0 }.f ^ 3 - 2 * { f := a, g := -b, h := 0 }.g ^ 3 + 4 * { f := a, g := -b, h := 0 }.h ^ 3 -
                    3 * { f := a, g := -b, h := 0 }.f ^ 2 * { f := a, g := -b, h := 0 }.g -
                  3 * { f := a, g := -b, h := 0 }.f ^ 2 * { f := a, g := -b, h := 0 }.h +
                6 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.g ^ 2 +
              6 * { f := a, g := -b, h := 0 }.g ^ 2 * { f := a, g := -b, h := 0 }.h +
            24 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.h ^ 2 -
          12 * { f := a, g := -b, h := 0 }.g * { f := a, g := -b, h := 0 }.h ^ 2 -
        12 * { f := a, g := -b, h := 0 }.f * { f := a, g := -b, h := 0 }.g * { f := a, g := -b, h := 0 }.h| =
    |a ^ 3 + 3 * a ^ 2 * b + 6 * a * b ^ 2 + 2 * b ^ 3|
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ℤθ.hMul_mule_3
Proof state before:
a✝ b✝ c a b : ℤθ
⊢ a * b =
    { f := a.f * b.f + 6 * a.h * b.h - 2 * a.g * b.h - 2 * a.h * b.g,
      g := a.f * b.g + a.g * b.f + 16 * a.h * b.h - 6 * a.g * b.h - 6 * a.h * b.g,
      h := a.f * b.h + a.h * b.f + a.g * b.g + 3 * a.h * b.h - 3 * a.g * b.h - 3 * a.h * b.g }
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤθ.norm_divides
Proof state before:
a✝ b c p a : ℤθ
h : p ∣ a
⊢ norm p ∣ norm a
Tactic:
cases' h with n hn
Proof state after:
case intro
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm p ∣ norm a
Theorem: ℤθ.norm_divides
Proof state before:
case intro
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm p ∣ norm a
Tactic:
use norm n
Proof state after:
case h
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm a = norm p * norm n
Theorem: ℤθ.norm_divides
Proof state before:
case h
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm a = norm p * norm n
Tactic:
rw [norm_hMul p n]
Proof state after:
case h
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm a = norm (p * n)
Theorem: ℤθ.norm_divides
Proof state before:
case h
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm a = norm (p * n)
Tactic:
rw [hn]
Proof state after:
no goals
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
⊢ IsUnit k → norm k = 1
Tactic:
intro h
Proof state after:
a b c k : ℤθ
h : IsUnit k
⊢ norm k = 1
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : IsUnit k
⊢ norm k = 1
Tactic:
rw [isUnit_iff_exists_inv] at h
Proof state after:
a b c k : ℤθ
h : ∃ b, k * b = 1
⊢ norm k = 1
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
⊢ norm k = 1
Tactic:
have p : ∃ b : ℤθ, 1 = k * b := by tauto
Proof state after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : ∃ b, 1 = k * b
⊢ norm k = 1
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : ∃ b, 1 = k * b
⊢ norm k = 1
Tactic:
change k ∣ 1 at p
Proof state after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
⊢ norm k = 1