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'
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
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
⊢ 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_4 : 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
Tactic: refine Ideal.add_mem _ (Ideal.mul_mem_mul ?_ ?_) (Ideal.mul_mem_mul ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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) (β := P'.Ring)
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (x * y) : P'.Ring)
        (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (x * y) : 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) +
        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 this₁ : 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
Tactic: have :
      (f.toAlgHom x - P'.σ (algebraMap P.Ring S' x)) * (f.toAlgHom y - g.toAlgHom y) +
      (g.toAlgHom y - P'.σ (algebraMap P.Ring S' y)) * (f.toAlgHom x - g.toAlgHom x)
        ∈ P'.ker ^ 2 := by
    rw [pow_two]
    refine Ideal.add_mem _ (Ideal.mul_mem_mul ?_ ?_) (Ideal.mul_mem_mul ?_ ?_) <;>
      simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_comp,
        Function.comp_apply,
        ker, RingHom.mem_ker, map_sub, algebraMap_toRingHom,
        algebraMap_σ, sub_self, toAlgHom_apply]
-- 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 g : P.Hom P'
⊢ LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker
have refine : ∀ (c : P.Ring),
  Membership.mem (α := P'.Ring) (γ := Submodule R P'.Ring) (Submodule.restrictScalars R P'.ker)
    ((HSub.hSub (α := LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Ring) (AlgHom.toLinearMap f.toAlgHom)
            (AlgHom.toLinearMap g.toAlgHom) :
          (a : P.Ring) → P'.Ring)
        c :
      P'.Ring)
Tactic: refine ((f.toAlgHom.toLinearMap - g.toAlgHom.toLinearMap).codRestrict
    (P'.ker.restrictScalars R) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
⊢ P.CotangentSpace →ₗ[S] P'.Cotangent
have this₁ : IsScalarTower.{w, v, v'} P.Ring S S'
Tactic: haveI : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
⊢ P.CotangentSpace →ₗ[S] P'.Cotangent
have this₁ : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
Tactic: haveI : IsScalarTower P.Ring P'.Ring S' :=
    IsScalarTower.of_algebraMap_eq fun x ↦ (f.algebraMap_toRingHom x).symm
-- 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''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
x : R
⊢ Eq.{v' + 1} (α := S') ((algebraMap R S' : (a : R) → S') x : S')
    ((algebraMap S S' : (a : S) → S')
        ((algebraMap P.Ring S : (a : P.Ring) → S) ((algebraMap R P.Ring : (a : R) → P.Ring) x : P.Ring) : S) :
      S')
have rw : Eq.{v' + 1} (α := S') ((algebraMap R S' : (a : R) → S') x : S')
  ((algebraMap S S' : (a : S) → S') ((algebraMap R S : (a : R) → S) x : S) : S')
Tactic: rw [← IsScalarTower.algebraMap_apply R P.Ring S, ← IsScalarTower.algebraMap_apply]
-- 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''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
x : R
rw :
  Eq.{v' + 1} (α := S') ((algebraMap R S' : (a : R) → S') x : S')
    ((algebraMap S S' : (a : S) → S') ((algebraMap R S : (a : R) → S) x : S) : S')
⊢ Eq.{v' + 1} (α := S') ((algebraMap R S' : (a : R) → S') x : S')
    ((algebraMap S S' : (a : S) → S')
        ((algebraMap P.Ring S : (a : P.Ring) → S) ((algebraMap R P.Ring : (a : R) → P.Ring) x : P.Ring) : S) :
      S')
have rw₁ : Eq.{v' + 1} (α := S') ((algebraMap R S' : (a : R) → S') x : S') ((algebraMap R S' : (a : R) → S') x : S')
Tactic: rw [← IsScalarTower.algebraMap_apply R P.Ring S, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
⊢ P.CotangentSpace →ₗ[S] P'.Cotangent
have this₁ : IsScalarTower.{u, w, v'} R P.Ring S'
Tactic: haveI : IsScalarTower R P.Ring S' :=
    IsScalarTower.of_algebraMap_eq fun x ↦
      show algebraMap R S' x = algebraMap S S' (algebraMap P.Ring S (algebraMap R P.Ring x)) by
        rw [← IsScalarTower.algebraMap_apply R P.Ring S, ← IsScalarTower.algebraMap_apply]
-- 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''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this_4 : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
this : IsScalarTower.{u, w, v'} R P.Ring S'
⊢ P.CotangentSpace →ₗ[S] P'.Cotangent
have refine : Derivation.{u, w, w'} R P.Ring P'.Cotangent
Tactic: refine (Derivation.liftKaehlerDifferential ?_).liftBaseChange S
-- 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''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this_4 : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
this : IsScalarTower.{u, w, v'} R P.Ring S'
⊢ Derivation.{u, w, w'} R P.Ring P'.Cotangent
have refine_1 : Eq.{w' + 1} (α := P'.Cotangent)
  ((((↑R :
              {S M M₂ : Type w'} →
                [inst : Semiring R] →
                  [inst_24 : Semiring S] →
                    [inst_25 : AddCommMonoid M] →
                      [inst_26 : AddCommMonoid M₂] →
                        [inst_27 : Module R M] →
                          [inst_28 : Module R M₂] →
                            [inst_29 : Module S M] →
                              [inst_30 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            Cotangent.mk ∘ₗ
          f.subToKer g :
        LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
      (a : P.Ring) → P'.Cotangent)
    1)
  0
Tactic: refine
  { __ := Cotangent.mk.restrictScalars R ∘ₗ f.subToKer g
    map_one_eq_zero' := ?_
    leibniz' := ?_ }
-- 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'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
⊢ CotangentSpace.map f - CotangentSpace.map g =
    (↑S :
          {S_1 : Type v'} →
            {M : Type w'} →
              {M₂ : Type (max v' w')} →
                [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₂)
        P'.cotangentComplex ∘ₗ
      f.sub g
have h : ∀ (x : P.CotangentSpace),
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) x : P'.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [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₂)
              P'.cotangentComplex ∘ₗ
            f.sub g :
          (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'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : S
y : Ω[P.Ring⁄R]
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) (x ⊗ₜ[P.Ring] y) :
      P'.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [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₂)
              P'.cotangentComplex ∘ₗ
            f.sub g :
          (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] y) :
      P'.CotangentSpace)
have h : ∀ (y : P.Ring ⊗[R] P.Ring),
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) y) :
      P'.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [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₂)
              P'.cotangentComplex ∘ₗ
            f.sub g :
          (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) y) :
      P'.CotangentSpace)
Tactic: obtain ⟨y, rfl⟩ := KaehlerDifferential.tensorProductTo_surjective _ _ y
Cleared hypotheses: y
-- 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'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
⊢ map f - map g = f.sub g ∘ₗ P.cotangentComplex
have h : ∀ (x : P.Cotangent),
  Eq.{w' + 1} (α := P'.ker.Cotangent) (val ((map f - map g : (a : P.Cotangent) → P'.Cotangent) x))
    (val ((f.sub g ∘ₗ P.cotangentComplex : (a : P.Cotangent) → P'.Cotangent) x))
Tactic: ext x