Theorem: ℤθ.unit_pow_three_pow_1
Proof 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]
Proof 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