internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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)
Proof 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)
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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)
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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]
Proof 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)
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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)
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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)
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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)
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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)
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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]
Proof 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)
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.rep_mod_three
Proof state before:
a b c : ℤθ
n : ℕ
⊢ ∃ a, n = 3 * a ∨ n = 3 * a + 1 ∨ n = 3 * a + 2
Tactic:
induction' n with k hk
Proof state after:
case zero
a b c : ℤθ
⊢ ∃ a, Nat.zero = 3 * a ∨ Nat.zero = 3 * a + 1 ∨ Nat.zero = 3 * a + 2

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Theorem: ℤθ.rep_mod_three
Proof state before:
case zero
a b c : ℤθ
⊢ ∃ a, Nat.zero = 3 * a ∨ Nat.zero = 3 * a + 1 ∨ Nat.zero = 3 * a + 2

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
use 0
Proof state after:
case h
a b c : ℤθ
⊢ Nat.zero = 3 * 0 ∨ Nat.zero = 3 * 0 + 1 ∨ Nat.zero = 3 * 0 + 2

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Theorem: ℤθ.rep_mod_three
Proof state before:
case h
a b c : ℤθ
⊢ Nat.zero = 3 * 0 ∨ Nat.zero = 3 * 0 + 1 ∨ Nat.zero = 3 * 0 + 2

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
left
Proof state after:
case h.h
a b c : ℤθ
⊢ Nat.zero = 3 * 0

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
⊢ Nat.zero = 3 * 0

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [MulZeroClass.mul_zero]
Proof state after:
case h.h
a b c : ℤθ
⊢ Nat.zero = 0

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
⊢ Nat.zero = 0

case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rfl
Proof state after:
case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Theorem: ℤθ.rep_mod_three
Proof state before:
case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
cases' hk with j hj
Proof state after:
case succ.intro
a b c : ℤθ
k j : ℕ
hj : k = 3 * j ∨ k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Theorem: ℤθ.rep_mod_three
Proof state before:
case succ.intro
a b c : ℤθ
k j : ℕ
hj : k = 3 * j ∨ k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
cases' hj with h1 h23
Proof state after:
case succ.intro.inl
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

case succ.intro.inr
a b c : ℤθ
k j : ℕ
h23 : k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2