Theorem: primesSuccEqPrimesSelf (FromTheBook/Ch02/Bertrand/ProdPrimes.lean)

State before:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ primes (Finset.range (Nat.succ (Nat.succ n))) = primes (Finset.range (Nat.succ n))
Tactic:
simp [primes]
State after:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (Finset.range (Nat.succ (Nat.succ n))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))

State before:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (Finset.range (Nat.succ (Nat.succ n))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))
Tactic:
rw [Finset.range_succ]
State after:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (insert (n + 1) (Finset.range (n + 1))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))

State before:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (insert (n + 1) (Finset.range (n + 1))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))
Tactic:
simp [Finset.filter_insert]
State after:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Nat.Prime (n + 1) → False

State before:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Nat.Prime (n + 1) → False
Tactic:
assumption
State after:
no goals