awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 →ₗ[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)
have 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)
Tactic: ext x
-- 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
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 : (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)
have 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)
Tactic: obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: x
-- 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
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.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)
have rw : Eq (α := P'.CotangentSpace)
  ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
      (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (↑x : P.Ring)) :
    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)
Tactic: rw [cotangentComplex_mk, map_tmul, map_one, Cotangent.map_mk, cotangentComplex_mk]
-- 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
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.ker
rw :
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (↑x : P.Ring)) :
      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) ((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)
have rw₁ : Eq (α := P'.CotangentSpace)
  ((algebraMap S S' : (a : S) → S') 1 ⊗ₜ[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) (↑x : P.Ring)) :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
  ((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)
Tactic: rw [cotangentComplex_mk, map_tmul, map_one, Cotangent.map_mk, cotangentComplex_mk]
-- 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
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.ker
rw :
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (↑x : P.Ring)) :
      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)
rw₁ :
  Eq (α := P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') 1 ⊗ₜ[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) (↑x : P.Ring)) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((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) ((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)
have rw₂ : Eq (α := P'.CotangentSpace)
  (1 ⊗ₜ[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) (↑x : P.Ring)) :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
  ((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)
Tactic: rw [cotangentComplex_mk, map_tmul, map_one, Cotangent.map_mk, cotangentComplex_mk]
-- 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
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.ker
rw :
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (↑x : P.Ring)) :
      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)
rw₁ :
  Eq (α := P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') 1 ⊗ₜ[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) (↑x : P.Ring)) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((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)
rw₂ :
  Eq (α := P'.CotangentSpace)
    (1 ⊗ₜ[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) (↑x : P.Ring)) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((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) ((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)
have rw₃ : Eq (α := P'.CotangentSpace)
  (1 ⊗ₜ[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) (↑x : P.Ring)) :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
  ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
      ((Cotangent.mk : (a : ↥P'.ker) → P'.Cotangent)
        (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry)) :
    P'.CotangentSpace)
Tactic: rw [cotangentComplex_mk, map_tmul, map_one, Cotangent.map_mk, cotangentComplex_mk]
-- 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
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'
⊢ 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
have 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)
Tactic: ext x
-- 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
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 g : P.Hom P'
x y : P.Ring
this : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
⊢ HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
      HSub.hSub (α := P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring) ∈
    HPow.hPow (β := ℕ) P'.ker 2
have rw : HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
        (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) *
      HSub.hSub (α := P'.Ring) (β := P'.Ring)
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
        (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
    HSub.hSub (α := P'.Ring) (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
        (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y)) *
      HSub.hSub (α := P'.Ring) (β := P'.Ring)
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
        (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring) ∈
  P'.ker * P'.ker
Tactic: rw [pow_two]
-- 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
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 g : P.Hom P'
x y : P.Ring
this : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
⊢ HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
      HSub.hSub (α := P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring) ∈
    P'.ker * P'.ker
have refine_1 : HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
    (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) ∈
  P'.ker
Tactic: refine Ideal.add_mem _ (Ideal.mul_mem_mul ?_ ?_) (Ideal.mul_mem_mul ?_ ?_)
-- 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
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 g : P.Hom P'
x y : P.Ring
this : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
refine_1 :
  HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
      (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) ∈
    P'.ker
⊢ HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
      HSub.hSub (α := P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring) ∈
    P'.ker * P'.ker
have refine_2 : HSub.hSub (α := P'.Ring) (β := P'.Ring)
    (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
    (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) ∈
  P'.ker
Tactic: refine Ideal.add_mem _ (Ideal.mul_mem_mul ?_ ?_) (Ideal.mul_mem_mul ?_ ?_)
-- 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
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 g : P.Hom P'
x y : P.Ring
this : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
refine_1 :
  HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
      (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) ∈
    P'.ker
refine_2 :
  HSub.hSub (α := P'.Ring) (β := P'.Ring)
      (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
      (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) ∈
    P'.ker
⊢ HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
      HSub.hSub (α := P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring) ∈
    P'.ker * P'.ker
have refine_3 : HSub.hSub (α := P'.Ring) (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
    (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y)) ∈
  P'.ker
Tactic: refine Ideal.add_mem _ (Ideal.mul_mem_mul ?_ ?_) (Ideal.mul_mem_mul ?_ ?_)