Theorem: IMOSL.IMO2010A4.final_solution_extra (IMOSLLean4/IMO2010/A4/A4.lean)

State before:
k : ℕ
⊢ S k = 0 ↔ ∀ c ∈ Nat.digits 4 k, c = 0 ∨ c = 2
Tactic:
induction' k using Nat.strong_induction_on with k k_ih
State after:
case h
k : ℕ
k_ih : ∀ m < k, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ S k = 0 ↔ ∀ c ∈ Nat.digits 4 k, c = 0 ∨ c = 2

State before:
case h
k : ℕ
k_ih : ∀ m < k, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ S k = 0 ↔ ∀ c ∈ Nat.digits 4 k, c = 0 ∨ c = 2
Tactic:
obtain ⟨q, r, h, rfl⟩ : ∃ q r : ℕ, r < 4 ∧ 4 * q + r = k :=
  ⟨k / 4, k % 4, Nat.mod_lt k four_pos, Nat.div_add_mod k 4⟩
State after:
case h.intro.intro.intro
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ S (4 * q + r) = 0 ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ S (4 * q + r) = 0 ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
rw [S_four_mul_add_eq_zero_iff q h]
State after:
case h.intro.intro.intro
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
rcases q.eq_zero_or_pos with (rfl | h0)
State after:
case h.intro.intro.intro.inl
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ S 0 = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * 0 + r), c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inl
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ S 0 = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * 0 + r), c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
rw [S_zero, eq_self_iff_true, true_and_iff, MulZeroClass.mul_zero, zero_add]
State after:
case h.intro.intro.intro.inl
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inl
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
rcases r.eq_zero_or_pos with (rfl | h0)
State after:
case h.intro.intro.intro.inl.inl
h : 0 < 4
k_ih : ∀ m < 4 * 0 + 0, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ 0 = 0 ∨ 0 = 2 ↔ ∀ c ∈ Nat.digits 4 0, c = 0 ∨ c = 2

case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inl.inl
h : 0 < 4
k_ih : ∀ m < 4 * 0 + 0, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ 0 = 0 ∨ 0 = 2 ↔ ∀ c ∈ Nat.digits 4 0, c = 0 ∨ c = 2

case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
rw [eq_self_iff_true, true_or_iff, true_iff_iff, Nat.digits_zero]
State after:
case h.intro.intro.intro.inl.inl
h : 0 < 4
k_ih : ∀ m < 4 * 0 + 0, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ ∀ c ∈ [], c = 0 ∨ c = 2

case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inl.inl
h : 0 < 4
k_ih : ∀ m < 4 * 0 + 0, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
⊢ ∀ c ∈ [], c = 0 ∨ c = 2

case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
intro c h0
State after:
case h.intro.intro.intro.inl.inl
h : 0 < 4
k_ih : ∀ m < 4 * 0 + 0, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
c : ℕ
h0 : c ∈ []
⊢ c = 0 ∨ c = 2

case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inl.inl
h : 0 < 4
k_ih : ∀ m < 4 * 0 + 0, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
c : ℕ
h0 : c ∈ []
⊢ c = 0 ∨ c = 2

case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
exact absurd h0 (by exact List.not_mem_nil c)
State after:
case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ Nat.digits 4 r, c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
rw [Nat.digits_def' (Nat.succ_lt_succ <| Nat.succ_pos 2) h0,
  Nat.mod_eq_of_lt h, Nat.div_eq_of_lt h, Nat.digits_zero]
State after:
case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ [r], c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ c ∈ [r], c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
simp_rw [List.mem_singleton]
State after:
case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ (c : ℕ), c = r → c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inl.inr
r : ℕ
h : r < 4
k_ih : ∀ m < 4 * 0 + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : r > 0
⊢ r = 0 ∨ r = 2 ↔ ∀ (c : ℕ), c = r → c = 0 ∨ c = 2

case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
rw [forall_eq]
State after:
case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
h0 : q > 0
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
replace k_ih :=
  k_ih q (Nat.lt_add_right _ <| lt_mul_left h0 <| Nat.succ_lt_succ <| Nat.succ_pos 2)
State after:
case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
h0 : q > 0
k_ih : S q = 0 ↔ ∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
h0 : q > 0
k_ih : S q = 0 ↔ ∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2
⊢ S q = 0 ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ Nat.digits 4 (4 * q + r), c = 0 ∨ c = 2
Tactic:
rw [k_ih, add_comm,
  Nat.digits_add 4 (Nat.succ_lt_succ <| Nat.succ_pos 2) r q h <| Or.inr h0.ne.symm]
State after:
case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
h0 : q > 0
k_ih : S q = 0 ↔ ∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2
⊢ (∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2) ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ r :: Nat.digits 4 q, c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
h0 : q > 0
k_ih : S q = 0 ↔ ∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2
⊢ (∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2) ∧ (r = 0 ∨ r = 2) ↔ ∀ c ∈ r :: Nat.digits 4 q, c = 0 ∨ c = 2
Tactic:
simp_rw [List.mem_cons]
State after:
case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
h0 : q > 0
k_ih : S q = 0 ↔ ∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2
⊢ (∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2) ∧ (r = 0 ∨ r = 2) ↔ ∀ (c : ℕ), c = r ∨ c ∈ Nat.digits 4 q → c = 0 ∨ c = 2

State before:
case h.intro.intro.intro.inr
q r : ℕ
h : r < 4
h0 : q > 0
k_ih : S q = 0 ↔ ∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2
⊢ (∀ c ∈ Nat.digits 4 q, c = 0 ∨ c = 2) ∧ (r = 0 ∨ r = 2) ↔ ∀ (c : ℕ), c = r ∨ c ∈ Nat.digits 4 q → c = 0 ∨ c = 2
Tactic:
rw [forall_eq_or_imp, and_comm]
State after:
no goals

State before:
h : 0 < 4
k_ih : ∀ m < 4 * 0 + 0, S m = 0 ↔ ∀ c ∈ Nat.digits 4 m, c = 0 ∨ c = 2
c : ℕ
h0 : c ∈ []
⊢ c ∉ []
Tactic:
exact List.not_mem_nil c
State after:
no goals