-- Lean 4 proof step from Mathlib.RingTheory.Etale.Kaehler (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : Algebra.FormallyEtale S T
⊢ Eq (α := (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
    (⇑(lift
          ((↑S :
              {S_1 M : Type u_3} →
                {M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring S] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (S := T)
            (((LinearMap.flip
                    (Algebra.linearMap T (Module.End T (LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]))) :
                  LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R] →ₗ[T]
                    T →ₗ[T] LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) :
                (a : Ω[S⁄R] →ₗ[S] Ω[T⁄R]) → T →ₗ[T] Ω[S⁄R] →ₗ[S] Ω[T⁄R])
              (map R R S T)))) :
      (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
    (⇑((↑S :
            {S_1 : Type u_3} →
              {M : Type (max u_2 u_3)} →
                {M₂ : Type u_3} →
                  [inst : Semiring S] →
                    [inst_8 : Semiring S_1] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [inst_13 : Module S_1 M] →
                                [inst_14 : Module S_1 M₂] →
                                  [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
          (↑(tensorKaehlerEquivOfFormallyEtale R S T) : T ⊗[S] Ω[S⁄R] →ₗ[T] Ω[T⁄R])) :
      (a : T ⊗[S] Ω[S⁄R]) → Ω[T⁄R])
have h : Eq (α := T ⊗[S] Ω[S⁄R] →ₗ[S] Ω[T⁄R])
  (lift
    ((↑S :
        {S_1 M : Type u_3} →
          {M₂ : Type (max u_2 u_3)} →
            [inst : Semiring S] →
              [inst_8 : Semiring S_1] →
                [inst_9 : AddCommMonoid M] →
                  [inst_10 : AddCommMonoid M₂] →
                    [inst_11 : Module S M] →
                      [inst_12 : Module S M₂] →
                        [inst_13 : Module S_1 M] →
                          [inst_14 : Module S_1 M₂] →
                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
      (S := T)
      (((LinearMap.flip
              (Algebra.linearMap T (Module.End T (LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]))) :
            LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R] →ₗ[T]
              T →ₗ[T] LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) Ω[S⁄R] Ω[T⁄R]) :
          (a : Ω[S⁄R] →ₗ[S] Ω[T⁄R]) → T →ₗ[T] Ω[S⁄R] →ₗ[S] Ω[T⁄R])
        (map R R S T))))
  ((↑S :
      {S_1 : Type u_3} →
        {M : Type (max u_2 u_3)} →
          {M₂ : Type u_3} →
            [inst : Semiring S] →
              [inst_8 : Semiring S_1] →
                [inst_9 : AddCommMonoid M] →
                  [inst_10 : AddCommMonoid M₂] →
                    [inst_11 : Module S M] →
                      [inst_12 : Module S M₂] →
                        [inst_13 : Module S_1 M] →
                          [inst_14 : Module S_1 M₂] →
                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
    (↑(tensorKaehlerEquivOfFormallyEtale R S T) : T ⊗[S] Ω[S⁄R] →ₗ[T] Ω[T⁄R]))
Tactic: congr!