case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
⊢ IsCoprime p n → ¬p ∣ n

case mpr
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
⊢ ¬p ∣ n → IsCoprime p n
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
⊢ IsCoprime p n ↔ ¬p ∣ n
constructor
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ False
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
⊢ IsCoprime p n → ¬p ∣ n
intro co H
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ IsUnit p
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ False
apply pp.not_unit
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ 1
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ IsUnit p
rw [isUnit_iff_dvd_one]
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ n * 1
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ 1
apply IsCoprime.dvd_of_dvd_mul_left co
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ n
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ n * 1
rw [mul_one n]
no goals
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ n
exact H
case mpr
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ IsCoprime p n
case mpr
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
⊢ ¬p ∣ n → IsCoprime p n
intro nd
case mpr.nonzero
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ ¬(p = 0 ∧ n = 0)

case mpr.H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ ∀ (z : R), Irreducible z → z ∣ p → ¬z ∣ n
case mpr
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ IsCoprime p n
apply isCoprime_of_irreducible_dvd
case mpr.H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
z : R
zi : Irreducible z
zp : z ∣ p
zn : z ∣ n
⊢ False
case mpr.H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ ∀ (z : R), Irreducible z → z ∣ p → ¬z ∣ n
rintro z zi zp zn
no goals
case mpr.H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
z : R
zi : Irreducible z
zp : z ∣ p
zn : z ∣ n
⊢ False
exact nd ((zi.associated_of_dvd pp zp).symm.dvd.trans zn)
case mpr.nonzero.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
hp : p = 0
⊢ False
case mpr.nonzero
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ ¬(p = 0 ∧ n = 0)
rintro ⟨hp, -⟩
no goals
case mpr.nonzero.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
hp : p = 0
⊢ False
exact pp.ne_zero hp