R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
⊢ 1 ∈ J
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
⊢ Ideal.IsMaximal (ker f)
refine'
  Ideal.isMaximal_iff.mpr
    ⟨fun h1 => one_ne_zero' K <| map_one f ▸ (mem_ker f).mp h1, fun J x hJ hxf hxJ => _⟩
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
⊢ 1 ∈ J
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
⊢ 1 ∈ J
obtain ⟨y, hy⟩ := hf (f x)⁻¹
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
H : 1 = y * x - (y * x - 1)
⊢ 1 ∈ J
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
⊢ 1 ∈ J
have H : 1 = y * x - (y * x - 1) := (sub_sub_cancel _ _).symm
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
H : 1 = y * x - (y * x - 1)
⊢ y * x - (y * x - 1) ∈ J
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
H : 1 = y * x - (y * x - 1)
⊢ 1 ∈ J
rw [H]
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
H : 1 = y * x - (y * x - 1)
⊢ y * x - 1 ∈ ker f
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
H : 1 = y * x - (y * x - 1)
⊢ y * x - (y * x - 1) ∈ J
refine' J.sub_mem (J.mul_mem_left _ hxJ) (hJ _)
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
H : 1 = y * x - (y * x - 1)
⊢ ↑f (y * x - 1) = 0
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
H : 1 = y * x - (y * x - 1)
⊢ y * x - 1 ∈ ker f
rw [mem_ker]
no goals
case intro
R✝ : Type u
S : Type v
T : Type w
R : Type u_1
K : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Field K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ↑f
J : Ideal R
x : R
hJ : ker f ≤ J
hxf : ¬x ∈ ker f
hxJ : x ∈ J
y : R
hy : ↑f y = (↑f x)⁻¹
H : 1 = y * x - (y * x - 1)
⊢ ↑f (y * x - 1) = 0
simp only [hy, map_sub, map_one, map_mul, inv_mul_cancel (mt (mem_ker f).mpr hxf), sub_self]