-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst_3 : CommRing S'
inst_4 : Algebra R S'
T : Type w
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
inst_9 : Algebra S' T
inst_10 : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this_1 : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this_2 : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this_3 : IsScalarTower R S S'
this_4 : IsScalarTower R S' S
this_5 : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S
rw :
  ((↑S :
              {S_1 : Type u_2} →
                {M : Type (max u u_2)} →
                  {M₂ : Type (max u v)} →
                    [inst : Semiring S] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Extension.H1Cotangent.map
              (Generators.Hom.toExtensionHom (Generators.defaultHom (Generators.self R S') (Generators.self R S)))) ∘ₗ
          map R R S S' :
        (a : H1Cotangent R S) → H1Cotangent R S)
      x =
    x
rw₁ :
  ((↑S :
              {S_1 : Type u_2} →
                {M : Type (max u u_2)} →
                  {M₂ : Type (max u v)} →
                    [inst : Semiring S] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (Extension.H1Cotangent.map
              (Generators.Hom.toExtensionHom (Generators.defaultHom (Generators.self R S') (Generators.self R S)))) ∘ₗ
          Extension.H1Cotangent.map
            (Generators.Hom.toExtensionHom (Generators.defaultHom (Generators.self R S) (Generators.self R S'))) :
        (a : H1Cotangent R S) → H1Cotangent R S)
      x =
    x
⊢ ((↑S :
              {S_1 : Type u_2} →
                {M : Type (max u u_2)} →
                  {M₂ : Type (max u v)} →
                    [inst : Semiring S] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (map R R S' S) ∘ₗ
          map R R S S' :
        (a : H1Cotangent R S) → H1Cotangent R S)
      x =
    x
have rw₂ : (Extension.H1Cotangent.map
        (Extension.Hom.comp (P' := Generators.toExtension (Generators.self R S'))
          (Generators.Hom.toExtensionHom (Generators.defaultHom (Generators.self R S') (Generators.self R S)))
          (Generators.Hom.toExtensionHom (Generators.defaultHom (Generators.self R S) (Generators.self R S')))) :
      (a : H1Cotangent R S) → H1Cotangent R S)
    x =
  x
Tactic: rw [map, map, ← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq,
        Extension.H1Cotangent.map_id, LinearMap.id_apply]