awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx :
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x) :
      P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)

Tactic:
rw [CotangentSpace.map_cotangentComplex] at hx

Premises used: Algebra.Extension.CotangentSpace.map_cotangentComplex
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx :
  Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)
rw : Eq (α := P'.CotangentSpace) ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0) 0
⊢ Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    (0 : P'.CotangentSpace)

Tactic:
rw [hx]
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx :
  Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace) ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0) 0

Tactic:
LinearMap.map_zero _

Premises used: LinearMap.map_zero
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f : P.Hom P'
x : P.Cotangent
hx :
  Eq (α := P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0 : P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace) ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) 0) 0

Tactic:
exact LinearMap.map_zero _

Premises used: LinearMap.map_zero
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f g : P.Hom P'
h :
  ∀ (x : P.H1Cotangent),
    Eq.{w' + 1} (α := P'.ker.Cotangent)
      (Cotangent.val (↑((map f : (a : P.H1Cotangent) → P'.H1Cotangent) x) : P'.Cotangent))
      (Cotangent.val (↑((map g : (a : P.H1Cotangent) → P'.H1Cotangent) x) : P'.Cotangent))
⊢ map f = map g

Tactic:
ext x
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f g : P.Hom P'
x : P.H1Cotangent
h :
  Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent)))
    (Cotangent.val ((Cotangent.map g : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent)))
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val (↑((map f : (a : P.H1Cotangent) → P'.H1Cotangent) x) : P'.Cotangent))
    (Cotangent.val (↑((map g : (a : P.H1Cotangent) → P'.H1Cotangent) x) : P'.Cotangent))

Tactic:
simp only [map_apply_coe]

Premises used: Algebra.Extension.H1Cotangent.map_apply_coe
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f g : P.Hom P'
x : P.H1Cotangent
h :
  Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent))) 0
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent)))
    (Cotangent.val ((Cotangent.map g : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent)))

Tactic:
rw [← sub_eq_zero, ← Cotangent.val_sub, ← LinearMap.sub_apply, Cotangent.map_sub_map]

Premises used: Algebra.Extension.Cotangent.val_sub, sub_eq_zero, LinearMap.sub_apply, Algebra.Extension.Cotangent.map_sub_map
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
P : Extension.{u_1, u, v} R S
f g : P.Hom P'
x : P.H1Cotangent
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) (↑x : P.Cotangent))) 0

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.map_coe_ker, map_zero,
    Cotangent.val_zero]

Premises used: map_zero, LinearMap.coe_comp, LinearMap.map_coe_ker, Function.comp_apply, Algebra.Extension.Cotangent.val_zero
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
h :
  ∀ (x : P.H1Cotangent),
    Eq.{u_1 + 1} (α := P.ker.Cotangent)
      (Cotangent.val (↑((map (Hom.id P) : (a : P.H1Cotangent) → P.H1Cotangent) x) : P.Cotangent))
      (Cotangent.val (↑((LinearMap.id : (a : P.H1Cotangent) → P.H1Cotangent) x) : P.Cotangent))
⊢ map (Hom.id P) = LinearMap.id

Tactic:
ext
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u_1, u, v} R S
x : P.H1Cotangent
⊢ Eq.{u_1 + 1} (α := P.ker.Cotangent)
    (Cotangent.val (↑((map (Hom.id P) : (a : P.H1Cotangent) → P.H1Cotangent) x) : P.Cotangent))
    (Cotangent.val (↑((LinearMap.id : (a : P.H1Cotangent) → P.H1Cotangent) x) : P.Cotangent))

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
P : Extension.{u_1, u, v} R S
f : P.Hom P'
g : P'.Hom P''
h :
  ∀ (x : P.H1Cotangent),
    Eq.{w'' + 1} (α := P''.ker.Cotangent)
      (Cotangent.val
        (↑(((map (g.comp f) : LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) :
                (a : P.H1Cotangent) → P''.H1Cotangent)
              x) :
          P''.Cotangent))
      (Cotangent.val
        (↑((((↑S :
                        {S_1 : Type v'} →
                          {M : Type w'} →
                            {M₂ : Type w''} →
                              [inst : Semiring S] →
                                [inst_23 : Semiring S_1] →
                                  [inst_24 : AddCommMonoid M] →
                                    [inst_25 : AddCommMonoid M₂] →
                                      [inst_26 : Module S M] →
                                        [inst_27 : Module S M₂] →
                                          [inst_28 : Module S_1 M] →
                                            [inst_29 : Module S_1 M₂] →
                                              [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                      (map g) ∘ₗ
                    map f :
                  LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) :
                (a : P.H1Cotangent) → P''.H1Cotangent)
              x) :
          P''.Cotangent))
⊢ Eq (α := LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) (map (g.comp f))
    ((↑S :
          {S_1 : Type v'} →
            {M : Type w'} →
              {M₂ : Type w''} →
                [inst : Semiring S] →
                  [inst_23 : Semiring S_1] →
                    [inst_24 : AddCommMonoid M] →
                      [inst_25 : AddCommMonoid M₂] →
                        [inst_26 : Module S M] →
                          [inst_27 : Module S M₂] →
                            [inst_28 : Module S_1 M] →
                              [inst_29 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (map g) ∘ₗ
      map f)

Tactic:
ext
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
P : Extension.{u_1, u, v} R S
f : P.Hom P'
g : P'.Hom P''
x : P.H1Cotangent
⊢ Eq.{w'' + 1} (α := P''.ker.Cotangent)
    (Cotangent.val
      (↑(((map (g.comp f) : LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) :
              (a : P.H1Cotangent) → P''.H1Cotangent)
            x) :
        P''.Cotangent))
    (Cotangent.val
      (↑((((↑S :
                      {S_1 : Type v'} →
                        {M : Type w'} →
                          {M₂ : Type w''} →
                            [inst : Semiring S] →
                              [inst_23 : Semiring S_1] →
                                [inst_24 : AddCommMonoid M] →
                                  [inst_25 : AddCommMonoid M₂] →
                                    [inst_26 : Module S M] →
                                      [inst_27 : Module S M₂] →
                                        [inst_28 : Module S_1 M] →
                                          [inst_29 : Module S_1 M₂] →
                                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                    (map g) ∘ₗ
                  map f :
                LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) :
              (a : P.H1Cotangent) → P''.H1Cotangent)
            x) :
        P''.Cotangent))

Tactic:
simp [Cotangent.map_comp]

Premises used: Algebra.Extension.Cotangent.map_comp
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
P : Extension.{u_1, u, v} R S
f : P.Hom P'
g : P'.Hom P''
x : P.H1Cotangent
⊢ Eq.{w'' + 1} (α := P''.H1Cotangent)
    (((map (g.comp f) : LinearMap.{v, v, u_1, w''} (RingHom.id S) P.H1Cotangent P''.H1Cotangent) :
          (a : P.H1Cotangent) → P''.H1Cotangent)
        x :
      P''.H1Cotangent)
    ((map g : (a : P'.H1Cotangent) → P''.H1Cotangent) ((map f : (a : P.H1Cotangent) → P'.H1Cotangent) x) :
      P''.H1Cotangent)

Tactic:
congr($(H1Cotangent.map_comp f g) x)

Premises used: congrArg, id, DFunLike.coe, Algebra.Extension.H1Cotangent.map_comp
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension R S
P₁ : Extension.{u_1, u, v} R S
P₂ : Extension.{u_2, u, v} R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₁.H1Cotangent
rw :
  Eq (α := P₁.H1Cotangent)
    (((↑S :
                {S_1 : Type v} →
                  {M : Type u_2} →
                    {M₂ : Type u_1} →
                      [inst : Semiring S] →
                        [inst_24 : Semiring S_1] →
                          [inst_25 : AddCommMonoid M] →
                            [inst_26 : AddCommMonoid M₂] →
                              [inst_27 : Module S M] →
                                [inst_28 : Module S M₂] →
                                  [inst_29 : Module S_1 M] →
                                    [inst_30 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (map f₂) ∘ₗ
            map f₁ :
          (a : P₁.H1Cotangent) → P₁.H1Cotangent)
        x :
      P₁.H1Cotangent)
    ((map f₂ ∘ₗ map f₁ : (a : P₁.H1Cotangent) → P₁.H1Cotangent) x : P₁.H1Cotangent)
⊢ Eq (α := P₁.H1Cotangent) ((map f₂ ∘ₗ map f₁ : (a : P₁.H1Cotangent) → P₁.H1Cotangent) x : P₁.H1Cotangent)
    ((LinearMap.id : (a : P₁.H1Cotangent) → P₁.H1Cotangent) x : P₁.H1Cotangent)

Tactic:
rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₂.comp f₁),
      Extension.H1Cotangent.map_comp]

Premises used: Algebra.Extension.H1Cotangent.map_id, Algebra.Extension.H1Cotangent.map_eq, Algebra.Extension.Hom.comp, eq_comm, Algebra.Extension.H1Cotangent.map_comp
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension R S
P₁ : Extension.{u_1, u, v} R S
P₂ : Extension.{u_2, u, v} R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₁.H1Cotangent
⊢ Eq (α := P₁.H1Cotangent)
    (((↑S :
                {S_1 : Type v} →
                  {M : Type u_2} →
                    {M₂ : Type u_1} →
                      [inst : Semiring S] →
                        [inst_24 : Semiring S_1] →
                          [inst_25 : AddCommMonoid M] →
                            [inst_26 : AddCommMonoid M₂] →
                              [inst_27 : Module S M] →
                                [inst_28 : Module S M₂] →
                                  [inst_29 : Module S_1 M] →
                                    [inst_30 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (map f₂) ∘ₗ
            map f₁ :
          (a : P₁.H1Cotangent) → P₁.H1Cotangent)
        x :
      P₁.H1Cotangent)
    ((map f₂ ∘ₗ map f₁ : (a : P₁.H1Cotangent) → P₁.H1Cotangent) x : P₁.H1Cotangent)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
P : Extension R S
P₁ : Extension.{u_1, u, v} R S
P₂ : Extension.{u_2, u, v} R S
f₁ : P₁.Hom P₂
f₂ : P₂.Hom P₁
x : P₂.H1Cotangent
rw :
  Eq (α := P₂.H1Cotangent)
    (((↑S :
                {S_1 : Type v} →
                  {M : Type u_1} →
                    {M₂ : Type u_2} →
                      [inst : Semiring S] →
                        [inst_24 : Semiring S_1] →
                          [inst_25 : AddCommMonoid M] →
                            [inst_26 : AddCommMonoid M₂] →
                              [inst_27 : Module S M] →
                                [inst_28 : Module S M₂] →
                                  [inst_29 : Module S_1 M] →
                                    [inst_30 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (map f₁) ∘ₗ
            map f₂ :
          (a : P₂.H1Cotangent) → P₂.H1Cotangent)
        x :
      P₂.H1Cotangent)
    ((map f₁ ∘ₗ map f₂ : (a : P₂.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
⊢ Eq (α := P₂.H1Cotangent) ((map f₁ ∘ₗ map f₂ : (a : P₂.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
    ((LinearMap.id : (a : P₂.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)

Tactic:
rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₁.comp f₂),
      Extension.H1Cotangent.map_comp]

Premises used: Algebra.Extension.H1Cotangent.map_id, Algebra.Extension.H1Cotangent.map_eq, Algebra.Extension.Hom.comp, eq_comm, Algebra.Extension.H1Cotangent.map_comp