R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ IsCoprime x y
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
⊢ x ∣ y ∨ IsCoprime x y
refine' or_iff_not_imp_left.2 fun h' => _
case nonzero
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ ¬(x = 0 ∧ y = 0)

case H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ IsCoprime x y
apply isCoprime_of_dvd
case nonzero.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
h : Irreducible 0
h' : ¬0 ∣ 0
⊢ False
case nonzero
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ ¬(x = 0 ∧ y = 0)
rintro ⟨rfl, rfl⟩
no goals
case nonzero.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
h : Irreducible 0
h' : ¬0 ∣ 0
⊢ False
simp at h
case H.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
y z : R
nu : z ∈ nonunits R
w : R
h : Irreducible (z * w)
h' : ¬z * w ∣ y
dy : z ∣ y
⊢ False
case H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
rintro z nu - ⟨w, rfl⟩ dy
case H.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
y z : R
nu : z ∈ nonunits R
w : R
h : Irreducible (z * w)
h' : ¬z * w ∣ y
dy : z ∣ y
⊢ z * w ∣ z
case H.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
y z : R
nu : z ∈ nonunits R
w : R
h : Irreducible (z * w)
h' : ¬z * w ∣ y
dy : z ∣ y
⊢ False
refine' h' (dvd_trans _ dy)
no goals
case H.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
y z : R
nu : z ∈ nonunits R
w : R
h : Irreducible (z * w)
h' : ¬z * w ∣ y
dy : z ∣ y
⊢ z * w ∣ z
simpa using mul_dvd_mul_left z (isUnit_iff_dvd_one.1 <| (of_irreducible_mul h).resolve_left nu)