internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h0 : q > 0
k_ih : x q = false
h : (S q).bodd = Int.bodd 0
⊢ x (4 * q + 0) = false
Tactic:
rw [Int.bodd_zero, S_parity] at h
Proof state after:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h0 : q > 0
k_ih : x q = false
h : q.bodd = false
⊢ x (4 * q + 0) = false
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h0 : q > 0
k_ih : x q = false
h : q.bodd = false
⊢ x (4 * q + 0) = false
Tactic:
rw [add_zero, x_mul4, h, k_ih]
Proof state after:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h0 : q > 0
k_ih : x q = false
h : q.bodd = false
⊢ xor false false = false
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h0 : q > 0
k_ih : x q = false
h : q.bodd = false
⊢ xor false false = false
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
this : ∀ (k : ℕ), S k = 0 → x k = false
⊢ ∀ (k : ℕ), 0 ≤ S k
Tactic:
refine Nat.rec (Int.le_refl 0) (λ k h ↦ ?_)
Proof state after:
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 ≤ S k
⊢ 0 ≤ S k.succ
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 ≤ S k
⊢ 0 ≤ S k.succ
Tactic:
rw [le_iff_lt_or_eq, Int.lt_iff_add_one_le, zero_add, or_comm] at h
Proof state after:
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k ∨ 1 ≤ S k
⊢ 0 ≤ S k.succ
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k ∨ 1 ≤ S k
⊢ 0 ≤ S k.succ
Tactic:
rw [S_succ]
Proof state after:
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k ∨ 1 ≤ S k
⊢ 0 ≤ S k + bif x k then -1 else 1
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k ∨ 1 ≤ S k
⊢ 0 ≤ S k + bif x k then -1 else 1
Tactic:
rcases h with h | h
Proof state after:
case inl
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k
⊢ 0 ≤ S k + bif x k then -1 else 1

case inr
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 1 ≤ S k
⊢ 0 ≤ S k + bif x k then -1 else 1
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case inl
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k
⊢ 0 ≤ S k + bif x k then -1 else 1
Tactic:
rw [← h, zero_add, this k h.symm]
Proof state after:
case inl
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k
⊢ 0 ≤ bif false then -1 else 1
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case inl
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k
⊢ 0 ≤ bif false then -1 else 1
Tactic:
exact Int.zero_lt_one.le
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case inr
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 1 ≤ S k
⊢ 0 ≤ S k + bif x k then -1 else 1
Tactic:
rw [← add_neg_self (1 : ℤ)]
Proof state after:
case inr
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 1 ≤ S k
⊢ 1 + -1 ≤ S k + bif x k then -1 else 1
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case inr
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 1 ≤ S k
⊢ 1 + -1 ≤ S k + bif x k then -1 else 1
Tactic:
exact add_le_add h ((x k).rec (neg_le_self zero_le_one) (-1).le_refl)
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case h.intro.intro.intro.intro.inl
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 2, S m = 0 → x m = false
⊢ x (4 * q + 2) = false
Tactic:
rw [x_mul4_add2]
Proof state after:
case h.intro.intro.intro.intro.inl
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 2, S m = 0 → x m = false
⊢ x q = false
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
case h.intro.intro.intro.intro.inl
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 2, S m = 0 → x m = false
⊢ x q = false
Tactic:
exact k_ih q (lt_add_of_le_of_pos (Nat.le_mul_of_pos_left _ four_pos) two_pos) h
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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)
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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)
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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)
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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)
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.final_solution_extra
Proof 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
Proof state after:
no goals
Theorem: Nat.one_le_succ
Proof state before:
x : ℕ
⊢ 1 ≤ succ x
Tactic:
exact tsub_add_cancel_iff_le.mp rfl
Proof state after:
no goals
Theorem: Nat.modCore_one
Proof state before:
x : ℕ
⊢ Nat.modCore x 1 = 0
Tactic:
induction x <;> (try unfold Nat.modCore; simp [*])
Proof state after:
no goals
Theorem: Nat.modCore_one
Proof state before:
case succ
n✝ : ℕ
n_ih✝ : Nat.modCore n✝ 1 = 0
⊢ Nat.modCore (succ n✝) 1 = 0
Tactic:
try unfold Nat.modCore; simp [*]
Proof state after:
no goals
Theorem: Nat.modCore_one
Proof state before:
case succ
n✝ : ℕ
n_ih✝ : Nat.modCore n✝ 1 = 0
⊢ Nat.modCore (succ n✝) 1 = 0
Tactic:
unfold Nat.modCore
Proof state after:
case succ
n✝ : ℕ
n_ih✝ : Nat.modCore n✝ 1 = 0
⊢ (if 0 < 1 ∧ 1 ≤ succ n✝ then Nat.modCore (succ n✝ - 1) 1 else succ n✝) = 0
Theorem: Nat.modCore_one
Proof state before:
case succ
n✝ : ℕ
n_ih✝ : Nat.modCore n✝ 1 = 0
⊢ (if 0 < 1 ∧ 1 ≤ succ n✝ then Nat.modCore (succ n✝ - 1) 1 else succ n✝) = 0
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Nat.modCore_zero
Proof state before:
x : ℕ
⊢ Nat.modCore 0 x = 0
Tactic:
unfold Nat.modCore
Proof state after:
x : ℕ
⊢ (if 0 < x ∧ x ≤ 0 then Nat.modCore (0 - x) x else 0) = 0
Theorem: Nat.modCore_zero
Proof state before:
x : ℕ
⊢ (if 0 < x ∧ x ≤ 0 then Nat.modCore (0 - x) x else 0) = 0
Tactic:
simp only [nonpos_iff_eq_zero, ge_iff_le, _root_.zero_le, tsub_eq_zero_of_le, ite_eq_right_iff,
  and_imp]
Proof state after:
x : ℕ
⊢ 0 < x → x = 0 → Nat.modCore 0 x = 0
Theorem: Nat.modCore_zero
Proof state before:
x : ℕ
⊢ 0 < x → x = 0 → Nat.modCore 0 x = 0
Tactic:
rintro _ ⟨⟩
Proof state after:
case refl
a✝ : 0 < 0
⊢ Nat.modCore 0 0 = 0
Theorem: Nat.modCore_zero
Proof state before:
case refl
a✝ : 0 < 0
⊢ Nat.modCore 0 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.ge_mod
Proof state before:
n x : ℕ
⊢ (match x, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Tactic:
cases x
Proof state after:
case zero
n : ℕ
⊢ (match zero, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1

case succ
n n✝ : ℕ
⊢ (match succ n✝, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Theorem: Nat.ge_mod
Proof state before:
case zero
n : ℕ
⊢ (match zero, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1

case succ
n n✝ : ℕ
⊢ (match succ n✝, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Tactic:
next => simp
Proof state after:
case succ
n n✝ : ℕ
⊢ (match succ n✝, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Theorem: Nat.ge_mod
Proof state before:
n : ℕ
⊢ (match zero, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.ge_mod
Proof state before:
n x : ℕ
⊢ (match succ x, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Tactic:
simp
Proof state after:
n x : ℕ
⊢ Nat.modCore (succ x) (n + 1) < n + 1
Theorem: Nat.ge_mod
Proof state before:
n x : ℕ
⊢ Nat.modCore (succ x) (n + 1) < n + 1
Tactic:
induction x using Nat.strongInductionOn
Proof state after:
case ind
n n✝ : ℕ
a✝ : ∀ m < n✝, Nat.modCore (succ m) (n + 1) < n + 1
⊢ Nat.modCore (succ n✝) (n + 1) < n + 1
Theorem: Nat.ge_mod
Proof state before:
n x : ℕ
ih : ∀ m < x, Nat.modCore (succ m) (n + 1) < n + 1
⊢ Nat.modCore (succ x) (n + 1) < n + 1
Tactic:
unfold Nat.modCore
Proof state after:
n x : ℕ
ih : ∀ m < x, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if 0 < n + 1 ∧ n + 1 ≤ succ x then Nat.modCore (succ x - (n + 1)) (n + 1) else succ x) < n + 1
Theorem: Nat.ge_mod
Proof state before:
n x : ℕ
ih : ∀ m < x, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if 0 < n + 1 ∧ n + 1 ≤ succ x then Nat.modCore (succ x - (n + 1)) (n + 1) else succ x) < n + 1
Tactic:
cases x <;> simp [Nat.succ_le_succ_iff]
Proof state after:
case zero
n : ℕ
ih : ∀ m < zero, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n = 0 then 0 else succ 0) < n + 1

case succ
n n✝ : ℕ
ih : ∀ m < succ n✝, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n ≤ n✝ + 1 then Nat.modCore (n✝ + 1 - n) (n + 1) else succ (succ n✝)) < n + 1
Theorem: Nat.ge_mod
Proof state before:
case zero
n : ℕ
ih : ∀ m < zero, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n = 0 then 0 else succ 0) < n + 1

case succ
n n✝ : ℕ
ih : ∀ m < succ n✝, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n ≤ n✝ + 1 then Nat.modCore (n✝ + 1 - n) (n + 1) else succ (succ n✝)) < n + 1
Tactic:
next =>
  cases n <;> simp
Proof state after:
case succ
n n✝ : ℕ
ih : ∀ m < succ n✝, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n ≤ n✝ + 1 then Nat.modCore (n✝ + 1 - n) (n + 1) else succ (succ n✝)) < n + 1
Theorem: Nat.ge_mod
Proof state before:
n : ℕ
ih : ∀ m < zero, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n = 0 then 0 else succ 0) < n + 1
Tactic:
cases n <;> simp
Proof state after:
no goals
Theorem: Nat.ge_mod
Proof state before:
n x : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n ≤ x + 1 then Nat.modCore (x + 1 - n) (n + 1) else succ (succ x)) < n + 1
Tactic:
cases' n with n <;> simp
Proof state after:
case succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
⊢ (if succ n ≤ x + 1 then Nat.modCore (x - n) (succ n + 1) else succ (succ x)) < succ n + 1
Theorem: Nat.ge_mod
Proof state before:
case succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
⊢ (if succ n ≤ x + 1 then Nat.modCore (x - n) (succ n + 1) else succ (succ x)) < succ n + 1
Tactic:
split_ifs with h
Proof state after:
case pos
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
⊢ Nat.modCore (x - n) (succ n + 1) < succ n + 1

case neg
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : ¬succ n ≤ x + 1
⊢ succ (succ x) < succ n + 1
Theorem: Nat.ge_mod
Proof state before:
case pos
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
⊢ Nat.modCore (x - n) (succ n + 1) < succ n + 1
Tactic:
cases hm : x - n
Proof state after:
case pos.zero
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
hm : x - n = zero
⊢ Nat.modCore zero (succ n + 1) < succ n + 1

case pos.succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1
Theorem: Nat.ge_mod
Proof state before:
case pos.zero
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
hm : x - n = zero
⊢ Nat.modCore zero (succ n + 1) < succ n + 1

case pos.succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1
Tactic:
next => simp
Proof state after:
case pos.succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1
Theorem: Nat.ge_mod
Proof state before:
case pos.succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1
Tactic:
next =>
  apply ih
  apply Nat.lt_of_succ_le
  apply Nat.le_succ_of_le
  rw [←hm]
  apply sub_le
Proof state after:
no goals
Theorem: Nat.ge_mod
Proof state before:
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
hm : x - n = zero
⊢ Nat.modCore zero (succ n + 1) < succ n + 1
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.ge_mod
Proof state before:
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1
Tactic:
apply ih
Proof state after:
case a
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ n✝ < succ x