-- Lean 4 proof step from Mathlib.RingTheory.Kaehler.TensorProduct (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 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ Eq (α := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) Ω[A⁄R] Ω[B⁄S])
    ((↑R :
        {S M : Type u_3} →
          {M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_11 : Semiring S] →
                [inst_12 : AddCommMonoid M] →
                  [inst_13 : AddCommMonoid M₂] →
                    [inst_14 : Module R M] →
                      [inst_15 : Module R M₂] →
                        [inst_16 : Module S M] →
                          [inst_17 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (map R S A B))
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑(tensorKaehlerEquivBase R S A B) : S ⊗[R] Ω[A⁄R] →ₗ[S] Ω[B⁄S]) ∘ₗ
      (mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1)
have h₁ : ∀ (x : Ω[A⁄R]),
  Eq.{u_4 + 1} (α := Ω[B⁄S])
    ((((↑R :
                {S M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (map R S A B) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) Ω[A⁄R] Ω[B⁄S]) :
          (a : Ω[A⁄R]) → Ω[B⁄S])
        x :
      Ω[B⁄S])
    (((↑R :
                {S : Type u_2} →
                  {M : Type (max u_2 u_3)} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (↑(tensorKaehlerEquivBase R S A B) : S ⊗[R] Ω[A⁄R] →ₗ[S] Ω[B⁄S]) ∘ₗ
            (mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 :
          (a : Ω[A⁄R]) → Ω[B⁄S])
        x :
      Ω[B⁄S])
Tactic: refine LinearMap.ext fun x ↦ ?_