rw [Nat.mul_div_cancel_left _ (by norm_num : 11 > 0), mul_comm] at h₂
case neg
m : ℕ
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
H' : m = sumOfSquares (digits 10 (m * 11)) → m = 50 ∨ m = 73
H : ∀ m_1 < m * 11, ProblemPredicate m_1 → SolutionPredicate m_1
l : 11 * m < m * 11 + 11
h : ¬11 * m < m * 11
⊢ SolutionPredicate (11 * m)
case neg
m : ℕ
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : m = sumOfSquares (digits 10 (m * 11))
H' : m = sumOfSquares (digits 10 (m * 11)) → m = 50 ∨ m = 73
H : ∀ m_1 < m * 11, ProblemPredicate m_1 → SolutionPredicate m_1
l : 11 * m < m * 11 + 11
h : ¬11 * m < m * 11
⊢ SolutionPredicate (11 * m)