Theorem: IMOSL.IMO2015N1.main_claim (IMOSLLean4/IMO2015/N1/N1.lean)

State before:
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
⊢ 2 * (2 * c) ∣ m - 3
Tactic:
by_cases h1 : c = 0
State after:
case pos
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
h1 : c = 0
⊢ 2 * (2 * c) ∣ m - 3

case neg
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
⊢ 2 * (2 * c) ∣ m - 3

State before:
case pos
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
h1 : c = 0
⊢ 2 * (2 * c) ∣ m - 3
Tactic:
rwa [h1, mul_zero, ← h1]
State after:
no goals

State before:
case neg
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
⊢ 2 * (2 * c) ∣ m - 3
Tactic:
rcases h with ⟨d, h⟩
State after:
case neg.intro
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 * (2 * c) ∣ m - 3

State before:
case neg.intro
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 * (2 * c) ∣ m - 3
Tactic:
rw [h, mul_comm]
State after:
case neg.intro
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 * c * 2 ∣ 2 * c * d

State before:
case neg.intro
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 * c * 2 ∣ 2 * c * d
Tactic:
apply mul_dvd_mul_left
State after:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 ∣ d

State before:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 ∣ d
Tactic:
have X : (2 : ℤ) ≠ 0 := two_ne_zero
State after:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
X : 2 ≠ 0
⊢ 2 ∣ d

State before:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
X : 2 ≠ 0
⊢ 2 ∣ d
Tactic:
have X0 : (3 / 2 : ℤ) = 1 := rfl
State after:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
X : 2 ≠ 0
X0 : 3 / 2 = 1
⊢ 2 ∣ d

State before:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
X : 2 ≠ 0
X0 : 3 / 2 = 1
⊢ 2 ∣ d
Tactic:
rw [f, eq_add_of_sub_eq h, add_mul, add_sub_assoc, mul_assoc, ← mul_sub_one,
  dvd_add_right ⟨_, rfl⟩, mul_assoc, add_comm, Int.add_mul_ediv_left _ _ X,
  X0, add_sub_cancel_left, ← two_add_one_eq_three, add_one_mul (α := ℤ),
  ← mul_assoc, dvd_add_right ⟨_, rfl⟩, mul_comm] at h0
State after:
case neg.intro.h
c m : ℤ
h1 : ¬c = 0
d : ℤ
h0 : c * 2 ∣ c * d
h : m - 3 = 2 * c * d
X : 2 ≠ 0
X0 : 3 / 2 = 1
⊢ 2 ∣ d

State before:
case neg.intro.h
c m : ℤ
h1 : ¬c = 0
d : ℤ
h0 : c * 2 ∣ c * d
h : m - 3 = 2 * c * d
X : 2 ≠ 0
X0 : 3 / 2 = 1
⊢ 2 ∣ d
Tactic:
exact Int.dvd_of_mul_dvd_mul_left h1 h0
State after:
no goals