case refine'_1
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
H : IsDomain (R ⧸ I)
⊢ 0 ≠ 1

case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
⊢ IsDomain (R ⧸ I) ↔ IsPrime I
refine' ⟨fun H => ⟨zero_ne_one_iff.1 _, fun {x y} h => _⟩, fun h => inferInstance⟩
case refine'_1
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
H : IsDomain (R ⧸ I)
this : Nontrivial (R ⧸ I)
⊢ 0 ≠ 1
case refine'_1
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
H : IsDomain (R ⧸ I)
⊢ 0 ≠ 1
haveI : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
no goals
case refine'_1
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
H : IsDomain (R ⧸ I)
this : Nontrivial (R ⧸ I)
⊢ 0 ≠ 1
exact zero_ne_one
case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : ↑(mk I) x * ↑(mk I) y = 0
⊢ ↑(mk I) x = 0 ∨ ↑(mk I) y = 0
case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
simp only [← eq_zero_iff_mem, (mk I).map_mul] at h⊢
case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : ↑(mk I) x * ↑(mk I) y = 0
this : NoZeroDivisors (R ⧸ I)
⊢ ↑(mk I) x = 0 ∨ ↑(mk I) y = 0
case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : ↑(mk I) x * ↑(mk I) y = 0
⊢ ↑(mk I) x = 0 ∨ ↑(mk I) y = 0
haveI := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H
no goals
case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : ↑(mk I) x * ↑(mk I) y = 0
this : NoZeroDivisors (R ⧸ I)
⊢ ↑(mk I) x = 0 ∨ ↑(mk I) y = 0
exact eq_zero_or_eq_zero_of_mul_eq_zero h