-- Module: Mathlib.RingTheory.Smooth.Basic
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
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)
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)
    (((map (P₂.toInfinitesimal.comp 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)
h₂ :
  Eq.{u_5 + 1} (α := P₂.infinitesimal.H1Cotangent)
    (((map (P₂.toInfinitesimal.comp 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)
    (((map (P₂.toInfinitesimal.comp 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)
h₃ : P₁.Hom P₂.infinitesimal
h₄ :
  Eq.{u_5 + 1} (α := P₂.infinitesimal.H1Cotangent)
    (((map (P₂.toInfinitesimal.comp 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)
    (((map (P₂.toInfinitesimal.comp 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)
h₅ : P₁.Hom P₂.infinitesimal
⊢ 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)

Tactic:
rw [← map_comp, ← map_comp, map_eq]

Premises used: Algebra.Extension.H1Cotangent.map_eq, Algebra.Extension.H1Cotangent.map_comp