-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem comp_C_integral_of_surjective_of_isJacobsonRing {S : Type*} [Field S] (f : R[X] →+* S)
    (hf : Function.Surjective ↑f) : (f.comp C).IsIntegral

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective ⇑(g.comp (Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g

Tactic:
norm_num at hf

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ (g.comp ((Ideal.Quotient.mk (RingHom.ker f)).comp C)).IsIntegral

Tactic:
refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f)).trans _ g
  (g.isIntegral_of_surjective ?_)

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ (f.comp C).IsIntegral

Tactic:
rw [← hfg, RingHom.comp_assoc]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ (g.comp ((Ideal.Quotient.mk (RingHom.ker f)).comp C)).IsIntegral

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
⊢ (f.comp C).IsIntegral

Tactic:
haveI : f.ker.IsMaximal := RingHom.ker_isMaximal_of_surjective f hf

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
⊢ (f.comp C).IsIntegral

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
⊢ (f.comp C).IsIntegral

Tactic:
let g : R[X] ⧸ (RingHom.ker f) →+* S := Ideal.Quotient.lift (RingHom.ker f) f fun _ h => h

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
⊢ (f.comp C).IsIntegral

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g

Tactic:
exact Function.Surjective.of_comp hf

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
⊢ (f.comp C).IsIntegral

Tactic:
have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f := ringHom_ext' rfl rfl

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ (f.comp C).IsIntegral

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
hf : Function.Surjective ⇑f
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g

Tactic:
rw [← hfg] at hf

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
S : Type u_2
inst✝ : Field S
f : R[X] →+* S
this : (RingHom.ker f).IsMaximal
g : R[X] ⧸ RingHom.ker f →+* S := Ideal.Quotient.lift (RingHom.ker f) f ⋯
hf : Function.Surjective ⇑(g.comp (Ideal.Quotient.mk (RingHom.ker f)))
hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
⊢ Function.Surjective ⇑g