-- Lean 4 proof step from Mathlib.Analysis.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
F : Type u_2
inst_1 : AddCommGroup F
inst_2 : Module ℝ F
inst_3 : Module 𝕜 F
inst_4 : IsScalarTower ℝ 𝕜 F
f : Dual 𝕜 F
x : F
h :
  Eq (α := ℝ)
    ((re : (a : 𝕜) → ℝ)
        ((extendRCLike
                ((fun (f : Dual 𝕜 F) ↦
                    (reLm ∘ₗ
                        (↑ℝ :
                            {S : Type u_1} →
                              {M : Type u_2} →
                                {M₂ : Type u_1} →
                                  [inst : Semiring ℝ] →
                                    [inst_5 : Semiring S] →
                                      [inst_6 : AddCommMonoid M] →
                                        [inst_7 : AddCommMonoid M₂] →
                                          [inst_8 : Module ℝ M] →
                                            [inst_9 : Module ℝ M₂] →
                                              [inst_10 : Module S M] →
                                                [inst_11 : Module S M₂] →
                                                  [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                          f :
                      F →ₗ[ℝ] ℝ))
                  f) :
              (a : F) → 𝕜)
            x :
          𝕜) :
      ℝ)
    ((re : (a : 𝕜) → ℝ) ((f : (a : F) → 𝕜) x : 𝕜) : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((extendRCLike
            ((fun (f : Dual 𝕜 F) ↦
                (reLm ∘ₗ
                    (↑ℝ :
                        {S : Type u_1} →
                          {M : Type u_2} →
                            {M₂ : Type u_1} →
                              [inst : Semiring ℝ] →
                                [inst_5 : Semiring S] →
                                  [inst_6 : AddCommMonoid M] →
                                    [inst_7 : AddCommMonoid M₂] →
                                      [inst_8 : Module ℝ M] →
                                        [inst_9 : Module ℝ M₂] →
                                          [inst_10 : Module S M] →
                                            [inst_11 : Module S M₂] →
                                              [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                      f :
                  F →ₗ[ℝ] ℝ))
              f) :
          (a : F) → 𝕜)
        x :
      𝕜)
    ((f : (a : F) → 𝕜) x : 𝕜)
have h₁ : Eq (α := ℝ)
  ((im : (a : 𝕜) → ℝ)
      ((extendRCLike
              ((fun (f : Dual 𝕜 F) ↦
                  (reLm ∘ₗ
                      (↑ℝ :
                          {S : Type u_1} →
                            {M : Type u_2} →
                              {M₂ : Type u_1} →
                                [inst : Semiring ℝ] →
                                  [inst_5 : Semiring S] →
                                    [inst_6 : AddCommMonoid M] →
                                      [inst_7 : AddCommMonoid M₂] →
                                        [inst_8 : Module ℝ M] →
                                          [inst_9 : Module ℝ M₂] →
                                            [inst_10 : Module S M] →
                                              [inst_11 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                        f :
                    F →ₗ[ℝ] ℝ))
                f) :
            (a : F) → 𝕜)
          x :
        𝕜) :
    ℝ)
  ((im : (a : 𝕜) → ℝ) ((f : (a : F) → 𝕜) x : 𝕜) : ℝ)
Tactic: apply RCLike.ext