R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
⊢ ∀ (x : Ideal R), ¬x ∈ nonPrincipals R
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
⊢ IsPrincipalIdealRing R
rw [← nonPrincipals_eq_empty_iff, Set.eq_empty_iff_forall_not_mem]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
⊢ False
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
⊢ ∀ (x : Ideal R), ¬x ∈ nonPrincipals R
intro J hJ
case intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
⊢ False
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
⊢ False
obtain ⟨I, Ibad, -, Imax⟩ := zorn_nonempty_partialOrder₀ (nonPrincipals R) nonPrincipals_zorn _ hJ
case intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
⊢ False
case intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
⊢ False
have Imax' : ∀ {J}, I < J → J.IsPrincipal := by
  intro J hJ
  by_contra He
  exact hJ.ne (Imax _ ((nonPrincipals_def R).2 He) hJ.le).symm
case pos
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : I = ⊤
⊢ False

case neg
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
⊢ False
case intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
⊢ False
by_cases hI1 : I = ⊤
case neg
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
⊢ x ∈ I
case neg
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
⊢ False
refine' Ibad (H I ⟨hI1, fun {x y} hxy => or_iff_not_imp_right.mpr fun hy => _⟩)
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
⊢ x ∈ I
case neg
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
⊢ x ∈ I
obtain ⟨a, ha⟩ : (I ⊔ span {y}).IsPrincipal :=
  Imax' (left_lt_sup.mpr (mt I.span_singleton_le_iff_mem.mp hy))
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
He : ¬IsPrincipal (colon I (Ideal.span {y}))
⊢ x ∈ I

case He
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
⊢ ¬IsPrincipal (colon I (Ideal.span {y}))
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
⊢ x ∈ I
suffices He : ¬(I.colon (span {y})).IsPrincipal
case He.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ False
case He
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
⊢ ¬IsPrincipal (colon I (Ideal.span {y}))
rintro ⟨b, hb⟩
case He.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ I = Submodule.span R {a * b}
case He.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ False
refine (nonPrincipals_def _).1 Ibad ⟨a * b, ?_⟩
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
⊢ i ∈ Submodule.span R {a * b}

case He.mk.intro.refine'_2
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ Ideal.span {a} * Ideal.span {b} ≤ I
case He.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ I = Submodule.span R {a * b}
refine'
  le_antisymm (α := Ideal R) (fun i hi => _) <| (span_singleton_mul_span_singleton a b).ge.trans _
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J✝ : Ideal R
hJ✝ : J✝ ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
J : Ideal R
hJ : I < J
⊢ IsPrincipal J
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
⊢ ∀ {J : Ideal R}, I < J → IsPrincipal J
intro J hJ
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J✝ : Ideal R
hJ✝ : J✝ ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
J : Ideal R
hJ : I < J
He : ¬IsPrincipal J
⊢ False
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J✝ : Ideal R
hJ✝ : J✝ ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
J : Ideal R
hJ : I < J
⊢ IsPrincipal J
by_contra He
no goals
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J✝ : Ideal R
hJ✝ : J✝ ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
J : Ideal R
hJ : I < J
He : ¬IsPrincipal J
⊢ False
exact hJ.ne (Imax _ ((nonPrincipals_def R).2 He) hJ.le).symm
case pos
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
Ibad : ⊤ ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → ⊤ ≤ z → z = ⊤
Imax' : ∀ {J : Ideal R}, ⊤ < J → IsPrincipal J
⊢ False
case pos
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : I = ⊤
⊢ False
subst hI1
no goals
case pos
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
Ibad : ⊤ ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → ⊤ ≤ z → z = ⊤
Imax' : ∀ {J : Ideal R}, ⊤ < J → IsPrincipal J
⊢ False
exact Ibad top_isPrincipal
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
He : ¬IsPrincipal (colon I (Ideal.span {y}))
⊢ x ∈ colon I (Ideal.span {y})
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
He : ¬IsPrincipal (colon I (Ideal.span {y}))
⊢ x ∈ I
rw [← Imax _ ((nonPrincipals_def R).2 He) fun a ha =>
    Ideal.mem_colon_singleton.2 (mul_mem_right _ _ ha)]
no goals
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
He : ¬IsPrincipal (colon I (Ideal.span {y}))
⊢ x ∈ colon I (Ideal.span {y})
exact Ideal.mem_colon_singleton.2 hxy
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ Ideal.span {y}
⊢ i ∈ Submodule.span R {a * b}
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
⊢ i ∈ Submodule.span R {a * b}
have hisup : i ∈ I ⊔ span {y} := Ideal.mem_sup_left hi
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ Ideal.span {y}
this : y ∈ I ⊔ Ideal.span {y}
⊢ i ∈ Submodule.span R {a * b}
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ Ideal.span {y}
⊢ i ∈ Submodule.span R {a * b}
have : y ∈ I ⊔ span {y} := Ideal.mem_sup_right (Ideal.mem_span_singleton_self y)
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : ∃ a_1, a_1 * a = i
this : ∃ a_1, a_1 * a = y
⊢ i ∈ Submodule.span R {a * b}
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ Ideal.span {y}
this : y ∈ I ⊔ Ideal.span {y}
⊢ i ∈ Submodule.span R {a * b}
erw [ha, mem_span_singleton'] at hisup this
case He.mk.intro.refine'_1.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b i : R
hi : i ∈ I
hisup : ∃ a_1, a_1 * a = i
v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
⊢ i ∈ Submodule.span R {a * b}
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : ∃ a_1, a_1 * a = i
this : ∃ a_1, a_1 * a = y
⊢ i ∈ Submodule.span R {a * b}
obtain ⟨v, rfl⟩ := this
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u * a ∈ Submodule.span R {a * b}
case He.mk.intro.refine'_1.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b i : R
hi : i ∈ I
hisup : ∃ a_1, a_1 * a = i
v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
⊢ i ∈ Submodule.span R {a * b}
obtain ⟨u, rfl⟩ := hisup
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
hucolon : u ∈ colon I (Ideal.span {v * a})
⊢ u * a ∈ Submodule.span R {a * b}
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u * a ∈ Submodule.span R {a * b}
have hucolon : u ∈ I.colon (span {v * a}) := by
  rw [Ideal.mem_colon_singleton, mul_comm v, ← mul_assoc]
  exact mul_mem_right _ _ hi
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
hucolon : ∃ a, a * b = u
⊢ u * a ∈ Submodule.span R {a * b}
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
hucolon : u ∈ colon I (Ideal.span {v * a})
⊢ u * a ∈ Submodule.span R {a * b}
erw [hb, mem_span_singleton'] at hucolon
case He.mk.intro.refine'_1.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
z : R
hi : z * b * a ∈ I
⊢ z * b * a ∈ Submodule.span R {a * b}
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
hucolon : ∃ a, a * b = u
⊢ u * a ∈ Submodule.span R {a * b}
obtain ⟨z, rfl⟩ := hucolon
no goals
case He.mk.intro.refine'_1.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
z : R
hi : z * b * a ∈ I
⊢ z * b * a ∈ Submodule.span R {a * b}
exact mem_span_singleton'.2 ⟨z, by ring⟩
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u * a * v ∈ I
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u ∈ colon I (Ideal.span {v * a})
rw [Ideal.mem_colon_singleton, mul_comm v, ← mul_assoc]
no goals
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u * a * v ∈ I
exact mul_mem_right _ _ hi
no goals
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
z : R
hi : z * b * a ∈ I
⊢ z * (a * b) = z * b * a
ring
case He.mk.intro.refine'_2
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ I * Ideal.span {b} ≤ I ∧ b * y ∈ I
case He.mk.intro.refine'_2
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ Ideal.span {a} * Ideal.span {b} ≤ I
rw [← Ideal.submodule_span_eq, ← ha, Ideal.sup_mul, sup_le_iff,
  span_singleton_mul_span_singleton, mul_comm y, Ideal.span_singleton_le_iff_mem]
no goals
case He.mk.intro.refine'_2
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ I * Ideal.span {b} ≤ I ∧ b * y ∈ I
exact ⟨mul_le_right, Ideal.mem_colon_singleton.1 <| hb.symm ▸ Ideal.mem_span_singleton_self b⟩