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

State before:
⊢ ∀ (k : ℕ), S k = 0 → x k = false
Tactic:
intro k h
State after:
k : ℕ
h : S k = 0
⊢ x k = false

State before:
k : ℕ
h : S k = 0
⊢ x k = false
Tactic:
induction' k using Nat.strong_induction_on with k k_ih
State after:
case h
k : ℕ
k_ih : ∀ m < k, S m = 0 → x m = false
h : S k = 0
⊢ x k = false

State before:
case h
k : ℕ
k_ih : ∀ m < k, S m = 0 → x m = false
h : S k = 0
⊢ x k = false
Tactic:
obtain ⟨q, r, h0, 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 : ℕ
h0 : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 → x m = false
h : S (4 * q + r) = 0
⊢ x (4 * q + r) = false

State before:
case h.intro.intro.intro
q r : ℕ
h0 : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 → x m = false
h : S (4 * q + r) = 0
⊢ x (4 * q + r) = false
Tactic:
rw [S_four_mul_add_eq_zero_iff q h0, or_comm] at h
State after:
case h.intro.intro.intro
q r : ℕ
h0 : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 → x m = false
h : S q = 0 ∧ (r = 2 ∨ r = 0)
⊢ x (4 * q + r) = false

State before:
case h.intro.intro.intro
q r : ℕ
h0 : r < 4
k_ih : ∀ m < 4 * q + r, S m = 0 → x m = false
h : S q = 0 ∧ (r = 2 ∨ r = 0)
⊢ x (4 * q + r) = false
Tactic:
clear h0
State after:
case h.intro.intro.intro
q r : ℕ
k_ih : ∀ m < 4 * q + r, S m = 0 → x m = false
h : S q = 0 ∧ (r = 2 ∨ r = 0)
⊢ x (4 * q + r) = false

State before:
case h.intro.intro.intro
q r : ℕ
k_ih : ∀ m < 4 * q + r, S m = 0 → x m = false
h : S q = 0 ∧ (r = 2 ∨ r = 0)
⊢ x (4 * q + r) = false
Tactic:
rcases h with ⟨h, rfl | rfl⟩
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 (4 * q + 2) = false

case h.intro.intro.intro.intro.inr
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 0, S m = 0 → x m = false
⊢ x (4 * q + 0) = false

State before:
case h.intro.intro.intro.intro.inr
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 0, S m = 0 → x m = false
⊢ x (4 * q + 0) = false
Tactic:
rcases q.eq_zero_or_pos with (rfl | h0)
State after:
case h.intro.intro.intro.intro.inr.inl
h : S 0 = 0
k_ih : ∀ m < 4 * 0 + 0, S m = 0 → x m = false
⊢ x (4 * 0 + 0) = false

case h.intro.intro.intro.intro.inr.inr
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 0, S m = 0 → x m = false
h0 : q > 0
⊢ x (4 * q + 0) = false

State before:
case h.intro.intro.intro.intro.inr.inl
h : S 0 = 0
k_ih : ∀ m < 4 * 0 + 0, S m = 0 → x m = false
⊢ x (4 * 0 + 0) = false

case h.intro.intro.intro.intro.inr.inr
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 0, S m = 0 → x m = false
h0 : q > 0
⊢ x (4 * q + 0) = false
Tactic:
rw [add_zero, MulZeroClass.mul_zero, x_zero]
State after:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 0, S m = 0 → x m = false
h0 : q > 0
⊢ x (4 * q + 0) = false

State before:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h : S q = 0
k_ih : ∀ m < 4 * q + 0, S m = 0 → x m = false
h0 : q > 0
⊢ x (4 * q + 0) = false
Tactic:
replace k_ih := k_ih q (lt_mul_left h0 <| Nat.succ_lt_succ <| Nat.succ_pos 2) h
State after:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h : S q = 0
h0 : q > 0
k_ih : x q = false
⊢ x (4 * q + 0) = false

State before:
case h.intro.intro.intro.intro.inr.inr
q : ℕ
h : S q = 0
h0 : q > 0
k_ih : x q = false
⊢ x (4 * q + 0) = false
Tactic:
apply_fun Int.bodd at h
State after:
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

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
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

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]
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

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
State after:
no goals

State before:
this : ∀ (k : ℕ), S k = 0 → x k = false
⊢ ∀ (k : ℕ), 0 ≤ S k
Tactic:
refine Nat.rec (Int.le_refl 0) (λ k h ↦ ?_)
State after:
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 ≤ S k
⊢ 0 ≤ S k.succ

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
State after:
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k ∨ 1 ≤ S k
⊢ 0 ≤ S k.succ

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]
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

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
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

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]
State after:
case inl
this : ∀ (k : ℕ), S k = 0 → x k = false
k : ℕ
h : 0 = S k
⊢ 0 ≤ bif false then -1 else 1

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
State after:
no goals

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 : ℤ)]
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

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)
State after:
no goals

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]
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

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
State after:
no goals