R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ DiscreteValuationRing R
rw [iff_pid_with_one_nonzero_prime]
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
haveI PID : IsPrincipalIdealRing R := aux_pid_of_ufd_of_unique_irreducible R h₁ h₂
case intro
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₁ : ∃ p, Irreducible p
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
obtain ⟨p, hp⟩ := h₁
case intro.refine'_1
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ span {p} ≠ ⊥

case intro.refine'_2
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ IsPrime (span {p})

case intro.refine'_3
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = span {p}
case intro
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ IsPrincipalIdealRing R ∧ ∃! P, P ≠ ⊥ ∧ IsPrime P
refine' ⟨PID, ⟨Ideal.span {p}, ⟨_, _⟩, _⟩⟩
case intro.refine'_1
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∃ x, x ∈ span {p} ∧ x ≠ 0
case intro.refine'_1
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ span {p} ≠ ⊥
rw [Submodule.ne_bot_iff]
no goals
case intro.refine'_1
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∃ x, x ∈ span {p} ∧ x ≠ 0
refine' ⟨p, Ideal.mem_span_singleton.mpr (dvd_refl p), hp.ne_zero⟩
no goals
case intro.refine'_2
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ IsPrime (span {p})
rwa [Ideal.span_singleton_prime hp.ne_zero, ← UniqueFactorizationMonoid.irreducible_iff_prime]
case intro.refine'_3
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
⊢ (fun P => P ≠ ⊥ ∧ IsPrime P) I → I = span {p}
case intro.refine'_3
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
⊢ ∀ (y : Ideal R), (fun P => P ≠ ⊥ ∧ IsPrime P) y → y = span {p}
intro I
case intro.refine'_3
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
⊢ (fun P => P ≠ ⊥ ∧ IsPrime P) (Submodule.span R {Submodule.IsPrincipal.generator I}) →
    Submodule.span R {Submodule.IsPrincipal.generator I} = span {p}
case intro.refine'_3
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
⊢ (fun P => P ≠ ⊥ ∧ IsPrime P) I → I = span {p}
rw [← Submodule.IsPrincipal.span_singleton_generator I]
case intro.refine'_3.intro
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Submodule.span R {Submodule.IsPrincipal.generator I} ≠ ⊥
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Submodule.span R {Submodule.IsPrincipal.generator I} = span {p}
case intro.refine'_3
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
⊢ (fun P => P ≠ ⊥ ∧ IsPrime P) (Submodule.span R {Submodule.IsPrincipal.generator I}) →
    Submodule.span R {Submodule.IsPrincipal.generator I} = span {p}
rintro ⟨I0, hI⟩
case intro.refine'_3.intro
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Submodule.span R {Submodule.IsPrincipal.generator I} ≠ ⊥
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Associated (Submodule.IsPrincipal.generator I) p
case intro.refine'_3.intro
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Submodule.span R {Submodule.IsPrincipal.generator I} ≠ ⊥
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Submodule.span R {Submodule.IsPrincipal.generator I} = span {p}
apply span_singleton_eq_span_singleton.mpr
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Submodule.span R {Submodule.IsPrincipal.generator I} ≠ ⊥
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Irreducible (Submodule.IsPrincipal.generator I)
case intro.refine'_3.intro
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Submodule.span R {Submodule.IsPrincipal.generator I} ≠ ⊥
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Associated (Submodule.IsPrincipal.generator I) p
apply h₂ _ hp
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : ¬Submodule.IsPrincipal.generator I = 0
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Irreducible (Submodule.IsPrincipal.generator I)
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : Submodule.span R {Submodule.IsPrincipal.generator I} ≠ ⊥
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Irreducible (Submodule.IsPrincipal.generator I)
erw [Ne.def, span_singleton_eq_bot] at I0
no goals
R✝ : Type ?u.105600
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : UniqueFactorizationMonoid R
h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q
PID : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
I0 : ¬Submodule.IsPrincipal.generator I = 0
hI : IsPrime (Submodule.span R {Submodule.IsPrincipal.generator I})
⊢ Irreducible (Submodule.IsPrincipal.generator I)
rwa [UniqueFactorizationMonoid.irreducible_iff_prime, ← Ideal.span_singleton_prime I0]