Theorem: Imo1981P3.k_bound (Compfiles/Imo1981P3.lean)

State before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
have h2 : 0 ≤ m := h1.m_range.left.le
State after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 0 ≤ m
⊢ m ^ 2 + n ^ 2 ≤ ↑M

State before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 0 ≤ m
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
have h3 : 0 ≤ n := h1.n_range.left.le
State after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M

State before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
rw [← natAbs_of_nonneg h2, ← natAbs_of_nonneg h3] at h1
State after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M

State before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h2 : 0 ≤ m
h3 : 0 ≤ n
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
clear h2 h3
State after:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
⊢ m ^ 2 + n ^ 2 ≤ ↑M

State before:
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
obtain ⟨h4 : m.natAbs ≤ fib K, h5 : n.natAbs ≤ fib (K + 1)⟩ := m_n_bounds HK h1
State after:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
⊢ m ^ 2 + n ^ 2 ≤ ↑M

State before:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
have h6 : m ^ 2 ≤ (fib K : ℤ) ^ 2 := Int.natAbs_le_iff_sq_le.mp h4
State after:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
h6 : m ^ 2 ≤ ↑K.fib ^ 2
⊢ m ^ 2 + n ^ 2 ≤ ↑M

State before:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
h6 : m ^ 2 ≤ ↑K.fib ^ 2
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
have h7 : n ^ 2 ≤ (fib (K + 1) : ℤ) ^ 2 := Int.natAbs_le_iff_sq_le.mp h5
State after:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
h6 : m ^ 2 ≤ ↑K.fib ^ 2
h7 : n ^ 2 ≤ ↑(K + 1).fib ^ 2
⊢ m ^ 2 + n ^ 2 ≤ ↑M

State before:
case intro
N K : ℕ
HK : N < K.fib + (K + 1).fib
M : ℕ
HM : M = K.fib ^ 2 + (K + 1).fib ^ 2
m n : ℤ
h1 : ProblemPredicate N ↑m.natAbs ↑n.natAbs
h4 : m.natAbs ≤ K.fib
h5 : n.natAbs ≤ (K + 1).fib
h6 : m ^ 2 ≤ ↑K.fib ^ 2
h7 : n ^ 2 ≤ ↑(K + 1).fib ^ 2
⊢ m ^ 2 + n ^ 2 ≤ ↑M
Tactic:
linarith
State after:
no goals