case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
⊢ q / GCDMonoid.gcd p q ≠ 0
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0
obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_right p q
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
⊢ q / GCDMonoid.gcd p q ≠ 0
obtain ⟨pq0, r0⟩ : GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ q / GCDMonoid.gcd p q ≠ 0
nth_rw 1 [hr]
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
rw [mul_comm, EuclideanDomain.mul_div_cancel _ pq0]
no goals
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
exact r0