Zulip Chat Archive
Stream: Is there code for X?
Topic: a * b^2 = c^2 implies IsSquare a
David Renshaw (Dec 06 2023 at 01:30):
import Mathlib.Tactic
lemma foo {a b c : ℤ} (hb : b ≠ 0) (h : a * b^2 = c^2) : IsSquare a := by
sorry
I'm stuck on this. It seems like it ought to be easy. Am I missing something?
Eric Wieser (Dec 06 2023 at 02:39):
import Mathlib
lemma foo {a b c : ℤ} (hb : b ≠ 0) (h : a * b^2 = c^2) : IsSquare a := by
have : b^2 ∣ c^2 := by dsimp only [Int.instDvdInt]; exact ⟨a, h.symm.trans <| mul_comm _ _⟩
rw [Int.pow_dvd_pow_iff two_pos] at this
obtain ⟨k, rfl⟩ := this
rw [mul_pow, mul_comm, mul_right_inj' (pow_ne_zero _ hb)] at h
rw [h]
exact ⟨k, sq k⟩
David Renshaw (Dec 06 2023 at 02:41):
Nice!
David Renshaw (Dec 06 2023 at 02:41):
Surely that first line should be
have : b^2 ∣ c^2 := Dvd.intro_left a h
Eric Wieser (Dec 06 2023 at 02:41):
I was struggling to find the lemma, thanks
David Renshaw (Dec 06 2023 at 02:41):
does exact? not find it for you?
Eric Wieser (Dec 06 2023 at 02:41):
I didn't try
David Renshaw (Dec 06 2023 at 02:43):
Int.pow_dvd_pow_iff two_pos is the big thing I was missing here. I suppose that exact? didn't find it for me because it needed the two_pos.
Eric Wieser (Dec 06 2023 at 02:50):
Maybe a more general form:
lemma IsSquare.of_int_mul {a b : ℤ} (ha : IsSquare a) (ha0 : a ≠ 0) (hb : IsSquare (a * b)) : IsSquare b := by
obtain ⟨a, rfl⟩ := ha
obtain ⟨z, hb⟩ := hb
rw [mul_comm] at hb
have := Dvd.intro_left _ hb
rw [← sq, ← sq, Int.pow_dvd_pow_iff two_pos] at this
obtain ⟨k, rfl⟩ := this
rw [mul_mul_mul_comm, mul_comm, mul_right_inj' ha0] at hb
rw [hb]
exact ⟨k, rfl⟩
Eric Wieser (Dec 06 2023 at 02:50):
Not golfed at all
Heather Macbeth (Dec 06 2023 at 03:09):
I can give you a proof with an "explicit" witness:
import Mathlib.Tactic.Polyrith
import Mathlib.RingTheory.Int.Basic
open Int hiding gcd gcd_dvd_left gcd_dvd_right
lemma foo {a b c : ℤ} (hb : b ≠ 0) (h : a * b^2 = c^2) : IsSquare a := by
obtain ⟨k, hk⟩ : ∃ k, b = gcd b c * k := gcd_dvd_left b c
obtain ⟨l, hl⟩ : ∃ l, c = gcd b c * l := gcd_dvd_right b c
use a * k * gcdB b c + l * gcdA b c
have hd : gcd b c ≠ 0 := fun hd => hb (by simpa [hd] using hk)
apply mul_right_cancel₀ (pow_ne_zero 2 hd)
have H : gcd b c = b * gcdA b c + c * gcdB b c := Int.gcd_eq_gcd_ab b c
polyrith
Ruben Van de Velde (Dec 06 2023 at 08:17):
My mind went to docs#exists_associated_pow_of_mul_eq_pow, but it doesn't apply here
David Renshaw (Dec 06 2023 at 11:37):
Some previous cases of folks getting stuck on basically the same thing:
David Renshaw (Dec 06 2023 at 11:40):
Neither exact?nor rw? are helpful here. Nor is moogle.ai (at least with the queries I tried).
Yury G. Kudryashov (Dec 06 2023 at 13:48):
Should we add Int.div_pow with some divisibility assumption?
Yury G. Kudryashov (Dec 06 2023 at 13:48):
(and Nat.div_pow)
Yaël Dillies (Dec 06 2023 at 13:49):
docs#Nat.pow_div is something to look out for
Yury G. Kudryashov (Dec 06 2023 at 14:25):
It's about x ^ m / x ^ n, we need (x / y) ^ n.
Yaël Dillies (Dec 06 2023 at 14:26):
Yes, so you should make clear in the lemma names how your new lemma is different from the old.
Yury G. Kudryashov (Dec 06 2023 at 14:27):
IMHO, Nat.pow_div should be renamed to Nat.pow_sub with swapped LHS and RHS.
Yury G. Kudryashov (Dec 06 2023 at 14:28):
Compare with docs#pow_sub
Yury G. Kudryashov (Dec 06 2023 at 14:31):
BTW, should we have a typeclass for b ≠ 0 → (a * b) / b = a? It's true for GroupWithZeros but also for Nat and Int.
Yaël Dillies (Dec 06 2023 at 14:32):
Semi-related: #8839
Last updated: Dec 20 2023 at 11:08 UTC