R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ 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
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
⊢ IsCoprime x y
apply isCoprime_of_dvd x y nonzero
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
⊢ False
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
⊢ ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
intro z znu znz zx zy
case intro.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ False
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
⊢ False
obtain ⟨i, h1, h2⟩ := WfDvdMonoid.exists_irreducible_factor znu znz
case intro.intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ z ∣ y
case intro.intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ i ∣ y
apply dvd_trans h2
no goals
case intro.intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ z ∣ y
assumption