Theorem: Imo1989P5.get_primes (Compfiles/Imo1989P5.lean)

State before:
case zero
m : ℕ
⊢ ∃ lst, lst.length = 0 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
Tactic:
use ∅
State after:
case h
m : ℕ
⊢ ∅.length = 0 ∧ ∅.Nodup ∧ ∀ x ∈ ∅, x.Prime ∧ m ≤ x

State before:
case h
m : ℕ
⊢ ∅.length = 0 ∧ ∅.Nodup ∧ ∀ x ∈ ∅, x.Prime ∧ m ≤ x
Tactic:
simp
State after:
no goals

State before:
case succ
m n : ℕ
ih : ∃ lst, lst.length = n ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
Tactic:
obtain ⟨l', hl', hlnd, hlp⟩ := ih
State after:
case succ.intro.intro.intro
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x

State before:
case succ.intro.intro.intro
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
Tactic:
obtain ⟨mx, hmx⟩ := list_upper_bound l'
State after:
case succ.intro.intro.intro.intro
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x

State before:
case succ.intro.intro.intro.intro
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
Tactic:
obtain ⟨p, hpm, hp⟩ := Nat.exists_infinite_primes (max m (mx + 1))
State after:
case succ.intro.intro.intro.intro.intro.intro
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x

State before:
case succ.intro.intro.intro.intro.intro.intro
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ ∃ lst, lst.length = n + 1 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
Tactic:
use p :: l'
State after:
case h
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').length = n + 1 ∧ (p :: l').Nodup ∧ ∀ x ∈ p :: l', x.Prime ∧ m ≤ x

State before:
case h
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').length = n + 1 ∧ (p :: l').Nodup ∧ ∀ x ∈ p :: l', x.Prime ∧ m ≤ x
Tactic:
constructor
State after:
case h.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').length = n + 1

case h.right
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').Nodup ∧ ∀ x ∈ p :: l', x.Prime ∧ m ≤ x

State before:
case h.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').length = n + 1
Tactic:
exact Iff.mpr Nat.succ_inj' hl'
State after:
no goals

State before:
case h.right
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').Nodup ∧ ∀ x ∈ p :: l', x.Prime ∧ m ≤ x
Tactic:
constructor
State after:
case h.right.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').Nodup

case h.right.right
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ ∀ x ∈ p :: l', x.Prime ∧ m ≤ x

State before:
case h.right.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ (p :: l').Nodup
Tactic:
rw [List.nodup_cons]
State after:
case h.right.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ p ∉ l' ∧ l'.Nodup

State before:
case h.right.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ p ∉ l' ∧ l'.Nodup
Tactic:
constructor
State after:
case h.right.left.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ p ∉ l'

case h.right.left.right
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ l'.Nodup

State before:
case h.right.left.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ p ∉ l'
Tactic:
intro hpl
State after:
case h.right.left.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
hpl : p ∈ l'
⊢ False

State before:
case h.right.left.left
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
hpl : p ∈ l'
⊢ False
Tactic:
exact Iff.mpr Nat.not_le (le_of_max_le_right hpm) (hmx p hpl)
State after:
no goals

State before:
case h.right.left.right
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ l'.Nodup
Tactic:
exact hlnd
State after:
no goals

State before:
case h.right.right
m n : ℕ
l' : List ℕ
hl' : l'.length = n
hlnd : l'.Nodup
hlp : ∀ x ∈ l', x.Prime ∧ m ≤ x
mx : ℕ
hmx : ∀ x ∈ l', x ≤ mx
p : ℕ
hpm : max m (mx + 1) ≤ p
hp : p.Prime
⊢ ∀ x ∈ p :: l', x.Prime ∧ m ≤ x
Tactic:
aesop
State after:
no goals