internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
⊢ norm k = 1
Tactic:
have l := norm_divides p
Proof state after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
⊢ norm k = 1
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
⊢ norm k = 1
Tactic:
have d : norm 1 = 1 := by ring
Proof state after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
d : norm 1 = 1
⊢ norm k = 1
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
d : norm 1 = 1
⊢ norm k = 1
Tactic:
rw [d] at l
Proof state after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ 1
d : norm 1 = 1
⊢ norm k = 1
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ 1
d : norm 1 = 1
⊢ norm k = 1
Tactic:
refine' Int.eq_one_of_dvd_one _ l
Proof state after:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ 1
d : norm 1 = 1
⊢ 0 ≤ norm k
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ 1
d : norm 1 = 1
⊢ 0 ≤ norm k
Tactic:
exact abs_nonneg _
Proof state after:
no goals
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
⊢ ∃ b, 1 = k * b
Tactic:
tauto
Proof state after:
no goals
Theorem: ℤθ.norm_one_if_unit
Proof state before:
a b c k : ℤθ
h : ∃ b, k * b = 1
p : k ∣ 1
l : norm k ∣ norm 1
⊢ norm 1 = 1
Tactic:
ring
Proof state after:
no goals
Theorem: ℤθ.units_are
Proof state before:
a✝ b c : ℤθ
a : ℤθˣ
⊢ ∃ n, a = unit ^ n ∨ a = -unit ^ n
Tactic:
sorry
Proof state after:
no goals
Theorem: ℤθ.y_mod_three
Proof state before:
a b c : ℤθ
y s : ℤ
h : y % 3 = s
⊢ ∃ k, y = 3 * k + s
Tactic:
have q := Int.dvd_sub_of_emod_eq h
Proof state after:
a b c : ℤθ
y s : ℤ
h : y % 3 = s
q : 3 ∣ y - s
⊢ ∃ k, y = 3 * k + s
Theorem: ℤθ.y_mod_three
Proof state before:
a b c : ℤθ
y s : ℤ
h : y % 3 = s
q : 3 ∣ y - s
⊢ ∃ k, y = 3 * k + s
Tactic:
cases' q with l lh
Proof state after:
case intro
a b c : ℤθ
y s : ℤ
h : y % 3 = s
l : ℤ
lh : y - s = 3 * l
⊢ ∃ k, y = 3 * k + s
Theorem: ℤθ.y_mod_three
Proof state before:
case intro
a b c : ℤθ
y s : ℤ
h : y % 3 = s
l : ℤ
lh : y - s = 3 * l
⊢ ∃ k, y = 3 * k + s
Tactic:
use l
Proof state after:
case h
a b c : ℤθ
y s : ℤ
h : y % 3 = s
l : ℤ
lh : y - s = 3 * l
⊢ y = 3 * l + s
Theorem: ℤθ.y_mod_three
Proof state before:
case h
a b c : ℤθ
y s : ℤ
h : y % 3 = s
l : ℤ
lh : y - s = 3 * l
⊢ y = 3 * l + s
Tactic:
exact eq_add_of_sub_eq lh
Proof state after:
no goals
Theorem: ℤθ.unit_sq
Proof state before:
a b c : ℤθ
⊢ ↑(unit ^ 2) = { f := -5, g := -14, h := -4 }
Tactic:
rw [pow_two]
Proof state after:
a b c : ℤθ
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }
Theorem: ℤθ.unit_sq
Proof state before:
a b c : ℤθ
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }
Tactic:
have h1 : ((unit * unit : ℤθˣ) : ℤθ) = ((unit : ℤθˣ) : ℤθ) * ((unit : ℤθˣ) : ℤθ) := by rfl
Proof state after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }
Theorem: ℤθ.unit_sq
Proof state before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }
Tactic:
rw [h1]
Proof state after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑unit * ↑unit = { f := -5, g := -14, h := -4 }
Theorem: ℤθ.unit_sq
Proof state before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑unit * ↑unit = { f := -5, g := -14, h := -4 }
Tactic:
rw [unit_l]
Proof state after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 } = { f := -5, g := -14, h := -4 }
Theorem: ℤθ.unit_sq
Proof state before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 } = { f := -5, g := -14, h := -4 }
Tactic:
rw [hMul_mule_3]
Proof state after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ {
      f :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.f +
              6 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            2 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          2 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g,
      g :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.g +
                { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.f +
              16 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            6 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          6 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g,
      h :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.h +
                  { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.f +
                { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.g +
              3 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            3 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          3 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g } =
    { f := -5, g := -14, h := -4 }
Theorem: ℤθ.unit_sq
Proof state before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ {
      f :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.f +
              6 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            2 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          2 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g,
      g :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.g +
                { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.f +
              16 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            6 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          6 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g,
      h :=
        { f := -1, g := -3, h := -1 }.f * { f := -1, g := -3, h := -1 }.h +
                  { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.f +
                { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.g +
              3 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.h -
            3 * { f := -1, g := -3, h := -1 }.g * { f := -1, g := -3, h := -1 }.h -
          3 * { f := -1, g := -3, h := -1 }.h * { f := -1, g := -3, h := -1 }.g } =
    { f := -5, g := -14, h := -4 }
Tactic:
dsimp
Proof state after:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1 * -1 + 6 * -1 * -1 - 2 * -3 * -1 - 2 * -1 * -3,
      g := -1 * -3 + -3 * -1 + 16 * -1 * -1 - 6 * -3 * -1 - 6 * -1 * -3,
      h := -1 * -1 + -1 * -1 + -3 * -3 + 3 * -1 * -1 - 3 * -3 * -1 - 3 * -1 * -3 } =
    { f := -5, g := -14, h := -4 }
Theorem: ℤθ.unit_sq
Proof state before:
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1 * -1 + 6 * -1 * -1 - 2 * -3 * -1 - 2 * -1 * -3,
      g := -1 * -3 + -3 * -1 + 16 * -1 * -1 - 6 * -3 * -1 - 6 * -1 * -3,
      h := -1 * -1 + -1 * -1 + -3 * -3 + 3 * -1 * -1 - 3 * -3 * -1 - 3 * -1 * -3 } =
    { f := -5, g := -14, h := -4 }
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_sq
Proof state before:
a b c : ℤθ
⊢ ↑(unit * unit) = ↑unit * ↑unit
Tactic:
rfl
Proof state after:
no goals
Theorem: ℤθ.unit_cubed
Proof state before:
a b c : ℤθ
⊢ ↑unit ^ 3 = { f := -23, g := -63, h := -15 }
Tactic:
rw [unit_l, pow_three, hMul_mule_3]
Proof state after:
a b c : ℤθ
⊢ {
      f :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
              6 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            2 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          2 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g,
      g :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g +
                { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
              16 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            6 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          6 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g,
      h :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h +
                  { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
                { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g +
              3 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            3 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          3 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g } =
    { f := -23, g := -63, h := -15 }
Theorem: ℤθ.unit_cubed
Proof state before:
a b c : ℤθ
⊢ {
      f :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
              6 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            2 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          2 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g,
      g :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g +
                { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
              16 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            6 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          6 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g,
      h :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h +
                  { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
                { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g +
              3 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            3 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          3 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g } =
    { f := -23, g := -63, h := -15 }
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_inv_cubed
Proof state before:
a b c : ℤθ
⊢ ↑(unit ^ (-3)) = { f := 10591, g := 5553, h := 2139 }
Tactic:
norm_cast
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero
Proof state before:
a b c : ℤθ
⊢ (↑(unit ^ (3 * 0))).f % 3 = 1 ∧ (↑(unit ^ (3 * 0))).g % 3 = 0 ∧ (↑(unit ^ (3 * 0))).h % 3 = 0
Tactic:
norm_cast
Proof state after:
no goals
Theorem: ℤθ.unit_pow_one
Proof state before:
a b c : ℤθ
⊢ (↑(unit ^ 1)).f % 3 = 2 ∧ (↑(unit ^ 1)).g % 3 = 0 ∧ (↑(unit ^ 1)).h % 3 = 2
Tactic:
norm_cast
Proof state after:
no goals
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b c : ℤθ
⊢ ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
Tactic:
intro k
Proof state after:
a b c : ℤθ
k : ℕ
⊢ ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
a b c : ℤθ
k : ℕ
⊢ ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
Tactic:
constructor
Proof state after:
case left
a b c : ℤθ
k : ℕ
⊢ (↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0

case right
a b c : ℤθ
k : ℕ
⊢ (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left
a b c : ℤθ
k : ℕ
⊢ (↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0
Tactic:
induction' k with b hb
Proof state after:
case left.zero
a b c : ℤθ
⊢ (↑(unit ^ (3 * ↑Nat.zero))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑Nat.zero))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑Nat.zero))).h % 3 = 0

case left.succ
a b✝ c : ℤθ
b : ℕ
hb : (↑(unit ^ (3 * ↑b))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * ↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Nat.succ b)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ
a b✝ c : ℤθ
b : ℕ
hb : (↑(unit ^ (3 * ↑b))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * ↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Nat.succ b)))).h % 3 = 0
Tactic:
cases' hb with h1 h23
Proof state after:
case left.succ.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h23 : (↑(unit ^ (3 * ↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * ↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Nat.succ b)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h23 : (↑(unit ^ (3 * ↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * ↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Nat.succ b)))).h % 3 = 0
Tactic:
cases' h23 with h2 h3
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * ↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Nat.succ b)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * ↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Nat.succ b)))).h % 3 = 0
Tactic:
have p : b.succ = b + 1 := by rfl
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ (↑(unit ^ (3 * ↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Nat.succ b)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ (↑(unit ^ (3 * ↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Nat.succ b)))).h % 3 = 0
Tactic:
rw [p]
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ (↑(unit ^ (3 * ↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ (↑(unit ^ (3 * ↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(b + 1)))).h % 3 = 0
Tactic:
norm_cast
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have w : (unit ^ (3 * (b + 1)) : ℤθ) = (unit ^ (3 * b) : ℤθ) * ((unit:ℤθ) ^ 3 : ℤθ) :=
by
  norm_cast
  rw [mul_add, mul_one, pow_add]
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have t1 : ((unit ) ^ (3 * b):ℤθ).f % 3 = 1 :=
  by
    norm_cast
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have t2 : ((unit) ^ (3 * b) : ℤθ).g % 3 = 0 :=
  by
    norm_cast
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have t3 : ((unit ) ^ (3 * b): ℤθ).h % 3 = 0 :=
  by
    norm_cast
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have r1 := y_mod_three (unit ^ (3 * b) : ℤθ).f 1 t1
Proof state after:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
r1 : ∃ k, (↑(unit ^ (3 * b))).f = 3 * k + 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
r1 : ∃ k, (↑(unit ^ (3 * b))).f = 3 * k + 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
cases' r1 with c1 hc1
Proof state after:
case left.succ.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
c1 : ℤ
hc1 : (↑(unit ^ (3 * b))).f = 3 * c1 + 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Theorem: ℤθ.unit_pow_zero_mod_three
Proof state before:
case left.succ.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
c1 : ℤ
hc1 : (↑(unit ^ (3 * b))).f = 3 * c1 + 1
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0
Tactic:
have r2 := y_mod_three (unit ^ (3 * b) : ℤθ).g 0 t2
Proof state after:
case left.succ.intro.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * ↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * ↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * ↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * (b + 1))) = ↑(unit ^ (3 * b)) * ↑unit ^ 3
t1 : (↑(unit ^ (3 * b))).f % 3 = 1
t2 : (↑(unit ^ (3 * b))).g % 3 = 0
t3 : (↑(unit ^ (3 * b))).h % 3 = 0
c1 : ℤ
hc1 : (↑(unit ^ (3 * b))).f = 3 * c1 + 1
r2 : ∃ k, (↑(unit ^ (3 * b))).g = 3 * k + 0
⊢ (↑(unit ^ (3 * (b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * (b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * (b + 1)))).h % 3 = 0