-- Lean 4 proof step from Mathlib.RingTheory.QuasiFinite.Weakly (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal T
inst_7 : q.IsPrime
inst_8 : WeaklyQuasiFiniteAt R q
this :
  QuasiFiniteAt S (S :=
    HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
    (Ideal.map (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) q)
H :
  LE.le.{u_3} (α := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))
    (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))
⊢ Eq (α := Ideal T)
    (Ideal.comap (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.map (F :=
        T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) q))
    (Ideal.comap (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.comap (F :=
        HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)) →+*
          HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
        (AlgHom.toRingHom
          (Ideal.quotientMapₐ (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)) (AlgHom.id S T) H))
        (Ideal.map (F :=
          T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
          (Ideal.Quotient.mk (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))) q)))
have a : q ⊔
    Ideal.comap (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q)))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) ⊥ =
  Ideal.comap (F :=
    T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
    (@RingHom.comp _
      (HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))) _ _
      Semiring.toNonAssocSemiring _
      (AlgHom.toRingHom
        (Ideal.quotientMapₐ (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)) (AlgHom.id S T) H))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.under R q))))
    (Ideal.map (F :=
      T →+* HasQuotient.Quotient T (B := Ideal T) (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q)))
      (Ideal.Quotient.mk (Ideal.map (F := S →+* T) (algebraMap S T) (Ideal.under S q))) q)
Tactic: rw [Ideal.comap_comap, Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective]