-- Mathlib/RingTheory/Ideal/Maps.lean
theorem ker_isMaximal_of_surjective {R K F : Type*} [Ring R] [DivisionRing K]
    [FunLike F R K] [RingHomClass F R K] (f : F)
    (hf : Function.Surjective f) : (ker f).IsMaximal

Proof state:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Tactic:
rw [H]

Result:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Proof state:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Tactic:
simp only [hy, map_sub, map_one, map_mul, inv_mul_cancel₀ (mt mem_ker.mpr hxf :), sub_self]

Result:
no goals

Proof state:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Tactic:
rw [mem_ker]

Result:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Proof state:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Tactic:
refine J.sub_mem (J.mul_mem_left _ hxJ) (hJ ?_)

Result:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Proof state:
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Tactic:
obtain ⟨y, hy⟩ := hf (f x)⁻¹

Result:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Proof state:
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R K
inst✝ : RingHomClass F R K
f : F
hf : Function.Surjective ⇑f
⊢ (ker f).IsMaximal

Tactic:
refine
  Ideal.isMaximal_iff.mpr
    ⟨fun h1 => one_ne_zero' K <| map_one f ▸ mem_ker.mp h1, fun J x hJ hxf hxJ => ?_⟩

Result:
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Proof state:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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

Tactic:
have H : 1 = y * x - (y * x - 1) := (sub_sub_cancel _ _).symm

Result:
case intro
R : Type u_1
K : Type u_2
F : Type u_3
inst✝³ : Ring R
inst✝² : DivisionRing K
inst✝¹ : FunLike F R 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