Theorem: Imo1960P1.right_direction (Compfiles/Imo1960P1.lean)

State before:
n : ℕ
⊢ ProblemPredicate n → SolutionPredicate n
Tactic:
have := searchUpTo_start
State after:
n : ℕ
this : SearchUpTo 9 99
⊢ ProblemPredicate n → SolutionPredicate n

State before:
n : ℕ
this : SearchUpTo 9 99
⊢ ProblemPredicate n → SolutionPredicate n
Tactic:
iterate 82
  replace :=
    searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) rfl
      (by norm_num <;> decide)
State after:
n : ℕ
this : SearchUpTo 91 1001
⊢ ProblemPredicate n → SolutionPredicate n

State before:
n : ℕ
this : SearchUpTo 91 1001
⊢ ProblemPredicate n → SolutionPredicate n
Tactic:
exact searchUpTo_end this
State after:
no goals

State before:
n : ℕ
this : SearchUpTo 90 990
⊢ ProblemPredicate n → SolutionPredicate n
Tactic:
replace :=
  searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) rfl
    (by norm_num <;> decide)
State after:
n : ℕ
this : SearchUpTo 91 1001
⊢ ProblemPredicate n → SolutionPredicate n

State before:
n : ℕ
this : SearchUpTo 90 990
⊢ 90 + 1 = ?m.34900
Tactic:
norm_num1
State after:
n : ℕ
this : SearchUpTo 90 990
⊢ 91 = ?m.34900

State before:
n : ℕ
this : SearchUpTo 90 990
⊢ 91 = ?m.34900
Tactic:
rfl
State after:
no goals

State before:
n : ℕ
this : SearchUpTo 90 990
⊢ 990 + 11 = ?m.34901
Tactic:
norm_num1
State after:
n : ℕ
this : SearchUpTo 90 990
⊢ 1001 = ?m.34901

State before:
n : ℕ
this : SearchUpTo 90 990
⊢ 1001 = ?m.34901
Tactic:
rfl
State after:
no goals

State before:
n : ℕ
this : SearchUpTo 90 990
⊢ 90 = sumOfSquares (digits 10 990) → 90 = 50 ∨ 90 = 73
Tactic:
norm_num <;> decide
State after:
no goals