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

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
⊢ (f.comp C).IsIntegral

Tactic:
have : (f'.comp C).IsIntegral := by
  haveI : f'.ker.IsMaximal := ker_isMaximal_of_surjective f' hf'
  let g : MvPolynomial _ R ⧸ (RingHom.ker f') →+* S :=
    Ideal.Quotient.lift (RingHom.ker f') f' fun _ h => h
  have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f')) = f' :=
    ringHom_ext (fun r => rfl) fun i => rfl
  rw [← hfg, RingHom.comp_assoc]
  refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f')).trans _ g
    (g.isIntegral_of_surjective ?_)
  rw [← hfg] at hf'
  norm_num at hf'
  exact Function.Surjective.of_comp hf'

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f'.comp C).IsIntegral
⊢ (f.comp C).IsIntegral

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
⊢ (f'.comp C).IsIntegral

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

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
⊢ (f'.comp C).IsIntegral

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f'.comp C).IsIntegral
⊢ (f.comp C).IsIntegral

Tactic:
rw [RingHom.comp_assoc] at this

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp C)).IsIntegral
⊢ (f.comp C).IsIntegral

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective (⇑f ∘ ⇑(renameEquiv R e))
⊢ (f.comp C).IsIntegral

Tactic:
change Function.Surjective ↑f' at hf'

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
⊢ (f.comp C).IsIntegral

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ (g.comp ((Ideal.Quotient.mk (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
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
⊢ (f.comp C).IsIntegral

Tactic:
have hf' := Function.Surjective.comp hf (renameEquiv R e).surjective

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective (⇑f ∘ ⇑(renameEquiv R e))
⊢ (f.comp C).IsIntegral

Proof state:
case h.e'_5.h.e'_8
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp C)).IsIntegral
⊢ C = (renameEquiv R e).toRingEquiv.toRingHom.comp C

Tactic:
refine RingHom.ext fun x => ?_

Result:
case h.e'_5.h.e'_8
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
hf' : Function.Surjective ⇑f'
this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp C)).IsIntegral
x : R
⊢ C x = ((renameEquiv R e).toRingEquiv.toRingHom.comp C) x