case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
⊢ x ∣ a ∨ x ∣ b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
⊢ x ∣ a ∨ x ∣ b
cases' gcd_dvd_left x a with y hy
case intro.inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ x ∣ a ∨ x ∣ b

case intro.inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit y
⊢ x ∣ a ∨ x ∣ b
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
⊢ x ∣ a ∨ x ∣ b
cases' hi.isUnit_or_isUnit hy with hu hu
case intro.inl.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ x ∣ b
case intro.inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ x ∣ a ∨ x ∣ b
right
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ x ∣ gcd (x * b) (a * b)

α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ gcd (x * b) (a * b) ∣ b
case intro.inl.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ x ∣ b
trans gcd (x * b) (a * b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ gcd (x * b) (a * b) ∣ b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ x ∣ gcd (x * b) (a * b)

α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ gcd (x * b) (a * b) ∣ b
apply dvd_gcd (dvd_mul_right x b) h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ gcd x a * b ∣ b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ gcd (x * b) (a * b) ∣ b
rw [(gcd_mul_right' b x a).dvd_iff_dvd_left]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit (gcd x a)
⊢ gcd x a * b ∣ b
exact (associated_unit_mul_left _ _ hu).dvd
case intro.inr.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit y
⊢ x ∣ a
case intro.inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit y
⊢ x ∣ a ∨ x ∣ b
left
case intro.inr.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit y
⊢ gcd x a * y ∣ a
case intro.inr.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit y
⊢ x ∣ a
rw [hy]
no goals
case intro.inr.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
x : α
hi : Irreducible x
a b : α
h : x ∣ a * b
y : α
hy : x = gcd x a * y
hu : IsUnit y
⊢ gcd x a * y ∣ a
exact dvd_trans (associated_mul_unit_left _ _ hu).dvd (gcd_dvd_right x a)