-- Mathlib/RingTheory/Ideal/Quotient/Basic.lean
theorem maximal_of_isField {R} [CommRing R] (I : Ideal R) (hqf : IsField (R ⧸ I)) :
    I.IsMaximal

Proof state:
case left.intro.mk.intro.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
w✝¹ : R ⧸ I
x : R
w✝ : R ⧸ I
y : R
hxy : Quot.mk (⇑(Submodule.quotientRel I)) x ≠ Quot.mk (⇑(Submodule.quotientRel I)) y
⊢ False

Tactic:
exact hxy (Ideal.Quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h))

Result:
no goals

Proof state:
case right.intro.mk
R : Type u_1
inst✝ : CommRing 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 (⇑(Submodule.quotientRel I)) y = 1
⊢ 1 ∈ J

Tactic:
rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]

Result:
case right.intro.mk
R : Type u_1
inst✝ : CommRing 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 (⇑(Submodule.quotientRel I)) y = 1
⊢ x * y - (x * y - 1) ∈ J

Proof state:
case right.intro.mk
R : Type u_1
inst✝ : CommRing 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 (⇑(Submodule.quotientRel I)) y = 1
⊢ x * y - (x * y - 1) ∈ J

Tactic:
exact J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ I.IsMaximal

Tactic:
apply Ideal.isMaximal_iff.2

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Proof state:
case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ 1 ∉ I

Tactic:
intro h

Result:
case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
⊢ False

Proof state:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
⊢ 1 ∈ J

Tactic:
rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩

Result:
case right.intro.mk
R : Type u_1
inst✝ : CommRing 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 (⇑(Submodule.quotientRel I)) y = 1
⊢ 1 ∈ J

Proof state:
case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
⊢ False

Tactic:
rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩

Result:
case left.intro.mk.intro.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
w✝¹ : R ⧸ I
x : R
w✝ : R ⧸ I
y : R
hxy : Quot.mk (⇑(Submodule.quotientRel I)) x ≠ Quot.mk (⇑(Submodule.quotientRel I)) y
⊢ False

Proof state:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
intro J x hIJ hxnI hxJ

Result:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
⊢ 1 ∈ J

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
constructor

Result:
case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ 1 ∉ I

case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J