internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro.intro.intro.intro.intro.inr
a b c : ℤθ
k : ℕ
l : k + 1 = Nat.succ k
p q r : ℤ
h1 : (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p
h2 : (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q
h3 : (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r
t :
  ↑(unit ^ 3 ^ Nat.succ k) =
    { f := 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p, g := 3 ^ (Nat.succ k + 1) * q,
      h := 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r }
g2 : 2 ≤ Nat.succ k
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ (Nat.succ k + 1))).f = 1 + 3 ^ (Nat.succ k + 1) + 3 ^ (Nat.succ k + 2) * a ∧
      (↑(unit ^ 3 ^ (Nat.succ k + 1))).g = 3 ^ (Nat.succ k + 2) * b ∧
        (↑(unit ^ 3 ^ (Nat.succ k + 1))).h = 3 ^ (Nat.succ k + 1) + 3 ^ (Nat.succ k + 2) * c
Tactic:
sorry
Proof state after:
no goals
Theorem: ℤθ.unit_pow_three_pow_2
Proof state before:
a b c : ℤθ
n : ℕ
⊢ ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
Tactic:
induction' n with n ih
Proof state after:
case zero
a b c : ℤθ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * φ

case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Theorem: ℤθ.unit_pow_three_pow_2
Proof state before:
case zero
a b c : ℤθ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * φ

case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Tactic:
use⟨-8, -21, -5⟩
Proof state after:
case h
a b c : ℤθ
⊢ ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * { f := -8, g := -21, h := -5 }

case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Theorem: ℤθ.unit_pow_three_pow_2
Proof state before:
case h
a b c : ℤθ
⊢ ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * { f := -8, g := -21, h := -5 }

case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Tactic:
rfl
Proof state after:
case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Theorem: ℤθ.unit_pow_three_pow_2
Proof state before:
case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Tactic:
obtain ⟨ψ, hψ⟩ := ih
Proof state after:
case succ.intro
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Theorem: ℤθ.unit_pow_three_pow_2
Proof state before:
case succ.intro
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Tactic:
use ψ + 3 ^ (n + 1) * ψ ^ 2 + 3 ^ (2 * n + 2) * ψ ^ 3
Proof state after:
case h
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * (ψ + 3 ^ (n + 1) * ψ ^ 2 + 3 ^ (2 * n + 2) * ψ ^ 3)
Theorem: ℤθ.unit_pow_three_pow_2
Proof state before:
case h
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * (ψ + 3 ^ (n + 1) * ψ ^ 2 + 3 ^ (2 * n + 2) * ψ ^ 3)
Tactic:
sorry
Proof state after:
no goals
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 : ℤα
z✝ w✝ : ℤ
⊢ add (add { z := z✝, w := w✝ } b) c = add { z := z✝, w := w✝ } (add b c)
Theorem: ℤα.my_add_assoc
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ add (add { z := z✝, w := w✝ } b) c = add { z := z✝, w := w✝ } (add b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ add (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) c = add { z := z✝¹, w := w✝¹ } (add { z := z✝, w := w✝ } c)
Theorem: ℤα.my_add_assoc
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ add (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) c = add { z := z✝¹, w := w✝¹ } (add { z := z✝, w := w✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ add (add { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) { z := z✝, w := w✝ } =
    add { z := z✝², w := w✝² } (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ })
Theorem: ℤα.my_add_assoc
Proof state before:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ add (add { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) { z := z✝, w := w✝ } =
    add { z := z✝², w := w✝² } (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ })
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 { z := x, w := y } = { z := x, w := y }
Theorem: ℤα.my_zero_add
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ add zero { z := x, w := y } = { z := x, w := 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 { z := x, w := y } zero = { z := x, w := y }
Theorem: ℤα.my_add_zero
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ add { z := x, w := y } zero = { z := x, w := 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 : ℤα
z✝ w✝ : ℤ
⊢ add (neg { z := z✝, w := w✝ }) { z := z✝, w := w✝ } = zero
Theorem: ℤα.my_add_left_neg
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ add (neg { z := z✝, w := w✝ }) { z := z✝, w := w✝ } = zero
Tactic:
simp only [neg, add]
Proof state after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ { z := -z✝ + z✝, w := -w✝ + w✝ } = zero
Theorem: ℤα.my_add_left_neg
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ { z := -z✝ + z✝, w := -w✝ + w✝ } = zero
Tactic:
simp only [add_left_neg]
Proof state after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ { z := 0, w := 0 } = zero
Theorem: ℤα.my_add_left_neg
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ { z := 0, w := 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 : ℤα
z✝ w✝ : ℤ
⊢ add { z := z✝, w := w✝ } b = add b { z := z✝, w := w✝ }
Theorem: ℤα.my_add_comm
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ add { z := z✝, w := w✝ } b = add b { z := z✝, w := w✝ }
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ } = add { z := z✝, w := w✝ } { z := z✝¹, w := w✝¹ }
Theorem: ℤα.my_add_comm
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ } = add { z := z✝, w := w✝ } { z := z✝¹, w := w✝¹ }
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 : ℤα
z✝ w✝ : ℤ
⊢ mul (mul { z := z✝, w := w✝ } b) c = mul { z := z✝, w := w✝ } (mul b c)
Theorem: ℤα.my_mul_assoc
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul (mul { z := z✝, w := w✝ } b) c = mul { z := z✝, w := w✝ } (mul b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) c = mul { z := z✝¹, w := w✝¹ } (mul { z := z✝, w := w✝ } c)
Theorem: ℤα.my_mul_assoc
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) c = mul { z := z✝¹, w := w✝¹ } (mul { z := z✝, w := w✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (mul { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) { z := z✝, w := w✝ } =
    mul { z := z✝², w := w✝² } (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ })
Theorem: ℤα.my_mul_assoc
Proof state before:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (mul { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) { z := z✝, w := w✝ } =
    mul { z := z✝², w := w✝² } (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ })
Tactic:
simp only [mul]
Proof state after:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := (z✝² * z✝¹ - 2 * w✝² * w✝¹) * z✝ - 2 * (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * w✝,
      w :=
        (z✝² * z✝¹ - 2 * w✝² * w✝¹) * w✝ + (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * z✝ +
          (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * w✝ } =
    { z := z✝² * (z✝¹ * z✝ - 2 * w✝¹ * w✝) - 2 * w✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝),
      w :=
        z✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) + w✝² * (z✝¹ * z✝ - 2 * w✝¹ * w✝) +
          w✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) }
Theorem: ℤα.my_mul_assoc
Proof state before:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := (z✝² * z✝¹ - 2 * w✝² * w✝¹) * z✝ - 2 * (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * w✝,
      w :=
        (z✝² * z✝¹ - 2 * w✝² * w✝¹) * w✝ + (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * z✝ +
          (z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹) * w✝ } =
    { z := z✝² * (z✝¹ * z✝ - 2 * w✝¹ * w✝) - 2 * w✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝),
      w :=
        z✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) + w✝² * (z✝¹ * z✝ - 2 * w✝¹ * w✝) +
          w✝² * (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) }
Tactic:
ring
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 : ℤα
z✝ w✝ : ℤ
⊢ mul one { z := z✝, w := w✝ } = { z := z✝, w := w✝ }
Theorem: ℤα.my_one_mul
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul one { z := z✝, w := w✝ } = { z := z✝, w := w✝ }
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 : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } one = { z := z✝, w := w✝ }
Theorem: ℤα.my_mul_one
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } one = { z := z✝, w := w✝ }
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 : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } (add b c) = add (mul { z := z✝, w := w✝ } b) (mul { z := z✝, w := w✝ } c)
Theorem: ℤα.my_left_distrib
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } (add b c) = add (mul { z := z✝, w := w✝ } b) (mul { z := z✝, w := w✝ } c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝¹, w := w✝¹ } (add { z := z✝, w := w✝ } c) =
    add (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) (mul { z := z✝¹, w := w✝¹ } c)
Theorem: ℤα.my_left_distrib
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝¹, w := w✝¹ } (add { z := z✝, w := w✝ } c) =
    add (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) (mul { z := z✝¹, w := w✝¹ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝², w := w✝² } (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) =
    add (mul { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) (mul { z := z✝², w := w✝² } { z := z✝, w := w✝ })
Theorem: ℤα.my_left_distrib
Proof state before:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝², w := w✝² } (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) =
    add (mul { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) (mul { z := z✝², w := w✝² } { z := z✝, w := w✝ })
Tactic:
simp only [mul, add]
Proof state after:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := z✝² * (z✝¹ + z✝) - 2 * w✝² * (w✝¹ + w✝), w := z✝² * (w✝¹ + w✝) + w✝² * (z✝¹ + z✝) + w✝² * (w✝¹ + w✝) } =
    { z := z✝² * z✝¹ - 2 * w✝² * w✝¹ + (z✝² * z✝ - 2 * w✝² * w✝),
      w := z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹ + (z✝² * w✝ + w✝² * z✝ + w✝² * w✝) }
Theorem: ℤα.my_left_distrib
Proof state before:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := z✝² * (z✝¹ + z✝) - 2 * w✝² * (w✝¹ + w✝), w := z✝² * (w✝¹ + w✝) + w✝² * (z✝¹ + z✝) + w✝² * (w✝¹ + w✝) } =
    { z := z✝² * z✝¹ - 2 * w✝² * w✝¹ + (z✝² * z✝ - 2 * w✝² * w✝),
      w := z✝² * w✝¹ + w✝² * z✝¹ + w✝² * w✝¹ + (z✝² * w✝ + w✝² * z✝ + w✝² * w✝) }
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 : ℤα
z✝ w✝ : ℤ
⊢ mul (add { z := z✝, w := w✝ } b) c = add (mul { z := z✝, w := w✝ } c) (mul b c)
Theorem: ℤα.my_right_distrib
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul (add { z := z✝, w := w✝ } b) c = add (mul { z := z✝, w := w✝ } c) (mul b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) c =
    add (mul { z := z✝¹, w := w✝¹ } c) (mul { z := z✝, w := w✝ } c)
Theorem: ℤα.my_right_distrib
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (add { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ }) c =
    add (mul { z := z✝¹, w := w✝¹ } c) (mul { z := z✝, w := w✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (add { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) { z := z✝, w := w✝ } =
    add (mul { z := z✝², w := w✝² } { z := z✝, w := w✝ }) (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ })
Theorem: ℤα.my_right_distrib
Proof state before:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul (add { z := z✝², w := w✝² } { z := z✝¹, w := w✝¹ }) { z := z✝, w := w✝ } =
    add (mul { z := z✝², w := w✝² } { z := z✝, w := w✝ }) (mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ })
Tactic:
simp only [mul, add]
Proof state after:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := (z✝² + z✝¹) * z✝ - 2 * (w✝² + w✝¹) * w✝, w := (z✝² + z✝¹) * w✝ + (w✝² + w✝¹) * z✝ + (w✝² + w✝¹) * w✝ } =
    { z := z✝² * z✝ - 2 * w✝² * w✝ + (z✝¹ * z✝ - 2 * w✝¹ * w✝),
      w := z✝² * w✝ + w✝² * z✝ + w✝² * w✝ + (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) }
Theorem: ℤα.my_right_distrib
Proof state before:
case mk.mk.mk
z✝² w✝² z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := (z✝² + z✝¹) * z✝ - 2 * (w✝² + w✝¹) * w✝, w := (z✝² + z✝¹) * w✝ + (w✝² + w✝¹) * z✝ + (w✝² + w✝¹) * w✝ } =
    { z := z✝² * z✝ - 2 * w✝² * w✝ + (z✝¹ * z✝ - 2 * w✝¹ * w✝),
      w := z✝² * w✝ + w✝² * z✝ + w✝² * w✝ + (z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝) }
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 : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } b = mul b { z := z✝, w := w✝ }
Theorem: ℤα.my_mul_comm
Proof state before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } b = mul b { z := z✝, w := w✝ }
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ } = mul { z := z✝, w := w✝ } { z := z✝¹, w := w✝¹ }
Theorem: ℤα.my_mul_comm
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ mul { z := z✝¹, w := w✝¹ } { z := z✝, w := w✝ } = mul { z := z✝, w := w✝ } { z := z✝¹, w := w✝¹ }
Tactic:
simp only [mul]
Proof state after:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := z✝¹ * z✝ - 2 * w✝¹ * w✝, w := z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝ } =
    { z := z✝ * z✝¹ - 2 * w✝ * w✝¹, w := z✝ * w✝¹ + w✝ * z✝¹ + w✝ * w✝¹ }
Theorem: ℤα.my_mul_comm
Proof state before:
case mk.mk
c : ℤα
z✝¹ w✝¹ z✝ w✝ : ℤ
⊢ { z := z✝¹ * z✝ - 2 * w✝¹ * w✝, w := z✝¹ * w✝ + w✝¹ * z✝ + w✝¹ * w✝ } =
    { z := z✝ * z✝¹ - 2 * w✝ * w✝¹, w := z✝ * w✝¹ + w✝ * z✝¹ + w✝ * w✝¹ }
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 : ℤα
⊢ { z := 0 * a.z, w := 0 * a.w } = zero
Theorem: ℤα.my_zsmul_zero'
Proof state before:
a✝ b c a : ℤα
⊢ { z := 0 * a.z, w := 0 * a.w } = zero
Tactic:
rw [MulZeroClass.zero_mul]
Proof state after:
a✝ b c a : ℤα
⊢ { z := 0, w := 0 * a.w } = zero
Theorem: ℤα.my_zsmul_zero'
Proof state before:
a✝ b c a : ℤα
⊢ { z := 0, w := 0 * a.w } = zero
Tactic:
rw [MulZeroClass.zero_mul]
Proof state after:
a✝ b c a : ℤα
⊢ { z := 0, w := 0 } = zero
Theorem: ℤα.my_zsmul_zero'
Proof state before:
a✝ b c a : ℤα
⊢ { z := 0, w := 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.z, Int.ofNat n.succ * a.w⟩ : ℤα) =
    (⟨a.z + Int.ofNat n * a.z, a.w + Int.ofNat n * a.w⟩ : ℤα)
Proof state after:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ { z := Int.ofNat (Nat.succ n) * a.z, w := Int.ofNat (Nat.succ n) * a.w } =
    { z := a.z + Int.ofNat n * a.z, w := a.w + Int.ofNat n * a.w }
Theorem: ℤα.my_zsmul_succ'
Proof state before:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ { z := Int.ofNat (Nat.succ n) * a.z, w := Int.ofNat (Nat.succ n) * a.w } =
    { z := a.z + Int.ofNat n * a.z, w := a.w + Int.ofNat n * a.w }
Tactic:
norm_num
Proof state after:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.z = a.z + ↑n * a.z ∧ (↑n + 1) * a.w = a.w + ↑n * a.w
Theorem: ℤα.my_zsmul_succ'
Proof state before:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.z = a.z + ↑n * a.z ∧ (↑n + 1) * a.w = a.w + ↑n * a.w
Tactic:
constructor
Proof state after:
case left
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.z = a.z + ↑n * a.z

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

case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.w = a.w + ↑n * a.w
Tactic:
linarith
Proof state after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.w = a.w + ↑n * a.w
Theorem: ℤα.my_zsmul_succ'
Proof state before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.w = a.w + ↑n * a.w
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.z, Int.negSucc n * a.w⟩ : ℤα) =
    (⟨-(Int.ofNat n.succ * a.z), -(Int.ofNat n.succ * a.w)⟩ : ℤα)
Proof state after:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ { z := Int.negSucc n * a.z, w := Int.negSucc n * a.w } =
    { z := -(Int.ofNat (Nat.succ n) * a.z), w := -(Int.ofNat (Nat.succ n) * a.w) }
Theorem: ℤα.my_zsmul_neg'
Proof state before:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ { z := Int.negSucc n * a.z, w := Int.negSucc n * a.w } =
    { z := -(Int.ofNat (Nat.succ n) * a.z), w := -(Int.ofNat (Nat.succ n) * a.w) }
Tactic:
simp
Proof state after:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.z = -((↑n + 1) * a.z) ∧ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Theorem: ℤα.my_zsmul_neg'
Proof state before:
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.z = -((↑n + 1) * a.z) ∧ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Tactic:
constructor
Proof state after:
case left
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.z = -((↑n + 1) * a.z)

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

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

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

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

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

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

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

case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.ofNat_one]
Proof state after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Theorem: ℤα.my_zsmul_neg'
Proof state before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.negSucc_coe]
Proof state after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -↑(n + 1) * a.w = -((↑n + 1) * a.w)
Theorem: ℤα.my_zsmul_neg'
Proof state before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -↑(n + 1) * a.w = -((↑n + 1) * a.w)
Tactic:
rw [Int.neg_mul_eq_neg_mul_symm]
Proof state after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -(↑(n + 1) * a.w) = -((↑n + 1) * a.w)
Theorem: ℤα.my_zsmul_neg'
Proof state before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -(↑(n + 1) * a.w) = -((↑n + 1) * a.w)
Tactic:
rw [Int.ofNat_add]
Proof state after:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -((↑n + ↑1) * a.w) = -((↑n + 1) * a.w)
Theorem: ℤα.my_zsmul_neg'
Proof state before:
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -((↑n + ↑1) * a.w) = -((↑n + 1) * a.w)
Tactic:
rw [Int.ofNat_one]
Proof state after:
no goals
Theorem: ℤα.my_natCast_zero
Proof state before:
a b c : ℤα
⊢ natCast 0 = zero
Tactic:
unfold natCast
Proof state after:
a b c : ℤα
⊢ { z := ↑0, w := 0 } = zero
Theorem: ℤα.my_natCast_zero
Proof state before:
a b c : ℤα
⊢ { z := ↑0, w := 0 } = zero
Tactic:
rw [Int.ofNat_zero]
Proof state after:
a b c : ℤα
⊢ { z := 0, w := 0 } = zero
Theorem: ℤα.my_natCast_zero
Proof state before:
a b c : ℤα
⊢ { z := 0, w := 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⟩ : ℤα) = (⟨Int.ofNat n + 1, 0⟩ : ℤα)
Proof state after:
a b c : ℤα
n : ℕ
⊢ { z := Int.ofNat (n + 1), w := 0 } = { z := Int.ofNat n + 1, w := 0 }
Theorem: ℤα.my_natCast_succ
Proof state before:
a b c : ℤα
n : ℕ
⊢ { z := Int.ofNat (n + 1), w := 0 } = { z := Int.ofNat n + 1, w := 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