-- 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 ⧸ 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)
have obtain : ∀ (x : A),
  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)
          ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) 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)
          ((Ideal.Quotient.mk p : (a : A) → A ⧸ p) x)) :
      B ⧸ q)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x