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 : 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'
f : P.Hom P'
x : S
y : P.Ring
simp :
  HSMul.hSMul (β := P'.CotangentSpace) x
      (1 ⊗ₜ[P'.Ring]
          (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R']) ((algebraMap P.Ring P'.Ring : (a : P.Ring) → P'.Ring) y) :
        TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R']) =
    (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y)
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) y) :
      P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])

Tactic:
simp only [CotangentSpace.map, AlgHom.toRingHom_eq_coe, LinearMap.liftBaseChange_tmul,
    LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, map_D, mk_apply]

Premises used: TensorProduct.mk_apply, LinearMap.coe_restrictScalars, Algebra.Extension.CotangentSpace.map, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, AlgHom.toRingHom_eq_coe, Function.comp_apply, KaehlerDifferential.map_D
-- 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.{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'
f : P.Hom P'
x : S
y : P.Ring
rw :
  Eq (α := P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R']) ((algebraMap P.Ring P'.Ring : (a : P.Ring) → P'.Ring) y) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
⊢ HSMul.hSMul (β := P'.CotangentSpace) x
      (1 ⊗ₜ[P'.Ring]
          (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R']) ((algebraMap P.Ring P'.Ring : (a : P.Ring) → P'.Ring) y) :
        TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R']) =
    (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y)

Tactic:
rw [smul_tmul', ← Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul'
-- 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.{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'
f : P.Hom P'
x : S
y : P.Ring
⊢ Eq (α := P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R']) ((algebraMap P.Ring P'.Ring : (a : P.Ring) → P'.Ring) y) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])

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 : Extension.{w, u, v} R S
a :
  ∀ (a : P.Ring),
    Eq (α := P.CotangentSpace)
      (((((LinearMap.compDer
                      (((AlgebraTensorModule.curry (CotangentSpace.map (Hom.id P)) :
                            S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P.CotangentSpace) :
                          (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] P.CotangentSpace)
                        1) :
                    LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
                      (Derivation R P.Ring P.CotangentSpace)) :
                  (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring P.CotangentSpace)
                (D R P.Ring) :
              Derivation R P.Ring P.CotangentSpace) :
            (a : P.Ring) → P.CotangentSpace)
          a :
        P.CotangentSpace)
      (((((LinearMap.compDer
                      (((AlgebraTensorModule.curry LinearMap.id :
                            S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P.CotangentSpace) :
                          (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] P.CotangentSpace)
                        1) :
                    LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
                      (Derivation R P.Ring P.CotangentSpace)) :
                  (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring P.CotangentSpace)
                (D R P.Ring) :
              Derivation R P.Ring P.CotangentSpace) :
            (a : P.Ring) → P.CotangentSpace)
          a :
        P.CotangentSpace)
⊢ CotangentSpace.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.{w, u, v} R S
a : P.Ring
⊢ Eq (α := P.CotangentSpace)
    (((((LinearMap.compDer
                    (((AlgebraTensorModule.curry (CotangentSpace.map (Hom.id P)) :
                          S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P.CotangentSpace) :
                        (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] P.CotangentSpace)
                      1) :
                  LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
                    (Derivation R P.Ring P.CotangentSpace)) :
                (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring P.CotangentSpace)
              (D R P.Ring) :
            Derivation R P.Ring P.CotangentSpace) :
          (a : P.Ring) → P.CotangentSpace)
        a :
      P.CotangentSpace)
    (((((LinearMap.compDer
                    (((AlgebraTensorModule.curry LinearMap.id :
                          S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P.CotangentSpace) :
                        (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] P.CotangentSpace)
                      1) :
                  LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
                    (Derivation R P.Ring P.CotangentSpace)) :
                (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring P.CotangentSpace)
              (D R P.Ring) :
            Derivation R P.Ring P.CotangentSpace) :
          (a : P.Ring) → P.CotangentSpace)
        a :
      P.CotangentSpace)

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
P : 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''
f : P.Hom P'
g : P'.Hom P''
h :
  ∀ (x : P.CotangentSpace),
    Eq (α := P''.CotangentSpace)
      ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace) x : P''.CotangentSpace)
      (((↑S :
                  {S_1 : Type v'} →
                    {M : Type (max v' w')} →
                      {M₂ : Type (max v'' 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₂)
                (CotangentSpace.map g) ∘ₗ
              CotangentSpace.map f :
            (a : P.CotangentSpace) → P''.CotangentSpace)
          x :
        P''.CotangentSpace)
⊢ Eq (α := P.CotangentSpace →ₗ[S] P''.CotangentSpace) (CotangentSpace.map (g.comp f))
    ((↑S :
          {S_1 : Type v'} →
            {M : Type (max v' w')} →
              {M₂ : Type (max v'' 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₂)
        (CotangentSpace.map g) ∘ₗ
      CotangentSpace.map f)

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
P : 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''
f : P.Hom P'
g : P'.Hom P''
⊢ Eq (α := P''.CotangentSpace) ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace) 0)
    (((↑S :
              {S_1 : Type v'} →
                {M : Type (max v' w')} →
                  {M₂ : Type (max v'' 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₂)
            (CotangentSpace.map g) ∘ₗ
          CotangentSpace.map f :
        (a : P.CotangentSpace) → P''.CotangentSpace)
      0)

Tactic:
simp only [map_zero]

Premises used: 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 : 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''
f : P.Hom P'
g : P'.Hom P''
x : S
⊢ Eq (α := P''.CotangentSpace)
    ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) 0) :
      P''.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type (max v' w')} →
                    {M₂ : Type (max v'' 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₂)
              (CotangentSpace.map g) ∘ₗ
            CotangentSpace.map f :
          (a : P.CotangentSpace) → P''.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) 0) :
      P''.CotangentSpace)

Tactic:
simp only [map_zero, tmul_zero]

Premises used: TensorProduct.tmul_zero, 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 : 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''
f : P.Hom P'
g : P'.Hom P''
x : S
x_1 y : P.Ring
⊢ Eq (α := P''.CotangentSpace)
    ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace)
        (x ⊗ₜ[P.Ring]
          (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) (x_1 ⊗ₜ[R] y)) :
      P''.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type (max v' w')} →
                    {M₂ : Type (max v'' 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₂)
              (CotangentSpace.map g) ∘ₗ
            CotangentSpace.map f :
          (a : P.CotangentSpace) → P''.CotangentSpace)
        (x ⊗ₜ[P.Ring]
          (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) (x_1 ⊗ₜ[R] y)) :
      P''.CotangentSpace)

Tactic:
simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', map_tmul,
        Hom.toAlgHom_apply, Hom.comp_toRingHom, RingHom.coe_comp, Function.comp_apply,
        LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        ← IsScalarTower.algebraMap_apply S S' S'']

Premises used: Algebra.Extension.CotangentSpace.map_tmul, LinearMap.coe_restrictScalars, TensorProduct.tmul_smul, TensorProduct.smul_tmul', LinearMap.coe_comp, RingHom.coe_comp, Derivation.tensorProductTo_tmul, Function.comp_apply, IsScalarTower.algebraMap_apply, Algebra.Extension.Hom.comp_toRingHom, Algebra.Extension.Hom.toAlgHom_apply
-- 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.{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''
f : P.Hom P'
g : P'.Hom P''
x : P.CotangentSpace
⊢ Eq (α := P''.CotangentSpace)
    ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace) x : P''.CotangentSpace)
    ((CotangentSpace.map g : (a : P'.CotangentSpace) → P''.CotangentSpace)
        ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) x) :
      P''.CotangentSpace)

Tactic:
DFunLike.congr_fun (map_comp f g) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, Algebra.Extension.CotangentSpace.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 : 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'
f : P.Hom P'
x : P.Cotangent
obtain :
  ∀ (x : ↥P.ker),
    Eq (α := P'.CotangentSpace)
      ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
          ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace)
            ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x)) :
        P'.CotangentSpace)
      ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
          ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x)) :
        P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) x) :
      P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) x) :
      P'.CotangentSpace)

Tactic:
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x

Premises used: Algebra.Extension.Cotangent.mk_surjective, 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 : 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'
f : P.Hom P'
h :
  ∀ (x : P.Cotangent),
    Eq (α := P'.CotangentSpace)
      ((CotangentSpace.map f ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.CotangentSpace) x : P'.CotangentSpace)
      (((↑S :
                  {S_1 : Type v'} →
                    {M : Type w'} →
                      {M₂ : Type (max v' w')} →
                        [inst : Semiring S] →
                          [inst_10 : Semiring S_1] →
                            [inst_11 : AddCommMonoid M] →
                              [inst_12 : AddCommMonoid M₂] →
                                [inst_13 : Module S M] →
                                  [inst_14 : Module S M₂] →
                                    [inst_15 : Module S_1 M] →
                                      [inst_16 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                P'.cotangentComplex ∘ₗ
              Cotangent.map f :
            (a : P.Cotangent) → P'.CotangentSpace)
          x :
        P'.CotangentSpace)
⊢ CotangentSpace.map f ∘ₗ P.cotangentComplex =
    (↑S :
          {S_1 : Type v'} →
            {M : Type w'} →
              {M₂ : Type (max v' w')} →
                [inst : Semiring S] →
                  [inst_10 : Semiring S_1] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module S M] →
                          [inst_14 : Module S M₂] →
                            [inst_15 : Module S_1 M] →
                              [inst_16 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        P'.cotangentComplex ∘ₗ
      Cotangent.map f

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
P : 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'
f : P.Hom P'
x : P.Cotangent
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.CotangentSpace) x : P'.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [inst : Semiring S] →
                        [inst_10 : Semiring S_1] →
                          [inst_11 : AddCommMonoid M] →
                            [inst_12 : AddCommMonoid M₂] →
                              [inst_13 : Module S M] →
                                [inst_14 : Module S M₂] →
                                  [inst_15 : Module S_1 M] →
                                    [inst_16 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              P'.cotangentComplex ∘ₗ
            Cotangent.map f :
          (a : P.Cotangent) → P'.CotangentSpace)
        x :
      P'.CotangentSpace)

Tactic:
map_cotangentComplex f x

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.Extension.CotangentSpace.map_cotangentComplex