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

State before:
n : ℕ
spn : SolutionPredicate n
⊢ ProblemPredicate n
Tactic:
rcases spn with (rfl | rfl) <;> exact ⟨by norm_num, by decide, by norm_num; rfl⟩
State after:
no goals

State before:
⊢ (digits 10 803).length = 3
Tactic:
norm_num
State after:
no goals

State before:
⊢ 11 ∣ 803
Tactic:
decide
State after:
no goals

State before:
⊢ 803 / 11 = sumOfSquares (digits 10 803)
Tactic:
norm_num
State after:
⊢ 73 = sumOfSquares [3, 0, 8]

State before:
⊢ 73 = sumOfSquares [3, 0, 8]
Tactic:
rfl
State after:
no goals