awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
hf : RingHom.IsIntegral.{u, v} (A := S ⧸ Q') (algebraMap R (S ⧸ Q'))
hf₁ : w'.IsIntegral
⊢ RingHom.IsIntegral (w'.comp (algebraMap R (S ⧸ Q')))

Tactic:
apply RingHom.IsIntegral.trans

Premises used: RingHom.IsIntegral.trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
hf : Q'.IsMaximal
⊢ RingHom.IsIntegral.{u, v} (A := S ⧸ Q') (algebraMap R (S ⧸ Q'))

Tactic:
apply IH
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
⊢ Q'.IsMaximal

Tactic:
apply Polynomial.isMaximal_comap_C_of_isJacobsonRing

Premises used: Polynomial.isMaximal_comap_C_of_isJacobsonRing
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
rw : RingHom.IsIntegral (quotientMap Q Polynomial.C ⋯)
⊢ w'.IsIntegral

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
rw : RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk Q) Polynomial.C)
⊢ RingHom.IsIntegral (quotientMap Q Polynomial.C ⋯)

Tactic:
rw [isIntegral_quotientMap_iff _]

Premises used: isIntegral_quotientMap_iff
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
this : w'.toRingHom = quotientMap Q Polynomial.C ⋯
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk Q) Polynomial.C)

Tactic:
apply Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing

Premises used: Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
hf : w'.toRingHom = quotientMap Q Polynomial.C ⋯
⊢ w'.IsIntegral

Tactic:
suffices w'.toRingHom = Ideal.quotientMap Q (Polynomial.C) le_rfl by
        rw [this]
        rw [isIntegral_quotientMap_iff _]
        apply Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
⊢ w'.toRingHom = quotientMap Q Polynomial.C ⋯

Tactic:
rfl
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
hg : Function.Surjective.{v + 1, w + 1} (α := S[X] ⧸ Q) (β := T ⧸ P) (⇑w.toRingEquiv.toRingHom : (a : S[X] ⧸ Q) → T ⧸ P)
⊢ w.toRingEquiv.toRingHom.IsIntegral

Tactic:
apply RingHom.isIntegral_of_surjective

Premises used: RingHom.isIntegral_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
⊢ Function.Surjective.{v + 1, w + 1} (α := S[X] ⧸ Q) (β := T ⧸ P) (⇑w.toRingEquiv.toRingHom : (a : S[X] ⧸ Q) → T ⧸ P)

Tactic:
w.surjective

Premises used: AlgEquiv.surjective, Ideal.quotientEquiv
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u
S : Type v
T : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : IsJacobsonRing S
inst_4 : Algebra R S
inst_5 : Algebra R T
IH : ∀ (Q : Ideal S), Q.IsMaximal → RingHom.IsIntegral.{u, v} (A := S ⧸ Q) (algebraMap R (S ⧸ Q))
v : AlgEquiv.{u, v, w} R S[X] T
P : Ideal T
hP : P.IsMaximal
Q : Ideal S[X] := comap (↑v : S[X] →ₐ[R] T).toRingHom P
hw : Ideal.map v Q = P
hQ : Q.IsMaximal
w : AlgEquiv.{u, v, w} R (S[X] ⧸ Q) (T ⧸ P) := Q.quotientEquivAlg P v ⋯
Q' : Ideal S := comap (F := S →+* S[X]) Polynomial.C Q
w' : S ⧸ Q' →ₐ[R] S[X] ⧸ Q := quotientMapₐ Q (Cₐ R S) ⋯
h_eq :
  Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
⊢ Function.Surjective.{v + 1, w + 1} (α := S[X] ⧸ Q) (β := T ⧸ P) (⇑w.toRingEquiv.toRingHom : (a : S[X] ⧸ Q) → T ⧸ P)

Tactic:
exact w.surjective

Premises used: AlgEquiv.surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
zero :
  Function.Surjective (α := R) (β := MvPolynomial (Fin 0) R ⧸ P)
    (⇑(algebraMap R (MvPolynomial (Fin 0) R ⧸ P)) : (a : R) → MvPolynomial (Fin 0) R ⧸ P)
⊢ RingHom.IsIntegral (A := MvPolynomial (Fin 0) R ⧸ P) (algebraMap R (MvPolynomial (Fin 0) R ⧸ P))

Tactic:
apply RingHom.isIntegral_of_surjective

Premises used: RingHom.isIntegral_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
zero :
  Function.Surjective (α := R) (β := MvPolynomial (Fin 0) R)
    (⇑(algebraMap R (MvPolynomial (Fin 0) R)) : (a : R) → MvPolynomial (Fin 0) R)
⊢ Function.Surjective (α := R) (β := MvPolynomial (Fin 0) R ⧸ P)
    (⇑(algebraMap R (MvPolynomial (Fin 0) R ⧸ P)) : (a : R) → MvPolynomial (Fin 0) R ⧸ P)

Tactic:
apply Function.Surjective.comp Quotient.mk_surjective

Premises used: Function.Surjective.comp, Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective (α := R) (β := MvPolynomial (Fin 0) R)
    (⇑(algebraMap R (MvPolynomial (Fin 0) R)) : (a : R) → MvPolynomial (Fin 0) R)

Tactic:
C_surjective (Fin 0)

Premises used: MvPolynomial.C_surjective, OfNat.ofNat, Fin
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ Function.Surjective (α := R) (β := MvPolynomial (Fin 0) R)
    (⇑(algebraMap R (MvPolynomial (Fin 0) R)) : (a : R) → MvPolynomial (Fin 0) R)

Tactic:
exact C_surjective (Fin 0)

Premises used: MvPolynomial.C_surjective, OfNat.ofNat, Fin
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n_1 : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
n : ℕ
IH :
  ∀ (P : Ideal (MvPolynomial (Fin n) R)) (hP : P.IsMaximal),
    RingHom.IsIntegral (A := MvPolynomial (Fin n) R ⧸ P) (algebraMap R (MvPolynomial (Fin n) R ⧸ P))
P : Ideal (MvPolynomial (Fin (n + 1)) R)
hP : P.IsMaximal
⊢ RingHom.IsIntegral (A := MvPolynomial (Fin (n + 1)) R ⧸ P) (algebraMap R (MvPolynomial (Fin (n + 1)) R ⧸ P))

Tactic:
apply aux_IH IH (finSuccEquiv R n).symm P hP

Premises used: AlgEquiv.symm, MvPolynomial.finSuccEquiv, _private.0.MvPolynomial.aux_IH
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
zero :
  ∀ (P : Ideal (MvPolynomial (Fin 0) R)) (hP : P.IsMaximal),
    RingHom.IsIntegral (A := MvPolynomial (Fin 0) R ⧸ P) (algebraMap R (MvPolynomial (Fin 0) R ⧸ P))
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ (P : Ideal (MvPolynomial (Fin n) R)) (hP : P.IsMaximal),
        RingHom.IsIntegral (A := MvPolynomial (Fin n) R ⧸ P) (algebraMap R (MvPolynomial (Fin n) R ⧸ P)))
    (P : Ideal (MvPolynomial (Fin (n + 1)) R)) (hP : P.IsMaximal),
    RingHom.IsIntegral (A := MvPolynomial (Fin (n + 1)) R ⧸ P) (algebraMap R (MvPolynomial (Fin (n + 1)) R ⧸ P))
⊢ RingHom.IsIntegral (A := MvPolynomial (Fin n) R ⧸ P) (algebraMap R (MvPolynomial (Fin n) R ⧸ P))

Tactic:
induction n with
  | zero =>
    apply RingHom.isIntegral_of_surjective
    apply Function.Surjective.comp Quotient.mk_surjective
    exact C_surjective (Fin 0)
  | succ n IH => apply aux_IH IH (finSuccEquiv R n).symm P hP

Premises used: MvPolynomial.C_surjective, RingHom.isIntegral_of_surjective, Function.Surjective.comp, Quotient.mk_surjective, OfNat.ofNat, Fin
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
change : RingHom.IsIntegral (A := MvPolynomial (Fin n) R ⧸ P) (algebraMap R (MvPolynomial (Fin n) R ⧸ P))
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)

Tactic:
change RingHom.IsIntegral (algebraMap R (MvPolynomial (Fin n) R ⧸ P))

Premises used: Algebra.algebraMap, HasQuotient.Quotient, MvPolynomial, RingHom.IsIntegral, Fin
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP hP₁ : P.IsMaximal
⊢ RingHom.IsIntegral (A := MvPolynomial (Fin n) R ⧸ P) (algebraMap R (MvPolynomial (Fin n) R ⧸ P))

Tactic:
apply quotient_mk_comp_C_isIntegral_of_isJacobsonRing'

Premises used: _private.0.MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing'
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ P.IsMaximal

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
intro : ∀ (val : Fintype σ), (f.comp C).IsIntegral
⊢ (f.comp C).IsIntegral

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
intro : ∀ (e : Fin (Fintype.card σ) ≃ σ), (f.comp C).IsIntegral
⊢ (f.comp C).IsIntegral

Tactic:
have e := (Fintype.equivFin σ).symm
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (Function.comp (β := MvPolynomial σ R) (⇑f : (a : MvPolynomial σ R) → S)
      (⇑(renameEquiv R e) : (a : MvPolynomial (Fin (Fintype.card σ)) R) → MvPolynomial σ R))

Tactic:
have hf' := Function.Surjective.comp hf (renameEquiv R e).surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (Function.comp (β := MvPolynomial σ R) (⇑f : (a : MvPolynomial σ R) → S)
      (⇑(renameEquiv R e) : (a : MvPolynomial (Fin (Fintype.card σ)) R) → MvPolynomial σ R))
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)

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

Premises used: DFunLike.coe, Function.Surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : IsMaximal (ker f')
g : RingHom.{u_1, u_3}
  (HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
    (ker f'))
  S :=
  Ideal.Quotient.lift (ker f') f' ⋯
⊢ g.comp (Ideal.Quotient.mk (ker f')) = f'

Tactic:
have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f')) = f' :=
      ringHom_ext (fun r => rfl) fun i => rfl
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : IsMaximal (ker f')
g : RingHom.{u_1, u_3}
  (HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
    (ker f'))
  S :=
  Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
rw : (g.comp (RingHom.comp (Ideal.Quotient.mk (ker f')) C)).IsIntegral
⊢ (f'.comp C).IsIntegral

Tactic:
rw [← hfg, RingHom.comp_assoc]

Premises used: RingHom.comp_assoc
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : IsMaximal (ker f')
g : RingHom.{u_1, u_3}
  (HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (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 (RingHom.comp (Ideal.Quotient.mk (ker f')) C)).IsIntegral

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

Premises used: RingHom.isIntegral_of_surjective, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, RingHom.IsIntegral.trans, RingHom.ker
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
σ : Type u_2
inst_2 : _root_.Finite σ
S : Type u_3
inst_3 : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective (α := MvPolynomial σ R) (β := S) (⇑f : (a : MvPolynomial σ R) → S)
val : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : RingHom.{u_1, u_3} (MvPolynomial (Fin (Fintype.card σ)) R) S :=
  f.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e)))
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (⇑f' : (a : MvPolynomial (Fin (Fintype.card σ)) R) → S)
this : IsMaximal (ker f')
g : RingHom.{u_1, u_3}
  (HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
    (ker f'))
  S :=
  Ideal.Quotient.lift (ker f') f' ⋯
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
refine :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α :=
    HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
      (ker f'))
    (β := S) (⇑g : (a : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f') → S)
⊢ (g.comp (RingHom.comp (Ideal.Quotient.mk (ker f')) C)).IsIntegral

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

Premises used: RingHom.isIntegral_of_surjective, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, RingHom.IsIntegral.trans, RingHom.ker