Theorem: Imo2007P5.bad_symm (Compfiles/Imo2007P5.lean)

State before:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑b * ↑a - 1 ∣ (n * ↑b ^ 2 - 1) ^ 2
Tactic:
rw [mul_right_comm, sub_sq', add_comm, mul_right_comm _ _ (1 : ℤ), ← sub_sq']
State after:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2

State before:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Tactic:
replace h := dvd_mul_of_dvd_left h ((n * b ^ 2) ^ 2)
State after:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 * (n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2

State before:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ (n * ↑a ^ 2 - 1) ^ 2 * (n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Tactic:
rw [← mul_pow, sub_one_mul, mul_mul_mul_comm, ← sq, ← mul_pow, ← mul_pow, ← mul_assoc] at h
State after:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2

State before:
n : ℤ
a b : ℕ
h : n * ↑a * ↑b - 1 ∣ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2
⊢ n * ↑a * ↑b - 1 ∣ (1 - n * ↑b ^ 2) ^ 2
Tactic:
rw [← Int.modEq_zero_iff_dvd] at h ⊢
State after:
n : ℤ
a b : ℕ
h : ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
⊢ (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]

State before:
n : ℤ
a b : ℕ
h : ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
⊢ (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
Tactic:
revert h
State after:
n : ℤ
a b : ℕ
⊢ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1] → (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]

State before:
n : ℤ
a b : ℕ
⊢ ((n * ↑a * ↑b) ^ 2 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1] → (1 - n * ↑b ^ 2) ^ 2 ≡ 0 [ZMOD n * ↑a * ↑b - 1]
Tactic:
refine ((Int.ModEq.sub_right _ ?_).pow _).trans
State after:
n : ℤ
a b : ℕ
⊢ 1 ≡ (n * ↑a * ↑b) ^ 2 [ZMOD n * ↑a * ↑b - 1]

State before:
n : ℤ
a b : ℕ
⊢ 1 ≡ (n * ↑a * ↑b) ^ 2 [ZMOD n * ↑a * ↑b - 1]
Tactic:
nth_rewrite 1 [← one_pow 2]
State after:
n : ℤ
a b : ℕ
⊢ 1 ≡ (n * ↑a * ↑b) ^ 2 [ZMOD n * ↑a * ↑b - 1 ^ 2]

State before:
n : ℤ
a b : ℕ
⊢ 1 ≡ (n * ↑a * ↑b) ^ 2 [ZMOD n * ↑a * ↑b - 1 ^ 2]
Tactic:
exact ((n * a * b).modEq_sub 1).symm.pow 2
State after:
no goals