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

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
⊢ ProblemPredicate N (n - m) m
Tactic:
obtain (rfl : m = n) | (h3 : m < n) := h1.m_le_n.eq_or_lt
State after:
case inl
N : ℕ
m : ℤ
h1 : ProblemPredicate N m m
h2 : 1 < m
⊢ ProblemPredicate N (m - m) m

case inr
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
⊢ ProblemPredicate N (n - m) m

State before:
case inr
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
⊢ ProblemPredicate N (n - m) m
Tactic:
exact
  { n_range := h1.m_range
    m_range := by
      have h5 : 0 < n - m := sub_pos.mpr h3
      have h6 : n - m < N := by
        calc
          _ < n := sub_lt_self n h1.m_range.left
          _ ≤ N := h1.n_range.right
      exact ⟨h5, h6.le⟩
    eq_one := by linear_combination h1.eq_one }
State after:
no goals

State before:
case inl
N : ℕ
m : ℤ
h1 : ProblemPredicate N m m
h2 : 1 < m
⊢ ProblemPredicate N (m - m) m
Tactic:
have h4 : m = 1 := h1.eq_imp_1
State after:
case inl
N : ℕ
m : ℤ
h1 : ProblemPredicate N m m
h2 : 1 < m
h4 : m = 1
⊢ ProblemPredicate N (m - m) m

State before:
case inl
N : ℕ
m : ℤ
h1 : ProblemPredicate N m m
h2 : 1 < m
h4 : m = 1
⊢ ProblemPredicate N (m - m) m
Tactic:
exact absurd h4.symm h2.ne
State after:
no goals

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
⊢ n - m ∈ Ioc 0 ↑N
Tactic:
have h5 : 0 < n - m := sub_pos.mpr h3
State after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
⊢ n - m ∈ Ioc 0 ↑N

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
⊢ n - m ∈ Ioc 0 ↑N
Tactic:
have h6 : n - m < N := by
  calc
    _ < n := sub_lt_self n h1.m_range.left
    _ ≤ N := h1.n_range.right
State after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
h6 : n - m < ↑N
⊢ n - m ∈ Ioc 0 ↑N

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
h6 : n - m < ↑N
⊢ n - m ∈ Ioc 0 ↑N
Tactic:
exact ⟨h5, h6.le⟩
State after:
no goals

State before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
⊢ n - m < ↑N
Tactic:
calc
  _ < n := sub_lt_self n h1.m_range.left
  _ ≤ N := h1.n_range.right
State after:
no goals

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