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

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
⊢ ∃ a, 3 ^ a ∣ 3 * n ∧ ¬3 ^ (a + 1) ∣ 3 * n
Tactic:
by_contra h
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ¬∃ a, 3 ^ a ∣ 3 * n ∧ ¬3 ^ (a + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ¬∃ a, 3 ^ a ∣ 3 * n ∧ ¬3 ^ (a + 1) ∣ 3 * n
⊢ False
Tactic:
push_neg at h
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
⊢ False
Tactic:
have r : ∀ x : ℕ, ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n :=
  by
  intro g
  specialize h g
  push_neg at h
  by_cases h2: 3 ^ g ∣ 3*n
  right; exact h h2
  left; exact h2
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
⊢ False
Tactic:
clear h
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
⊢ False
Tactic:
clear r
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : ∀ (f : ℕ), 3 ^ f ∣ 3 * n
⊢ False
Tactic:
specialize t (n + 1)
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
⊢ False
Tactic:
have q : ∀ f : ℕ, 3 ^ (f + 1) > 3 * f := by
  intro g
  induction' g with k hk
  norm_num
  change 3 ^ (k + 1 + 1) > 3 * (k + 1)
  have ss : k = 0 ∨ 0 < k := Nat.eq_zero_or_pos k
  cases ss with
  | inl ss =>
  rw [ss]; norm_num
  | inr ss =>
  change 1 ≤ k at ss
  have b : k < 2 * k := by
    change 0 < k at ss
    exact lt_two_mul_self ss
  have q1 : k + 1 < 3 * k :=
    by
    have finall := add_lt_add_of_lt_of_le b ss
    nth_rw 3 [← one_mul k] at finall
    rw [← right_distrib] at finall
    norm_num at finall
    exact finall
  have q2 := lt_trans q1 hk
  rw [pow_succ]
  apply (mul_lt_mul_left zero_lt_three  ).2 q2
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : ∀ (f : ℕ), 3 ^ (f + 1) > 3 * f
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : ∀ (f : ℕ), 3 ^ (f + 1) > 3 * f
⊢ False
Tactic:
specialize q n
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
⊢ False
Tactic:
have r : ¬3 ^ (n + 1) ∣ 3 * n := by
  clear t; by_contra h
  change ∃ l : ℕ, 3 * n = 3 ^ (n + 1) * l at h
  cases' h with p hp
  rw [hp] at q
  have ss : p = 0 ∨ 0 < p := Nat.eq_zero_or_pos p
  cases ss with
  | inl ss =>
  rw [ss] at hp ; norm_num at hp ; rw [hp] at j ; norm_num at j
  | inr ss =>
  simp at q ; rw [q] at ss ; norm_num at ss
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ False
Tactic:
have w : 3 ^ (n + 1) ∣ 3 * n ∧ ¬3 ^ (n + 1) ∣ 3 * n :=
by constructor; exact t; exact r
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
w : 3 ^ (n + 1) ∣ 3 * n ∧ ¬3 ^ (n + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
w : 3 ^ (n + 1) ∣ 3 * n ∧ ¬3 ^ (n + 1) ∣ 3 * n
⊢ False
Tactic:
simp at w
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
⊢ ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
Tactic:
intro g
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
g : ℕ
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
g : ℕ
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n
Tactic:
specialize h g
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n
Tactic:
by_cases h2: 3 ^ g ∣ 3*n
State after:
case pos
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n

case neg
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n

State before:
case pos
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n

case neg
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n
Tactic:
right
State after:
case pos.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : 3 ^ g ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n

case neg
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n

State before:
case pos.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : 3 ^ g ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n

case neg
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n
Tactic:
exact h h2
State after:
case neg
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n

State before:
case neg
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n
Tactic:
left
State after:
case neg.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n

State before:
case neg.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n
Tactic:
exact h2
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
⊢ ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
Tactic:
intro g
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
g : ℕ
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n ∨ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
g : ℕ
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n ∨ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n
Tactic:
specialize r g
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r : ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n ∨ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r : ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n ∨ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n
Tactic:
cases' r with r1 r2
State after:
case inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n ∨ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n

case inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n ∨ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n

State before:
case inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n ∨ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n
Tactic:
right
State after:
case inr.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n

State before:
case inr.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n
Tactic:
constructor
State after:
case inr.h.left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ g ∣ 3 * n

case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n

State before:
case inr.h.left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ g ∣ 3 * n

case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n
Tactic:
change ∃ l : ℕ, 3 * n = 3 ^ (g + 1) * l at r2
State after:
case inr.h.left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : ∃ l, 3 * n = 3 ^ (g + 1) * l
⊢ 3 ^ g ∣ 3 * n

case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n

State before:
case inr.h.left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : ∃ l, 3 * n = 3 ^ (g + 1) * l
⊢ 3 ^ g ∣ 3 * n

case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n
Tactic:
cases' r2 with k hk
State after:
case inr.h.left.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g k : ℕ
hk : 3 * n = 3 ^ (g + 1) * k
⊢ 3 ^ g ∣ 3 * n

case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n

State before:
case inr.h.left.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g k : ℕ
hk : 3 * n = 3 ^ (g + 1) * k
⊢ 3 ^ g ∣ 3 * n

case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n
Tactic:
rw [pow_add, pow_one, mul_assoc] at hk
State after:
case inr.h.left.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
⊢ 3 ^ g ∣ 3 * n

case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n

State before:
case inr.h.left.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
⊢ 3 ^ g ∣ 3 * n

case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n
Tactic:
use 3 * k
State after:
case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n

State before:
case inr.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r2 : 3 ^ (g + 1) ∣ 3 * n
⊢ 3 ^ (g + 1) ∣ 3 * n
Tactic:
exact r2
State after:
no goals

State before:
case inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n ∨ 3 ^ g ∣ 3 * n ∧ 3 ^ (g + 1) ∣ 3 * n
Tactic:
left
State after:
case inl.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n

State before:
case inl.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∧ ¬3 ^ (g + 1) ∣ 3 * n
Tactic:
constructor
State after:
case inl.h.left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n

case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ (g + 1) ∣ 3 * n

State before:
case inl.h.left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n

case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ (g + 1) ∣ 3 * n
Tactic:
exact r1
State after:
case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ (g + 1) ∣ 3 * n

State before:
case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ (g + 1) ∣ 3 * n
Tactic:
by_contra h
State after:
case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
h : 3 ^ (g + 1) ∣ 3 * n
⊢ False

State before:
case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
h : 3 ^ (g + 1) ∣ 3 * n
⊢ False
Tactic:
change ∃ l : ℕ, 3 * n = 3 ^ (g + 1) * l at h
State after:
case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
h : ∃ l, 3 * n = 3 ^ (g + 1) * l
⊢ False

State before:
case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
h : ∃ l, 3 * n = 3 ^ (g + 1) * l
⊢ False
Tactic:
cases' h with k hk
State after:
case inl.h.right.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ (g + 1) * k
⊢ False

State before:
case inl.h.right.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ (g + 1) * k
⊢ False
Tactic:
rw [pow_add, pow_one, mul_assoc] at hk
State after:
case inl.h.right.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
⊢ False

State before:
case inl.h.right.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
⊢ False
Tactic:
have f : 3 ^ g ∣ 3 * n := by
  use 3 * k
State after:
case inl.h.right.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ False

State before:
case inl.h.right.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ False
Tactic:
have s : 3 ^ g ∣ 3 * n ∧ ¬3 ^ g ∣ 3 * n := by constructor; exact f; exact r1
State after:
case inl.h.right.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
s : 3 ^ g ∣ 3 * n ∧ ¬3 ^ g ∣ 3 * n
⊢ False

State before:
case inl.h.right.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
s : 3 ^ g ∣ 3 * n ∧ ¬3 ^ g ∣ 3 * n
⊢ False
Tactic:
simp at s
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
⊢ 3 ^ g ∣ 3 * n
Tactic:
use 3 * k
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ 3 ^ g ∣ 3 * n ∧ ¬3 ^ g ∣ 3 * n
Tactic:
constructor
State after:
case left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ 3 ^ g ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n

State before:
case left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ 3 ^ g ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n
Tactic:
exact f
State after:
case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n

State before:
case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n
Tactic:
exact r1
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
⊢ ∀ (f : ℕ), 3 ^ f ∣ 3 * n
Tactic:
intro g
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
g : ℕ
⊢ 3 ^ g ∣ 3 * n

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
g : ℕ
⊢ 3 ^ g ∣ 3 * n
Tactic:
induction' g with k hk
State after:
case zero
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
⊢ 3 ^ Nat.zero ∣ 3 * n

case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ k ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n

State before:
case zero
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
⊢ 3 ^ Nat.zero ∣ 3 * n

case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ k ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
Tactic:
norm_num
State after:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ k ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n

State before:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ k ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
Tactic:
specialize s k
State after:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s : ¬3 ^ k ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n ∨ 3 ^ k ∣ 3 * n ∧ 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n

State before:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s : ¬3 ^ k ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n ∨ 3 ^ k ∣ 3 * n ∧ 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
Tactic:
cases' s with s1 s2
State after:
case succ.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s1 : ¬3 ^ k ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n

case succ.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s2 : 3 ^ k ∣ 3 * n ∧ 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n

State before:
case succ.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s2 : 3 ^ k ∣ 3 * n ∧ 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
Tactic:
cases' s2 with s5 s6
State after:
case succ.inr.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk s5 : 3 ^ k ∣ 3 * n
s6 : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n

State before:
case succ.inr.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk s5 : 3 ^ k ∣ 3 * n
s6 : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
Tactic:
exact s6
State after:
no goals

State before:
case succ.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s1 : ¬3 ^ k ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
Tactic:
exfalso
State after:
case succ.inl.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s1 : ¬3 ^ k ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ False

State before:
case succ.inl.h
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s1 : ¬3 ^ k ∣ 3 * n ∧ ¬3 ^ (k + 1) ∣ 3 * n
⊢ False
Tactic:
cases' s1 with s3 s4
State after:
case succ.inl.h.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ False

State before:
case succ.inl.h.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ False
Tactic:
have t : 3 ^ k ∣ 3 * n ∧ ¬3 ^ k ∣ 3 * n := by constructor; exact hk; exact s3
State after:
case succ.inl.h.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
t : 3 ^ k ∣ 3 * n ∧ ¬3 ^ k ∣ 3 * n
⊢ False

State before:
case succ.inl.h.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
t : 3 ^ k ∣ 3 * n ∧ ¬3 ^ k ∣ 3 * n
⊢ False
Tactic:
simp at t
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ k ∣ 3 * n ∧ ¬3 ^ k ∣ 3 * n
Tactic:
constructor
State after:
case left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ k ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ k ∣ 3 * n

State before:
case left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ k ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ k ∣ 3 * n
Tactic:
exact hk
State after:
case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ k ∣ 3 * n

State before:
case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ k ∣ 3 * n
Tactic:
exact s3
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
⊢ ∀ (f : ℕ), 3 ^ (f + 1) > 3 * f
Tactic:
intro g
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
g : ℕ
⊢ 3 ^ (g + 1) > 3 * g

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
g : ℕ
⊢ 3 ^ (g + 1) > 3 * g
Tactic:
induction' g with k hk
State after:
case zero
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
⊢ 3 ^ (Nat.zero + 1) > 3 * Nat.zero

case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
⊢ 3 ^ (Nat.succ k + 1) > 3 * Nat.succ k

State before:
case zero
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
⊢ 3 ^ (Nat.zero + 1) > 3 * Nat.zero

case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
⊢ 3 ^ (Nat.succ k + 1) > 3 * Nat.succ k
Tactic:
norm_num
State after:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
⊢ 3 ^ (Nat.succ k + 1) > 3 * Nat.succ k

State before:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
⊢ 3 ^ (Nat.succ k + 1) > 3 * Nat.succ k
Tactic:
change 3 ^ (k + 1 + 1) > 3 * (k + 1)
State after:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)

State before:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
Tactic:
have ss : k = 0 ∨ 0 < k := Nat.eq_zero_or_pos k
State after:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : k = 0 ∨ 0 < k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)

State before:
case succ
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : k = 0 ∨ 0 < k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
Tactic:
cases ss with
| inl ss =>
rw [ss]; norm_num
| inr ss =>
change 1 ≤ k at ss
have b : k < 2 * k := by
  change 0 < k at ss
  exact lt_two_mul_self ss
have q1 : k + 1 < 3 * k :=
  by
  have finall := add_lt_add_of_lt_of_le b ss
  nth_rw 3 [← one_mul k] at finall
  rw [← right_distrib] at finall
  norm_num at finall
  exact finall
have q2 := lt_trans q1 hk
rw [pow_succ]
apply (mul_lt_mul_left zero_lt_three  ).2 q2
State after:
no goals

State before:
case succ.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : k = 0
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
Tactic:
rw [ss]
State after:
case succ.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : k = 0
⊢ 3 ^ (0 + 1 + 1) > 3 * (0 + 1)

State before:
case succ.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : k = 0
⊢ 3 ^ (0 + 1 + 1) > 3 * (0 + 1)
Tactic:
norm_num
State after:
no goals

State before:
case succ.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 0 < k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
Tactic:
change 1 ≤ k at ss
State after:
case succ.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)

State before:
case succ.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
Tactic:
have b : k < 2 * k := by
  change 0 < k at ss
  exact lt_two_mul_self ss
State after:
case succ.inr
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)

State before:
case succ.inr
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
Tactic:
have q1 : k + 1 < 3 * k :=
  by
  have finall := add_lt_add_of_lt_of_le b ss
  nth_rw 3 [← one_mul k] at finall
  rw [← right_distrib] at finall
  norm_num at finall
  exact finall
State after:
case succ.inr
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
q1 : k + 1 < 3 * k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)

State before:
case succ.inr
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
q1 : k + 1 < 3 * k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
Tactic:
have q2 := lt_trans q1 hk
State after:
case succ.inr
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
q1 : k + 1 < 3 * k
q2 : k + 1 < 3 ^ (k + 1)
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)

State before:
case succ.inr
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
q1 : k + 1 < 3 * k
q2 : k + 1 < 3 ^ (k + 1)
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
Tactic:
rw [pow_succ]
State after:
case succ.inr
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
q1 : k + 1 < 3 * k
q2 : k + 1 < 3 ^ (k + 1)
⊢ 3 * 3 ^ (k + 1) > 3 * (k + 1)

State before:
case succ.inr
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
q1 : k + 1 < 3 * k
q2 : k + 1 < 3 ^ (k + 1)
⊢ 3 * 3 ^ (k + 1) > 3 * (k + 1)
Tactic:
apply (mul_lt_mul_left zero_lt_three  ).2 q2
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
⊢ k < 2 * k
Tactic:
change 0 < k at ss
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 0 < k
⊢ k < 2 * k

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 0 < k
⊢ k < 2 * k
Tactic:
exact lt_two_mul_self ss
State after:
no goals

State before:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
⊢ k + 1 < 3 * k
Tactic:
have finall := add_lt_add_of_lt_of_le b ss
State after:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
finall : k + 1 < 2 * k + k
⊢ k + 1 < 3 * k

State before:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
finall : k + 1 < 2 * k + k
⊢ k + 1 < 3 * k
Tactic:
nth_rw 3 [← one_mul k] at finall
State after:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
finall : k + 1 < 2 * k + 1 * k
⊢ k + 1 < 3 * k

State before:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
finall : k + 1 < 2 * k + 1 * k
⊢ k + 1 < 3 * k
Tactic:
rw [← right_distrib] at finall
State after:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
finall : k + 1 < (2 + 1) * k
⊢ k + 1 < 3 * k

State before:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
finall : k + 1 < (2 + 1) * k
⊢ k + 1 < 3 * k
Tactic:
norm_num at finall
State after:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
finall : k + 1 < 3 * k
⊢ k + 1 < 3 * k

State before:
a b✝ c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
finall : k + 1 < 3 * k
⊢ k + 1 < 3 * k
Tactic:
exact finall
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n
Tactic:
clear t
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n
Tactic:
by_contra h
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
h : 3 ^ (n + 1) ∣ 3 * n
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
h : 3 ^ (n + 1) ∣ 3 * n
⊢ False
Tactic:
change ∃ l : ℕ, 3 * n = 3 ^ (n + 1) * l at h
State after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
h : ∃ l, 3 * n = 3 ^ (n + 1) * l
⊢ False

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
h : ∃ l, 3 * n = 3 ^ (n + 1) * l
⊢ False
Tactic:
cases' h with p hp
State after:
case intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
p : ℕ
hp : 3 * n = 3 ^ (n + 1) * p
⊢ False

State before:
case intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
p : ℕ
hp : 3 * n = 3 ^ (n + 1) * p
⊢ False
Tactic:
rw [hp] at q
State after:
case intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * p
⊢ False

State before:
case intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * p
⊢ False
Tactic:
have ss : p = 0 ∨ 0 < p := Nat.eq_zero_or_pos p
State after:
case intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * p
ss : p = 0 ∨ 0 < p
⊢ False

State before:
case intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * p
ss : p = 0 ∨ 0 < p
⊢ False
Tactic:
cases ss with
| inl ss =>
rw [ss] at hp ; norm_num at hp ; rw [hp] at j ; norm_num at j
| inr ss =>
simp at q ; rw [q] at ss ; norm_num at ss
State after:
no goals

State before:
case intro.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * p
ss : p = 0
⊢ False
Tactic:
rw [ss] at hp
State after:
case intro.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * 0
ss : p = 0
⊢ False

State before:
case intro.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * 0
ss : p = 0
⊢ False
Tactic:
norm_num at hp
State after:
case intro.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
ss : p = 0
hp : n = 0
⊢ False

State before:
case intro.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
ss : p = 0
hp : n = 0
⊢ False
Tactic:
rw [hp] at j
State after:
case intro.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ 0
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
ss : p = 0
hp : n = 0
⊢ False

State before:
case intro.inl
a b c : ℤθ
n : ℕ
j : 1 ≤ 0
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
ss : p = 0
hp : n = 0
⊢ False
Tactic:
norm_num at j
State after:
no goals

State before:
case intro.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * p
ss : 0 < p
⊢ False
Tactic:
simp at q
State after:
case intro.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
hp : 3 * n = 3 ^ (n + 1) * p
ss : 0 < p
q : p = 0
⊢ False

State before:
case intro.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
hp : 3 * n = 3 ^ (n + 1) * p
ss : 0 < p
q : p = 0
⊢ False
Tactic:
rw [q] at ss
State after:
case intro.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
hp : 3 * n = 3 ^ (n + 1) * p
ss : 0 < 0
q : p = 0
⊢ False

State before:
case intro.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
hp : 3 * n = 3 ^ (n + 1) * p
ss : 0 < 0
q : p = 0
⊢ False
Tactic:
norm_num at ss
State after:
no goals

State before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ 3 ^ (n + 1) ∣ 3 * n ∧ ¬3 ^ (n + 1) ∣ 3 * n
Tactic:
constructor
State after:
case left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ 3 ^ (n + 1) ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n

State before:
case left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ 3 ^ (n + 1) ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n
Tactic:
exact t
State after:
case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n

State before:
case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n
Tactic:
exact r
State after:
no goals