-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearMap (goal)
Goal:
A : Type u_1
R : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : Semiring A
inst_1 : CommSemiring R
inst_2 : Semiring R₁
inst_3 : Semiring R₂
M : Type u_5
Mₗ : Type u_6
N : Type u_7
Nₗ : Type u_8
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid Mₗ
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid Nₗ
inst_8 : AddCommMonoid Pₗ
inst_9 : AddCommMonoid Qₗ
inst_10 : AddCommMonoid Qₗ'
inst_11 : Module R M
inst_12 : Module R Mₗ
inst_13 : Module R₁ Mₗ
inst_14 : Module R₂ N
inst_15 : Module R Nₗ
inst_16 : Module R Pₗ
inst_17 : Module R₂ Pₗ
inst_18 : Module R₁ Pₗ
inst_19 : Module R Qₗ
inst_20 : Module R₁ Qₗ
inst_21 : Module R Qₗ'
inst_22 : Module R₂ Qₗ'
Tₗ : Type u_12
Tₗ' : Type u_13
inst_23 : AddCommMonoid Tₗ
inst_24 : AddCommMonoid Tₗ'
inst_25 : Module R₁ Tₗ
inst_26 : Module R₂ Tₗ'
inst_27 : Module A Pₗ
inst_28 : SMulCommClass R A Pₗ
inst_29 : Module R A
inst_30 : Module A M
inst_31 : Module A Qₗ
inst_32 : SMulCommClass R A Qₗ
inst_33 : IsScalarTower R A Qₗ
inst_34 : IsScalarTower R A Pₗ
f : M →ₗ[A] Nₗ →ₗ[R] Pₗ
g : Pₗ →ₗ[A] Qₗ
x : A
x_1 : M
⊢ (↑R :
          {S : Type u_1} →
            {M : Type u_9} →
              {M₂ : Type u_10} →
                [inst : Semiring R] →
                  [inst_35 : Semiring S] →
                    [inst_36 : AddCommMonoid M] →
                      [inst_37 : AddCommMonoid M₂] →
                        [inst_38 : Module R M] →
                          [inst_39 : Module R M₂] →
                            [inst_40 : Module S M] →
                              [inst_41 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g ∘ₗ
      (f : (a : M) → Nₗ →ₗ[R] Pₗ) (x • x_1) =
    HSMul.hSMul (α := A) (β := Nₗ →ₗ[R] Qₗ) ((RingHom.id A : (a : A) → A) x : A)
      ((↑R :
            {S : Type u_1} →
              {M : Type u_9} →
                {M₂ : Type u_10} →
                  [inst : Semiring R] →
                    [inst_35 : Semiring S] →
                      [inst_36 : AddCommMonoid M] →
                        [inst_37 : AddCommMonoid M₂] →
                          [inst_38 : Module R M] →
                            [inst_39 : Module R M₂] →
                              [inst_40 : Module S M] →
                                [inst_41 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g ∘ₗ
        (f : (a : M) → Nₗ →ₗ[R] Pₗ) x_1)
have h : ∀ (x_2 : Nₗ),
  Eq.{u_10 + 1} (α := Qₗ)
    (((↑R :
                {S : Type u_1} →
                  {M : Type u_9} →
                    {M₂ : Type u_10} →
                      [inst : Semiring R] →
                        [inst_35 : Semiring S] →
                          [inst_36 : AddCommMonoid M] →
                            [inst_37 : AddCommMonoid M₂] →
                              [inst_38 : Module R M] →
                                [inst_39 : Module R M₂] →
                                  [inst_40 : Module S M] →
                                    [inst_41 : Module S M₂] →
                                      [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              g ∘ₗ
            (f : (a : M) → Nₗ →ₗ[R] Pₗ) (x • x_1) :
          (a : Nₗ) → Qₗ)
        x_2 :
      Qₗ)
    ((HSMul.hSMul (α := A) (β := Nₗ →ₗ[R] Qₗ) ((RingHom.id A : (a : A) → A) x : A)
            ((↑R :
                  {S : Type u_1} →
                    {M : Type u_9} →
                      {M₂ : Type u_10} →
                        [inst : Semiring R] →
                          [inst_35 : Semiring S] →
                            [inst_36 : AddCommMonoid M] →
                              [inst_37 : AddCommMonoid M₂] →
                                [inst_38 : Module R M] →
                                  [inst_39 : Module R M₂] →
                                    [inst_40 : Module S M] →
                                      [inst_41 : Module S M₂] →
                                        [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                g ∘ₗ
              (f : (a : M) → Nₗ →ₗ[R] Pₗ) x_1) :
          (a : Nₗ) → Qₗ)
        x_2 :
      Qₗ)
Tactic: ext