Theorem: IMOSL.IMO2019N4.dvd_sq_iff_dvd_sq_of_dvd_add (IMOSLLean4/IMO2019/N4/N4.lean)

State before:
a b c : ℕ
h : c ∣ a + b
⊢ c ∣ a ^ 2 ↔ c ∣ b ^ 2
Tactic:
have h0 {u v w : ℕ} (h0 : u ∣ v + w) : u ∣ v ^ 2 ↔ u ∣ v * w := by
  apply dvd_iff_of_dvd_add
  rw [sq, ← Nat.mul_add]
  exact h0.mul_left v
State after:
a b c : ℕ
h : c ∣ a + b
h0 : ∀ {u v w : ℕ}, u ∣ v + w → (u ∣ v ^ 2 ↔ u ∣ v * w)
⊢ c ∣ a ^ 2 ↔ c ∣ b ^ 2

State before:
a b c : ℕ
h : c ∣ a + b
h0 : ∀ {u v w : ℕ}, u ∣ v + w → (u ∣ v ^ 2 ↔ u ∣ v * w)
⊢ c ∣ a ^ 2 ↔ c ∣ b ^ 2
Tactic:
rw [h0 h, mul_comm, ← h0 (a.add_comm b ▸ h)]
State after:
no goals

State before:
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v ^ 2 ↔ u ∣ v * w
Tactic:
apply dvd_iff_of_dvd_add
State after:
case h
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v ^ 2 + v * w

State before:
case h
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v ^ 2 + v * w
Tactic:
rw [sq, ← Nat.mul_add]
State after:
case h
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v * (v + w)

State before:
case h
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v * (v + w)
Tactic:
exact h0.mul_left v
State after:
no goals