-- Mathlib/Algebra/Squarefree/Basic.lean
theorem dvd_of_squarefree_of_mul_dvd_mul_right (hx : Squarefree x) (h : d * d ∣ x * y) : d ∣ y

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
⊢ d ^ 2 = a * b

Tactic:
rw [sq, eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ b = d * c

Tactic:
rw [hc, ← eq, mul_comm]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ d ∣ y

Tactic:
exact dvd_trans ⟨c, by rw [hc, ← eq, mul_comm]⟩ hb

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
⊢ d ∣ y

Tactic:
obtain ⟨a, b, ha, hb, eq⟩ := exists_dvd_and_dvd_of_dvd_mul h

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
ha : a ∣ x
hb : b ∣ y
eq : d * d = a * b
⊢ d ∣ y

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
ha : a ∣ x
hb : b ∣ y
eq : d * d = a * b
⊢ d ∣ y

Tactic:
replace ha : Squarefree a := hx.squarefree_of_dvd ha

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
⊢ d ∣ y

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
c : R
hc : d = a * c
⊢ d ∣ y

Tactic:
rw [hc, mul_assoc, (mul_right_injective₀ ha.ne_zero).eq_iff] at eq

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ d ∣ y

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
⊢ d ∣ y

Tactic:
obtain ⟨c, hc⟩ : a ∣ d := ha.isRadical 2 d ⟨b, by rw [sq, eq]⟩

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
c : R
hc : d = a * c
⊢ d ∣ y

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
⊢ d ∣ y

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
⊢ d ∣ y