awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
⊢ IsMaximal (comap (F := R →+* R[X] ⧸ P) (RingHom.comp (Ideal.Quotient.mk P) C) ⊥)
have this : IsMaximal.{u_1} (α := R[X] ⧸ P) ⊥
Tactic: have := (bot_quotient_isMaximal_iff _).mpr hP
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
S : Type u_2
inst_2 : Field S
f : RingHom.{u_1, u_2} R[X] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
⊢ (f.comp C).IsIntegral
have this : IsMaximal (RingHom.ker f)
Tactic: have : (RingHom.ker f).IsMaximal := RingHom.ker_isMaximal_of_surjective f hf
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
S : Type u_2
inst_2 : Field S
f : RingHom.{u_1, u_2} R[X] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
this : IsMaximal (RingHom.ker f)
g : RingHom.{u_1, u_2} (HasQuotient.Quotient R[X] (B := Ideal R[X]) (RingHom.ker f)) S :=
  Ideal.Quotient.lift (RingHom.ker f) f ⋯
⊢ (f.comp C).IsIntegral
have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f
Tactic: have hfg : g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f := ringHom_ext' rfl rfl
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
S : Type u_2
inst_2 : Field S
f : RingHom.{u_1, u_2} R[X] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
this : IsMaximal (RingHom.ker f)
g : RingHom.{u_1, u_2} (HasQuotient.Quotient R[X] (B := Ideal 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
have rw : (g.comp (RingHom.comp (Ideal.Quotient.mk (RingHom.ker f)) C)).IsIntegral
Tactic: rw [← hfg, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
S : Type u_2
inst_2 : Field S
f : RingHom.{u_1, u_2} R[X] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
this : IsMaximal (RingHom.ker f)
g : RingHom.{u_1, u_2} (HasQuotient.Quotient R[X] (B := Ideal 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 (RingHom.comp (Ideal.Quotient.mk (RingHom.ker f)) C)).IsIntegral
have refine : Function.Surjective.{u_1 + 1, u_2 + 1} (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (RingHom.ker f)) (β := S)
  (⇑g : (a : R[X] ⧸ RingHom.ker f) → S)
Tactic: refine (quotient_mk_comp_C_isIntegral_of_isJacobsonRing (RingHom.ker f)).trans _ g
    (g.isIntegral_of_surjective ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
S : Type u_2
inst_2 : Field S
f : RingHom.{u_1, u_2} R[X] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
this : IsMaximal (RingHom.ker f)
g : RingHom.{u_1, u_2} (HasQuotient.Quotient R[X] (B := Ideal 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.{u_1 + 1, u_2 + 1} (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (RingHom.ker f)) (β := S)
    (⇑g : (a : R[X] ⧸ RingHom.ker f) → S)
have hf₁ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S)
  (Function.comp (β := HasQuotient.Quotient R[X] (B := Ideal R[X]) (RingHom.ker f))
    (⇑g : (a : R[X] ⧸ RingHom.ker f) → S) (⇑(Ideal.Quotient.mk (RingHom.ker f)) : (a : R[X]) → R[X] ⧸ RingHom.ker f))
Tactic: rw [← hfg, RingHom.coe_comp] at hf
Cleared hypotheses: hf, hfg
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : _root_.Finite ι
inst_2 : IsJacobsonRing R
⊢ IsJacobsonRing (MvPolynomial ι R)
have intro : ∀ (val : Fintype ι), IsJacobsonRing (MvPolynomial ι R)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : _root_.Finite ι
inst_2 : IsJacobsonRing R
val : Fintype ι
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ IsJacobsonRing (MvPolynomial ι R)
have intro : IsJacobsonRing.{u_1} (MvPolynomial (Fin (Fintype.card ι)) R)
Tactic: rw [isJacobsonRing_iso (renameEquiv R e).toRingEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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
⊢ RingHom.IsIntegral.{u, w} (A := T ⧸ P) (algebraMap R (T ⧸ P))
have hw : Ideal.map v Q = P
Tactic: have hw : Ideal.map v Q = P := map_comap_of_surjective v v.surjective P
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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
⊢ RingHom.IsIntegral.{u, w} (A := T ⧸ P) (algebraMap R (T ⧸ P))
have hQ : Q.IsMaximal
Tactic: have hQ : IsMaximal Q := comap_isMaximal_of_surjective _ v.surjective
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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) ⋯
⊢ Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
have a : ∀ (r : R),
  Eq.{w + 1} (α := T ⧸ P) ((algebraMap R (T ⧸ P) : (a : R) → T ⧸ P) r : T ⧸ P)
    (((w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))) : RingHom.{u, w} R (T ⧸ P)) : (a : R) → T ⧸ P) r :
      T ⧸ P)
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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) ⋯
⊢ RingHom.IsIntegral.{u, w} (A := T ⧸ P) (algebraMap R (T ⧸ P))
have h_eq : Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
  (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
Tactic: have h_eq : algebraMap R (T ⧸ P) =
    w.toRingEquiv.toRingHom.comp (w'.toRingHom.comp (algebraMap R (S ⧸ Q'))) := by
    ext r
    simp only [AlgHom.toRingHom_eq_coe,
      RingEquiv.toRingHom_eq_coe, AlgHom.comp_algebraMap_of_tower, coe_comp, coe_coe,
      AlgEquiv.coe_ringEquiv, Function.comp_apply, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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'))))
⊢ RingHom.IsIntegral.{u, w} (A := T ⧸ P) (algebraMap R (T ⧸ P))
have rw : RingHom.IsIntegral (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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'))))
⊢ RingHom.IsIntegral (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
have hf : RingHom.IsIntegral (w'.comp (algebraMap R (S ⧸ Q')))
Tactic: apply RingHom.IsIntegral.trans
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 (w'.comp (algebraMap R (S ⧸ Q')))
⊢ RingHom.IsIntegral (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
have hg : w.toRingEquiv.toRingHom.IsIntegral
Tactic: apply RingHom.IsIntegral.trans
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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'))))
⊢ RingHom.IsIntegral (w'.comp (algebraMap R (S ⧸ Q')))
have hf : RingHom.IsIntegral.{u, v} (A := S ⧸ Q') (algebraMap R (S ⧸ Q'))
Tactic: apply RingHom.IsIntegral.trans
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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'))
⊢ RingHom.IsIntegral (w'.comp (algebraMap R (S ⧸ Q')))
have hf₁ : w'.IsIntegral
Tactic: apply RingHom.IsIntegral.trans
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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'))))
⊢ RingHom.IsIntegral.{u, v} (A := S ⧸ Q') (algebraMap R (S ⧸ Q'))
have hf : Q'.IsMaximal
Tactic: apply IH
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 ⋯
⊢ w'.IsIntegral
have rw : RingHom.IsIntegral (quotientMap Q Polynomial.C sorry)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 (quotientMap Q Polynomial.C ⋯)
have rw : RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk Q) Polynomial.C)
Tactic: rw [isIntegral_quotientMap_iff _]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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'.IsIntegral
have hf : w'.toRingHom = quotientMap Q Polynomial.C sorry
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
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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.toRingEquiv.toRingHom.IsIntegral
have hg : Function.Surjective.{v + 1, w + 1} (α := S[X] ⧸ Q) (β := T ⧸ P) (⇑w.toRingEquiv.toRingHom : (a : S[X] ⧸ Q) → T ⧸ P)
Tactic: apply RingHom.isIntegral_of_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin 0) R)
hP : P.IsMaximal
⊢ RingHom.IsIntegral (A := MvPolynomial (Fin 0) R ⧸ P) (algebraMap R (MvPolynomial (Fin 0) R ⧸ P))
have zero : Function.Surjective (α := R) (β := MvPolynomial (Fin 0) R ⧸ P)
  (⇑(algebraMap R (MvPolynomial (Fin 0) R ⧸ P)) : (a : R) → MvPolynomial (Fin 0) R ⧸ P)
Tactic: apply RingHom.isIntegral_of_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 ⧸ P)
    (⇑(algebraMap R (MvPolynomial (Fin 0) R ⧸ P)) : (a : R) → MvPolynomial (Fin 0) R ⧸ P)
have zero : Function.Surjective (α := R) (β := MvPolynomial (Fin 0) R)
  (⇑(algebraMap R (MvPolynomial (Fin 0) R)) : (a : R) → MvPolynomial (Fin 0) R)
Tactic: apply Function.Surjective.comp Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ RingHom.IsIntegral (A := MvPolynomial (Fin n) R ⧸ P) (algebraMap R (MvPolynomial (Fin n) R ⧸ P))
have 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))
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
Cleared hypotheses: P, hP
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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))
⊢ RingHom.IsIntegral (A := MvPolynomial (Fin n) R ⧸ P) (algebraMap R (MvPolynomial (Fin n) R ⧸ P))
have 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))
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
Cleared hypotheses: P, hP
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)
have change : RingHom.IsIntegral (A := MvPolynomial (Fin n) R ⧸ P) (algebraMap R (MvPolynomial (Fin n) R ⧸ P))
Tactic: change RingHom.IsIntegral (algebraMap R (MvPolynomial (Fin n) R ⧸ P))
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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)
⊢ (f.comp C).IsIntegral
have intro : ∀ (val : Fintype σ), (f.comp C).IsIntegral
Tactic: cases nonempty_fintype σ
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 σ
⊢ (f.comp C).IsIntegral
have intro : ∀ (e : Fin (Fintype.card σ) ≃ σ), (f.comp C).IsIntegral
Tactic: have e := (Fintype.equivFin σ).symm
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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)))
⊢ (f.comp C).IsIntegral
have 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))
Tactic: have hf' := Function.Surjective.comp hf (renameEquiv R e).surjective
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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))
⊢ (f.comp C).IsIntegral
have hf'₁ : 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'
Cleared hypotheses: hf'