awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
⊢ Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)
        (t ⊗ₜ[R] (s ⊗ₜ[P.Ring] x)) :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          x :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
have simp : Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
  (((AlgebraTensorModule.congr (LinearEquiv.refl (Ring (R := T) (S := T ⊗[R] S) P.baseChange) (T ⊗[R] S))
            (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange)) :
          T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
              (Ring (R := T) (S := T ⊗[R] S) P.baseChange ⊗[P.Ring]
                Ω[P.Ring⁄R]) ≃ₗ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
            T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T]) :
        (a : T ⊗[R] S ⊗[P.baseChange.Ring] (P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R])) →
          T ⊗[R] S ⊗[P.baseChange.Ring] Ω[P.baseChange.Ring⁄T])
      (((LinearEquiv.symm
              (AlgebraTensorModule.cancelBaseChange P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange)
                (Ring (R := T) (S := T ⊗[R] S) P.baseChange) (T ⊗[R] S) Ω[P.Ring⁄R]) :
            T ⊗[R] S ⊗[P.Ring] Ω[P.Ring⁄R] ≃ₗ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
              T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
                (Ring (R := T) (S := T ⊗[R] S) P.baseChange ⊗[P.Ring] Ω[P.Ring⁄R])) :
          (a : T ⊗[R] S ⊗[P.Ring] Ω[P.Ring⁄R]) →
            T ⊗[R] S ⊗[P.baseChange.Ring] (P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]))
        ((((TensorProduct.mk R T S : (a : T) → S →ₗ[R] T ⊗[R] S) t : S →ₗ[R] T ⊗[R] S) : (a : S) → T ⊗[R] S)
            s ⊗ₜ[P.Ring]
          x)) :
    T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
  (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
      (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
          (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
        x :
    T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
Tactic: simp only [tensorCotangentSpace, LinearEquiv.trans_apply, LinearEquiv.restrictScalars_apply,
    ← mk_apply s x, IsTensorProduct.assocOfMapSMul_symm_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
⊢ Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (((AlgebraTensorModule.congr (LinearEquiv.refl (Ring (R := T) (S := T ⊗[R] S) P.baseChange) (T ⊗[R] S))
              (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange)) :
            T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
                (Ring (R := T) (S := T ⊗[R] S) P.baseChange ⊗[P.Ring]
                  Ω[P.Ring⁄R]) ≃ₗ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
              T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T]) :
          (a : T ⊗[R] S ⊗[P.baseChange.Ring] (P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R])) →
            T ⊗[R] S ⊗[P.baseChange.Ring] Ω[P.baseChange.Ring⁄T])
        (((LinearEquiv.symm
                (AlgebraTensorModule.cancelBaseChange P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange)
                  (Ring (R := T) (S := T ⊗[R] S) P.baseChange) (T ⊗[R] S) Ω[P.Ring⁄R]) :
              T ⊗[R] S ⊗[P.Ring] Ω[P.Ring⁄R] ≃ₗ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
                T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
                  (Ring (R := T) (S := T ⊗[R] S) P.baseChange ⊗[P.Ring] Ω[P.Ring⁄R])) :
            (a : T ⊗[R] S ⊗[P.Ring] Ω[P.Ring⁄R]) →
              T ⊗[R] S ⊗[P.baseChange.Ring] (P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]))
          ((((TensorProduct.mk R T S : (a : T) → S →ₗ[R] T ⊗[R] S) t : S →ₗ[R] T ⊗[R] S) : (a : S) → T ⊗[R] S)
              s ⊗ₜ[P.Ring]
            x)) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          x :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
have simp : Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
  (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
      (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
          (a : P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
        (1 ⊗ₜ[P.Ring] x) :
    T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
  (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
      (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
          (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
        x :
    T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
Tactic: simp only [mk_apply, AlgebraTensorModule.cancelBaseChange_symm_tmul,
    AlgebraTensorModule.congr_tmul, LinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
⊢ Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R])
    (Submodule.span P.Ring (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R]))) x
have rw : Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R]) ⊤ x
Tactic: rw [KaehlerDifferential.span_range_derivation]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
⊢ Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          (1 ⊗ₜ[P.Ring] x) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          x :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
have this : Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R])
  (Submodule.span P.Ring (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R]))) x
Tactic: have this : x ∈ Submodule.span P.Ring (Set.range (KaehlerDifferential.D R P.Ring)) := by
    rw [KaehlerDifferential.span_range_derivation]
    trivial
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
s : S
x y : Ω[P.Ring⁄R]
hy :
  Membership.mem (γ := Set Ω[P.Ring⁄R])
    (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R])) y
⊢ Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          (1 ⊗ₜ[P.Ring] y) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          y :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
have mem : ∀ (y : P.Ring),
  Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) y) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          ((KaehlerDifferential.D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) y) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
Tactic: obtain ⟨y, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
s : S
x : Ω[P.Ring⁄R]
this :
  Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R])
    (Submodule.span P.Ring (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R]))) x
⊢ Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          (1 ⊗ₜ[P.Ring] x) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          x :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
have zero : Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
  (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
      (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
          (a : P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
        (1 ⊗ₜ[P.Ring] 0) :
    T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
  (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
      (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
          (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
        0 :
    T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
Tactic: induction this using Submodule.span_induction with
  | zero => simp
  | add x y _ _ hx hy => simp [tmul_add, hx, hy]
  | mem y hy =>
    obtain ⟨y, rfl⟩ := hy
    simp
  | smul a x _ hx =>
    rw [tmul_smul, ← algebraMap_smul (P.baseChange (T := T)).Ring a, LinearEquiv.map_smul,
      tmul_smul, hx, LinearMap.map_smul, ← algebraMap_smul (P.baseChange (T := T)).Ring a,
      tmul_smul]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] 0) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
have zero : (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) 0 =
  HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
    ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
Tactic: rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
zero :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) 0 =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] 0) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
have zero₁ : 0 =
  HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
    ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
Tactic: rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
zero :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) 0 =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
zero₁ :
  0 =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] 0) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
have zero₂ : 0 = HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t 0
Tactic: rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
zero :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) 0 =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
zero₁ :
  0 =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
zero₂ : 0 = HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t 0
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] 0) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
have zero₃ : Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) 0 0
Tactic: rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
x y : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R]
hx :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
hy :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) y :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] (x + y)) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
have add : (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)
    (HAdd.hAdd (α := T ⊗[R] P.CotangentSpace) (t ⊗ₜ[R] x) (t ⊗ₜ[R] y)) =
  HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
    ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
Tactic: rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
x y : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R]
hx :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
hy :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) y :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
add :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)
      (HAdd.hAdd (α := T ⊗[R] P.CotangentSpace) (t ⊗ₜ[R] x) (t ⊗ₜ[R] y)) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] (x + y)) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
have add₁ : HAdd.hAdd (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) (β :=
    CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) =
  HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
    ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
Tactic: rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
x : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R]
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
have zero : (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] 0) =
  HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
    ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
Tactic: induction x with
  | zero => rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
  | add x y hx hy => rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
  | tmul s y =>
  simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
    smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]
Cleared hypotheses: x