awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
P' : Ideal R := comap (F := R →+* R[X]) C P
pX : R[X]
hpX : pX ∈ P
hp0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX) 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
hM : 0 ∉ M
M' : Submonoid (R[X] ⧸ P) := Submonoid.map φ M
⊢ RingHom.IsIntegral (quotientMap P C ⋯)

Tactic:
RingHom.IsIntegral.tower_bot φ (algebraMap _ (Localization M')) ?_ ?_

Premises used: RingHom.IsIntegral.tower_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
⊢ P'.IsPrime

Tactic:
have : P'.IsPrime := comap_isPrime C P
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
⊢ Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])

Tactic:
have hf : Function.Surjective ↑f := map_surjective (Ideal.Quotient.mk P') Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
rw : P = P ⊔ comap f ⊥
⊢ P = comap f (Ideal.map f P)

Tactic:
rw [comap_map_of_surjective _ hf]

Premises used: Ideal.comap_map_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
⊢ P = P ⊔ comap f ⊥

Tactic:
le_antisymm (le_sup_of_le_left le_rfl) (sup_le le_rfl ?_)

Premises used: le_rfl, le_sup_of_le_left, le_antisymm, sup_le
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
refine : comap f ⊥ ≤ P
⊢ P = P ⊔ comap f ⊥

Tactic:
refine le_antisymm (le_sup_of_le_left le_rfl) (sup_le le_rfl ?_)

Premises used: le_rfl, le_sup_of_le_left, le_antisymm, sup_le
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
⊢ comap f ⊥ ≤ P

Tactic:
fun p hp =>
      polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Quotient.eq_zero_iff_mem.mp ?_

Premises used: Set.Mem, Ideal.polynomial_mem_ideal_of_coeff_mem_ideal, Ideal.Quotient.eq_zero_iff_mem, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
refine :
  ∀ (p : R[X]) (hp : Membership.mem (γ := Submodule R[X] R[X]) (comap f ⊥) p) (n : ℕ),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
      ((Ideal.Quotient.mk (comap (F := R →+* R[X]) C P) : (a : R) → R ⧸ comap C P) (p.coeff n) :
        HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
      (0 : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
⊢ comap f ⊥ ≤ P

Tactic:
refine fun p hp =>
      polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Quotient.eq_zero_iff_mem.mp ?_

Premises used: Ideal.polynomial_mem_ideal_of_coeff_mem_ideal, Ideal.Quotient.eq_zero_iff_mem, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
p : R[X]
hp : Membership.mem (γ := Submodule R[X] R[X]) (comap f ⊥) p
n : ℕ
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    ((Ideal.Quotient.mk (comap (F := R →+* R[X]) C P) : (a : R) → R ⧸ comap C P) (p.coeff n) :
      HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (0 : HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))

Tactic:
simpa only [f, coeff_map, coe_mapRingHom] using (Polynomial.ext_iff.mp hp) n

Premises used: Polynomial.coeff_map, Polynomial.ext_iff, Polynomial.coe_mapRingHom, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
⊢ P = comap f (Ideal.map f P)

Tactic:
have hPJ : P = (P.map f).comap f := by
    rw [comap_map_of_surjective _ hf]
    refine le_antisymm (le_sup_of_le_left le_rfl) (sup_le le_rfl ?_)
    refine fun p hp =>
      polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Quotient.eq_zero_iff_mem.mp ?_
    simpa only [f, coeff_map, coe_mapRingHom] using (Polynomial.ext_iff.mp hp) n
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
f : R[X] →+* (R ⧸ P')[X] := mapRingHom (Ideal.Quotient.mk P')
hf : Function.Surjective (α := R[X]) (β := (R ⧸ P')[X]) (⇑f : (a : R[X]) → (R ⧸ P')[X])
hPJ : P = comap f (Ideal.map f P)
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)

Tactic:
RingHom.IsIntegral.tower_bot
    (T := (R ⧸ comap C P)[X] ⧸ _) _ _ (injective_quotient_le_comap_map P) ?_

Premises used: RingHom.IsIntegral.tower_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
rw : IsMaximal (comap (F := R →+* R[X] ⧸ P) (RingHom.comp (Ideal.Quotient.mk P) C) ⊥)
⊢ IsMaximal (comap (F := R →+* R[X]) C P)

Tactic:
rw [← @mk_ker _ _ P, RingHom.ker_eq_comap_bot, comap_comap]

Premises used: RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
⊢ IsMaximal.{u_1} (α := R[X] ⧸ P) ⊥

Tactic:
have := (bot_quotient_isMaximal_iff _).mpr hP
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
this : IsMaximal.{u_1} (α := R[X] ⧸ P) ⊥
⊢ IsMaximal (comap (F := R →+* R[X] ⧸ P) (RingHom.comp (Ideal.Quotient.mk P) C) ⊥)

Tactic:
isMaximal_comap_of_isIntegral_of_isMaximal' _
    (quotient_mk_comp_C_isIntegral_of_isJacobsonRing P) ⊥

Premises used: Bot.bot, Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : IsJacobsonRing R
this : IsMaximal.{u_1} (α := R[X] ⧸ P) ⊥
⊢ IsMaximal (comap (F := R →+* R[X] ⧸ P) (RingHom.comp (Ideal.Quotient.mk P) C) ⊥)

Tactic:
exact isMaximal_comap_of_isIntegral_of_isMaximal' _
    (quotient_mk_comp_C_isIntegral_of_isJacobsonRing P) ⊥

Premises used: Bot.bot, Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, Ideal.isMaximal_comap_of_isIntegral_of_isMaximal'
-- Module: Mathlib.RingTheory.Jacobson.Ring
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)
⊢ IsMaximal (RingHom.ker f)

Tactic:
have : (RingHom.ker f).IsMaximal := RingHom.ker_isMaximal_of_surjective f hf
-- Module: Mathlib.RingTheory.Jacobson.Ring
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 ⋯
⊢ 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
-- Module: Mathlib.RingTheory.Jacobson.Ring
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
rw : (g.comp (RingHom.comp (Ideal.Quotient.mk (RingHom.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
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

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

Premises used: RingHom.isIntegral_of_surjective, Polynomial.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
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
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)
⊢ (g.comp (RingHom.comp (Ideal.Quotient.mk (RingHom.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, Polynomial.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
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} (α := 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

Premises used: RingHom.coe_comp
-- Module: Mathlib.RingTheory.Jacobson.Ring
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
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))
⊢ g.comp (Ideal.Quotient.mk (RingHom.ker f)) = f

Tactic:
rw [← hfg, RingHom.coe_comp] at hf

Premises used: RingHom.coe_comp
-- Module: Mathlib.RingTheory.Jacobson.Ring
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
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 ⋯
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))
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)

Tactic:
Function.Surjective.of_comp hf

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.RingTheory.Jacobson.Ring
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
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 ⋯
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))
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)

Tactic:
exact Function.Surjective.of_comp hf

Premises used: Function.Surjective.of_comp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
inst_1 : _root_.Finite ι
inst_2 : IsJacobsonRing R
intro : ∀ (val : Fintype ι), IsJacobsonRing (MvPolynomial ι R)
⊢ IsJacobsonRing (MvPolynomial ι R)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Jacobson.Ring
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 ι
intro : IsJacobsonRing.{u_1} (MvPolynomial (Fin (Fintype.card ι)) R)
⊢ IsJacobsonRing (MvPolynomial ι R)

Tactic:
rw [isJacobsonRing_iso (renameEquiv R e).toRingEquiv]

Premises used: isJacobsonRing_iso, AlgEquiv.toRingEquiv, MvPolynomial.renameEquiv
-- Module: Mathlib.RingTheory.Jacobson.Ring
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.{u_1} (MvPolynomial (Fin (Fintype.card ι)) R)

Tactic:
isJacobsonRing_MvPolynomial_fin _

Premises used: MvPolynomial.isJacobsonRing_MvPolynomial_fin
-- Module: Mathlib.RingTheory.Jacobson.Ring
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.{u_1} (MvPolynomial (Fin (Fintype.card ι)) R)

Tactic:
exact isJacobsonRing_MvPolynomial_fin _

Premises used: MvPolynomial.isJacobsonRing_MvPolynomial_fin
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
⊢ Eq.{v + 1} (α := S[X])
    (OneHom.toFun (↑(↑Polynomial.C : S →* S[X]) : OneHom S S[X]) ((algebraMap R S : (a : R) → S) r) : S[X])
    ((algebraMap R S[X] : (a : R) → S[X]) r : S[X])

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
⊢ Ideal.map v Q = P

Tactic:
have hw : Ideal.map v Q = P := map_comap_of_surjective v v.surjective P
-- 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
⊢ Q.IsMaximal

Tactic:
have hQ : IsMaximal Q := comap_isMaximal_of_surjective _ v.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) ⋯
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)
⊢ Eq (α := RingHom.{u, w} R (T ⧸ P)) (algebraMap R (T ⧸ P))
    (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))

Tactic:
ext r
-- 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) ⋯
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:
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]

Premises used: RingHom.coe_coe, AlgEquiv.commutes, AlgHom.comp_algebraMap_of_tower, AlgEquiv.coe_ringEquiv, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingEquiv.toRingHom_eq_coe, Function.comp_apply
-- 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) ⋯
⊢ 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]
-- 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'))))
rw : RingHom.IsIntegral (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))
⊢ RingHom.IsIntegral.{u, w} (A := T ⧸ P) (algebraMap R (T ⧸ P))

Tactic:
rw [h_eq]
-- 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 (w'.comp (algebraMap R (S ⧸ Q')))
hg : w.toRingEquiv.toRingHom.IsIntegral
⊢ RingHom.IsIntegral (w.toRingEquiv.toRingHom.comp (w'.comp (algebraMap R (S ⧸ Q'))))

Tactic:
apply RingHom.IsIntegral.trans

Premises used: RingHom.IsIntegral.trans