-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
x : P₁.H1Cotangent
⊢ Eq.{u_5 + 1} (α := P₂.infinitesimal.H1Cotangent)
    ((((↑A :
                  {S : Type v} →
                    {M : Type u_4} →
                      {M₂ : Type u_5} →
                        [inst : Semiring A] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module A M] →
                                  [inst_9 : Module A M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
                (map (P₁.homInfinitesimal P₂)) ∘ₗ
              map P₁.toInfinitesimal :
            LinearMap.{v, v, u_4, u_5} (RingHom.id A) P₁.H1Cotangent P₂.infinitesimal.H1Cotangent) :
          (a : P₁.H1Cotangent) → P₂.infinitesimal.H1Cotangent)
        x :
      P₂.infinitesimal.H1Cotangent)
    ((((↑A :
                  {S : Type v} →
                    {M M₂ : Type u_5} →
                      [inst : Semiring A] →
                        [inst_5 : Semiring S] →
                          [inst_6 : AddCommMonoid M] →
                            [inst_7 : AddCommMonoid M₂] →
                              [inst_8 : Module A M] →
                                [inst_9 : Module A M₂] →
                                  [inst_10 : Module S M] →
                                    [inst_11 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
                (map P₂.toInfinitesimal) ∘ₗ
              map f :
            LinearMap.{v, v, u_4, u_5} (RingHom.id A) P₁.H1Cotangent P₂.infinitesimal.H1Cotangent) :
          (a : P₁.H1Cotangent) → P₂.infinitesimal.H1Cotangent)
        x :
      P₂.infinitesimal.H1Cotangent)
have h : Eq.{u_5 + 1} (α := P₂.infinitesimal.H1Cotangent)
  (((map ((P₁.homInfinitesimal P₂).comp P₁.toInfinitesimal) :
          LinearMap.{v, v, u_4, u_5} (RingHom.id A) P₁.H1Cotangent P₂.infinitesimal.H1Cotangent) :
        (a : P₁.H1Cotangent) → P₂.infinitesimal.H1Cotangent)
      x :
    P₂.infinitesimal.H1Cotangent)
  ((((↑A :
                {S : Type v} →
                  {M M₂ : Type u_5} →
                    [inst : Semiring A] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module A M] →
                              [inst_9 : Module A M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
              (map P₂.toInfinitesimal) ∘ₗ
            map f :
          LinearMap.{v, v, u_4, u_5} (RingHom.id A) P₁.H1Cotangent P₂.infinitesimal.H1Cotangent) :
        (a : P₁.H1Cotangent) → P₂.infinitesimal.H1Cotangent)
      x :
    P₂.infinitesimal.H1Cotangent)
Tactic: rw [← map_comp, ← map_comp, map_eq]