awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (Function.comp (β :=
      HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
        (ker f'))
      (⇑g : (a : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f') → S)
      (⇑(Ideal.Quotient.mk (ker f')) :
        (a : MvPolynomial (Fin (Fintype.card σ)) R) → MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f'))

Tactic:
rw [← hfg, 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
σ : 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'
hf'₁ :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (Function.comp (β :=
      HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
        (ker f'))
      (⇑g : (a : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f') → S)
      (⇑(Ideal.Quotient.mk (ker f')) :
        (a : MvPolynomial (Fin (Fintype.card σ)) R) → MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f'))
⊢ g.comp (Ideal.Quotient.mk (ker f')) = f'

Tactic:
rw [← hfg, 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
σ : 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)))
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' ⋯
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (Function.comp (β :=
      HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
        (ker f'))
      (⇑g : (a : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f') → S)
      (⇑(Ideal.Quotient.mk (ker f')) :
        (a : MvPolynomial (Fin (Fintype.card σ)) R) → MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f'))
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ 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)

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
σ : 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)))
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' ⋯
hf' :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R) (β := S)
    (Function.comp (β :=
      HasQuotient.Quotient (MvPolynomial (Fin (Fintype.card σ)) R) (B := Ideal (MvPolynomial (Fin (Fintype.card σ)) R))
        (ker f'))
      (⇑g : (a : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f') → S)
      (⇑(Ideal.Quotient.mk (ker f')) :
        (a : MvPolynomial (Fin (Fintype.card σ)) R) → MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f'))
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ 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)

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
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)
⊢ (f'.comp C).IsIntegral

Tactic:
have : (f'.comp C).IsIntegral := by
    have : (RingHom.ker f').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, coe_comp] at hf'
    exact Function.Surjective.of_comp hf'
-- 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 : (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral
⊢ (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral

Tactic:
this
-- 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 : (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral
h : Eq (α := R →+* MvPolynomial σ R) C (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)
⊢ (f.comp C).IsIntegral

Tactic:
convert! this
-- 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 : (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral
⊢ Eq (α := R →+* MvPolynomial σ R) C (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)

Tactic:
RingHom.ext fun x => ?_

Premises used: RingHom.ext
-- 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 : (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral
h :
  ∀ (x : R),
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
      ((RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C : (a : R) → MvPolynomial σ R) x :
        MvPolynomial σ R)
⊢ Eq (α := R →+* MvPolynomial σ R) C (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)

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

Premises used: RingHom.ext
-- 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 : (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral
x : R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C : (a : R) → MvPolynomial σ R) x :
      MvPolynomial σ R)

Tactic:
((renameEquiv R e).commutes' x).symm

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Eq.symm, AlgEquiv.commutes', MvPolynomial.renameEquiv, Finset.sum
-- 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 : (f.comp (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C)).IsIntegral
x : R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (renameEquiv R e))) C : (a : R) → MvPolynomial σ R) x :
      MvPolynomial σ R)

Tactic:
exact ((renameEquiv R e).commutes' x).symm

Premises used: Eq.symm, AlgEquiv.commutes', MvPolynomial.renameEquiv
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsJacobsonRing A
inst_4 : Algebra.FiniteType A B
obtain :
  ∀ (ι : Type u_2) (hι : Fintype ι) (f : MvPolynomial ι A →ₐ[A] B)
    (hf : Function.Surjective (α := MvPolynomial ι A) (β := B) (⇑f : (a : MvPolynomial ι A) → B)), IsJacobsonRing B
⊢ IsJacobsonRing B

Tactic:
obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›

Premises used: Algebra.FiniteType.iff_quotient_mvPolynomial', Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsJacobsonRing A
inst_4 : Algebra.FiniteType A B
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι A →ₐ[A] B
hf : Function.Surjective (α := MvPolynomial ι A) (β := B) (⇑f : (a : MvPolynomial ι A) → B)
⊢ IsJacobsonRing B

Tactic:
isJacobsonRing_of_surjective ⟨f.toRingHom, hf⟩

Premises used: isJacobsonRing_of_surjective, AlgHom.toRingHom, Exists.intro
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsJacobsonRing A
inst_4 : Algebra.FiniteType A B
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι A →ₐ[A] B
hf : Function.Surjective (α := MvPolynomial ι A) (β := B) (⇑f : (a : MvPolynomial ι A) → B)
⊢ IsJacobsonRing B

Tactic:
exact isJacobsonRing_of_surjective ⟨f.toRingHom, hf⟩

Premises used: isJacobsonRing_of_surjective, AlgHom.toRingHom, Exists.intro
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
inst_2 : IsJacobsonRing A
H : f.FiniteType
⊢ IsJacobsonRing B

Tactic:
@isJacobsonRing_of_finiteType A B _ _ f.toAlgebra _ H

Premises used: isJacobsonRing_of_finiteType
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
obtain :
  ∀ (ι : Type u_2) (hι : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S)
    (hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)), Module.Finite R S
⊢ Module.Finite R S

Tactic:
obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›

Premises used: Algebra.FiniteType.iff_quotient_mvPolynomial', Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
rw :
  RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial ι R →+* S)
      (algebraMap R (MvPolynomial ι R)))
⊢ RingHom.IsIntegral (algebraMap R S)

Tactic:
rw [← f.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
⊢ RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial ι R →+* S)
      (algebraMap R (MvPolynomial ι R)))

Tactic:
MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf

Premises used: MonoidHomClass.toMonoidHom, AlgHom.toRingHom, RingHomClass.toRingHom, MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing, MvPolynomial.C
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
⊢ RingHom.IsIntegral
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : MvPolynomial ι R →+* S)
      (algebraMap R (MvPolynomial ι R)))

Tactic:
exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf

Premises used: AlgHom.toRingHom, MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
⊢ RingHom.IsIntegral (algebraMap R S)

Tactic:
have : (algebraMap R S).IsIntegral := by
    rw [← f.comp_algebraMap]
    -- We need to write `f.toRingHom` instead of just `f`, to avoid unification issues.
    exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
this : RingHom.IsIntegral (algebraMap R S)
⊢ Algebra.IsIntegral R S

Tactic:
have : Algebra.IsIntegral R S := Algebra.isIntegral_def.mpr this
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
this_1 : RingHom.IsIntegral (algebraMap R S)
this : Algebra.IsIntegral R S
⊢ Module.Finite R S

Tactic:
Algebra.IsIntegral.finite

Premises used: Algebra.IsIntegral.finite
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : Algebra R S
inst_3 : IsJacobsonRing R
inst_4 : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
this_1 : RingHom.IsIntegral (algebraMap R S)
this : Algebra.IsIntegral R S
⊢ Module.Finite R S

Tactic:
exact Algebra.IsIntegral.finite

Premises used: Algebra.IsIntegral.finite
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsJacobsonRing R
inst_2 : Field S
f : R →+* S
h : f.FiniteType
⊢ Algebra.FiniteType R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsJacobsonRing R
inst_2 : Field S
f : R →+* S
h : f.FiniteType
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FiniteType R S
⊢ f.Finite

Tactic:
finite_of_finite_type_of_isJacobsonRing R S

Premises used: finite_of_finite_type_of_isJacobsonRing, RingHom.Finite
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsJacobsonRing R
inst_2 : Field S
f : R →+* S
h : f.FiniteType
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FiniteType R S
⊢ f.Finite

Tactic:
exact finite_of_finite_type_of_isJacobsonRing R S

Premises used: finite_of_finite_type_of_isJacobsonRing
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : DivisionRing L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
inst_6 : Algebra K L
inst_7 : Algebra K A
inst_8 : Algebra.FiniteType K A
f : L →ₐ[K] A
obtain : ∀ (m : Ideal A) (hm : m.IsMaximal), Module.Finite K L
⊢ Module.Finite K L

Tactic:
obtain ⟨m, hm⟩ := Ideal.exists_maximal A

Premises used: Ideal.exists_maximal
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : DivisionRing L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
inst_6 : Algebra K L
inst_7 : Algebra K A
inst_8 : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
this : Field (A ⧸ m) := Quotient.field m
⊢ Module.Finite.{u_1, u_3} K (A ⧸ m)

Tactic:
have := finite_of_finite_type_of_isJacobsonRing K (A ⧸ m)
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : DivisionRing L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
inst_6 : Algebra K L
inst_7 : Algebra K A
inst_8 : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
this_1 : Field (A ⧸ m) := Quotient.field m
this : Module.Finite.{u_1, u_3} K (A ⧸ m)
⊢ Module.Finite K L

Tactic:
Module.Finite.of_injective ((Ideal.Quotient.mkₐ K m).comp f).toLinearMap
    (RingHom.injective _)

Premises used: AlgHom.toLinearMap, Module.Finite.of_injective, RingHom.injective, AlgHom.comp, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : DivisionRing L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
inst_6 : Algebra K L
inst_7 : Algebra K A
inst_8 : Algebra.FiniteType K A
f : L →ₐ[K] A
m : Ideal A
hm : m.IsMaximal
this_1 : Field (A ⧸ m) := Quotient.field m
this : Module.Finite.{u_1, u_3} K (A ⧸ m)
⊢ Module.Finite K L

Tactic:
exact Module.Finite.of_injective ((Ideal.Quotient.mkₐ K m).comp f).toLinearMap
    (RingHom.injective _)

Premises used: AlgHom.toLinearMap, Module.Finite.of_injective, RingHom.injective, AlgHom.comp, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : Field L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
⊢ Algebra.FiniteType K A

Tactic:
algebraize [f, (g.comp f)]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
K : Type u_1
L : Type u_2
A : Type u_3
inst : CommRing K
inst_1 : Field L
inst_2 : CommRing A
inst_3 : IsJacobsonRing K
inst_4 : IsNoetherianRing K
inst_5 : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
algInst : Algebra K L := f.toAlgebra
algInst_1 : Algebra K A := (g.comp f).toAlgebra
algebraizeInst : Algebra.FiniteType K A
⊢ f.Finite

Tactic:
finite_of_algHom_finiteType_of_isJacobsonRing ⟨g, fun _ ↦ rfl⟩

Premises used: finite_of_algHom_finiteType_of_isJacobsonRing, AlgHom.mk, RingHom.Finite, rfl