-- Module: Mathlib.LinearAlgebra.BilinearMap
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
M' : Type u_5
P' : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : Module S M
inst_8 : Module S P
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower S R P
inst_11 : AddCommMonoid M'
inst_12 : Module S M'
inst_13 : AddCommMonoid P'
inst_14 : Module S P'
i : M' →ₗ[S] M
k : P' →ₗ[S] P
hk : Injective.{u_6 + 1, u_4 + 1} (α := P') (β := P) (⇑k : (a : P') → P)
f : M →ₗ[R] P
hf : ∀ (m : M'), Membership.mem (α := P) k.range ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
m : M'
this :
  Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
    ((k ∘ₗ
            codLift
              ((↑S :
                    {S_1 : Type u_1} →
                      {M : Type u_3} →
                        {M₂ : Type u_4} →
                          [inst : Semiring S] →
                            [inst_15 : Semiring S_1] →
                              [inst_16 : AddCommMonoid M] →
                                [inst_17 : AddCommMonoid M₂] →
                                  [inst_18 : Module S M] →
                                    [inst_19 : Module S M₂] →
                                      [inst_20 : Module S_1 M] →
                                        [inst_21 : Module S_1 M₂] →
                                          [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  f ∘ₗ
                i)
              k hk hf :
          (a : M') → P)
        m :
      P)
rw :
  Eq.{u_4 + 1} (α := P)
    ((k ∘ₗ
            codLift
              ((↑S :
                    {S_1 : Type u_1} →
                      {M : Type u_3} →
                        {M₂ : Type u_4} →
                          [inst : Semiring S] →
                            [inst_15 : Semiring S_1] →
                              [inst_16 : AddCommMonoid M] →
                                [inst_17 : AddCommMonoid M₂] →
                                  [inst_18 : Module S M] →
                                    [inst_19 : Module S M₂] →
                                      [inst_20 : Module S_1 M] →
                                        [inst_21 : Module S_1 M₂] →
                                          [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  f ∘ₗ
                i)
              k hk hf :
          (a : M') → P)
        m :
      P)
    ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
rw₁ :
  Eq.{u_4 + 1} (α := P)
    (((↑S :
                {S_1 : Type u_1} →
                  {M : Type u_3} →
                    {M₂ : Type u_4} →
                      [inst : Semiring S] →
                        [inst_15 : Semiring S_1] →
                          [inst_16 : AddCommMonoid M] →
                            [inst_17 : AddCommMonoid M₂] →
                              [inst_18 : Module S M] →
                                [inst_19 : Module S M₂] →
                                  [inst_20 : Module S_1 M] →
                                    [inst_21 : Module S_1 M₂] →
                                      [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              f ∘ₗ
            i :
          (a : M') → P)
        m :
      P)
    ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
rw₂ :
  Eq.{u_4 + 1} (α := P)
    (((↑S :
              {S_1 : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring S] →
                      [inst_15 : Semiring S_1] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module S M] →
                              [inst_19 : Module S M₂] →
                                [inst_20 : Module S_1 M] →
                                  [inst_21 : Module S_1 M₂] →
                                    [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            f :
          (a : M) → P)
        ((i : (a : M') → M) m : M) :
      P)
    ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
rw₃ rw₄ :
  Eq.{u_4 + 1} (α := P) ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
    ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)
⊢ Eq.{u_4 + 1} (α := P) ((k : (a : P') → P) ((i.restrictScalarsRange k hk f hf : (a : M') → P') m : P') : P)
    ((f : (a : M) → P) ((i : (a : M') → M) m : M) : P)

Tactic:
rw [this, comp_codLift, comp_apply, restrictScalars_apply]

Premises used: LinearMap.restrictScalars_apply, LinearMap.comp_apply, LinearMap.comp_codLift