R : Type u
S : Type ?u.193946
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : IsMaximal I
x : R
hx : ↑C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I
R : Type u
S : Type ?u.193946
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : IsMaximal I
x : R
hx : ↑C x ∈ I
⊢ x = 0
refine' Classical.by_contradiction fun hx0 => hI.ne_top ((eq_top_iff_one I).2 _)
case intro
R : Type u
S : Type ?u.193946
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : IsMaximal I
x : R
hx : ↑C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 ∈ I
R : Type u
S : Type ?u.193946
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : IsMaximal I
x : R
hx : ↑C x ∈ I
hx0 : ¬x = 0
⊢ 1 ∈ I
obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0
case h.e'_4
R : Type u
S : Type ?u.193946
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : IsMaximal I
x : R
hx : ↑C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = ↑C y * ↑C x
case intro
R : Type u
S : Type ?u.193946
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : IsMaximal I
x : R
hx : ↑C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 ∈ I
convert I.mul_mem_left (C y) hx
no goals
case h.e'_4
R : Type u
S : Type ?u.193946
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : IsMaximal I
x : R
hx : ↑C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = ↑C y * ↑C x
rw [← C.map_mul, hR.mul_comm y x, hy, RingHom.map_one]