-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
h :
  ∀ (g : Dual S N'),
    ∃ (m : M'),
      Eq (α := N' →ₗ[S] R)
        ((↑S :
              {S_1 : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_1} →
                    [inst : Semiring S] →
                      [inst_19 : Semiring S_1] →
                        [inst_20 : AddCommMonoid M] →
                          [inst_21 : AddCommMonoid M₂] →
                            [inst_22 : Module S M] →
                              [inst_23 : Module S M₂] →
                                [inst_24 : Module S_1 M] →
                                  [inst_25 : Module S_1 M₂] →
                                    [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (S := R) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m)) ∘ₗ
          j)
        (Algebra.linearMap S R ∘ₗ g)
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
g : Dual S N'
m : M'
hm :
  Eq (α := N' →ₗ[S] R)
    ((↑S :
          {S_1 : Type u_1} →
            {M : Type u_3} →
              {M₂ : Type u_1} →
                [inst : Semiring S] →
                  [inst_19 : Semiring S_1] →
                    [inst_20 : AddCommMonoid M] →
                      [inst_21 : AddCommMonoid M₂] →
                        [inst_22 : Module S M] →
                          [inst_23 : Module S M₂] →
                            [inst_24 : Module S_1 M] →
                              [inst_25 : Module S_1 M₂] →
                                [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (S := R) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m)) ∘ₗ
      j)
    (Algebra.linearMap S R ∘ₗ g)
n : N'
⊢ Eq.{u_1 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp : (a : M') → N' →ₗ[S] S) m : N' →ₗ[S] S) :
              (a : N') → S)
            n :
          S) :
      R)
    ((algebraMap S R : (a : S) → R) ((g : (a : N') → S) n : S) : R)
have h₁ : Eq.{u_1 + 1} (α := R)
  ((Algebra.linearMap S R : (a : S) → R)
      ((((i.restrictScalarsRange₂ j (Algebra.linearMap S R) sorry p hp : (a : M') → N' →ₗ[S] S) m : N' →ₗ[S] S) :
            (a : N') → S)
          n :
        S) :
    R)
  ((algebraMap S R : (a : S) → R) ((g : (a : N') → S) n : S) : R)
Tactic: change Algebra.linearMap S R _ = _