internlm/Lean-Github huggingface dataset:
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ p ≤ q
Tactic:
have h8 : m ∣ n := by
  apply Exists.intro p
  rewrite [n_eq_pm]
  ring
  done
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
⊢ p ≤ q
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
⊢ p ≤ q
Tactic:
have q_dvd_n : q ∣ n := dvd_trans h7 h8
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
⊢ p ≤ q
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
⊢ p ≤ q
Tactic:
have ap_L : all_prime L := ndpl_L.left
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : all_prime L
⊢ p ≤ q
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : all_prime L
⊢ p ≤ q
Tactic:
define at ap_L
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : ∀ p ∈ L, prime p
⊢ p ≤ q
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : ∀ p ∈ L, prime p
⊢ p ≤ q
Tactic:
have q_prime_factor : prime_factor q n :=
  And.intro (ap_L q q_in_L) q_dvd_n
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : ∀ p ∈ L, prime p
q_prime_factor : prime_factor q n
⊢ p ≤ q
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
h8 : m ∣ n
q_dvd_n : q ∣ n
ap_L : ∀ p ∈ L, prime p
q_prime_factor : prime_factor q n
⊢ p ≤ q
Tactic:
show p ≤ q from p_least q q_prime_factor
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ m ∣ n
Tactic:
apply Exists.intro p
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ n = m * p
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ n = m * p
Tactic:
rewrite [n_eq_pm]
Proof state after:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ p * m = m * p
Theorem: HTPI.exists_prime_factorization
Proof state before:
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
q : ℕ
q_in_L : q ∈ L
h7 : q ∣ m
⊢ p * m = m * p
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ prod (p :: L) = n
Tactic:
rewrite [prod_cons, h6.right, n_eq_pm]
Proof state after:
case neg.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ p * m = p * m
Theorem: HTPI.exists_prime_factorization
Proof state before:
case neg.right
n : ℕ
ih : ∀ n_1 < n, n_1 ≥ 1 → ∃ l, prime_factorization n_1 l
h1 : n ≥ 1
h2 : ¬n = 1
h3 : n ≥ 2
p : ℕ
h4 : prime_factor p n ∧ ∀ (q : ℕ), prime_factor q n → p ≤ q
p_prime_factor : prime p ∧ p ∣ n
p_prime : prime p
p_dvd_n : p ∣ n
p_least : ∀ (q : ℕ), prime_factor q n → p ≤ q
m : ℕ
n_eq_pm : n = p * m
h5 : m ≠ 0
m_pos : 0 < m
m_lt_n : m < n
L : List ℕ
h6 : nondec_prime_list L ∧ prod L = m
ndpl_L : all_prime L ∧ nondec L
⊢ p * m = p * m
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : c ∣ a * b
h2 : rel_prime a c
⊢ c ∣ b
Tactic:
rewrite [←Int.coe_nat_dvd]
Proof state after:
a b c : ℕ
h1 : c ∣ a * b
h2 : rel_prime a c
⊢ ↑c ∣ ↑b
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : c ∣ a * b
h2 : rel_prime a c
⊢ ↑c ∣ ↑b
Tactic:
define at h1
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : rel_prime a c
⊢ ↑c ∣ ↑b
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : rel_prime a c
⊢ ↑c ∣ ↑b
Tactic:
define at h2
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
⊢ ↑c ∣ ↑b
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
⊢ ↑c ∣ ↑b
Tactic:
define
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
⊢ ∃ c_1, ↑b = ↑c * c_1
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
obtain (j : Nat) (h3 : a * b = c * j) from h1
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
⊢ ∃ c_1, ↑b = ↑c * c_1
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
set s : Int := gcd_c1 a c
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
⊢ ∃ c_1, ↑b = ↑c * c_1
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
set t : Int := gcd_c2 a c
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
⊢ ∃ c_1, ↑b = ↑c * c_1
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
have h4 : s * ↑a + t * ↑c = ↑(gcd a c) := gcd_lin_comb c a
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = ↑(gcd a c)
⊢ ∃ c_1, ↑b = ↑c * c_1
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = ↑(gcd a c)
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
rewrite [h2, Nat.cast_one] at h4
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ ∃ c_1, ↑b = ↑c * c_1
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ ∃ c_1, ↑b = ↑c * c_1
Tactic:
apply Exists.intro (s * ↑j + t * ↑b)
Proof state after:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ ↑b = ↑c * (s * ↑j + t * ↑b)
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ ↑b = ↑c * (s * ↑j + t * ↑b)
Tactic:
show ↑b = ↑c * (s * ↑j + t * ↑b) from
  calc ↑b
    _ = (1 : Int) * ↑b := (one_mul _).symm
    _ = (s * ↑a + t * ↑c) * ↑b := by rw [h4]
    _ = s * (↑a * ↑b) + t * ↑c * ↑b := by ring
    _ = s * (↑c * ↑j) + t * ↑c * ↑b := by
          rw [←Nat.cast_mul a b, h3, Nat.cast_mul c j]
    _ = ↑c * (s * ↑j + t * ↑b) := by ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ 1 * ↑b = (s * ↑a + t * ↑c) * ↑b
Tactic:
rw [h4]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ (s * ↑a + t * ↑c) * ↑b = s * (↑a * ↑b) + t * ↑c * ↑b
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ s * (↑a * ↑b) + t * ↑c * ↑b = s * (↑c * ↑j) + t * ↑c * ↑b
Tactic:
rw [←Nat.cast_mul a b, h3, Nat.cast_mul c j]
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_2
Proof state before:
a b c : ℕ
h1 : ∃ c_1, a * b = c * c_1
h2 : gcd a c = 1
j : ℕ
h3 : a * b = c * j
s : ℤ := gcd_c1 a c
t : ℤ := gcd_c2 a c
h4 : s * ↑a + t * ↑c = 1
⊢ s * (↑c * ↑j) + t * ↑c * ↑b = ↑c * (s * ↑j + t * ↑b)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.le_nonzero_prod_left
Proof state before:
a b : ℕ
h : a * b ≠ 0
⊢ a ≤ a * b
Tactic:
have h1 : b ≠ 0 := by
  contradict h with h1
  rewrite [h1]
  ring
  done
Proof state after:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
⊢ a ≤ a * b
Theorem: HTPI.le_nonzero_prod_left
Proof state before:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
⊢ a ≤ a * b
Tactic:
have h2 : 1 ≤ b := Nat.pos_of_ne_zero h1
Proof state after:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
h2 : 1 ≤ b
⊢ a ≤ a * b
Theorem: HTPI.le_nonzero_prod_left
Proof state before:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
h2 : 1 ≤ b
⊢ a ≤ a * b
Tactic:
show a ≤ a * b from
  calc a
      = a * 1 := (mul_one a).symm
    _ ≤ a * b := by rel [h2]
Proof state after:
no goals
Theorem: HTPI.le_nonzero_prod_left
Proof state before:
a b : ℕ
h : a * b ≠ 0
⊢ b ≠ 0
Tactic:
contradict h with h1
Proof state after:
a b : ℕ
h : a * b ≠ 0
h1 : b = 0
⊢ a * b = 0
Theorem: HTPI.le_nonzero_prod_left
Proof state before:
a b : ℕ
h : a * b ≠ 0
h1 : b = 0
⊢ a * b = 0
Tactic:
rewrite [h1]
Proof state after:
a b : ℕ
h : a * b ≠ 0
h1 : b = 0
⊢ a * 0 = 0
Theorem: HTPI.le_nonzero_prod_left
Proof state before:
a b : ℕ
h : a * b ≠ 0
h1 : b = 0
⊢ a * 0 = 0
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.le_nonzero_prod_left
Proof state before:
a b : ℕ
h : a * b ≠ 0
h1 : b ≠ 0
h2 : 1 ≤ b
⊢ a * 1 ≤ a * b
Tactic:
rel [h2]
Proof state after:
no goals
Theorem: HTPI.le_nonzero_prod_right
Proof state before:
a b : ℕ
h : a * b ≠ 0
⊢ b ≤ a * b
Tactic:
rewrite [mul_comm]
Proof state after:
a b : ℕ
h : a * b ≠ 0
⊢ b ≤ b * a
Theorem: HTPI.le_nonzero_prod_right
Proof state before:
a b : ℕ
h : a * b ≠ 0
⊢ b ≤ b * a
Tactic:
rewrite [mul_comm] at h
Proof state after:
a b : ℕ
h : b * a ≠ 0
⊢ b ≤ b * a
Theorem: HTPI.le_nonzero_prod_right
Proof state before:
a b : ℕ
h : b * a ≠ 0
⊢ b ≤ b * a
Tactic:
show b ≤ b * a from le_nonzero_prod_left h
Proof state after:
no goals
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
⊢ rel_prime a p
Tactic:
have h3 : gcd a p ∣ a := gcd_dvd_left a p
Proof state after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
⊢ rel_prime a p
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
⊢ rel_prime a p
Tactic:
have h4 : gcd a p ∣ p := gcd_dvd_right a p
Proof state after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
⊢ rel_prime a p
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
⊢ rel_prime a p
Tactic:
have h5 : gcd a p = 1 ∨ gcd a p = p := dvd_prime h1 h4
Proof state after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
⊢ rel_prime a p
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
⊢ rel_prime a p
Tactic:
have h6 : gcd a p ≠ p := by
  contradict h2 with h6
  rewrite [h6] at h3
  show p ∣ a from h3
  done
Proof state after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p ≠ p
⊢ rel_prime a p
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p ≠ p
⊢ rel_prime a p
Tactic:
disj_syll h5 h6
Proof state after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h6 : gcd a p ≠ p
h5 : gcd a p = 1
⊢ rel_prime a p
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h6 : gcd a p ≠ p
h5 : gcd a p = 1
⊢ rel_prime a p
Tactic:
show rel_prime a p from h5
Proof state after:
no goals
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
⊢ gcd a p ≠ p
Tactic:
contradict h2 with h6
Proof state after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p = p
⊢ p ∣ a
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : gcd a p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p = p
⊢ p ∣ a
Tactic:
rewrite [h6] at h3
Proof state after:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p = p
⊢ p ∣ a
Theorem: HTPI.rel_prime_of_prime_not_dvd
Proof state before:
a p : ℕ
h1 : prime p
h2 : ¬p ∣ a
h3 : p ∣ a
h4 : gcd a p ∣ p
h5 : gcd a p = 1 ∨ gcd a p = p
h6 : gcd a p = p
⊢ p ∣ a
Tactic:
show p ∣ a from h3
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_3
Proof state before:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b
Tactic:
or_right with h3
Proof state after:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
h3 : ¬p ∣ a
⊢ p ∣ b
Theorem: HTPI.Theorem_7_2_3
Proof state before:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
h3 : ¬p ∣ a
⊢ p ∣ b
Tactic:
have h4 : rel_prime a p := rel_prime_of_prime_not_dvd h1 h3
Proof state after:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
h3 : ¬p ∣ a
h4 : rel_prime a p
⊢ p ∣ b
Theorem: HTPI.Theorem_7_2_3
Proof state before:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
h3 : ¬p ∣ a
h4 : rel_prime a p
⊢ p ∣ b
Tactic:
show p ∣ b from Theorem_7_2_2 h2 h4
Proof state after:
no goals
Theorem: HTPI.ge_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
⊢ a ≥ 1
Tactic:
have h1 : a ≠ 0 := by
  by_contra h1
  rewrite [h1] at h
  contradict h
  linarith
  done
Proof state after:
a b : ℕ
h : a * b = 1
h1 : a ≠ 0
⊢ a ≥ 1
Theorem: HTPI.ge_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
h1 : a ≠ 0
⊢ a ≥ 1
Tactic:
show a ≥ 1 from Nat.pos_of_ne_zero h1
Proof state after:
no goals
Theorem: HTPI.ge_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
⊢ a ≠ 0
Tactic:
by_contra h1
Proof state after:
a b : ℕ
h : a * b = 1
h1 : a = 0
⊢ False
Theorem: HTPI.ge_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
h1 : a = 0
⊢ False
Tactic:
rewrite [h1] at h
Proof state after:
a b : ℕ
h : 0 * b = 1
h1 : a = 0
⊢ False
Theorem: HTPI.ge_one_of_prod_one
Proof state before:
a b : ℕ
h : 0 * b = 1
h1 : a = 0
⊢ False
Tactic:
contradict h
Proof state after:
a b : ℕ
h : 0 * b = 1
h1 : a = 0
⊢ ¬0 * b = 1
Theorem: HTPI.ge_one_of_prod_one
Proof state before:
a b : ℕ
h : 0 * b = 1
h1 : a = 0
⊢ ¬0 * b = 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.eq_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
⊢ a = 1
Tactic:
have h1 : a ≥ 1 := ge_one_of_prod_one h
Proof state after:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
⊢ a = 1
Theorem: HTPI.eq_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
⊢ a = 1
Tactic:
have h2 : a * b ≠ 0 := by linarith
Proof state after:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
⊢ a = 1
Theorem: HTPI.eq_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
⊢ a = 1
Tactic:
have h3 : a ≤ a * b := le_nonzero_prod_left h2
Proof state after:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
h3 : a ≤ a * b
⊢ a = 1
Theorem: HTPI.eq_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
h3 : a ≤ a * b
⊢ a = 1
Tactic:
rewrite [h] at h3
Proof state after:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
h3 : a ≤ 1
⊢ a = 1
Theorem: HTPI.eq_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
h2 : a * b ≠ 0
h3 : a ≤ 1
⊢ a = 1
Tactic:
show a = 1 from Nat.le_antisymm h3 h1
Proof state after:
no goals
Theorem: HTPI.eq_one_of_prod_one
Proof state before:
a b : ℕ
h : a * b = 1
h1 : a ≥ 1
⊢ a * b ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.eq_one_of_dvd_one
Proof state before:
n : ℕ
h : n ∣ 1
⊢ n = 1
Tactic:
obtain (j : Nat) (h1 : 1 = n * j) from h
Proof state after:
n : ℕ
h : n ∣ 1
j : ℕ
h1 : 1 = n * j
⊢ n = 1
Theorem: HTPI.eq_one_of_dvd_one
Proof state before:
n : ℕ
h : n ∣ 1
j : ℕ
h1 : 1 = n * j
⊢ n = 1
Tactic:
show n = 1 from eq_one_of_prod_one h1.symm
Proof state after:
no goals
Theorem: HTPI.prime_not_one
Proof state before:
p : ℕ
h : prime p
⊢ p ≠ 1
Tactic:
define at h
Proof state after:
p : ℕ
h : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
⊢ p ≠ 1
Theorem: HTPI.prime_not_one
Proof state before:
p : ℕ
h : 2 ≤ p ∧ ¬∃ a b, a * b = p ∧ a < p ∧ b < p
⊢ p ≠ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Theorem_7_2_4
Proof state before:
p : ℕ
h1 : prime p
⊢ ∀ (l : List ℕ), p ∣ prod l → ∃ a ∈ l, p ∣ a
Tactic:
apply List.rec
Proof state after:
case nil
p : ℕ
h1 : prime p
⊢ p ∣ prod [] → ∃ a ∈ [], p ∣ a

case cons
p : ℕ
h1 : prime p
⊢ ∀ (head : ℕ) (tail : List ℕ),
    (p ∣ prod tail → ∃ a ∈ tail, p ∣ a) → p ∣ prod (head :: tail) → ∃ a ∈ head :: tail, p ∣ a