internlm/Lean-Github huggingface dataset:
Theorem: MyRing.zero_mulαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ 0 * a = 0
Tactic:
have h : 0 * a + 0 * a = 0 * a + 0 := by rw [← add_mul, add_zero, add_zero]
Proof state after:
R : Type u_1
inst✝ : Ring R
a : R
h : 0 * a + 0 * a = 0 * a + 0
⊢ 0 * a = 0
Theorem: MyRing.zero_mulαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
h : 0 * a + 0 * a = 0 * a + 0
⊢ 0 * a = 0
Tactic:
rw [add_left_cancel h]
Proof state after:
no goals
Theorem: MyRing.zero_mulαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ 0 * a + 0 * a = 0 * a + 0
Tactic:
rw [← add_mul, add_zero, add_zero]
Proof state after:
no goals
Theorem: MyRing.neg_eq_of_add_eq_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -a = b
Tactic:
sorry
Proof state after:
no goals
Theorem: MyRing.eq_neg_of_add_eq_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ a = -b
Tactic:
sorry
Proof state after:
no goals
Theorem: MyRing.neg_zero
Proof state before:
R : Type u_1
inst✝ : Ring R
⊢ -0 = 0
Tactic:
apply neg_eq_of_add_eq_zero
Proof state after:
case h
R : Type u_1
inst✝ : Ring R
⊢ 0 + 0 = 0
Theorem: MyRing.neg_zero
Proof state before:
case h
R : Type u_1
inst✝ : Ring R
⊢ 0 + 0 = 0
Tactic:
rw [add_zero]
Proof state after:
no goals
Theorem: MyRing.neg_neg
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ - -a = a
Tactic:
sorry
Proof state after:
no goals
Theorem: MyRing.neg_eq_of_add_eq_zeroαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -a = b
Tactic:
rw [← neg_add_cancel_left a b, h, add_zero]
Proof state after:
no goals
Theorem: MyRing.eq_neg_of_add_eq_zeroαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ a = -b
Tactic:
symm
Proof state after:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -b = a
Theorem: MyRing.eq_neg_of_add_eq_zeroαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ -b = a
Tactic:
apply neg_eq_of_add_eq_zero
Proof state after:
case h
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ b + a = 0
Theorem: MyRing.eq_neg_of_add_eq_zeroαα
Proof state before:
case h
R : Type u_1
inst✝ : Ring R
a b : R
h : a + b = 0
⊢ b + a = 0
Tactic:
rw [add_comm, h]
Proof state after:
no goals
Theorem: MyRing.neg_zeroαα
Proof state before:
R : Type u_1
inst✝ : Ring R
⊢ -0 = 0
Tactic:
apply neg_eq_of_add_eq_zero
Proof state after:
case h
R : Type u_1
inst✝ : Ring R
⊢ 0 + 0 = 0
Theorem: MyRing.neg_zeroαα
Proof state before:
case h
R : Type u_1
inst✝ : Ring R
⊢ 0 + 0 = 0
Tactic:
rw [add_zero]
Proof state after:
no goals
Theorem: MyRing.neg_negαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ - -a = a
Tactic:
apply neg_eq_of_add_eq_zero
Proof state after:
case h
R : Type u_1
inst✝ : Ring R
a : R
⊢ -a + a = 0
Theorem: MyRing.neg_negαα
Proof state before:
case h
R : Type u_1
inst✝ : Ring R
a : R
⊢ -a + a = 0
Tactic:
rw [add_left_neg]
Proof state after:
no goals
Theorem: MyRing.self_sub
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ a - a = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: MyRing.self_subαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ a - a = 0
Tactic:
rw [sub_eq_add_neg, add_right_neg]
Proof state after:
no goals
Theorem: MyRing.one_add_one_eq_two
Proof state before:
R : Type u_1
inst✝ : Ring R
⊢ 1 + 1 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: MyRing.two_mul
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ 2 * a = a + a
Tactic:
sorry
Proof state after:
no goals
Theorem: MyRing.two_mulαα
Proof state before:
R : Type u_1
inst✝ : Ring R
a : R
⊢ 2 * a = a + a
Tactic:
rw [← one_add_one_eq_two, add_mul, one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_right_inv
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.mul_one
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
⊢ a * 1 = a
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.mul_inv_rev
Proof state before:
G : Type u_1
inst✝ : Group G
a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic:
sorry
Proof state after:
no goals
Theorem: MyGroup.mul_right_invαα
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
Tactic:
have h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1 := by
  rw [mul_assoc, ← mul_assoc a⁻¹ a, mul_left_inv, one_mul, mul_left_inv]
Proof state after:
G : Type u_1
inst✝ : Group G
a : G
h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
⊢ a * a⁻¹ = 1
Theorem: MyGroup.mul_right_invαα
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
h : (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
⊢ a * a⁻¹ = 1
Tactic:
rw [← h, ← mul_assoc, mul_left_inv, one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_right_invαα
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
⊢ (a * a⁻¹)⁻¹ * (a * a⁻¹ * (a * a⁻¹)) = 1
Tactic:
rw [mul_assoc, ← mul_assoc a⁻¹ a, mul_left_inv, one_mul, mul_left_inv]
Proof state after:
no goals
Theorem: MyGroup.mul_oneαα
Proof state before:
G : Type u_1
inst✝ : Group G
a : G
⊢ a * 1 = a
Tactic:
rw [← mul_left_inv a, ← mul_assoc, mul_right_inv, one_mul]
Proof state after:
no goals
Theorem: MyGroup.mul_inv_revαα
Proof state before:
G : Type u_1
inst✝ : Group G
a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic:
rw [← one_mul (b⁻¹ * a⁻¹), ← mul_left_inv (a * b), mul_assoc, mul_assoc, ← mul_assoc b b⁻¹,
  mul_right_inv, one_mul, mul_right_inv, mul_one]
Proof state after:
no goals
Theorem: C05S03.two_le
Proof state before:
m : ℕ
h0 : m ≠ 0
h1 : m ≠ 1
⊢ 2 ≤ m
Tactic:
cases m
Proof state after:
case zero
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 2 ≤ 0

case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
⊢ 2 ≤ n✝ + 1
Theorem: C05S03.two_le
Proof state before:
case zero
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 2 ≤ 0

case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
⊢ 2 ≤ n✝ + 1
Tactic:
contradiction
Proof state after:
case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
⊢ 2 ≤ n✝ + 1
Theorem: C05S03.two_le
Proof state before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
⊢ 2 ≤ m + 1
Tactic:
case succ m =>
  cases m; contradiction
  repeat' apply Nat.succ_le_succ
  apply zero_le
Proof state after:
no goals
Theorem: C05S03.two_le
Proof state before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
⊢ 2 ≤ m + 1
Tactic:
cases m
Proof state after:
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 2 ≤ 0 + 1

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 2 ≤ n✝ + 1 + 1
Theorem: C05S03.two_le
Proof state before:
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
⊢ 2 ≤ 0 + 1

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 2 ≤ n✝ + 1 + 1
Tactic:
contradiction
Proof state after:
case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 2 ≤ n✝ + 1 + 1
Theorem: C05S03.two_le
Proof state before:
case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 2 ≤ n✝ + 1 + 1
Tactic:
repeat' apply Nat.succ_le_succ
Proof state after:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 0 ≤ n✝
Theorem: C05S03.two_le
Proof state before:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 0 ≤ n✝
Tactic:
apply zero_le
Proof state after:
no goals
Theorem: C05S03.two_le
Proof state before:
case succ.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 1 ≤ n✝ + 1
Tactic:
apply Nat.succ_le_succ
Proof state after:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
⊢ 0 ≤ n✝
Theorem: C05S03.exists_prime_factor
Proof state before:
n : ℕ
h : 2 ≤ n
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
by_cases np : n.Prime
Proof state after:
case pos
n : ℕ
h : 2 ≤ n
np : n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n

case neg
n : ℕ
h : 2 ≤ n
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg
n : ℕ
h : 2 ≤ n
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
induction' n using Nat.strong_induction_on with n ih
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
rw [Nat.prime_def_lt] at np
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
push_neg at np
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
rcases np h with ⟨m, mltn, mdvdn, mne1⟩
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
have : m ≠ 0 := by
  intro mz
  rw [mz, zero_dvd_iff] at mdvdn
  linarith
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
have mgt2 : 2 ≤ m := two_le this mne1
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
by_cases mp : m.Prime
Proof state after:
case pos
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n

case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
. rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
  use p, pp
  apply pdvd.trans mdvdn
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor
Proof state before:
case pos
n : ℕ
h : 2 ≤ n
np : n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
use n, np
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ m ≠ 0
Tactic:
intro mz
Proof state after:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mz : m = 0
⊢ False
Theorem: C05S03.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mz : m = 0
⊢ False
Tactic:
rw [mz, zero_dvd_iff] at mdvdn
Proof state after:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : n = 0
mne1 : m ≠ 1
mz : m = 0
⊢ False
Theorem: C05S03.exists_prime_factor
Proof state before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : n = 0
mne1 : m ≠ 1
mz : m = 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor
Proof state before:
case pos
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
use m, mp
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
Proof state after:
case neg.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
⊢ ∃ p, p.Prime ∧ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case neg.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
⊢ ∃ p, p.Prime ∧ p ∣ n
Tactic:
use p, pp
Proof state after:
case right
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
⊢ p ∣ n
Theorem: C05S03.exists_prime_factor
Proof state before:
case right
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬m.Prime
p : ℕ
pp : p.Prime
pdvd : p ∣ m
⊢ p ∣ n
Tactic:
apply pdvd.trans mdvdn
Proof state after:
no goals
Theorem: C05S03.primes_infinite
Proof state before:
⊢ ∀ (n : ℕ), ∃ p > n, p.Prime
Tactic:
intro n
Proof state after:
n : ℕ
⊢ ∃ p > n, p.Prime
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
⊢ ∃ p > n, p.Prime
Tactic:
have : 2 ≤ Nat.factorial (n + 1) + 1 := by
  apply Nat.succ_le_succ
  exact Nat.succ_le_of_lt (Nat.factorial_pos _)
Proof state after:
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime
Tactic:
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
Proof state after:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime
Tactic:
refine' ⟨p, _, pp⟩
Proof state after:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ p > n
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ p > n
Tactic:
by_contra ple
Proof state after:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : ¬p > n
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : ¬p > n
⊢ False
Tactic:
push_neg  at ple
Proof state after:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ False
Tactic:
have : p ∣ Nat.factorial (n + 1) := by
  apply Nat.dvd_factorial
  apply pp.pos
  linarith
Proof state after:
case intro.intro
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ False
Tactic:
have : p ∣ 1 := by
  convert Nat.dvd_sub' pdvd this
  simp
Proof state after:
case intro.intro
n : ℕ
this✝¹ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this✝ : p ∣ (n + 1).factorial
this : p ∣ 1
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this✝¹ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this✝ : p ∣ (n + 1).factorial
this : p ∣ 1
⊢ False
Tactic:
have := Nat.le_of_dvd zero_lt_one this
Proof state after:
case intro.intro
n : ℕ
this✝² : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this✝¹ : p ∣ (n + 1).factorial
this✝ : p ∣ 1
this : p ≤ 1
⊢ False
Theorem: C05S03.primes_infinite
Proof state before:
case intro.intro
n : ℕ
this✝² : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this✝¹ : p ∣ (n + 1).factorial
this✝ : p ∣ 1
this : p ≤ 1
⊢ False
Tactic:
linarith [pp.two_le]
Proof state after:
no goals
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
⊢ 2 ≤ (n + 1).factorial + 1
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a
n : ℕ
⊢ 1 ≤ (n + 1).factorial
Theorem: C05S03.primes_infinite
Proof state before:
case a
n : ℕ
⊢ 1 ≤ (n + 1).factorial
Tactic:
exact Nat.succ_le_of_lt (Nat.factorial_pos _)
Proof state after:
no goals
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ∣ (n + 1).factorial
Tactic:
apply Nat.dvd_factorial
Proof state after:
case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ 0 < p

case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ≤ n + 1
Theorem: C05S03.primes_infinite
Proof state before:
case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ 0 < p

case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ≤ n + 1
Tactic:
apply pp.pos
Proof state after:
case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ≤ n + 1
Theorem: C05S03.primes_infinite
Proof state before:
case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ≤ n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: C05S03.primes_infinite
Proof state before:
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ p ∣ 1
Tactic:
convert Nat.dvd_sub' pdvd this
Proof state after:
case h.e'_4
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ 1 = (n + 1).factorial + 1 - (n + 1).factorial
Theorem: C05S03.primes_infinite
Proof state before:
case h.e'_4
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ 1 = (n + 1).factorial + 1 - (n + 1).factorial
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.Prime.eq_of_dvd_of_prime
Proof state before:
p q : ℕ
prime_p : p.Prime
prime_q : q.Prime
h : p ∣ q
⊢ p = q
Tactic:
cases prime_q.eq_one_or_self_of_dvd _ h
Proof state after:
case inl
p q : ℕ
prime_p : p.Prime
prime_q : q.Prime
h : p ∣ q
h✝ : p = 1
⊢ p = q

case inr
p q : ℕ
prime_p : p.Prime
prime_q : q.Prime
h : p ∣ q
h✝ : p = q
⊢ p = q
Theorem: Nat.Prime.eq_of_dvd_of_prime
Proof state before:
case inr
p q : ℕ
prime_p : p.Prime
prime_q : q.Prime
h : p ∣ q
h✝ : p = q
⊢ p = q
Tactic:
assumption
Proof state after:
no goals
Theorem: Nat.Prime.eq_of_dvd_of_prime
Proof state before:
case inl
p q : ℕ
prime_p : p.Prime
prime_q : q.Prime
h : p ∣ q
h✝ : p = 1
⊢ p = q
Tactic:
linarith [prime_p.two_le]
Proof state after:
no goals
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
s : Finset ℕ
p : ℕ
prime_p : p.Prime
⊢ (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
Tactic:
intro h₀ h₁
Proof state after:
s : Finset ℕ
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ s, n.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p ∈ s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
s : Finset ℕ
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ s, n.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p ∈ s
Tactic:
induction' s using Finset.induction_on with a s ans ih
Proof state after:
case empty
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ ∅, n.Prime
h₁ : p ∣ ∏ n ∈ ∅, n
⊢ p ∈ ∅

case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : ∀ n ∈ insert a s, n.Prime
h₁ : p ∣ ∏ n ∈ insert a s, n
⊢ p ∈ insert a s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : ∀ n ∈ insert a s, n.Prime
h₁ : p ∣ ∏ n ∈ insert a s, n
⊢ p ∈ insert a s
Tactic:
simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁
Proof state after:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p ∈ insert a s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p ∈ insert a s
Tactic:
rw [mem_insert]
Proof state after:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p = a ∨ p ∈ s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p = a ∨ p ∈ s
Tactic:
rcases h₁ with h₁ | h₁
Proof state after:
case insert.inl
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a
⊢ p = a ∨ p ∈ s

case insert.inr
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p = a ∨ p ∈ s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert.inr
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p = a ∨ p ∈ s
Tactic:
right
Proof state after:
case insert.inr.h
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p ∈ s
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert.inr.h
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ ∏ n ∈ s, n
⊢ p ∈ s
Tactic:
exact ih h₀.2 h₁
Proof state after:
no goals