awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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)
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) ⋯) :
                  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) ⋯) :
                    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)
⊢ 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)))

Tactic:
ext x
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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)
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) ⋯) :
                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) ⋯) :
                  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:
simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]

Premises used: RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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)

Tactic:
Algebra.IsSeparable.of_equiv_equiv
    (.symm <| .ofBijective _ p.bijective_algebraMap_quotient_residueField)
    (.symm <| .ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_

Premises used: Algebra.IsSeparable.of_equiv_equiv, RingEquiv.ofBijective, Ideal.bijective_algebraMap_quotient_residueField, RingEquiv.symm
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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
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) ⋯)) :
        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))
⊢ Algebra.IsSeparable.{u_2, u_3} (A ⧸ p) (B ⧸ q)

Tactic:
refine Algebra.IsSeparable.of_equiv_equiv
    (.symm <| .ofBijective _ p.bijective_algebraMap_quotient_residueField)
    (.symm <| .ofBijective _ q.bijective_algebraMap_quotient_residueField) ?_

Premises used: Algebra.IsSeparable.of_equiv_equiv, RingEquiv.ofBijective, Ideal.bijective_algebraMap_quotient_residueField, RingEquiv.symm
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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
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) ⋯)) :
                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)
⊢ 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))

Tactic:
apply RingHom.ext fun x ↦ ?_

Premises used: RingHom.ext
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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
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) ⋯)) :
                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)
            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)
          ((RingEquiv.ofBijective (F := A ⧸ p →+* p.ResidueField)
                (algebraMap (A ⧸ p) p.ResidueField : A ⧸ p →+* p.ResidueField) ⋯ :
              (a : A ⧸ p) → p.ResidueField)
            x) :
        B ⧸ q)
⊢ 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)

Tactic:
obtain ⟨x, rfl⟩ :=
    (RingEquiv.ofBijective _ p.bijective_algebraMap_quotient_residueField).surjective x

Premises used: RingEquiv.surjective, RingEquiv.ofBijective, Ideal.bijective_algebraMap_quotient_residueField, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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)
        ((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) ⋯ :
            (a : A ⧸ p) → p.ResidueField)
          ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) x)) :
      q.ResidueField)

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]

Premises used: RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
Goal:
A : Type u_2
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
p : Ideal A
q : Ideal B
inst_3 : q.LiesOver p
inst_4 : p.IsMaximal
inst_5 : q.IsMaximal
inst_6 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime q)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Algebra.IsSeparable.{u_2, u_3} p.ResidueField q.ResidueField ↔ Algebra.IsSeparable.{u_2, u_3} (A ⧸ p) (B ⧸ q)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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
⊢ Algebra.IsAlgebraic.{u_2, u_2} (A ⧸ p) p.ResidueField

Tactic:
IsLocalization.isAlgebraic _ (nonZeroDivisors (A ⧸ p))

Premises used: nonZeroDivisors, HasQuotient.Quotient, IsLocalization.isAlgebraic
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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.IsIntegral.{u_2, u_3} (A ⧸ p) (B ⧸ q)

Tactic:
have : Algebra.IsIntegral (A ⧸ p) (B ⧸ q) :=
    .tower_top A
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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)))
⊢ 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
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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} (A ⧸ p) q.ResidueField

Tactic:
haveI : Algebra.IsAlgebraic (A ⧸ p) q.ResidueField := .trans _ (B ⧸ q) _
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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

Tactic:
.of_algebraMap_eq fun x ↦ ?_

Premises used: IsScalarTower.of_algebraMap_eq
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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
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)
⊢ IsScalarTower.{u_2, u_2, u_3} (A ⧸ p) p.ResidueField q.ResidueField

Tactic:
refine .of_algebraMap_eq fun x ↦ ?_
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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
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)
⊢ 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:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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
⊢ 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:
simp [RingHom.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_apply]

Premises used: RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Instances
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

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]