Theorem: HTPI.exists_prime_factor (HTPILib/Chap7.lean)

State before:
⊢ ∀ (n : ℕ), 2 ≤ n → ∃ p, prime_factor p n
Tactic:
by_strong_induc
State after:
⊢ ∀ (n : ℕ), (∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1) → 2 ≤ n → ∃ p, prime_factor p n

State before:
⊢ ∀ (n : ℕ), (∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1) → 2 ≤ n → ∃ p, prime_factor p n
Tactic:
fix n : Nat
State after:
n : ℕ
⊢ (∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1) → 2 ≤ n → ∃ p, prime_factor p n

State before:
n : ℕ
⊢ (∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1) → 2 ≤ n → ∃ p, prime_factor p n
Tactic:
assume ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ (p : Nat), prime_factor p n_1
State after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
⊢ 2 ≤ n → ∃ p, prime_factor p n

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
⊢ 2 ≤ n → ∃ p, prime_factor p n
Tactic:
assume h1 : 2 ≤ n
State after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
⊢ ∃ p, prime_factor p n

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
⊢ ∃ p, prime_factor p n
Tactic:
by_cases h2 : prime n
State after:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ ∃ p, prime_factor p n

case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬prime n
⊢ ∃ p, prime_factor p n

State before:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ ∃ p, prime_factor p n
Tactic:
apply Exists.intro n
State after:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ prime_factor n n

State before:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ prime_factor n n
Tactic:
define
State after:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ prime n ∧ n ∣ n

State before:
case pos
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : prime n
⊢ prime n ∧ n ∣ n
Tactic:
show prime n ∧ n ∣ n from And.intro h2 (dvd_self n)
State after:
no goals

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬prime n
⊢ ∃ p, prime_factor p n
Tactic:
define at h2
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬(2 ≤ n ∧ ¬∃ a b, a * b = n ∧ a < n ∧ b < n)
⊢ ∃ p, prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬(2 ≤ n ∧ ¬∃ a b, a * b = n ∧ a < n ∧ b < n)
⊢ ∃ p, prime_factor p n
Tactic:
demorgan at h2
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬2 ≤ n ∨ ∃ a b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ¬2 ≤ n ∨ ∃ a b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Tactic:
disj_syll h2 h1
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Tactic:
obtain (a : Nat) (h3 : ∃ (b : Nat), a * b = n ∧ a < n ∧ b < n) from h2
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Tactic:
obtain (b : Nat) (h4 : a * b = n ∧ a < n ∧ b < n) from h3
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
⊢ ∃ p, prime_factor p n
Tactic:
have h5 : 2 ≤ a := by
  by_contra h6
  have h7 : a ≤ 1 := by linarith
  have h8 : n ≤ b :=
    calc n
      _ = a * b := h4.left.symm
      _ ≤ 1 * b := by rel [h7]
      _ = b := by ring
  linarith        done
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
⊢ ∃ p, prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
⊢ ∃ p, prime_factor p n
Tactic:
have h6 : ∃ (p : Nat), prime_factor p a := ih a h4.right.left h5
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
⊢ ∃ p, prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
⊢ ∃ p, prime_factor p n
Tactic:
obtain (p : Nat) (h7 : prime_factor p a) from h6
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ ∃ p, prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ ∃ p, prime_factor p n
Tactic:
apply Exists.intro p
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ prime_factor p n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ prime_factor p n
Tactic:
define
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ prime p ∧ p ∣ n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime_factor p a
⊢ prime p ∧ p ∣ n
Tactic:
define at h7
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ prime p ∧ p ∣ n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ prime p ∧ p ∣ n
Tactic:
apply And.intro h7.left
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ p ∣ n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ p ∣ n
Tactic:
have h8 : a ∣ n := by
  apply Exists.intro b
  show n = a * b from (h4.left).symm
  done
State after:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
h8 : a ∣ n
⊢ p ∣ n

State before:
case neg
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
h8 : a ∣ n
⊢ p ∣ n
Tactic:
show p ∣ n from dvd_trans h7.right h8
State after:
no goals

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
⊢ 2 ≤ a
Tactic:
by_contra h6
State after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
⊢ False

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
⊢ False
Tactic:
have h7 : a ≤ 1 := by linarith
State after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
⊢ False

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
⊢ False
Tactic:
have h8 : n ≤ b :=
  calc n
    _ = a * b := h4.left.symm
    _ ≤ 1 * b := by rel [h7]
    _ = b := by ring
State after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
h8 : n ≤ b
⊢ False

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
h8 : n ≤ b
⊢ False
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
⊢ a ≤ 1
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
⊢ a * b ≤ 1 * b
Tactic:
rel [h7]
State after:
no goals

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h6 : ¬2 ≤ a
h7 : a ≤ 1
⊢ 1 * b = b
Tactic:
ring
State after:
no goals

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ a ∣ n
Tactic:
apply Exists.intro b
State after:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ n = a * b

State before:
n : ℕ
ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ p, prime_factor p n_1
h1 : 2 ≤ n
h2 : ∃ a b, a * b = n ∧ a < n ∧ b < n
a : ℕ
h3 : ∃ b, a * b = n ∧ a < n ∧ b < n
b : ℕ
h4 : a * b = n ∧ a < n ∧ b < n
h5 : 2 ≤ a
h6 : ∃ p, prime_factor p a
p : ℕ
h7 : prime p ∧ p ∣ a
⊢ n = a * b
Tactic:
show n = a * b from (h4.left).symm
State after:
no goals