Theorem: ℤθ.unit_pow_three_pow_1 (Mordell4/CubicRing.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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]
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

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]
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

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]
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

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]
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

State before:
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
Tactic:
change
  ∃ a b c : ℤ,
    ((unit : ℤθ) ^ 3).f = 1 + 3 + 3 ^ 2 * a ∧
      ((unit : ℤθ) ^ 3).g = 3 ^ 2 * b ∧ ((unit : ℤθ) ^ 3).h = 3 + 3 ^ 2 * c
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

State before:
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
Tactic:
rw [unit_cubed]
State after:
case zero
a b c : ℤθ
⊢ ∃ a b c,
    { f := -23, g := -63, h := -15 }.f = 1 + 3 + 3 ^ 2 * a ∧
      { f := -23, g := -63, h := -15 }.g = 3 ^ 2 * b ∧ { f := -23, g := -63, h := -15 }.h = 3 + 3 ^ 2 * c

State before:
case zero
a b c : ℤθ
⊢ ∃ a b c,
    { f := -23, g := -63, h := -15 }.f = 1 + 3 + 3 ^ 2 * a ∧
      { f := -23, g := -63, h := -15 }.g = 3 ^ 2 * b ∧ { f := -23, g := -63, h := -15 }.h = 3 + 3 ^ 2 * c
Tactic:
dsimp
State after:
case zero
a b c : ℤθ
⊢ ∃ a b c, -23 = 1 + 3 + 3 ^ 2 * a ∧ -63 = 3 ^ 2 * b ∧ -15 = 3 + 3 ^ 2 * c

State before:
case zero
a b c : ℤθ
⊢ ∃ a b c, -23 = 1 + 3 + 3 ^ 2 * a ∧ -63 = 3 ^ 2 * b ∧ -15 = 3 + 3 ^ 2 * c
Tactic:
use-3
State after:
case h
a b c : ℤθ
⊢ ∃ b c, -23 = 1 + 3 + 3 ^ 2 * -3 ∧ -63 = 3 ^ 2 * b ∧ -15 = 3 + 3 ^ 2 * c

State before:
case h
a b c : ℤθ
⊢ ∃ b c, -23 = 1 + 3 + 3 ^ 2 * -3 ∧ -63 = 3 ^ 2 * b ∧ -15 = 3 + 3 ^ 2 * c
Tactic:
use-7
State after:
case h
a b c : ℤθ
⊢ ∃ c, -23 = 1 + 3 + 3 ^ 2 * -3 ∧ -63 = 3 ^ 2 * -7 ∧ -15 = 3 + 3 ^ 2 * c

State before:
case h
a b c : ℤθ
⊢ ∃ c, -23 = 1 + 3 + 3 ^ 2 * -3 ∧ -63 = 3 ^ 2 * -7 ∧ -15 = 3 + 3 ^ 2 * c
Tactic:
use-2
State after:
case h
a b c : ℤθ
⊢ -23 = 1 + 3 + 3 ^ 2 * -3 ∧ -63 = 3 ^ 2 * -7 ∧ -15 = 3 + 3 ^ 2 * -2

State before:
case h
a b c : ℤθ
⊢ -23 = 1 + 3 + 3 ^ 2 * -3 ∧ -63 = 3 ^ 2 * -7 ∧ -15 = 3 + 3 ^ 2 * -2
Tactic:
norm_num
State after:
no goals

State before:
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
⊢ k + 1 = Nat.succ k
Tactic:
rfl
State after:
no goals

State before:
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
⊢ ↑(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 }
Tactic:
ext <;> dsimp
State after:
case f
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p

case g
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q

case h
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r

State before:
case f
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).f = 1 + 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * p

case g
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q

case h
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r
Tactic:
exact_mod_cast h1
State after:
case g
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q

case h
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r

State before:
case g
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).g = 3 ^ (Nat.succ k + 1) * q

case h
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r
Tactic:
exact_mod_cast h2
State after:
case h
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r

State before:
case h
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
⊢ (↑(unit ^ 3 ^ Nat.succ k)).h = 3 ^ Nat.succ k + 3 ^ (Nat.succ k + 1) * r
Tactic:
exact_mod_cast h3
State after:
no goals

State before:
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
⊢ 1 ≤ Nat.succ k
Tactic:
rw [← l]
State after:
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
⊢ 1 ≤ k + 1

State before:
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
⊢ 1 ≤ k + 1
Tactic:
simp
State after:
no goals

State before:
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
Tactic:
have upper : k.succ < 2 :=
by
  rw [← Nat.succ_le_succ_iff] at g1
  exact g1
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
upper : Nat.succ k < 2
⊢ ∃ 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

State before:
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
upper : Nat.succ k < 2
⊢ ∃ 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 elem := eq_or_lt_of_le g1
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
upper : Nat.succ k < 2
elem : 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

State before:
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
upper : Nat.succ k < 2
elem : 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:
cases' elem with f1 f2
State after:
case succ.intro.intro.intro.intro.intro.inl.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
upper : Nat.succ k < 2
f1 : 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.inl.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
g1 : Nat.succ k ≤ 1
upper : Nat.succ k < 2
f2 : 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

State before:
case succ.intro.intro.intro.intro.intro.inl.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
upper : Nat.succ k < 2
f1 : 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.inl.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
g1 : Nat.succ k ≤ 1
upper : Nat.succ k < 2
f2 : 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:
rw [f1]
State after:
case succ.intro.intro.intro.intro.intro.inl.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
upper : Nat.succ k < 2
f1 : Nat.succ k = 1
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ (1 + 1))).f = 1 + 3 ^ (1 + 1) + 3 ^ (1 + 2) * a ∧
      (↑(unit ^ 3 ^ (1 + 1))).g = 3 ^ (1 + 2) * b ∧ (↑(unit ^ 3 ^ (1 + 1))).h = 3 ^ (1 + 1) + 3 ^ (1 + 2) * c

case succ.intro.intro.intro.intro.intro.inl.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
g1 : Nat.succ k ≤ 1
upper : Nat.succ k < 2
f2 : 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

State before:
case succ.intro.intro.intro.intro.intro.inl.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
upper : Nat.succ k < 2
f1 : Nat.succ k = 1
⊢ ∃ a b c,
    (↑(unit ^ 3 ^ (1 + 1))).f = 1 + 3 ^ (1 + 1) + 3 ^ (1 + 2) * a ∧
      (↑(unit ^ 3 ^ (1 + 1))).g = 3 ^ (1 + 2) * b ∧ (↑(unit ^ 3 ^ (1 + 1))).h = 3 ^ (1 + 1) + 3 ^ (1 + 2) * c

case succ.intro.intro.intro.intro.intro.inl.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
g1 : Nat.succ k ≤ 1
upper : Nat.succ k < 2
f2 : 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:
norm_num
State after:
case succ.intro.intro.intro.intro.intro.inl.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
upper : Nat.succ k < 2
f1 : Nat.succ k = 1
⊢ (∃ x, ((-1 - 3 * θ - θ ^ 2) ^ 9).f = 10 + 27 * x) ∧
    (∃ x, ((-1 - 3 * θ - θ ^ 2) ^ 9).g = 27 * x) ∧ ∃ x, ((-1 - 3 * θ - θ ^ 2) ^ 9).h = 9 + 27 * x

case succ.intro.intro.intro.intro.intro.inl.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
g1 : Nat.succ k ≤ 1
upper : Nat.succ k < 2
f2 : 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

State before:
case succ.intro.intro.intro.intro.intro.inl.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
upper : Nat.succ k < 2
f1 : Nat.succ k = 1
⊢ (∃ x, ((-1 - 3 * θ - θ ^ 2) ^ 9).f = 10 + 27 * x) ∧
    (∃ x, ((-1 - 3 * θ - θ ^ 2) ^ 9).g = 27 * x) ∧ ∃ x, ((-1 - 3 * θ - θ ^ 2) ^ 9).h = 9 + 27 * x

case succ.intro.intro.intro.intro.intro.inl.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
g1 : Nat.succ k ≤ 1
upper : Nat.succ k < 2
f2 : 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:
sorry
State after:
case succ.intro.intro.intro.intro.intro.inl.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
g1 : Nat.succ k ≤ 1
upper : Nat.succ k < 2
f2 : 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

State before:
case succ.intro.intro.intro.intro.intro.inl.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
g1 : Nat.succ k ≤ 1
upper : Nat.succ k < 2
f2 : 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:
contradiction
State after:
no goals

State before:
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
⊢ Nat.succ k < 2
Tactic:
rw [← Nat.succ_le_succ_iff] at g1
State after:
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 (Nat.succ k) ≤ Nat.succ 1
⊢ Nat.succ k < 2

State before:
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 (Nat.succ k) ≤ Nat.succ 1
⊢ Nat.succ k < 2
Tactic:
exact g1
State after:
no goals

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 }
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
Tactic:
change 2 ≤ k.succ  at g2
State after:
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 : 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

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 }
lower : 1 ≤ Nat.succ k
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:
clear lower
State after:
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

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
State after:
no goals