Theorem: Usa1982P4.not_prime_of_dvd (Compfiles/Usa1982P4.lean)

State before:
⊢ ∀ n ≥ 2, (∃ m ≥ 2, m ≠ n ∧ m ∣ n) → ¬Prime n
Tactic:
intro n hn h p
State after:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
⊢ False

State before:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
⊢ False
Tactic:
have ngt0 : 0 < n := by omega
State after:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
ngt0 : 0 < n
⊢ False

State before:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
ngt0 : 0 < n
⊢ False
Tactic:
have p := (Nat.prime_iff).mpr p
State after:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
⊢ False

State before:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
⊢ False
Tactic:
obtain ⟨m, ⟨h1, ⟨h2, h3⟩⟩⟩ := h
State after:
case intro.intro.intro
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ False

State before:
case intro.intro.intro
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ False
Tactic:
apply (Nat.not_prime_iff_minFac_lt hn).mpr _ p
State after:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ n.minFac < n

State before:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
⊢ n.minFac < n
Tactic:
have h4 : m < n := lt_of_le_of_ne (Nat.le_of_dvd ngt0 h3) h2
State after:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
⊢ n.minFac < n

State before:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
⊢ n.minFac < n
Tactic:
have h5 : Nat.minFac n ≤ m := Nat.minFac_le_of_dvd h1 h3
State after:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
h5 : n.minFac ≤ m
⊢ n.minFac < n

State before:
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
h5 : n.minFac ≤ m
⊢ n.minFac < n
Tactic:
apply lt_of_le_of_lt h5 h4
State after:
no goals

State before:
n : ℕ
hn : n ≥ 2
h : ∃ m ≥ 2, m ≠ n ∧ m ∣ n
p : Prime n
⊢ 0 < n
Tactic:
omega
State after:
no goals