internlm/Lean-Github huggingface dataset:
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case empty
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ ∅, n.Prime
h₁ : p ∣ ∏ n ∈ ∅, n
⊢ p ∈ ∅
Tactic:
simp at h₁
Proof state after:
case empty
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ ∅, n.Prime
h₁ : p = 1
⊢ p ∈ ∅
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case empty
p : ℕ
prime_p : p.Prime
h₀ : ∀ n ∈ ∅, n.Prime
h₁ : p = 1
⊢ p ∈ ∅
Tactic:
linarith [prime_p.two_le]
Proof state after:
no goals
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
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
Tactic:
left
Proof state after:
case insert.inl.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 ∣ a
⊢ p = a
Theorem: C05S03.mem_of_dvd_prod_primes
Proof state before:
case insert.inl.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 ∣ a
⊢ p = a
Tactic:
exact prime_p.eq_of_dvd_of_prime h₀.1 h₁
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof state before:
⊢ ∀ (s : Finset ℕ), ∃ p, p.Prime ∧ p ∉ s
Tactic:
intro s
Proof state after:
s : Finset ℕ
⊢ ∃ p, p.Prime ∧ p ∉ s
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
⊢ ∃ p, p.Prime ∧ p ∉ s
Tactic:
by_contra h
Proof state after:
s : Finset ℕ
h : ¬∃ p, p.Prime ∧ p ∉ s
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ¬∃ p, p.Prime ∧ p ∉ s
⊢ False
Tactic:
push_neg  at h
Proof state after:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
⊢ False
Tactic:
set s' := s.filter Nat.Prime with s'_def
Proof state after:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
⊢ False
Tactic:
have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime := by
  intro n
  simp [s'_def]
  apply h
Proof state after:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ False
Tactic:
have : 2 ≤ (∏ i in s', i) + 1 := by
  apply Nat.succ_le_succ
  apply Nat.succ_le_of_lt
  apply Finset.prod_pos
  intro n ns'
  apply (mem_s'.mp ns').pos
Proof state after:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
⊢ False
Tactic:
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
Proof state after:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
⊢ False
Tactic:
have : p ∣ ∏ i in s', i := by
  apply dvd_prod_of_mem
  rw [mem_s']
  apply pp
Proof state after:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝ : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this : p ∣ ∏ i ∈ s', i
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝ : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this : p ∣ ∏ i ∈ s', i
⊢ False
Tactic:
have : p ∣ 1 := by
  convert Nat.dvd_sub' pdvd this
  simp
Proof state after:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝¹ : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this✝ : p ∣ ∏ i ∈ s', i
this : p ∣ 1
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝¹ : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this✝ : p ∣ ∏ i ∈ s', i
this : p ∣ 1
⊢ False
Tactic:
have := Nat.le_of_dvd zero_lt_one this
Proof state after:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝² : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this✝¹ : p ∣ ∏ i ∈ s', i
this✝ : p ∣ 1
this : p ≤ 1
⊢ False
Theorem: C05S03.primes_infinite'
Proof state before:
case intro.intro
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝² : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this✝¹ : p ∣ ∏ i ∈ s', i
this✝ : p ∣ 1
this : p ≤ 1
⊢ False
Tactic:
linarith [pp.two_le]
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
⊢ ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
Tactic:
intro n
Proof state after:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
n : ℕ
⊢ n ∈ s' ↔ n.Prime
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
n : ℕ
⊢ n ∈ s' ↔ n.Prime
Tactic:
simp [s'_def]
Proof state after:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
n : ℕ
⊢ n.Prime → n ∈ s
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
n : ℕ
⊢ n.Prime → n ∈ s
Tactic:
apply h
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ 2 ≤ ∏ i ∈ s', i + 1
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ 1 ≤ ∏ i ∈ s', i
Theorem: C05S03.primes_infinite'
Proof state before:
case a
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ 1 ≤ ∏ i ∈ s', i
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case a.h
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ 0 < ∏ i ∈ s', i
Theorem: C05S03.primes_infinite'
Proof state before:
case a.h
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ 0 < ∏ i ∈ s', i
Tactic:
apply Finset.prod_pos
Proof state after:
case a.h.h0
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ ∀ i ∈ s', 0 < i
Theorem: C05S03.primes_infinite'
Proof state before:
case a.h.h0
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ ∀ i ∈ s', 0 < i
Tactic:
intro n ns'
Proof state after:
case a.h.h0
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
n : ℕ
ns' : n ∈ s'
⊢ 0 < n
Theorem: C05S03.primes_infinite'
Proof state before:
case a.h.h0
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
n : ℕ
ns' : n ∈ s'
⊢ 0 < n
Tactic:
apply (mem_s'.mp ns').pos
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
⊢ p ∣ ∏ i ∈ s', i
Tactic:
apply dvd_prod_of_mem
Proof state after:
case ha
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
⊢ p ∈ s'
Theorem: C05S03.primes_infinite'
Proof state before:
case ha
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
⊢ p ∈ s'
Tactic:
rw [mem_s']
Proof state after:
case ha
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
⊢ p.Prime
Theorem: C05S03.primes_infinite'
Proof state before:
case ha
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
⊢ p.Prime
Tactic:
apply pp
Proof state after:
no goals
Theorem: C05S03.primes_infinite'
Proof state before:
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝ : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this : p ∣ ∏ i ∈ s', i
⊢ p ∣ 1
Tactic:
convert Nat.dvd_sub' pdvd this
Proof state after:
case h.e'_4
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝ : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this : p ∣ ∏ i ∈ s', i
⊢ 1 = ∏ i ∈ s', i + 1 - ∏ i ∈ s', i
Theorem: C05S03.primes_infinite'
Proof state before:
case h.e'_4
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
this✝ : 2 ≤ ∏ i ∈ s', i + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this : p ∣ ∏ i ∈ s', i
⊢ 1 = ∏ i ∈ s', i + 1 - ∏ i ∈ s', i
Tactic:
simp
Proof state after:
no goals
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
Q : ℕ → Prop
⊢ (∃ s, ∀ (k : ℕ), Q k → k ∈ s) → ∃ n, ∀ (k : ℕ), Q k → k < n
Tactic:
rintro ⟨s, hs⟩
Proof state after:
case intro
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∃ n, ∀ (k : ℕ), Q k → k < n
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case intro
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∃ n, ∀ (k : ℕ), Q k → k < n
Tactic:
use s.sup id + 1
Proof state after:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∀ (k : ℕ), Q k → k < s.sup id + 1
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∀ (k : ℕ), Q k → k < s.sup id + 1
Tactic:
intro k Qk
Proof state after:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k < s.sup id + 1
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k < s.sup id + 1
Tactic:
apply Nat.lt_succ_of_le
Proof state after:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k ≤ s.sup id
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k ≤ s.sup id
Tactic:
show id k ≤ s.sup id
Proof state after:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ id k ≤ s.sup id
Theorem: C05S03.bounded_of_ex_finset
Proof state before:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ id k ≤ s.sup id
Tactic:
apply le_sup (hs k Qk)
Proof state after:
no goals
Theorem: C05S03.ex_finset_of_bounded
Proof state before:
Q : ℕ → Prop
inst✝ : DecidablePred Q
⊢ (∃ n, ∀ (k : ℕ), Q k → k ≤ n) → ∃ s, ∀ (k : ℕ), Q k ↔ k ∈ s
Tactic:
rintro ⟨n, hn⟩
Proof state after:
case intro
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∃ s, ∀ (k : ℕ), Q k ↔ k ∈ s
Theorem: C05S03.ex_finset_of_bounded
Proof state before:
case intro
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∃ s, ∀ (k : ℕ), Q k ↔ k ∈ s
Tactic:
use (range (n + 1)).filter Q
Proof state after:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∀ (k : ℕ), Q k ↔ k ∈ filter Q (range (n + 1))
Theorem: C05S03.ex_finset_of_bounded
Proof state before:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∀ (k : ℕ), Q k ↔ k ∈ filter Q (range (n + 1))
Tactic:
intro k
Proof state after:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
k : ℕ
⊢ Q k ↔ k ∈ filter Q (range (n + 1))
Theorem: C05S03.ex_finset_of_bounded
Proof state before:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
k : ℕ
⊢ Q k ↔ k ∈ filter Q (range (n + 1))
Tactic:
simp [Nat.lt_succ_iff]
Proof state after:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
k : ℕ
⊢ Q k → k ≤ n
Theorem: C05S03.ex_finset_of_bounded
Proof state before:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
k : ℕ
⊢ Q k → k ≤ n
Tactic:
exact hn k
Proof state after:
no goals
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
m n : ℕ
h : m * n % 4 = 3
⊢ m % 4 = 3 ∨ n % 4 = 3
Tactic:
revert h
Proof state after:
m n : ℕ
⊢ m * n % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
m n : ℕ
⊢ m * n % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Tactic:
rw [Nat.mul_mod]
Proof state after:
m n : ℕ
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
m n : ℕ
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Tactic:
have : m % 4 < 4 := Nat.mod_lt m (by norm_num)
Proof state after:
m n : ℕ
this : m % 4 < 4
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
m n : ℕ
this : m % 4 < 4
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Tactic:
interval_cases m % 4 <;> simp [-Nat.mul_mod_mod]
Proof state after:
case «2»
m n : ℕ
this : 2 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
case «2»
m n : ℕ
this : 2 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Tactic:
have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
Proof state after:
case «2»
m n : ℕ
this✝ : 2 < 4
this : n % 4 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
case «2»
m n : ℕ
this✝ : 2 < 4
this : n % 4 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Tactic:
interval_cases n % 4 <;> simp
Proof state after:
no goals
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
m n : ℕ
⊢ 4 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: C05S03.mod_4_eq_3_or_mod_4_eq_3
Proof state before:
m n : ℕ
this : 2 < 4
⊢ 4 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: C05S03.two_le_of_mod_4_eq_3
Proof state before:
case h1
n : ℕ
h : n % 4 = 3
⊢ n ≠ 1
Tactic:
intro neq
Proof state after:
case h1
n : ℕ
h : n % 4 = 3
neq : n = 1
⊢ False
Theorem: C05S03.two_le_of_mod_4_eq_3
Proof state before:
case h1
n : ℕ
h : n % 4 = 3
neq : n = 1
⊢ False
Tactic:
rw [neq] at h
Proof state after:
case h1
n : ℕ
h : 1 % 4 = 3
neq : n = 1
⊢ False
Theorem: C05S03.two_le_of_mod_4_eq_3
Proof state before:
case h1
n : ℕ
h : 1 % 4 = 3
neq : n = 1
⊢ False
Tactic:
norm_num at h
Proof state after:
no goals
Theorem: C05S03.aux
Proof state before:
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n ∧ n / m < n
Tactic:
constructor
Proof state after:
case left
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n

case right
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m < n
Theorem: C05S03.aux
Proof state before:
case right
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m < n
Tactic:
exact Nat.div_lt_self (lt_of_le_of_lt (zero_le _) h₂) h₁
Proof state after:
no goals
Theorem: C05S03.aux
Proof state before:
case left
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n
Tactic:
exact Nat.div_dvd_of_dvd h₀
Proof state after:
no goals
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
n : ℕ
h : n % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
by_cases np : n.Prime
Proof state after:
case pos
n : ℕ
h : n % 4 = 3
np : n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

case neg
n : ℕ
h : n % 4 = 3
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg
n : ℕ
h : n % 4 = 3
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
induction' n using Nat.strong_induction_on with n ih
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬n.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rw [Nat.prime_def_lt] at np
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
push_neg  at np
Proof state after:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
have mge2 : 2 ≤ m := by
  apply two_le _ mne1
  intro mz
  rw [mz, zero_dvd_iff] at mdvdn
  linarith
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
have neq : m * (n / m) = n := Nat.mul_div_cancel' mdvdn
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
have : m % 4 = 3 ∨ n / m % 4 = 3 := by
  apply mod_4_eq_3_or_mod_4_eq_3
  rw [neq, h]
Proof state after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
this : m % 4 = 3 ∨ n / m % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
this : m % 4 = 3 ∨ n / m % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
rcases this with h1 | h1
Proof state after:
case neg.h.intro.intro.intro.inl
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : m % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3

case neg.h.intro.intro.intro.inr
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Theorem: C05S03.exists_prime_factor_mod_4_eq_3
Proof state before:
case neg.h.intro.intro.intro.inr
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3
Tactic:
obtain ⟨nmdvdn, nmltn⟩ := aux mdvdn mge2 mltn
Proof state after:
case neg.h.intro.intro.intro.inr.intro
n : ℕ
ih : ∀ m < n, m % 4 = 3 → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m ∧ p % 4 = 3
h : n % 4 = 3
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mge2 : 2 ≤ m
neq : m * (n / m) = n
h1 : n / m % 4 = 3
nmdvdn : n / m ∣ n
nmltn : n / m < n
⊢ ∃ p, p.Prime ∧ p ∣ n ∧ p % 4 = 3