internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.rep_mod_three
Proof state before:
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
Tactic:
use j
Proof state after:
case h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j ∨ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 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
Theorem: ℤθ.rep_mod_three
Proof state before:
case h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j ∨ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 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
Tactic:
right
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 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
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 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
Tactic:
left
Proof state after:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j + 1

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
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ Nat.succ k = 3 * j + 1

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
Tactic:
change k + 1 = 3 * j + 1
Proof state after:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ k + 1 = 3 * j + 1

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
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ k + 1 = 3 * j + 1

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
Tactic:
rw [add_left_inj 1]
Proof state after:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ k = 3 * j

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
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h.h
a b c : ℤθ
k j : ℕ
h1 : k = 3 * j
⊢ k = 3 * j

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
Tactic:
exact h1
Proof state after:
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
Theorem: ℤθ.rep_mod_three
Proof state before:
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
Tactic:
cases' h23 with h2 h3
Proof state after:
case succ.intro.inr.inl
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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.inr.inl
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
use j
Proof state after:
case h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j ∨ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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 h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j ∨ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
right
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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 h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j + 1 ∨ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
right
Proof state after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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 h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ Nat.succ k = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
change k + 1 = 3 * j + 2
Proof state after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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 h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + 2

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [← one_add_one_eq_two]
Proof state after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + (1 + 1)

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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 h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + (1 + 1)

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [← add_assoc]
Proof state after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + 1 + 1

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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 h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k + 1 = 3 * j + 1 + 1

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
rw [add_left_inj 1]
Proof state after:
case h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k = 3 * j + 1

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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 h.h.h
a b c : ℤθ
k j : ℕ
h2 : k = 3 * j + 1
⊢ k = 3 * j + 1

case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
exact h2
Proof state after:
case succ.intro.inr.inr
a b c : ℤθ
k j : ℕ
h3 : 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.inr.inr
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
Tactic:
use j + 1
Proof state after:
case h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1) ∨ Nat.succ k = 3 * (j + 1) + 1 ∨ Nat.succ k = 3 * (j + 1) + 2
Theorem: ℤθ.rep_mod_three
Proof state before:
case h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1) ∨ Nat.succ k = 3 * (j + 1) + 1 ∨ Nat.succ k = 3 * (j + 1) + 2
Tactic:
left
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1)
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1)
Tactic:
change k + 1 = 3 * (j + 1)
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * (j + 1)
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * (j + 1)
Tactic:
rw [mul_add]
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * j + 3 * 1
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * j + 3 * 1
Tactic:
rw [mul_one]
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * j + 3
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ k + 1 = 3 * j + 3
Tactic:
have babymath : 3 = 2 + 1 := by norm_num
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 3
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 3
Tactic:
nth_rw 2 [babymath]
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + (2 + 1)
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + (2 + 1)
Tactic:
rw [← add_assoc]
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 2 + 1
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 2 + 1
Tactic:
rw [add_left_inj 1]
Proof state after:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k = 3 * j + 2
Theorem: ℤθ.rep_mod_three
Proof state before:
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k = 3 * j + 2
Tactic:
exact h3
Proof state after:
no goals
Theorem: ℤθ.rep_mod_three
Proof state before:
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ 3 = 2 + 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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))
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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)
Theorem: ℤθ.hMul_three_expansion
Proof 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
Proof 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)