R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ¬1 ∈ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ IsMaximal I
apply Ideal.isMaximal_iff.2
case left
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ¬1 ∈ I

case right
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ¬1 ∈ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
constructor
case left
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
⊢ False
case left
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ¬1 ∈ I
intro h
case left.intro.mk.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
w✝¹ : R ⧸ I
x : R
w✝ : R ⧸ I
y : R
hxy : Quot.mk Setoid.r x ≠ Quot.mk Setoid.r y
⊢ False
case left
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
⊢ False
rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩
no goals
case left.intro.mk.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
w✝¹ : R ⧸ I
x : R
w✝ : R ⧸ I
y : R
hxy : Quot.mk Setoid.r x ≠ Quot.mk Setoid.r y
⊢ False
exact hxy (Ideal.Quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h))
case right
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
⊢ 1 ∈ J
case right
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
intro J x hIJ hxnI hxJ
case right.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : ↑(mk I) x * Quot.mk Setoid.r y = 1
⊢ 1 ∈ J
case right
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
⊢ 1 ∈ J
rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩
case right.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : ↑(mk I) x * Quot.mk Setoid.r y = 1
⊢ x * y - (x * y - 1) ∈ J
case right.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : ↑(mk I) x * Quot.mk Setoid.r y = 1
⊢ 1 ∈ J
rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]
no goals
case right.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : ↑(mk I) x * Quot.mk Setoid.r y = 1
⊢ x * y - (x * y - 1) ∈ J
refine' J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))