Theorem: Imo1969P1.polynomial_not_prime (Compfiles/Imo1969P1.lean)

State before:
m : ℕ
h1 : 1 < m
n : ℕ
⊢ ¬(n ^ 4 + 4 * m ^ 4).Prime
Tactic:
have h2 : 1 < (m : ℤ) := Int.ofNat_lt.mpr h1
State after:
m : ℕ
h1 : 1 < m
n : ℕ
h2 : 1 < ↑m
⊢ ¬(n ^ 4 + 4 * m ^ 4).Prime

State before:
m : ℕ
h1 : 1 < m
n : ℕ
h2 : 1 < ↑m
⊢ ¬(n ^ 4 + 4 * m ^ 4).Prime
Tactic:
refine not_prime_of_int_mul' (left_factor_large (n : ℤ) h2) (right_factor_large (n : ℤ) h2) ?_
State after:
m : ℕ
h1 : 1 < m
n : ℕ
h2 : 1 < ↑m
⊢ ((↑n - ↑m) ^ 2 + ↑m ^ 2) * ((↑n + ↑m) ^ 2 + ↑m ^ 2) = ↑(n ^ 4 + 4 * m ^ 4)

State before:
m : ℕ
h1 : 1 < m
n : ℕ
h2 : 1 < ↑m
⊢ ((↑n - ↑m) ^ 2 + ↑m ^ 2) * ((↑n + ↑m) ^ 2 + ↑m ^ 2) = ↑(n ^ 4 + 4 * m ^ 4)
Tactic:
apply factorization
State after:
no goals