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

State before:
q r : ℕ
h : r < 4
⊢ S (4 * q + r) = 0 ↔ S q = 0 ∧ (r = 0 ∨ r = 2)
Tactic:
refine ⟨fun h0 ↦ (and_iff_right_of_imp ?_).mpr ?_, fun h0 ↦ ?_⟩
State after:
case refine_1
q r : ℕ
h : r < 4
h0 : S (4 * q + r) = 0
⊢ r = 0 ∨ r = 2 → S q = 0

case refine_2
q r : ℕ
h : r < 4
h0 : S (4 * q + r) = 0
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_1
q r : ℕ
h : r < 4
h0 : S (4 * q + r) = 0
⊢ r = 0 ∨ r = 2 → S q = 0

case refine_2
q r : ℕ
h : r < 4
h0 : S (4 * q + r) = 0
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
replace h : (2 : ℤ) ≠ 0 := two_ne_zero
State after:
case refine_1
q r : ℕ
h0 : S (4 * q + r) = 0
h : 2 ≠ 0
⊢ r = 0 ∨ r = 2 → S q = 0

case refine_2
q r : ℕ
h : r < 4
h0 : S (4 * q + r) = 0
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_1
q r : ℕ
h0 : S (4 * q + r) = 0
h : 2 ≠ 0
⊢ r = 0 ∨ r = 2 → S q = 0

case refine_2
q r : ℕ
h : r < 4
h0 : S (4 * q + r) = 0
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
rintro (rfl | rfl)
State after:
case refine_1.inl
q : ℕ
h : 2 ≠ 0
h0 : S (4 * q + 0) = 0
⊢ S q = 0

case refine_1.inr
q : ℕ
h : 2 ≠ 0
h0 : S (4 * q + 2) = 0
⊢ S q = 0

case refine_2
q r : ℕ
h : r < 4
h0 : S (4 * q + r) = 0
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_2
q r : ℕ
h : r < 4
h0 : S (4 * q + r) = 0
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
apply_fun Int.bodd at h0
State after:
case refine_2
q r : ℕ
h : r < 4
h0 : (S (4 * q + r)).bodd = Int.bodd 0
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_2
q r : ℕ
h : r < 4
h0 : (S (4 * q + r)).bodd = Int.bodd 0
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
rw [Int.bodd_zero, S_parity, Nat.bodd_add, Nat.bodd_mul] at h0
State after:
case refine_2
q r : ℕ
h : r < 4
h0 : xor (Nat.bodd 4 && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_2
q r : ℕ
h : r < 4
h0 : xor (Nat.bodd 4 && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
change xor (false && q.bodd) r.bodd = false at h0
State after:
case refine_2
q r : ℕ
h : r < 4
h0 : xor (false && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_2
q r : ℕ
h : r < 4
h0 : xor (false && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
iterate 3 rw [Nat.lt_succ_iff_lt_or_eq] at h
State after:
case refine_2
q r : ℕ
h : ((r < 1 ∨ r = 1) ∨ r = 2) ∨ r = 3
h0 : xor (false && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_2
q r : ℕ
h : ((r < 1 ∨ r = 1) ∨ r = 2) ∨ r = 3
h0 : xor (false && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
rw [Nat.lt_one_iff, or_assoc, or_or_or_comm] at h
State after:
case refine_2
q r : ℕ
h : (r = 0 ∨ r = 2) ∨ r = 1 ∨ r = 3
h0 : xor (false && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_2
q r : ℕ
h : (r = 0 ∨ r = 2) ∨ r = 1 ∨ r = 3
h0 : xor (false && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
revert h
State after:
case refine_2
q r : ℕ
h0 : xor (false && q.bodd) r.bodd = false
⊢ (r = 0 ∨ r = 2) ∨ r = 1 ∨ r = 3 → r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_2
q r : ℕ
h0 : xor (false && q.bodd) r.bodd = false
⊢ (r = 0 ∨ r = 2) ∨ r = 1 ∨ r = 3 → r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
refine' (or_iff_left _).mp
State after:
case refine_2
q r : ℕ
h0 : xor (false && q.bodd) r.bodd = false
⊢ ¬(r = 1 ∨ r = 3)

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_2
q r : ℕ
h0 : xor (false && q.bodd) r.bodd = false
⊢ ¬(r = 1 ∨ r = 3)

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
rintro (rfl | rfl) <;> exact Bool.true_eq_false_eq_False h0
State after:
case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
rcases h0 with ⟨h0, rfl | rfl⟩
State after:
case refine_3.intro.inl
q : ℕ
h0 : S q = 0
h : 0 < 4
⊢ S (4 * q + 0) = 0

case refine_3.intro.inr
q : ℕ
h0 : S q = 0
h : 2 < 4
⊢ S (4 * q + 2) = 0

State before:
case refine_1.inl
q : ℕ
h : 2 ≠ 0
h0 : S (4 * q + 0) = 0
⊢ S q = 0
Tactic:
rwa [add_zero, S_mul4, mul_eq_zero, or_iff_right h] at h0
State after:
no goals

State before:
case refine_1.inr
q : ℕ
h : 2 ≠ 0
h0 : S (4 * q + 2) = 0
⊢ S q = 0
Tactic:
rwa [S_mul4_add2, S_mul4, mul_eq_zero, or_iff_right h] at h0
State after:
no goals

State before:
case refine_2
q r : ℕ
h : (r < 2 ∨ r = 2) ∨ r = 3
h0 : xor (false && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Tactic:
rw [Nat.lt_succ_iff_lt_or_eq] at h
State after:
case refine_2
q r : ℕ
h : ((r < 1 ∨ r = 1) ∨ r = 2) ∨ r = 3
h0 : xor (false && q.bodd) r.bodd = false
⊢ r = 0 ∨ r = 2

case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0

State before:
case refine_3.intro.inl
q : ℕ
h0 : S q = 0
h : 0 < 4
⊢ S (4 * q + 0) = 0
Tactic:
rw [add_zero, S_mul4, h0]
State after:
case refine_3.intro.inl
q : ℕ
h0 : S q = 0
h : 0 < 4
⊢ 2 * 0 = 0

State before:
case refine_3.intro.inl
q : ℕ
h0 : S q = 0
h : 0 < 4
⊢ 2 * 0 = 0
Tactic:
rfl
State after:
no goals

State before:
case refine_3.intro.inr
q : ℕ
h0 : S q = 0
h : 2 < 4
⊢ S (4 * q + 2) = 0
Tactic:
rw [S_mul4_add2, S_mul4, h0]
State after:
case refine_3.intro.inr
q : ℕ
h0 : S q = 0
h : 2 < 4
⊢ 2 * 0 = 0

State before:
case refine_3.intro.inr
q : ℕ
h0 : S q = 0
h : 2 < 4
⊢ 2 * 0 = 0
Tactic:
rfl
State after:
no goals