Theorem: Imo1981P3.ProblemPredicate.m_le_n (Compfiles/Imo1981P3.lean)

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
⊢ m ≤ n
Tactic:
by_contra h2
State after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
⊢ False

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
⊢ False
Tactic:
have h3 : 1 = (n * (n - m) - m ^ 2) ^ 2 := by linear_combination - h1.eq_one
State after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
⊢ False

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
⊢ False
Tactic:
have h4 : n * (n - m) - m ^ 2 < -1 := by nlinarith [h1.n_range.left]
State after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
⊢ False

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
⊢ False
Tactic:
have h5 : 1 < (n * (n - m) - m ^ 2) ^ 2 := by nlinarith
State after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
h5 : 1 < (n * (n - m) - m ^ 2) ^ 2
⊢ False

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
h5 : 1 < (n * (n - m) - m ^ 2) ^ 2
⊢ False
Tactic:
exact h5.ne h3
State after:
no goals

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
⊢ 1 = (n * (n - m) - m ^ 2) ^ 2
Tactic:
linear_combination - h1.eq_one
State after:
no goals

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
⊢ n * (n - m) - m ^ 2 < -1
Tactic:
nlinarith [h1.n_range.left]
State after:
no goals

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
⊢ 1 < (n * (n - m) - m ^ 2) ^ 2
Tactic:
nlinarith
State after:
no goals