awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
p : Ideal R
inst_7 : p.IsPrime
q : Ideal A
inst_8 : q.IsPrime
inst_9 : q.LiesOver p
inst_10 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) (F :=
    RingHom.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q))
    (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))
have rw : IsLocalHom (R := Localization.AtPrime p) (S := Localization.AtPrime q) (F :=
  RingHom.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q))
  (Localization.localRingHom p q (algebraMap R A) sorry)
Tactic: rw [Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (hypothesis)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Algebra R A
inst_5 : Algebra R B
I : Ideal R
inst_6 : I.IsPrime
inst_7 : Algebra.EssFiniteType R A
p : Ideal R
inst_8 : p.IsPrime
q : Ideal A
inst_9 : q.IsPrime
inst_10 : q.LiesOver p
inst_11 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_12 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Algebra.EssFiniteType.{u_1, u_3} p.ResidueField q.ResidueField
have this : Algebra.EssFiniteType.{u_1, u_3} R q.ResidueField
Tactic: have : Algebra.EssFiniteType R q.ResidueField := .comp _ A _
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Ideal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : I.IsPrime
f : R →+* S
hf₁ : I ≤ RingHom.ker f
hf₂ : I.primeCompl ≤ Submonoid.comap f (IsUnit.submonoid S)
r : R
⊢ Eq.{u_2 + 1} (α := S)
    ((lift I f hf₁ hf₂ : (a : I.ResidueField) → S)
        ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) r : I.ResidueField) :
      S)
    ((f : (a : R) → S) r : S)
have rw : Eq.{u_2 + 1} (α := S)
  ((Quotient.lift I f hf₁ : (a : R ⧸ I) → S) ((algebraMap R (R ⧸ I) : (a : R) → R ⧸ I) r : R ⧸ I) : S)
  ((f : (a : R) → S) r : S)
Tactic: rw [lift, IsScalarTower.algebraMap_apply R (R ⧸ I) I.ResidueField, IsLocalization.lift_eq]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsMaximal
inst_9 : q.IsMaximal
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsSeparable.{u_2, u_3} (A ⧸ p) (B ⧸ q)
⊢ Algebra.IsSeparable.{u_2, u_3} p.ResidueField q.ResidueField
have refine : Eq (α := RingHom.{u_2, u_3} (A ⧸ p) q.ResidueField)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
    (↑(RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
          (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) sorry) :
      A ⧸ p →+* p.ResidueField))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
          (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) sorry) :
      B ⧸ q →+* q.ResidueField)
    (algebraMap (A ⧸ p) (B ⧸ q)))
Tactic: refine Algebra.IsSeparable.of_equiv_equiv
    (.ofBijective _ p.bijective_algebraMap_quotient_residueField)
    (.ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsMaximal
inst_9 : q.IsMaximal
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsSeparable.{u_2, u_3} (A ⧸ p) (B ⧸ q)
⊢ Eq (α := RingHom.{u_2, u_3} (A ⧸ p) q.ResidueField)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
      (↑(RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
            (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) ⋯) :
        A ⧸ p →+* p.ResidueField))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
            (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) ⋯) :
        B ⧸ q →+* q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
have h : ∀ (x : A),
  Eq.{u_3 + 1} (α := q.ResidueField)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap p.ResidueField q.ResidueField)
              (↑(RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
                    (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) sorry) :
                A ⧸ p →+* p.ResidueField))
            (Ideal.Quotient.mk p) :
          (a : A) → q.ResidueField)
        x :
      q.ResidueField)
    (((RingHom.comp
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
                      (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) sorry) :
                  B ⧸ q →+* q.ResidueField)
                (algebraMap (A ⧸ p) (B ⧸ q)))
              (Ideal.Quotient.mk p) :
            RingHom.{u_2, u_3} A q.ResidueField) :
          (a : A) → q.ResidueField)
        x :
      q.ResidueField)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsMaximal
inst_9 : q.IsMaximal
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : p.IsMaximal
inst_13 : q.IsMaximal
inst_14 : Algebra.IsSeparable.{u_2, u_3} p.ResidueField q.ResidueField
⊢ Algebra.IsSeparable.{u_2, u_3} (A ⧸ p) (B ⧸ q)
have refine : Eq (α := RingHom.{u_2, u_3} p.ResidueField (B ⧸ q))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ p) (B ⧸ q))
    (↑(RingEquiv.symm
          (RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
            (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) sorry)) :
      p.ResidueField →+* A ⧸ p))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(RingEquiv.symm
          (RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
            (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) sorry)) :
      q.ResidueField →+* B ⧸ q)
    (algebraMap p.ResidueField q.ResidueField))
Tactic: refine Algebra.IsSeparable.of_equiv_equiv
    (.symm <| .ofBijective _ p.bijective_algebraMap_quotient_residueField)
    (.symm <| .ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsMaximal
inst_9 : q.IsMaximal
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : p.IsMaximal
inst_13 : q.IsMaximal
inst_14 : Algebra.IsSeparable.{u_2, u_3} p.ResidueField q.ResidueField
⊢ Eq (α := RingHom.{u_2, u_3} p.ResidueField (B ⧸ q))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ p) (B ⧸ q))
      (↑(RingEquiv.symm
            (RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
              (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) ⋯)) :
        p.ResidueField →+* A ⧸ p))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(RingEquiv.symm
            (RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
              (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) ⋯)) :
        q.ResidueField →+* B ⧸ q)
      (algebraMap p.ResidueField q.ResidueField))
have apply : ∀ (x : p.ResidueField),
  Eq.{u_3 + 1} (α := B ⧸ q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ p) (B ⧸ q))
            (↑(RingEquiv.symm
                  (RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
                    (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) sorry)) :
              p.ResidueField →+* A ⧸ p) :
          (a : p.ResidueField) → B ⧸ q)
        x :
      B ⧸ q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(RingEquiv.symm
                  (RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
                    (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) sorry)) :
              q.ResidueField →+* B ⧸ q)
            (algebraMap p.ResidueField q.ResidueField) :
          (a : p.ResidueField) → B ⧸ q)
        x :
      B ⧸ q)
Tactic: apply RingHom.ext fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsMaximal
inst_9 : q.IsMaximal
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : p.IsMaximal
inst_13 : q.IsMaximal
inst_14 : Algebra.IsSeparable.{u_2, u_3} p.ResidueField q.ResidueField
x : p.ResidueField
⊢ Eq.{u_3 + 1} (α := B ⧸ q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ p) (B ⧸ q))
            (↑(RingEquiv.symm
                  (RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
                    (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) ⋯)) :
              p.ResidueField →+* A ⧸ p) :
          (a : p.ResidueField) → B ⧸ q)
        x :
      B ⧸ q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(RingEquiv.symm
                  (RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
                    (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) ⋯)) :
              q.ResidueField →+* B ⧸ q)
            (algebraMap p.ResidueField q.ResidueField) :
          (a : p.ResidueField) → B ⧸ q)
        x :
      B ⧸ q)
have obtain : ∀ (x : A ⧸ p),
  Eq.{u_3 + 1} (α := B ⧸ q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ p) (B ⧸ q))
            (↑(RingEquiv.symm
                  (RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
                    (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) sorry)) :
              p.ResidueField →+* A ⧸ p) :
          (a : p.ResidueField) → B ⧸ q)
        ((RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
              (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) sorry :
            (a : A ⧸ p) → p.ResidueField)
          x) :
      B ⧸ q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(RingEquiv.symm
                  (RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
                    (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) sorry)) :
              q.ResidueField →+* B ⧸ q)
            (algebraMap p.ResidueField q.ResidueField) :
          (a : p.ResidueField) → B ⧸ q)
        ((RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
              (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) sorry :
            (a : A ⧸ p) → p.ResidueField)
          x) :
      B ⧸ q)
Tactic: obtain ⟨x, rfl⟩ :=
    (RingEquiv.ofBijective _ p.bijective_algebraMap_quotient_residueField).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsMaximal
inst_9 : q.IsMaximal
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : p.IsMaximal
inst_13 : q.IsMaximal
inst_14 : Algebra.IsSeparable.{u_2, u_3} p.ResidueField q.ResidueField
x : A
⊢ Eq (α := q.ResidueField)
    ((RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
            (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) ⋯ :
          (a : B ⧸ q) → q.ResidueField)
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (A ⧸ p) (B ⧸ q))
              (↑(RingEquiv.symm
                    (RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
                      (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) ⋯)) :
                p.ResidueField →+* A ⧸ p) :
            (a : p.ResidueField) → B ⧸ q)
          ((RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
                (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) ⋯ :
              (a : A ⧸ p) → p.ResidueField)
            ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) x))) :
      q.ResidueField)
    ((RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
            (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) ⋯ :
          (a : B ⧸ q) → q.ResidueField)
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(RingEquiv.symm
                    (RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField)
                      (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField) ⋯)) :
                q.ResidueField →+* B ⧸ q)
              (algebraMap p.ResidueField q.ResidueField) :
            (a : p.ResidueField) → B ⧸ q)
          ((RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
                (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) ⋯ :
              (a : A ⧸ p) → p.ResidueField)
            ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) x))) :
      q.ResidueField)
have a : Eq (α := q.ResidueField)
  ((RingEquiv.ofBijective (F := B ⧸ q →+* q.ResidueField) (algebraMap (B ⧸ q) q.ResidueField : B ⧸ q →+* q.ResidueField)
          sorry :
        (a : B ⧸ q) → q.ResidueField)
      ((algebraMap (A ⧸ p) (B ⧸ q) : (a : A ⧸ p) → B ⧸ q) ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) x)) :
    q.ResidueField)
  ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField)
      ((RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
            (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) sorry :
          (a : A ⧸ p) → p.ResidueField)
        ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) x)) :
    q.ResidueField)
Tactic: simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, RingEquiv.symm_apply_apply,
    RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (hypothesis)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsPrime
inst_9 : q.IsPrime
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsIntegral A B
⊢ Algebra.IsAlgebraic.{u_2, u_3} p.ResidueField q.ResidueField
have this : Algebra.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)
Tactic: have : Algebra.IsIntegral (A ⧸ p) (B ⧸ q) :=
    .tower_top A
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (hypothesis)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsPrime
inst_9 : q.IsPrime
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsIntegral A B
this_1 : Algebra.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)
this : Algebra.{u_2, u_3} (A ⧸ p) q.ResidueField :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ q) q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
⊢ Algebra.IsAlgebraic.{u_2, u_3} p.ResidueField q.ResidueField
have this₁ : IsScalarTower.{u_2, u_3, u_3} (A ⧸ p) (B ⧸ q) q.ResidueField
Tactic: haveI : IsScalarTower (A ⧸ p) (B ⧸ q) q.ResidueField := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (hypothesis)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsPrime
inst_9 : q.IsPrime
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsIntegral A B
this_1 : Algebra.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)
this_2 : Algebra.{u_2, u_3} (A ⧸ p) q.ResidueField :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ q) q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
this : IsScalarTower.{u_2, u_3, u_3} (A ⧸ p) (B ⧸ q) q.ResidueField
⊢ Algebra.IsAlgebraic.{u_2, u_3} p.ResidueField q.ResidueField
have this₁ : Algebra.IsAlgebraic.{u_2, u_3} (A ⧸ p) q.ResidueField
Tactic: haveI : Algebra.IsAlgebraic (A ⧸ p) q.ResidueField := .trans _ (B ⧸ q) _
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsPrime
inst_9 : q.IsPrime
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsIntegral A B
this_1 : Algebra.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)
this_2 : Algebra.{u_2, u_3} (A ⧸ p) q.ResidueField :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ q) q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
this_3 : IsScalarTower.{u_2, u_3, u_3} (A ⧸ p) (B ⧸ q) q.ResidueField
this : Algebra.IsAlgebraic.{u_2, u_3} (A ⧸ p) q.ResidueField
⊢ IsScalarTower.{u_2, u_2, u_3} (A ⧸ p) p.ResidueField q.ResidueField
have refine : ∀ (x : A ⧸ p),
  Eq.{u_3 + 1} (α := q.ResidueField)
    ((algebraMap (A ⧸ p) q.ResidueField : (a : A ⧸ p) → q.ResidueField) x : q.ResidueField)
    ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField)
        ((algebraMap (A ⧸ p) p.ResidueField : (a : A ⧸ p) → p.ResidueField) x) :
      q.ResidueField)
Tactic: refine .of_algebraMap_eq fun x ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsPrime
inst_9 : q.IsPrime
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsIntegral A B
this_1 : Algebra.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)
this_2 : Algebra.{u_2, u_3} (A ⧸ p) q.ResidueField :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ q) q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
this_3 : IsScalarTower.{u_2, u_3, u_3} (A ⧸ p) (B ⧸ q) q.ResidueField
this : Algebra.IsAlgebraic.{u_2, u_3} (A ⧸ p) q.ResidueField
x : A ⧸ p
⊢ Eq.{u_3 + 1} (α := q.ResidueField)
    ((algebraMap (A ⧸ p) q.ResidueField : (a : A ⧸ p) → q.ResidueField) x : q.ResidueField)
    ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField)
        ((algebraMap (A ⧸ p) p.ResidueField : (a : A ⧸ p) → p.ResidueField) x) :
      q.ResidueField)
have obtain : ∀ (x : A),
  Eq.{u_3 + 1} (α := q.ResidueField)
    ((algebraMap (A ⧸ p) q.ResidueField : (a : A ⧸ p) → q.ResidueField) ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) x) :
      q.ResidueField)
    ((algebraMap p.ResidueField q.ResidueField : (a : p.ResidueField) → q.ResidueField)
        ((algebraMap (A ⧸ p) p.ResidueField : (a : A ⧸ p) → p.ResidueField)
          ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) x)) :
      q.ResidueField)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (hypothesis)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
inst_8 : p.IsPrime
inst_9 : q.IsPrime
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra p q
inst_12 : Algebra.IsIntegral A B
this_1 : Algebra.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)
this_2 : Algebra.{u_2, u_3} (A ⧸ p) q.ResidueField :=
  RingHom.toAlgebra
    (@RingHom.comp _ (B ⧸ q) _ _ Semiring.toNonAssocSemiring _ (algebraMap (B ⧸ q) q.ResidueField)
      (algebraMap (A ⧸ p) (B ⧸ q)))
this_3 : IsScalarTower.{u_2, u_3, u_3} (A ⧸ p) (B ⧸ q) q.ResidueField
this : Algebra.IsAlgebraic.{u_2, u_3} (A ⧸ p) q.ResidueField
⊢ Algebra.IsAlgebraic.{u_2, u_3} p.ResidueField q.ResidueField
have this₁ : IsScalarTower.{u_2, u_2, u_3} (A ⧸ p) p.ResidueField q.ResidueField
Tactic: haveI : IsScalarTower (A ⧸ p) p.ResidueField q.ResidueField := by
    refine .of_algebraMap_eq fun x ↦ ?_
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R_1 : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R_1 A
inst_4 : Algebra A B
inst_5 : Algebra R_1 B
inst_6 : IsScalarTower R_1 A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
R : Type u_4
k : Type u_5
inst_8 : CommRing R
inst_9 : IsLocalRing R
inst_10 : Field k
inst_11 : Algebra R k
inst_12 : Module.Finite R k
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥) (maximalIdeal R)
have rw : Eq (α := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥) (RingHom.ker (F := R →+* k) (algebraMap R k))
Tactic: rw [← eq_maximalIdeal (Algebra.ker_algebraMap_isMaximal_of_isIntegral R k), RingHom.ker]