-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f g : AlgHom.{u_1, u_4, u_3} R A[ε] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  Eq (α := A →ₗ[R] B)
    (f.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LinearMap.toSpanSingleton A A[ε] ε))
    (g.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LinearMap.toSpanSingleton A A[ε] ε))
h :
  ∀ (a : A),
    Eq.{u_3 + 1} (α := B)
      ((f.toLinearMap ∘ₗ
              (↑R :
                  {S M M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module R M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (inrHom A A) :
            (a : A) → B)
          a :
        B)
      ((g.toLinearMap ∘ₗ
              (↑R :
                  {S M M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module R M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (inrHom A A) :
            (a : A) → B)
          a :
        B)
⊢ Eq (α := A →ₗ[R] B)
    (f.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (inrHom A A))
    (g.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (inrHom A A))

Tactic:
ext a