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

State before:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
have q := hMul_three_pow_dvd n h
State after:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
q : ∃ a, 3 ^ a ∣ 3 * n ∧ ¬3 ^ (a + 1) ∣ 3 * n
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
q : ∃ a, 3 ^ a ∣ 3 * n ∧ ¬3 ^ (a + 1) ∣ 3 * n
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
cases' q with k hk
State after:
case intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
cases' hk with h1 h2
State after:
case intro.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
have ss : k = 0 ∨ 0 < k := Nat.eq_zero_or_pos k
State after:
case intro.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
ss : k = 0 ∨ 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
ss : k = 0 ∨ 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
cases' ss with s1 s2
State after:
case intro.intro.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s1 : k = 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s1 : k = 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
rw [s1, zero_add, pow_one] at h2
State after:
case intro.intro.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
exfalso
State after:
case intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
⊢ False

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
⊢ False

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
have p : 3 ∣ 3 * n := by use n
State after:
case intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ False

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ False

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
have contra : 3 ∣ 3 * n ∧ ¬3 ∣ 3 * n := by constructor; exact p; exact h2
State after:
case intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
contra : 3 ∣ 3 * n ∧ ¬3 ∣ 3 * n
⊢ False

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
contra : 3 ∣ 3 * n ∧ ¬3 ∣ 3 * n
⊢ False

case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
simp at contra
State after:
case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 0 < k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
change 1 ≤ k at s2
State after:
case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
change ∃ l : ℕ, 3 * n = 3 ^ k * l at h1
State after:
case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
h1 : ∃ l, 3 * n = 3 ^ k * l
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
h1 : ∃ l, 3 * n = 3 ^ k * l
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
cases' h1 with j hj
State after:
case intro.intro.inr.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
have p := rep_mod_three j
State after:
case intro.intro.inr.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
p : ∃ a, j = 3 * a ∨ j = 3 * a + 1 ∨ j = 3 * a + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
p : ∃ a, j = 3 * a ∨ j = 3 * a + 1 ∨ j = 3 * a + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
cases' p with r hr
State after:
case intro.intro.inr.intro.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
hr : j = 3 * r ∨ j = 3 * r + 1 ∨ j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr.intro.intro
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
hr : j = 3 * r ∨ j = 3 * r + 1 ∨ j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
cases' hr with t1 t23
State after:
case intro.intro.inr.intro.intro.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t1 : j = 3 * r
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

case intro.intro.inr.intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t23 : j = 3 * r + 1 ∨ j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr.intro.intro.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t23 : j = 3 * r + 1 ∨ j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
cases' t23 with t2 t3
State after:
case intro.intro.inr.intro.intro.inr.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t2 : j = 3 * r + 1
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

case intro.intro.inr.intro.intro.inr.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t3 : j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr.intro.intro.inr.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t3 : j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
rw [t3] at hj
State after:
case intro.intro.inr.intro.intro.inr.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr.intro.intro.inr.inr
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
use k
State after:
case h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ ∃ b, 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * b + 1) ∨ 3 * ↑n = 3 ^ k * (3 * b + 2))

State before:
case h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ ∃ b, 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * b + 1) ∨ 3 * ↑n = 3 ^ k * (3 * b + 2))
Tactic:
use r
State after:
case h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2))

State before:
case h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2))
Tactic:
constructor
State after:
case h.left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 1 ≤ k

case h.right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)

State before:
case h.left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 1 ≤ k

case h.right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
exact s2
State after:
case h.right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)

State before:
case h.right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
right
State after:
case h.right.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)

State before:
case h.right.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
exact_mod_cast hj
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
⊢ 3 ∣ 3 * n
Tactic:
use n
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ 3 ∣ 3 * n ∧ ¬3 ∣ 3 * n
Tactic:
constructor
State after:
case left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ 3 ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ ¬3 ∣ 3 * n

State before:
case left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ 3 ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ ¬3 ∣ 3 * n
Tactic:
exact p
State after:
case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ ¬3 ∣ 3 * n

State before:
case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h1 : 3 ^ k ∣ 3 * n
h2 : ¬3 ∣ 3 * n
s1 : k = 0
p : 3 ∣ 3 * n
⊢ ¬3 ∣ 3 * n
Tactic:
exact h2
State after:
no goals

State before:
case intro.intro.inr.intro.intro.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t1 : j = 3 * r
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
exfalso
State after:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t1 : j = 3 * r
⊢ False

State before:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t1 : j = 3 * r
⊢ False
Tactic:
rw [t1] at hj
State after:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r)
t1 : j = 3 * r
⊢ False

State before:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r)
t1 : j = 3 * r
⊢ False
Tactic:
rw [← mul_assoc] at hj
State after:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * 3 * r
t1 : j = 3 * r
⊢ False

State before:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * 3 * r
t1 : j = 3 * r
⊢ False
Tactic:
nth_rw 3 [← pow_one 3] at hj
State after:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ k * 3 ^ 1 * r
t1 : j = 3 * r
⊢ False

State before:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ k * 3 ^ 1 * r
t1 : j = 3 * r
⊢ False
Tactic:
rw [← pow_add] at hj
State after:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
⊢ False

State before:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
⊢ False
Tactic:
have g : 3 ^ (k + 1) ∣ 3 * n := by use r;
State after:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ False

State before:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ False
Tactic:
have combine : 3 ^ (k + 1) ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n := by constructor; exact g; exact h2
State after:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
combine : 3 ^ (k + 1) ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ False

State before:
case intro.intro.inr.intro.intro.inl.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
combine : 3 ^ (k + 1) ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ False
Tactic:
simp at combine
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
⊢ 3 ^ (k + 1) ∣ 3 * n
Tactic:
use r
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ (k + 1) ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
Tactic:
constructor
State after:
case left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ (k + 1) ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n

State before:
case left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ (k + 1) ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n
Tactic:
exact g
State after:
case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n

State before:
case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n
Tactic:
exact h2
State after:
no goals

State before:
case intro.intro.inr.intro.intro.inr.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j : ℕ
hj : 3 * n = 3 ^ k * j
r : ℕ
t2 : j = 3 * r + 1
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
rw [t2] at hj
State after:
case intro.intro.inr.intro.intro.inr.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))

State before:
case intro.intro.inr.intro.intro.inr.inl
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ ∃ a b, 1 ≤ a ∧ (3 * ↑n = 3 ^ a * (3 * b + 1) ∨ 3 * ↑n = 3 ^ a * (3 * b + 2))
Tactic:
use k
State after:
case h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ ∃ b, 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * b + 1) ∨ 3 * ↑n = 3 ^ k * (3 * b + 2))

State before:
case h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ ∃ b, 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * b + 1) ∨ 3 * ↑n = 3 ^ k * (3 * b + 2))
Tactic:
use r
State after:
case h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2))

State before:
case h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2))
Tactic:
constructor
State after:
case h.left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 1 ≤ k

case h.right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)

State before:
case h.left
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 1 ≤ k

case h.right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
exact s2
State after:
case h.right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)

State before:
case h.right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)
Tactic:
left
State after:
case h.right.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1)

State before:
case h.right.h
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj : 3 * n = 3 ^ k * (3 * r + 1)
t2 : j = 3 * r + 1
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1)
Tactic:
exact_mod_cast hj
State after:
no goals