Theorem: infinity_of_primes₁ (FormalBook/Chapter_01.lean)

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
⊢ ∃ p, p.Prime ∧ p ∉ S
Tactic:
let n := 1 + ∏ q in S, q
State after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
⊢ ∃ p, p.Prime ∧ p ∉ S

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
⊢ ∃ p, p.Prime ∧ p ∉ S
Tactic:
let p := n.minFac
State after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ ∃ p, p.Prime ∧ p ∉ S

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ ∃ p, p.Prime ∧ p ∉ S
Tactic:
use p
State after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ p.Prime ∧ p ∉ S

State before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ p.Prime ∧ p ∉ S
Tactic:
have hp : Nat.Prime p := by
  have hn : 0 < ∏ q in S, q := by
    refine' Finset.prod_pos _
    intros q hq
    refine' Prime.pos <| h hq
  exact Nat.minFac_prime <| Nat.ne_of_gt <| lt_add_of_pos_right 1 hn
State after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p.Prime ∧ p ∉ S

State before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p.Prime ∧ p ∉ S
Tactic:
refine' ⟨hp, _⟩
State after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p ∉ S

State before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p ∉ S
Tactic:
by_contra a
State after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
⊢ False

State before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
⊢ False
Tactic:
have h_p_div_prod : p ∣ ∏ q in S, q := dvd_prod_of_mem (fun (i : ℕ) => i) a
State after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
⊢ False

State before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
⊢ False
Tactic:
have h_p_div_diff : p ∣ n - ∏ q in S, q := dvd_sub' (minFac_dvd n) h_p_div_prod
State after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
⊢ False

State before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
⊢ False
Tactic:
have h_p_div_one : p ∣ 1 := by aesop
State after:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
h_p_div_one : p ∣ 1
⊢ False

State before:
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
h_p_div_one : p ∣ 1
⊢ False
Tactic:
exact Nat.Prime.not_dvd_one hp h_p_div_one
State after:
no goals

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ p.Prime
Tactic:
have hn : 0 < ∏ q in S, q := by
  refine' Finset.prod_pos _
  intros q hq
  refine' Prime.pos <| h hq
State after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hn : 0 < ∏ q ∈ S, q
⊢ p.Prime

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hn : 0 < ∏ q ∈ S, q
⊢ p.Prime
Tactic:
exact Nat.minFac_prime <| Nat.ne_of_gt <| lt_add_of_pos_right 1 hn
State after:
no goals

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ 0 < ∏ q ∈ S, q
Tactic:
refine' Finset.prod_pos _
State after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ ∀ i ∈ S, 0 < i

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ ∀ i ∈ S, 0 < i
Tactic:
intros q hq
State after:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
q : ℕ
hq : q ∈ S
⊢ 0 < q

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
q : ℕ
hq : q ∈ S
⊢ 0 < q
Tactic:
refine' Prime.pos <| h hq
State after:
no goals

State before:
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
h_p_div_diff : p ∣ n - ∏ q ∈ S, q
⊢ p ∣ 1
Tactic:
aesop
State after:
no goals