-- 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 : Type v} →
                {M : Type (max u v)} →
                  {M₂ : Type (max u u_2)} →
                    [inst : Semiring S'] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S' M] →
                              [inst_15 : Module S' M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S' S] → (fₗ : M →ₗ[S] 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 : Type v} →
                {M : Type (max u v)} →
                  {M₂ : Type (max u u_2)} →
                    [inst : Semiring S'] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S' M] →
                              [inst_15 : Module S' M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S' S] → (fₗ : M →ₗ[S] 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
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
rw₃ :
  (Extension.H1Cotangent.map (Extension.Hom.id (Generators.toExtension (Generators.self R S'))) :
        (a : H1Cotangent R S') → H1Cotangent R S')
      x =
    x
g : Extension.Hom (Generators.toExtension (Generators.self R S')) (Generators.toExtension (Generators.self R S'))
⊢ ((↑S' :
              {S : Type v} →
                {M : Type (max u v)} →
                  {M₂ : Type (max u u_2)} →
                    [inst : Semiring S'] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S' M] →
                              [inst_15 : Module S' M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S' S] → (fₗ : M →ₗ[S] 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₄ : (LinearMap.id : (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]