internlm/Lean-Github huggingface dataset:
Theorem: HTPI.gcd_dvd
Proof state before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
by_cases h1 : b = 0
Proof state after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ gcd a b ∣ a ∧ gcd a b ∣ b

case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
Theorem: HTPI.gcd_dvd
Proof state before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
rewrite [h1, gcd_base]
Proof state after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ a ∣ a ∧ a ∣ 0
Theorem: HTPI.gcd_dvd
Proof state before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ a ∣ a ∧ a ∣ 0
Tactic:
apply And.intro (dvd_self a)
Proof state after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ a ∣ 0
Theorem: HTPI.gcd_dvd
Proof state before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ a ∣ 0
Tactic:
define
Proof state after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ ∃ c, 0 = a * c
Theorem: HTPI.gcd_dvd
Proof state before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ ∃ c, 0 = a * c
Tactic:
apply Exists.intro 0
Proof state after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ 0 = a * 0
Theorem: HTPI.gcd_dvd
Proof state before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ 0 = a * 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.gcd_dvd
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
rewrite [gcd_nonzero a h1]
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Theorem: HTPI.gcd_dvd
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Tactic:
have h2 : a % b < b := mod_nonzero_lt a h1
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Theorem: HTPI.gcd_dvd
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Tactic:
have h3 : (gcd b (a % b)) ∣ b ∧ (gcd b (a % b)) ∣ (a % b) :=
  ih (a % b) h2 b
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
h3 : gcd b (a % b) ∣ b ∧ gcd b (a % b) ∣ a % b
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Theorem: HTPI.gcd_dvd
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
h3 : gcd b (a % b) ∣ b ∧ gcd b (a % b) ∣ a % b
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Tactic:
apply And.intro _ h3.left
Proof state after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
h3 : gcd b (a % b) ∣ b ∧ gcd b (a % b) ∣ a % b
⊢ gcd b (a % b) ∣ a
Theorem: HTPI.gcd_dvd
Proof state before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
h3 : gcd b (a % b) ∣ b ∧ gcd b (a % b) ∣ a % b
⊢ gcd b (a % b) ∣ a
Tactic:
show (gcd b (a % b)) ∣ a from dvd_a_of_dvd_b_mod h3.left h3.right
Proof state after:
no goals
Theorem: HTPI.gcd_c1_base
Proof state before:
a : ℕ
⊢ gcd_c1 a 0 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.gcd_c1_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
⊢ gcd_c1 a b = gcd_c2 b (a % b)
Tactic:
obtain (n : Nat) (h2 : b = n + 1) from exists_eq_add_one_of_ne_zero h
Proof state after:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c1 a b = gcd_c2 b (a % b)
Theorem: HTPI.gcd_c1_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c1 a b = gcd_c2 b (a % b)
Tactic:
rewrite [h2]
Proof state after:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c1 a (n + 1) = gcd_c2 (n + 1) (a % (n + 1))
Theorem: HTPI.gcd_c1_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c1 a (n + 1) = gcd_c2 (n + 1) (a % (n + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.gcd_c2_base
Proof state before:
a : ℕ
⊢ gcd_c2 a 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.gcd_c2_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
⊢ gcd_c2 a b = gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)
Tactic:
obtain (n : Nat) (h2 : b = n + 1) from exists_eq_add_one_of_ne_zero h
Proof state after:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c2 a b = gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)
Theorem: HTPI.gcd_c2_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c2 a b = gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)
Tactic:
rewrite [h2]
Proof state after:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c2 a (n + 1) = gcd_c1 (n + 1) (a % (n + 1)) - gcd_c2 (n + 1) (a % (n + 1)) * ↑(a / (n + 1))
Theorem: HTPI.gcd_c2_nonzero
Proof state before:
a b : ℕ
h : b ≠ 0
n : ℕ
h2 : b = n + 1
⊢ gcd_c2 a (n + 1) = gcd_c1 (n + 1) (a % (n + 1)) - gcd_c2 (n + 1) (a % (n + 1)) * ↑(a / (n + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.gcd_lin_comb
Proof state before:
⊢ ∀ (b a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
by_strong_induc
Proof state after:
⊢ ∀ (b : ℕ),
    (∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)) →
      ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Theorem: HTPI.gcd_lin_comb
Proof state before:
⊢ ∀ (b : ℕ),
    (∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)) →
      ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
fix b : Nat
Proof state after:
b : ℕ
⊢ (∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)) →
    ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Theorem: HTPI.gcd_lin_comb
Proof state before:
b : ℕ
⊢ (∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)) →
    ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
assume ih : ∀ b_1 < b, ∀ (a : Nat),
  (gcd_c1 a b_1) * ↑a + (gcd_c2 a b_1) * ↑b_1 = ↑(gcd a b_1)
Proof state after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
⊢ ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Theorem: HTPI.gcd_lin_comb
Proof state before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
⊢ ∀ (a : ℕ), gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
fix a : Nat
Proof state after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Theorem: HTPI.gcd_lin_comb
Proof state before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
by_cases h1 : b = 0
Proof state after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : b = 0
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)

case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Theorem: HTPI.gcd_lin_comb
Proof state before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : b = 0
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
rewrite [h1, gcd_c1_base, gcd_c2_base, gcd_base]
Proof state after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : b = 0
⊢ 1 * ↑a + 0 * ↑0 = ↑a
Theorem: HTPI.gcd_lin_comb
Proof state before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : b = 0
⊢ 1 * ↑a + 0 * ↑0 = ↑a
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
⊢ gcd_c1 a b * ↑a + gcd_c2 a b * ↑b = ↑(gcd a b)
Tactic:
rewrite [gcd_c1_nonzero a h1, gcd_c2_nonzero a h1, gcd_nonzero a h1]
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
⊢ gcd_c2 b (a % b) * ↑a + (gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)) * ↑b = ↑(gcd b (a % b))
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
⊢ gcd_c2 b (a % b) * ↑a + (gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)) * ↑b = ↑(gcd b (a % b))
Tactic:
set r : Nat := a % b
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
⊢ gcd_c2 b r * ↑a + (gcd_c1 b r - gcd_c2 b r * ↑(a / b)) * ↑b = ↑(gcd b r)
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
⊢ gcd_c2 b r * ↑a + (gcd_c1 b r - gcd_c2 b r * ↑(a / b)) * ↑b = ↑(gcd b r)
Tactic:
set q : Nat := a / b
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
⊢ gcd_c2 b r * ↑a + (gcd_c1 b r - gcd_c2 b r * ↑q) * ↑b = ↑(gcd b r)
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
⊢ gcd_c2 b r * ↑a + (gcd_c1 b r - gcd_c2 b r * ↑q) * ↑b = ↑(gcd b r)
Tactic:
set s : Int := gcd_c1 b r
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
⊢ gcd_c2 b r * ↑a + (s - gcd_c2 b r * ↑q) * ↑b = ↑(gcd b r)
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
⊢ gcd_c2 b r * ↑a + (s - gcd_c2 b r * ↑q) * ↑b = ↑(gcd b r)
Tactic:
set t : Int := gcd_c2 b r
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Tactic:
have h2 : r < b := mod_nonzero_lt a h1
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Tactic:
have h3 : s * ↑b + t * ↑r = ↑(gcd b r) := ih r h2 b
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Tactic:
have h4 : b * q + r = a := Nat.div_add_mod a b
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
Tactic:
rewrite [←h3, ←h4]
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * ↑(b * q + r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * ↑(b * q + r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r
Tactic:
rewrite [Nat.cast_add, Nat.cast_mul]
Proof state after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * (↑b * ↑q + ↑r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r
Theorem: HTPI.gcd_lin_comb
Proof state before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd_c1 a b_1 * ↑a + gcd_c2 a b_1 * ↑b_1 = ↑(gcd a b_1)
a : ℕ
h1 : ¬b = 0
r : ℕ := a % b
q : ℕ := a / b
s : ℤ := gcd_c1 b r
t : ℤ := gcd_c2 b r
h2 : r < b
h3 : s * ↑b + t * ↑r = ↑(gcd b r)
h4 : b * q + r = a
⊢ t * (↑b * ↑q + ↑r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
⊢ d ∣ gcd a b
Tactic:
rewrite [←Int.coe_nat_dvd]
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
⊢ ↑d ∣ ↑(gcd a b)
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
⊢ ↑d ∣ ↑(gcd a b)
Tactic:
set s : Int := gcd_c1 a b
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
⊢ ↑d ∣ ↑(gcd a b)
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
⊢ ↑d ∣ ↑(gcd a b)
Tactic:
set t : Int := gcd_c2 a b
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
⊢ ↑d ∣ ↑(gcd a b)
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
⊢ ↑d ∣ ↑(gcd a b)
Tactic:
have h3 : s * ↑a + t * ↑b = ↑(gcd a b) := gcd_lin_comb b a
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
⊢ ↑d ∣ ↑(gcd a b)
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
⊢ ↑d ∣ ↑(gcd a b)
Tactic:
rewrite [←h3]
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
⊢ ↑d ∣ s * ↑a + t * ↑b
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
⊢ ↑d ∣ s * ↑a + t * ↑b
Tactic:
obtain (j : Nat) (h4 : a = d * j) from h1
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
⊢ ↑d ∣ s * ↑a + t * ↑b
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
⊢ ↑d ∣ s * ↑a + t * ↑b
Tactic:
obtain (k : Nat) (h5 : b = d * k) from h2
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ↑d ∣ s * ↑a + t * ↑b
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ↑d ∣ s * ↑a + t * ↑b
Tactic:
rewrite [h4, h5, Nat.cast_mul, Nat.cast_mul]
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ↑d ∣ s * (↑d * ↑j) + t * (↑d * ↑k)
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ↑d ∣ s * (↑d * ↑j) + t * (↑d * ↑k)
Tactic:
define
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ∃ c, s * (↑d * ↑j) + t * (↑d * ↑k) = ↑d * c
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ ∃ c, s * (↑d * ↑j) + t * (↑d * ↑k) = ↑d * c
Tactic:
apply Exists.intro (s * ↑j + t * ↑k)
Proof state after:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ s * (↑d * ↑j) + t * (↑d * ↑k) = ↑d * (s * ↑j + t * ↑k)
Theorem: HTPI.Theorem_7_1_6
Proof state before:
d a b : ℕ
h1 : d ∣ a
h2 : d ∣ b
s : ℤ := gcd_c1 a b
t : ℤ := gcd_c2 a b
h3 : s * ↑a + t * ↑b = ↑(gcd a b)
j : ℕ
h4 : a = d * j
k : ℕ
h5 : b = d * k
⊢ s * (↑d * ↑j) + t * (↑d * ↑k) = ↑d * (s * ↑j + t * ↑k)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.dvd_trans
Proof state before:
a b c : ℕ
h1 : a ∣ b
h2 : b ∣ c
⊢ a ∣ c
Tactic:
define at h1
Proof state after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : b ∣ c
⊢ a ∣ c
Theorem: HTPI.dvd_trans
Proof state before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : b ∣ c
⊢ a ∣ c
Tactic:
define at h2
Proof state after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ a ∣ c
Theorem: HTPI.dvd_trans
Proof state before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ a ∣ c
Tactic:
define
Proof state after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ ∃ c_1, c = a * c_1
Theorem: HTPI.dvd_trans
Proof state before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ ∃ c_1, c = a * c_1
Tactic:
obtain (m : Nat) (h3 : b = a * m) from h1
Proof state after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
⊢ ∃ c_1, c = a * c_1
Theorem: HTPI.dvd_trans
Proof state before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
⊢ ∃ c_1, c = a * c_1
Tactic:
obtain (n : Nat) (h4 : c = b * n) from h2
Proof state after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = b * n
⊢ ∃ c_1, c = a * c_1
Theorem: HTPI.dvd_trans
Proof state before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = b * n
⊢ ∃ c_1, c = a * c_1
Tactic:
rewrite [h3, mul_assoc] at h4
Proof state after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = a * (m * n)
⊢ ∃ c_1, c = a * c_1
Theorem: HTPI.dvd_trans
Proof state before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = a * (m * n)
⊢ ∃ c_1, c = a * c_1
Tactic:
apply Exists.intro (m * n)
Proof state after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = a * (m * n)
⊢ c = a * (m * n)
Theorem: HTPI.dvd_trans
Proof state before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = a * (m * n)
⊢ c = a * (m * n)
Tactic:
show c = a * (m * n) from h4
Proof state after:
no goals
Theorem: HTPI.exists_prime_factor
Proof state before:
⊢ ∀ (n : ℕ), 2 ≤ n → ∃ p, prime_factor p n
Tactic:
by_strong_induc
Proof state after:
⊢ ∀ (n : ℕ), (∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1) → 2 ≤ n → ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
⊢ ∀ (n : ℕ), (∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1) → 2 ≤ n → ∃ p, prime_factor p n
Tactic:
fix n : Nat
Proof state after:
n : ℕ
⊢ (∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1) → 2 ≤ n → ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
⊢ (∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1) → 2 ≤ n → ∃ p, prime_factor p n
Tactic:
assume ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ (p : Nat), prime_factor p n_1
Proof state after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
⊢ 2 ≤ n → ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
⊢ 2 ≤ n → ∃ p, prime_factor p n
Tactic:
assume h1 : 2 ≤ n
Proof state after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
⊢ ∃ p, prime_factor p n
Tactic:
by_cases h2 : prime n
Proof state after:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ ∃ p, prime_factor p n

case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬prime n
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ ∃ p, prime_factor p n
Tactic:
apply Exists.intro n
Proof state after:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ prime_factor n n
Theorem: HTPI.exists_prime_factor
Proof state before:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ prime_factor n n
Tactic:
define
Proof state after:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ prime n ∧ n ∣ n
Theorem: HTPI.exists_prime_factor
Proof state before:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ prime n ∧ n ∣ n
Tactic:
show prime n ∧ n ∣ n from And.intro h2 (dvd_self n)
Proof state after:
no goals
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬prime n
⊢ ∃ p, prime_factor p n
Tactic:
define at h2
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬(2 ≤ n ∧ ¬∃ a b, a * b = n ∧ a < n ∧ b < n)
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬(2 ≤ n ∧ ¬∃ a b, a * b = n ∧ a < n ∧ b < n)
⊢ ∃ p, prime_factor p n
Tactic:
demorgan at h2
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬2 ≤ n ∨ ∃ a b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Theorem: HTPI.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬2 ≤ n ∨ ∃ a b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Tactic:
disj_syll h2 h1
Proof state after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n