internlm/Lean-Github huggingface dataset:
Theorem: Imo1989P5.coprime_of_product
Proof state before:
n : ℕ
lst : List ℕ
h : ∀ y ∈ lst, n.Coprime y
⊢ n.Coprime lst.prod
Tactic:
induction lst with
| nil => simp only [List.prod_nil, Nat.coprime_one_right_eq_true]
| cons x xs ih =>
  have hy : ∀ (y : ℕ), y ∈ xs → Nat.Coprime n y :=
    fun y hy ↦ h y (List.mem_cons.mpr (Or.inr hy))
  have h1 := h x (by simp)
  rw [List.prod_cons]
  exact Nat.Coprime.mul_right h1 (ih hy)
Proof state after:
no goals
Theorem: Imo1989P5.coprime_of_product
Proof state before:
case nil
n : ℕ
h : ∀ y ∈ [], n.Coprime y
⊢ n.Coprime [].prod
Tactic:
simp only [List.prod_nil, Nat.coprime_one_right_eq_true]
Proof state after:
no goals
Theorem: Imo1989P5.coprime_of_product
Proof state before:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
⊢ n.Coprime (x :: xs).prod
Tactic:
have hy : ∀ (y : ℕ), y ∈ xs → Nat.Coprime n y :=
  fun y hy ↦ h y (List.mem_cons.mpr (Or.inr hy))
Proof state after:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
⊢ n.Coprime (x :: xs).prod
Theorem: Imo1989P5.coprime_of_product
Proof state before:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
⊢ n.Coprime (x :: xs).prod
Tactic:
have h1 := h x (by simp)
Proof state after:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x :: xs).prod
Theorem: Imo1989P5.coprime_of_product
Proof state before:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x :: xs).prod
Tactic:
rw [List.prod_cons]
Proof state after:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x * xs.prod)
Theorem: Imo1989P5.coprime_of_product
Proof state before:
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
h1 : n.Coprime x
⊢ n.Coprime (x * xs.prod)
Tactic:
exact Nat.Coprime.mul_right h1 (ih hy)
Proof state after:
no goals
Theorem: Imo1989P5.coprime_of_product
Proof state before:
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
⊢ x ∈ x :: xs
Tactic:
simp
Proof state after:
no goals
Theorem: Imo1989P5.modulus_of_product
Proof state before:
a b : ℕ
xs : List ℕ
h : a ≡ b [MOD xs.prod]
x : ℕ
hx : x ∈ xs
⊢ a ≡ b [MOD x]
Tactic:
induction xs with
| nil => aesop
| cons y ys ih =>
  rw [List.prod_cons] at h
  cases hx with
  | head => exact Nat.ModEq.of_mul_right _ h
  | tail w hw =>
    exact ih (Nat.ModEq.of_mul_left _ h) hw
Proof state after:
no goals
Theorem: Imo1989P5.modulus_of_product
Proof state before:
case nil
a b x : ℕ
h : a ≡ b [MOD [].prod]
hx : x ∈ []
⊢ a ≡ b [MOD x]
Tactic:
aesop
Proof state after:
no goals
Theorem: Imo1989P5.modulus_of_product
Proof state before:
case cons
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD (y :: ys).prod]
hx : x ∈ y :: ys
⊢ a ≡ b [MOD x]
Tactic:
rw [List.prod_cons] at h
Proof state after:
case cons
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD y * ys.prod]
hx : x ∈ y :: ys
⊢ a ≡ b [MOD x]
Theorem: Imo1989P5.modulus_of_product
Proof state before:
case cons
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD y * ys.prod]
hx : x ∈ y :: ys
⊢ a ≡ b [MOD x]
Tactic:
cases hx with
| head => exact Nat.ModEq.of_mul_right _ h
| tail w hw =>
  exact ih (Nat.ModEq.of_mul_left _ h) hw
Proof state after:
no goals
Theorem: Imo1989P5.modulus_of_product
Proof state before:
case cons.head
a b x : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD x * ys.prod]
⊢ a ≡ b [MOD x]
Tactic:
exact Nat.ModEq.of_mul_right _ h
Proof state after:
no goals
Theorem: Imo1989P5.modulus_of_product
Proof state before:
case cons.tail
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD y * ys.prod]
hw : List.Mem x ys
⊢ a ≡ b [MOD x]
Tactic:
exact ih (Nat.ModEq.of_mul_left _ h) hw
Proof state after:
no goals
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case nil
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) []
⊢ ∃ m, ∀ x ∈ [], m ≡ x.remainder [MOD x.modulus]
Tactic:
use 0
Proof state after:
case h
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) []
⊢ ∀ x ∈ [], 0 ≡ x.remainder [MOD x.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case h
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) []
⊢ ∀ x ∈ [], 0 ≡ x.remainder [MOD x.modulus]
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case cons
x : ChinesePair
xs : List ChinesePair
ih : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs → ∃ m, ∀ x ∈ xs, m ≡ x.remainder [MOD x.modulus]
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
obtain ⟨b, hb⟩ := ih x_coprime.tail
Proof state after:
case cons.intro
x : ChinesePair
xs : List ChinesePair
ih : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs → ∃ m, ∀ x ∈ xs, m ≡ x.remainder [MOD x.modulus]
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case cons.intro
x : ChinesePair
xs : List ChinesePair
ih : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs → ∃ m, ∀ x ∈ xs, m ≡ x.remainder [MOD x.modulus]
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
clear ih
Proof state after:
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : List.Pairwise (fun x y => x.modulus.Coprime y.modulus) (x :: xs)
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
rw [List.pairwise_cons] at x_coprime
Proof state after:
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case cons.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
obtain ⟨k, hk1, hk2⟩ := Nat.chineseRemainder h1 x.remainder b
Proof state after:
case cons.intro.mk.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case cons.intro.mk.intro
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
use k
Proof state after:
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ ∀ x_1 ∈ x :: xs, k ≡ x_1.remainder [MOD x_1.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ ∀ x_1 ∈ x :: xs, k ≡ x_1.remainder [MOD x_1.modulus]
Tactic:
intro z hz
Proof state after:
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hz : z ∈ x :: xs
⊢ k ≡ z.remainder [MOD z.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hz : z ∈ x :: xs
⊢ k ≡ z.remainder [MOD z.modulus]
Tactic:
cases hz with
| head => exact hk1
| tail w hw =>
  have h2 := hb z hw
  have h4 := modulus_of_product hk2 _ (List.mem_map_of_mem ChinesePair.modulus hw)
  exact Nat.ModEq.trans h4 h2
Proof state after:
no goals
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
⊢ ∀ y ∈ List.map (fun x => x.modulus) xs, x.modulus.Coprime y
Tactic:
intro z hz
Proof state after:
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
z : ℕ
hz : z ∈ List.map (fun x => x.modulus) xs
⊢ x.modulus.Coprime z
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
z : ℕ
hz : z ∈ List.map (fun x => x.modulus) xs
⊢ x.modulus.Coprime z
Tactic:
aesop
Proof state after:
no goals
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case h.head
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
⊢ k ≡ x.remainder [MOD x.modulus]
Tactic:
exact hk1
Proof state after:
no goals
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
⊢ k ≡ z.remainder [MOD z.modulus]
Tactic:
have h2 := hb z hw
Proof state after:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
h2 : b ≡ z.remainder [MOD z.modulus]
⊢ k ≡ z.remainder [MOD z.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
h2 : b ≡ z.remainder [MOD z.modulus]
⊢ k ≡ z.remainder [MOD z.modulus]
Tactic:
have h4 := modulus_of_product hk2 _ (List.mem_map_of_mem ChinesePair.modulus hw)
Proof state after:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
h2 : b ≡ z.remainder [MOD z.modulus]
h4 : k ≡ b [MOD z.modulus]
⊢ k ≡ z.remainder [MOD z.modulus]
Theorem: Imo1989P5.general_chinese_remainder
Proof state before:
case h.tail
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hw : List.Mem z xs
h2 : b ≡ z.remainder [MOD z.modulus]
h4 : k ≡ b [MOD z.modulus]
⊢ k ≡ z.remainder [MOD z.modulus]
Tactic:
exact Nat.ModEq.trans h4 h2
Proof state after:
no goals
Theorem: Imo1989P5.list_upper_bound
Proof state before:
l : List ℕ
⊢ ∃ m, ∀ x ∈ l, x ≤ m
Tactic:
use List.foldr max ⊥ l
Proof state after:
case h
l : List ℕ
⊢ ∀ x ∈ l, x ≤ List.foldr max ⊥ l
Theorem: Imo1989P5.list_upper_bound
Proof state before:
case h
l : List ℕ
⊢ ∀ x ∈ l, x ≤ List.foldr max ⊥ l
Tactic:
intro a ha
Proof state after:
case h
l : List ℕ
a : ℕ
ha : a ∈ l
⊢ a ≤ List.foldr max ⊥ l
Theorem: Imo1989P5.list_upper_bound
Proof state before:
case h
l : List ℕ
a : ℕ
ha : a ∈ l
⊢ a ≤ List.foldr max ⊥ l
Tactic:
exact List.le_max_of_le ha (le_refl _)
Proof state after:
no goals
Theorem: Imo1989P5.get_primes
Proof state before:
case zero
m : ℕ
⊢ ∃ lst, lst.length = 0 ∧ lst.Nodup ∧ ∀ x ∈ lst, x.Prime ∧ m ≤ x
Tactic:
use ∅
Proof state after:
case h
m : ℕ
⊢ ∅.length = 0 ∧ ∅.Nodup ∧ ∀ x ∈ ∅, x.Prime ∧ m ≤ x
Theorem: Imo1989P5.get_primes
Proof state before:
case h
m : ℕ
⊢ ∅.length = 0 ∧ ∅.Nodup ∧ ∀ x ∈ ∅, x.Prime ∧ m ≤ x
Tactic:
simp
Proof state after:
no goals
Theorem: Imo1989P5.get_primes
Proof 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
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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'
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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))
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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'
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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'
Proof state after:
no goals
Theorem: Imo1989P5.get_primes
Proof 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
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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]
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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
Proof 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
Theorem: Imo1989P5.get_primes
Proof 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)
Proof state after:
no goals
Theorem: Imo1989P5.get_primes
Proof 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
Proof state after:
no goals
Theorem: Imo1989P5.get_primes
Proof 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
Proof state after:
no goals
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
⊢ ¬IsPrimePow n
Tactic:
intro hpp
Proof state after:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
hpp : IsPrimePow n
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
hpp : IsPrimePow n
⊢ False
Tactic:
have h0 : n ≠ 0 := IsPrimePow.ne_zero hpp
Proof state after:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
hpp : IsPrimePow n
h0 : n ≠ 0
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
hpp : IsPrimePow n
h0 : n ≠ 0
⊢ False
Tactic:
obtain ⟨r, k, hr, hk, hrk⟩ := hpp
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : Prime r
hk : 0 < k
hrk : r ^ k = n
⊢ False
Theorem: Imo1989P5.not_prime_power_of_two_factors
Proof state before:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : Prime r
hk : 0 < k
hrk : r ^ k = n
⊢ False
Tactic:
rw [← Nat.prime_iff] at hr
Proof state after:
case intro.intro.intro.intro
n p q : ℕ
hp : p.Prime
hq : q.Prime
hpq : p ≠ q
hpn : p ∣ n
hqn : q ∣ n
h0 : n ≠ 0
r k : ℕ
hr : r.Prime
hk : 0 < k
hrk : r ^ k = n
⊢ False