Theorem: Imo1962P1.no_smaller_solutions (Compfiles/Imo1962P1.lean)

State before:
n : ℕ
h1 : ProblemPredicate n
⊢ n ≥ 153846
Tactic:
have ⟨c, h2⟩ := without_digits h1
State after:
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
⊢ n ≥ 153846

State before:
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
⊢ n ≥ 153846
Tactic:
have h3 : (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6 := by apply lt_or_ge
State after:
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h3 : (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6
⊢ n ≥ 153846

State before:
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
⊢ (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6
Tactic:
apply lt_or_ge
State after:
no goals

State before:
case inr
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h3 : (digits 10 c).length ≥ 6
⊢ n ≥ 153846
Tactic:
exact case_more_digits h3 h2
State after:
no goals

State before:
case inl
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h3 : (digits 10 c).length < 6
⊢ n ≥ 153846
Tactic:
interval_cases h : (digits 10 c).length
State after:
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ n ≥ 153846

case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ n ≥ 153846

case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ n ≥ 153846

case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ n ≥ 153846

case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ n ≥ 153846

case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
⊢ n ≥ 153846

State before:
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ n ≥ 153846
Tactic:
exfalso
State after:
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ False

State before:
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ False
Tactic:
exact case_0_digit h h2
State after:
no goals

State before:
case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ n ≥ 153846
Tactic:
exfalso
State after:
case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ False

State before:
case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ False
Tactic:
exact case_1_digit h h2
State after:
no goals

State before:
case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ n ≥ 153846
Tactic:
exfalso
State after:
case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ False

State before:
case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ False
Tactic:
exact case_2_digit h h2
State after:
no goals

State before:
case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ n ≥ 153846
Tactic:
exfalso
State after:
case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ False

State before:
case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ False
Tactic:
exact case_3_digit h h2
State after:
no goals

State before:
case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ n ≥ 153846
Tactic:
exfalso
State after:
case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ False

State before:
case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ False
Tactic:
exact case_4_digit h h2
State after:
no goals

State before:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
⊢ n ≥ 153846
Tactic:
have h4 : c = 15384 := case_5_digit h h2
State after:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
⊢ n ≥ 153846

State before:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
⊢ n ≥ 153846
Tactic:
have h5 : n = 10 * 15384 + 6 := h4 ▸ h2.left
State after:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 10 * 15384 + 6
⊢ n ≥ 153846

State before:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 10 * 15384 + 6
⊢ n ≥ 153846
Tactic:
norm_num at h5
State after:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 153846
⊢ n ≥ 153846

State before:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 153846
⊢ n ≥ 153846
Tactic:
exact h5.ge
State after:
no goals