internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ {
      f :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.f +
              6 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            2 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          2 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g,
      g :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.g +
                { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.f +
              16 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            6 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          6 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g,
      h :=
        { f := -1901, g := -4842, h := -336 }.f * { f := -23, g := -63, h := -15 }.h +
                  { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.f +
                { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.g +
              3 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.h -
            3 * { f := -1901, g := -4842, h := -336 }.g * { f := -23, g := -63, h := -15 }.h -
          3 * { f := -1901, g := -4842, h := -336 }.h * { f := -23, g := -63, h := -15 }.g } =
    { f := -113633, g := -251019, h := 75015 }
Tactic:
dsimp
Proof state after:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ { f := -1901 * -23 + 6 * -336 * -15 - 2 * -4842 * -15 - 2 * -336 * -63,
      g := -1901 * -63 + -4842 * -23 + 16 * -336 * -15 - 6 * -4842 * -15 - 6 * -336 * -63,
      h := -1901 * -15 + -336 * -23 + -4842 * -63 + 3 * -336 * -15 - 3 * -4842 * -15 - 3 * -336 * -63 } =
    { f := -113633, g := -251019, h := 75015 }
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
elem1 : 3 + 3 = 6
⊢ { f := -1901 * -23 + 6 * -336 * -15 - 2 * -4842 * -15 - 2 * -336 * -63,
      g := -1901 * -63 + -4842 * -23 + 16 * -336 * -15 - 6 * -4842 * -15 - 6 * -336 * -63,
      h := -1901 * -15 + -336 * -23 + -4842 * -63 + 3 * -336 * -15 - 3 * -4842 * -15 - 3 * -336 * -63 } =
    { f := -113633, g := -251019, h := 75015 }
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
⊢ 9 = 3 + 3 + 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_nine
Proof state before:
a b c : ℤθ
elem : 9 = 3 + 3 + 3
⊢ 3 + 3 = 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
a b c : ℤθ
n : ℕ
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ (n + 1))).f = 1 + 3 ^ (n + 1) + 3 ^ (n + 2) * a ∧
      (↑(unit ^ 3 ^ (n + 1))).g = 3 ^ (n + 2) * b ∧ (↑(unit ^ 3 ^ (n + 1))).h = 3 ^ (n + 1) + 3 ^ (n + 2) * c
Tactic:
induction' n with k hk
Proof state after:
case zero
a b c : ℤθ
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ (Nat.zero + 1))).f = 1 + 3 ^ (Nat.zero + 1) + 3 ^ (Nat.zero + 2) * a ∧
      (↑(unit ^ 3 ^ (Nat.zero + 1))).g = 3 ^ (Nat.zero + 2) * b ∧
        (↑(unit ^ 3 ^ (Nat.zero + 1))).h = 3 ^ (Nat.zero + 1) + 3 ^ (Nat.zero + 2) * c

case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + 2) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + 2) * b ∧ (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + 2) * c
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + 2) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + 2) * b ∧ (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + 2) * c
⊢ ∃ 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:
have l : k + 1 = k.succ := by rfl
Proof state after:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + 2) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + 2) * b ∧ (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + 2) * c
l : k + 1 = 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + 2) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + 2) * b ∧ (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + 2) * c
l : k + 1 = 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:
rw [← one_add_one_eq_two] at hk
Proof state after:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + (1 + 1)) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + (1 + 1)) * b ∧
        (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + (1 + 1)) * c
l : k + 1 = 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + (1 + 1)) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + (1 + 1)) * b ∧
        (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + (1 + 1)) * c
l : k + 1 = 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:
rw [← add_assoc] at hk
Proof state after:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + 1 + 1) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + 1 + 1) * b ∧ (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + 1 + 1) * c
l : k + 1 = 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ (k + 1))).f = 1 + 3 ^ (k + 1) + 3 ^ (k + 1 + 1) * a ∧
      (↑(unit ^ 3 ^ (k + 1))).g = 3 ^ (k + 1 + 1) * b ∧ (↑(unit ^ 3 ^ (k + 1))).h = 3 ^ (k + 1) + 3 ^ (k + 1 + 1) * c
l : k + 1 = 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:
rw [l] at hk
Proof state after:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * a ∧
      (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * b ∧
        (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * c
l : k + 1 = 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ
a b c : ℤθ
k : ℕ
hk :
  ∃ a b c,
    (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * a ∧
      (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * b ∧
        (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * c
l : k + 1 = 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:
cases' hk with p hp
Proof state after:
case succ.intro
a b c : ℤθ
k : ℕ
l : k + 1 = Nat.succ k
p : ℤ
hp :
  ∃ b c,
    (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p ∧
      (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * b ∧
        (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * c
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro
a b c : ℤθ
k : ℕ
l : k + 1 = Nat.succ k
p : ℤ
hp :
  ∃ b c,
    (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p ∧
      (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * b ∧
        (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * c
⊢ ∃ 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:
cases' hp with q hq
Proof state after:
case succ.intro.intro
a b c : ℤθ
k : ℕ
l : k + 1 = Nat.succ k
p q : ℤ
hq :
  ∃ c,
    (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p ∧
      (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q ∧
        (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * c
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro.intro
a b c : ℤθ
k : ℕ
l : k + 1 = Nat.succ k
p q : ℤ
hq :
  ∃ c,
    (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p ∧
      (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q ∧
        (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * c
⊢ ∃ 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:
cases' hq with r hr
Proof state after:
case succ.intro.intro.intro
a b c : ℤθ
k : ℕ
l : k + 1 = Nat.succ k
p q r : ℤ
hr :
  (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p ∧
    (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q ∧
      (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro.intro.intro
a b c : ℤθ
k : ℕ
l : k + 1 = Nat.succ k
p q r : ℤ
hr :
  (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p ∧
    (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q ∧
      (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r
⊢ ∃ 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:
cases' hr with h1 h23
Proof state after:
case succ.intro.intro.intro.intro
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
h23 :
  (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q ∧
    (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro.intro.intro.intro
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
h23 :
  (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q ∧
    (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r
⊢ ∃ 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:
cases' h23 with h2 h3
Proof state after:
case succ.intro.intro.intro.intro.intro
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
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro.intro.intro.intro.intro
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
⊢ ∃ 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:
have t :
  (unit ^ 3 ^ k.succ : ℤθ) =
    ⟨1 + 3 ^ k.succ + 3 ^ (k.succ + 1) * p, 3 ^ (k.succ + 1) * q,
      3 ^ k.succ + 3 ^ (k.succ + 1) * r⟩ :=
  by
  ext <;> dsimp
  exact_mod_cast h1; exact_mod_cast h2; exact_mod_cast h3
Proof state after:
case succ.intro.intro.intro.intro.intro
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 }
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro.intro.intro.intro.intro
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 }
⊢ ∃ 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:
have g := le_or_gt k.succ 1
Proof state after:
case succ.intro.intro.intro.intro.intro
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 }
g : Nat.succ k ≤ 1 ∨ Nat.succ k > 1
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro.intro.intro.intro.intro
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 }
g : Nat.succ k ≤ 1 ∨ Nat.succ k > 1
⊢ ∃ 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:
have lower : 1 ≤ k.succ := by rw [← l]; simp
Proof state after:
case succ.intro.intro.intro.intro.intro
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 }
g : Nat.succ k ≤ 1 ∨ Nat.succ k > 1
lower : 1 ≤ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case succ.intro.intro.intro.intro.intro
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 }
g : Nat.succ k ≤ 1 ∨ Nat.succ k > 1
lower : 1 ≤ 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:
cases' g with g1 g2
Proof state after:
case succ.intro.intro.intro.intro.intro.inl
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 }
lower : 1 ≤ Nat.succ k
g1 : Nat.succ k ≤ 1
⊢ ∃ 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

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 }
lower : 1 ≤ Nat.succ k
g2 : Nat.succ k > 1
⊢ ∃ 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
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case zero
a b c : ℤθ
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ (Nat.zero + 1))).f = 1 + 3 ^ (Nat.zero + 1) + 3 ^ (Nat.zero + 2) * a ∧
      (↑(unit ^ 3 ^ (Nat.zero + 1))).g = 3 ^ (Nat.zero + 2) * b ∧
        (↑(unit ^ 3 ^ (Nat.zero + 1))).h = 3 ^ (Nat.zero + 1) + 3 ^ (Nat.zero + 2) * c
Tactic:
rw [Nat.zero_add]
Proof state after:
case zero
a b c : ℤθ
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ 1)).f = 1 + 3 ^ 1 + 3 ^ (Nat.zero + 2) * a ∧
      (↑(unit ^ 3 ^ 1)).g = 3 ^ (Nat.zero + 2) * b ∧ (↑(unit ^ 3 ^ 1)).h = 3 ^ 1 + 3 ^ (Nat.zero + 2) * c
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case zero
a b c : ℤθ
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ 1)).f = 1 + 3 ^ 1 + 3 ^ (Nat.zero + 2) * a ∧
      (↑(unit ^ 3 ^ 1)).g = 3 ^ (Nat.zero + 2) * b ∧ (↑(unit ^ 3 ^ 1)).h = 3 ^ 1 + 3 ^ (Nat.zero + 2) * c
Tactic:
rw [Nat.zero_add]
Proof state after:
case zero
a b c : ℤθ
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ 1)).f = 1 + 3 ^ 1 + 3 ^ 2 * a ∧
      (↑(unit ^ 3 ^ 1)).g = 3 ^ 2 * b ∧ (↑(unit ^ 3 ^ 1)).h = 3 ^ 1 + 3 ^ 2 * c
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case zero
a b c : ℤθ
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ 1)).f = 1 + 3 ^ 1 + 3 ^ 2 * a ∧
      (↑(unit ^ 3 ^ 1)).g = 3 ^ 2 * b ∧ (↑(unit ^ 3 ^ 1)).h = 3 ^ 1 + 3 ^ 2 * c
Tactic:
rw [pow_one]
Proof state after:
case zero
a b c : ℤθ
⊢ ∃ a b c, (↑(unit ^ 3)).f = 1 + 3 ^ 1 + 3 ^ 2 * a ∧ (↑(unit ^ 3)).g = 3 ^ 2 * b ∧ (↑(unit ^ 3)).h = 3 ^ 1 + 3 ^ 2 * c
Theorem: ℤθ.unit_pow_three_pow_1
Proof state before:
case zero
a b c : ℤθ
⊢ ∃ a b c, (↑(unit ^ 3)).f = 1 + 3 ^ 1 + 3 ^ 2 * a ∧ (↑(unit ^ 3)).g = 3 ^ 2 * b ∧ (↑(unit ^ 3)).h = 3 ^ 1 + 3 ^ 2 * c
Tactic:
rw [pow_one]
Proof state after:
case zero
a b c : ℤθ
⊢ ∃ a b c, (↑(unit ^ 3)).f = 1 + 3 + 3 ^ 2 * a ∧ (↑(unit ^ 3)).g = 3 ^ 2 * b ∧ (↑(unit ^ 3)).h = 3 + 3 ^ 2 * c