internlm/Lean-Github huggingface dataset:
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.right.right
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝¹ : 12 % 3 = 0
this✝ : 75 % 3 = 0
this : 6 % 3 = 0
⊢ ((-4 % 3 - j1 % 3 * 0 % 3) % 3 + (j3 % 3 * 0 % 3 - j2 % 3 * 0 % 3) % 3) % 3 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
⊢ 12 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this : 12 % 3 = 0
⊢ 75 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.unit_zpow_two_mod_three
Proof state before:
a b c : ℤθ
k j1 j2 j3 : ℤ
s : ↑(unit ^ (3 * k)) = { f := 3 * j1 + 1, g := 3 * j2, h := 3 * j3 }
w1 : (↑(unit ^ (3 * k + 2))).f = -5 - j1 * 15 + j3 * 12 + j2 * 24
w2 : (↑(unit ^ (3 * k + 2))).g = -14 - j1 * 42 + j3 * 60 + j2 * 57
w3 : (↑(unit ^ (3 * k + 2))).h = -4 - j1 * 12 + (j3 * 75 - j2 * 6)
this✝ : 12 % 3 = 0
this : 75 % 3 = 0
⊢ 6 % 3 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof state before:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
⊢ ∃ a, 3 ^ a ∣ 3 * n ∧ ¬3 ^ (a + 1) ∣ 3 * n
Tactic:
by_contra h
Proof state after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ¬∃ a, 3 ^ a ∣ 3 * n ∧ ¬3 ^ (a + 1) ∣ 3 * n
⊢ False
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
h : ∀ (a : ℕ), 3 ^ a ∣ 3 * n → 3 ^ (a + 1) ∣ 3 * n
⊢ False
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
a b c : ℤθ
n : ℕ
j : 1 ≤ n
r : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∨ 3 ^ (x + 1) ∣ 3 * n
⊢ False
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
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
⊢ 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
t : ∀ (f : ℕ), 3 ^ f ∣ 3 * n
⊢ False
Tactic:
specialize t (n + 1)
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
⊢ 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
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
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
q : ∀ (f : ℕ), 3 ^ (f + 1) > 3 * f
⊢ 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
t : 3 ^ (n + 1) ∣ 3 * n
q : ∀ (f : ℕ), 3 ^ (f + 1) > 3 * f
⊢ False
Tactic:
specialize q n
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
q : 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
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
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
q : 3 ^ (n + 1) > 3 * n
r : ¬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
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
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
q : 3 ^ (n + 1) > 3 * n
r : ¬3 ^ (n + 1) ∣ 3 * n
w : 3 ^ (n + 1) ∣ 3 * n ∧ ¬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
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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
case inl.h.right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ (g + 1) ∣ 3 * n
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
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
⊢ ∀ (f : ℕ), 3 ^ f ∣ 3 * n
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
g : ℕ
⊢ 3 ^ g ∣ 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
g : ℕ
⊢ 3 ^ g ∣ 3 * n
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
⊢ 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
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
⊢ 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
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
k : ℕ
hk : 3 ^ k ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
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
k : ℕ
hk : 3 ^ k ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
Tactic:
specialize s k
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof state after:
no goals
Theorem: ℤθ.hMul_three_pow_dvd
Proof 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
Proof 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