internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + (a * a⁻¹ + b * b⁻¹ + 1)
⊢ a = b
Tactic:
rw [mul_inv_cancel ha, mul_inv_cancel hb, one_add_one_eq_two, h, zero_add] at h7
Proof state after:
case inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
⊢ a = b
Tactic:
rw [← h2, ← h7, add_add_add_comm, add_add_add_comm a, ← add_add_add_comm,
  ← h0, add_right_comm, add_left_eq_self, ← h2, add_assoc,
  one_add_one_eq_two, h, add_zero, h5, mul_eq_zero, h5, h5] at h6
Proof state after:
case inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
⊢ a = b
Tactic:
replace h3 : ∀ c : F, -c = c := λ c ↦ by
  rw [neg_eq_iff_add_eq_zero, ← two_mul, h, zero_mul]
Proof state after:
case inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
⊢ a = b
Tactic:
rcases h6 with h6 | h6
Proof state after:
case inr.inr.inl
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
h6 : a + b = 0
⊢ a = b

case inr.inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
h6 : b⁻¹ + a⁻¹ = 0
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
c d : F
h3 : d ≠ 0
h4 : f (c + 1) = f (d + 1)
⊢ f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
Tactic:
rw [good_shift2 h0 h1, ← h0, h4, add_assoc, ← add_assoc (c + 1), h2,
  good_special_equality h0 (mul_inv_cancel h3), zero_add, add_right_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inl
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
b : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
h4 : f (0 + 1) = f (b + 1)
⊢ 0 = b
Tactic:
rwa [zero_add, good_map_one h0, eq_comm, h5, eq_comm] at h4
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inl
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
h4 : f (a + 1) = f (0 + 1)
⊢ a = 0
Tactic:
rwa [zero_add, good_map_one h0, h5] at h4
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
⊢ ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
Tactic:
ring
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
c d : F
⊢ (c + 1) * (d + 1) = c * d + c + d + 1
Tactic:
rw [add_one_mul (α := F), mul_add_one (α := F), ← add_assoc]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
⊢ (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + (a * a⁻¹ + b * b⁻¹ + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : a + b = 0 ∨ b⁻¹ + a⁻¹ = 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
c : F
⊢ -c = c
Tactic:
rw [neg_eq_iff_add_eq_zero, ← two_mul, h, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr.inl
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
h6 : a + b = 0
⊢ a = b
Tactic:
rwa [add_eq_zero_iff_eq_neg, h3] at h6
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr.inr
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + 1
h3 : ∀ (c : F), -c = c
h6 : b⁻¹ + a⁻¹ = 0
⊢ a = b
Tactic:
rwa [add_eq_zero_iff_eq_neg, h3, inv_inj, eq_comm] at h6
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.x_mul4
Proof state before:
k : ℕ
⊢ x (4 * k) = xor k.bodd (x k)
Tactic:
change x (2 * 2 * k) = xor k.bodd (x k)
Proof state after:
k : ℕ
⊢ x (2 * 2 * k) = xor k.bodd (x k)
Theorem: IMOSL.IMO2010A4.x_mul4
Proof state before:
k : ℕ
⊢ x (2 * 2 * k) = xor k.bodd (x k)
Tactic:
rw [mul_assoc, x_mul2, x_mul2, ← Nat.bit0_val, Nat.bodd_bit0, Bool.false_xor]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.x_mul4_add1
Proof state before:
k : ℕ
⊢ x (4 * k + 1) = !x (4 * k)
Tactic:
change x (2 * 2 * k + 1) = !x (2 * 2 * k)
Proof state after:
k : ℕ
⊢ x (2 * 2 * k + 1) = !x (2 * 2 * k)
Theorem: IMOSL.IMO2010A4.x_mul4_add1
Proof state before:
k : ℕ
⊢ x (2 * 2 * k + 1) = !x (2 * 2 * k)
Tactic:
rw [mul_assoc, x_mul2, x_mul2_add1,
  ← Nat.bit0_val, Nat.bodd_bit0, Bool.false_xor]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.x_mul4_add2
Proof state before:
k : ℕ
⊢ x (4 * k + 2) = x k
Tactic:
change x (2 * 2 * k + 2) = x k
Proof state after:
k : ℕ
⊢ x (2 * 2 * k + 2) = x k
Theorem: IMOSL.IMO2010A4.x_mul4_add2
Proof state before:
k : ℕ
⊢ x (2 * 2 * k + 2) = x k
Tactic:
rw [mul_assoc, ← mul_add_one, x_mul2, x_mul2_add1,
  ← Nat.bit1_val, Nat.bodd_bit1, Bool.true_xor, Bool.not_not]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.x_mul4_add3
Proof state before:
k : ℕ
⊢ x (4 * k + 3) = x k
Tactic:
change x (2 * 2 * k + 2 + 1) = x k
Proof state after:
k : ℕ
⊢ x (2 * 2 * k + 2 + 1) = x k
Theorem: IMOSL.IMO2010A4.x_mul4_add3
Proof state before:
k : ℕ
⊢ x (2 * 2 * k + 2 + 1) = x k
Tactic:
rw [mul_assoc, ← mul_add_one, x_mul2_add1, x_mul2_add1, Bool.not_not]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.S_mul4_add2
Proof state before:
k : ℕ
⊢ S (4 * k + 2) = S (4 * k)
Tactic:
rw [S_succ, S_succ, add_assoc, add_right_eq_self, x_mul4_add1]
Proof state after:
k : ℕ
⊢ ((bif x (4 * k) then -1 else 1) + bif !x (4 * k) then -1 else 1) = 0
Theorem: IMOSL.IMO2010A4.S_mul4_add2
Proof state before:
k : ℕ
⊢ ((bif x (4 * k) then -1 else 1) + bif !x (4 * k) then -1 else 1) = 0
Tactic:
exact (x (4 * k)).recOn rfl rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.S_mul4
Proof state before:
k : ℕ
h : S (4 * k) = 2 * S k
⊢ S (4 * k.succ) = 2 * S k.succ
Tactic:
change S (4 * k + 4) = 2 * S k.succ
Proof state after:
k : ℕ
h : S (4 * k) = 2 * S k
⊢ S (4 * k + 4) = 2 * S k.succ
Theorem: IMOSL.IMO2010A4.S_mul4
Proof state before:
k : ℕ
h : S (4 * k) = 2 * S k
⊢ S (4 * k + 4) = 2 * S k.succ
Tactic:
rw [S_succ, x_mul4_add3, S_succ, x_mul4_add2, S_mul4_add2,
  h, add_assoc, ← two_mul, ← mul_add, ← S_succ]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.S_parity
Proof state before:
k : ℕ
h : (S k).bodd = k.bodd
⊢ (S k.succ).bodd = k.succ.bodd
Tactic:
rw [Nat.bodd_succ, S_succ, Int.bodd_add, h, ← Bool.xor_true]
Proof state after:
k : ℕ
h : (S k).bodd = k.bodd
⊢ xor k.bodd (bif x k then -1 else 1).bodd = xor k.bodd true
Theorem: IMOSL.IMO2010A4.S_parity
Proof state before:
k : ℕ
h : (S k).bodd = k.bodd
⊢ xor k.bodd (bif x k then -1 else 1).bodd = xor k.bodd true
Tactic:
exact (x k).rec rfl rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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 ↦ ?_⟩
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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)
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof state after:
case refine_3
q r : ℕ
h : r < 4
h0 : S q = 0 ∧ (r = 0 ∨ r = 2)
⊢ S (4 * q + r) = 0
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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]
Proof state after:
case refine_3.intro.inl
q : ℕ
h0 : S q = 0
h : 0 < 4
⊢ 2 * 0 = 0
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof state before:
case refine_3.intro.inl
q : ℕ
h0 : S q = 0
h : 0 < 4
⊢ 2 * 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof 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]
Proof state after:
case refine_3.intro.inr
q : ℕ
h0 : S q = 0
h : 2 < 4
⊢ 2 * 0 = 0
Theorem: IMOSL.IMO2010A4.S_four_mul_add_eq_zero_iff
Proof state before:
case refine_3.intro.inr
q : ℕ
h0 : S q = 0
h : 2 < 4
⊢ 2 * 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
⊢ ∀ (k : ℕ), S k = 0 → x k = false
Tactic:
intro k h
Proof state after:
k : ℕ
h : S k = 0
⊢ x k = false
Theorem: IMOSL.IMO2010A4.final_solution
Proof state before:
k : ℕ
h : S k = 0
⊢ x k = false
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 → x m = false
h : S k = 0
⊢ x k = false
Theorem: IMOSL.IMO2010A4.final_solution
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution
Proof 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⟩
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 (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
Theorem: IMOSL.IMO2010A4.final_solution
Proof 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)
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution
Proof 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]
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution
Proof 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
Proof 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
Theorem: IMOSL.IMO2010A4.final_solution
Proof 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
Proof 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