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

State before:
a b c : ℤθ
n : ℕ
⊢ ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
Tactic:
induction' n with n ih
State after:
case zero
a b c : ℤθ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * φ

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

State before:
case zero
a b c : ℤθ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * φ

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

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

State before:
case h
a b c : ℤθ
⊢ ↑(unit ^ 3 ^ (Nat.zero + 1)) = 1 + 3 ^ (Nat.zero + 1) * { f := -8, g := -21, h := -5 }

case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Tactic:
rfl
State after:
case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ

State before:
case succ
a b c : ℤθ
n : ℕ
ih : ∃ φ, ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * φ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Tactic:
obtain ⟨ψ, hψ⟩ := ih
State after:
case succ.intro
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ

State before:
case succ.intro
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ∃ φ, ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * φ
Tactic:
use ψ + 3 ^ (n + 1) * ψ ^ 2 + 3 ^ (2 * n + 2) * ψ ^ 3
State after:
case h
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * (ψ + 3 ^ (n + 1) * ψ ^ 2 + 3 ^ (2 * n + 2) * ψ ^ 3)

State before:
case h
a b c : ℤθ
n : ℕ
ψ : ℤθ
hψ : ↑(unit ^ 3 ^ (n + 1)) = 1 + 3 ^ (n + 1) * ψ
⊢ ↑(unit ^ 3 ^ (Nat.succ n + 1)) = 1 + 3 ^ (Nat.succ n + 1) * (ψ + 3 ^ (n + 1) * ψ ^ 2 + 3 ^ (2 * n + 2) * ψ ^ 3)
Tactic:
sorry
State after:
no goals