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

State before:
c n : ℕ
H : SearchUpTo c n
c' n' : ℕ
ec : c + 1 = c'
en : n + 11 = n'
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo c' n'
Tactic:
subst ec
State after:
c n : ℕ
H : SearchUpTo c n
n' : ℕ
en : n + 11 = n'
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) n'

State before:
c n : ℕ
H : SearchUpTo c n
n' : ℕ
en : n + 11 = n'
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) n'
Tactic:
subst en
State after:
c n : ℕ
H : SearchUpTo c n
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)

State before:
c n : ℕ
H : SearchUpTo c n
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)
Tactic:
subst el
State after:
c n : ℕ
H : SearchUpTo c n
H' : c = sumOfSquares (digits 10 n) → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)

State before:
c n : ℕ
H : SearchUpTo c n
H' : c = sumOfSquares (digits 10 n) → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)
Tactic:
obtain ⟨rfl, H⟩ := H
State after:
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
⊢ SearchUpTo (c + 1) (c * 11 + 11)

State before:
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
⊢ SearchUpTo (c + 1) (c * 11 + 11)
Tactic:
refine ⟨by ring, fun m l p => ?_⟩
State after:
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : m < c * 11 + 11
p : ProblemPredicate m
⊢ SolutionPredicate m

State before:
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : m < c * 11 + 11
p : ProblemPredicate m
⊢ SolutionPredicate m
Tactic:
obtain ⟨h₁, ⟨m, rfl⟩, h₂⟩ := id p
State after:
case intro.intro.intro.intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
⊢ SolutionPredicate (11 * m)

State before:
case intro.intro.intro.intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
⊢ SolutionPredicate (11 * m)
Tactic:
by_cases h : 11 * m < c * 11
State after:
case pos
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : 11 * m < c * 11
⊢ SolutionPredicate (11 * m)

case neg
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : ¬11 * m < c * 11
⊢ SolutionPredicate (11 * m)

State before:
case neg
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : ¬11 * m < c * 11
⊢ SolutionPredicate (11 * m)
Tactic:
obtain rfl : m = c := by omega
State after:
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)

State before:
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)
Tactic:
rw [Nat.mul_div_cancel_left _ (by norm_num : 11 > 0), mul_comm] at h₂
State after:
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)

State before:
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
⊢ c * 11 + 11 = (c + 1) * 11
Tactic:
ring
State after:
no goals

State before:
case pos
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : 11 * m < c * 11
⊢ SolutionPredicate (11 * m)
Tactic:
exact H _ h p
State after:
no goals

State before:
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : ¬11 * m < c * 11
⊢ m = c
Tactic:
omega
State after:
no goals

State before:
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
⊢ 11 > 0
Tactic:
norm_num
State after:
no goals

State before:
case neg.refine_2
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
⊢ m = 73 → 11 * m = 803
Tactic:
rintro rfl
State after:
case neg.refine_2
p : ProblemPredicate (11 * 73)
h₁ : (digits 10 (11 * 73)).length = 3
h₂ : 73 = sumOfSquares (digits 10 (73 * 11))
H' : 73 = sumOfSquares (digits 10 (73 * 11)) → 73 = 50 ∨ 73 = 73
H : ∀ m < 73 * 11, ProblemPredicate m → SolutionPredicate m
l : 11 * 73 < 73 * 11 + 11
h : ¬11 * 73 < 73 * 11
⊢ 11 * 73 = 803

State before:
case neg.refine_2
p : ProblemPredicate (11 * 73)
h₁ : (digits 10 (11 * 73)).length = 3
h₂ : 73 = sumOfSquares (digits 10 (73 * 11))
H' : 73 = sumOfSquares (digits 10 (73 * 11)) → 73 = 50 ∨ 73 = 73
H : ∀ m < 73 * 11, ProblemPredicate m → SolutionPredicate m
l : 11 * 73 < 73 * 11 + 11
h : ¬11 * 73 < 73 * 11
⊢ 11 * 73 = 803
Tactic:
norm_num
State after:
no goals