awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
p : Submonoid R
inst_11 : IsLocalization p S
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid A p) B
⊢ IsLocalizedModule (M := Ω[A⁄R]) (M' := Ω[B⁄S]) p
    ((↑R :
        {S M : Type u_3} →
          {M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_13 : Semiring S] →
                [inst_14 : AddCommMonoid M] →
                  [inst_15 : AddCommMonoid M₂] →
                    [inst_16 : Module R M] →
                      [inst_17 : Module R M₂] →
                        [inst_18 : Module S M] →
                          [inst_19 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (map R S A B))

Tactic:
have := (Algebra.isPushout_of_isLocalization p S A B).symm
  (isLocalizedModule_iff_isBaseChange p S _).mpr (isBaseChange R S A B)

Premises used: Iff.mpr, LinearMap.restrictScalars, Algebra.isPushout_of_isLocalization, isLocalizedModule_iff_isBaseChange, KaehlerDifferential.isBaseChange, Algebra.IsPushout.symm, KaehlerDifferential.map
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
p : Submonoid R
inst_11 : IsLocalization p S
inst_12 : IsLocalizedModule p (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B))
⊢ IsLocalizedModule (M := Ω[A⁄R]) (M' := Ω[B⁄S]) p
    ((↑R :
        {S M : Type u_3} →
          {M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_13 : Semiring S] →
                [inst_14 : AddCommMonoid M] →
                  [inst_15 : AddCommMonoid M₂] →
                    [inst_16 : Module R M] →
                      [inst_17 : Module R M₂] →
                        [inst_18 : Module S M] →
                          [inst_19 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (map R S A B))

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid A p) B :=
    isLocalizedModule_iff_isLocalization.mp inferInstance
  inferInstance

Premises used: inferInstance, isLocalizedModule_iff_isLocalization, Iff.mp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
⊢ Algebra.IsPushout R A S B

Tactic:
have : Algebra.IsPushout R A S B := .symm inferInstance
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
refine :
  ∀ (m : B) (x : B ⊗[A] Ω[A⁄R]),
    (↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun (m • x) =
      HSMul.hSMul (α := B) ((RingHom.id B : (a : B) → B) m : B) ((↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun x)
⊢ B ⊗[A] Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]

Tactic:
refine { __ := e₂, map_smul' := ?_ }
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
m : B
x : B ⊗[A] Ω[A⁄R]
obtain :
  ∀ (m : A ⊗[R] S),
    (↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun
        (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) x) =
      HSMul.hSMul (α := B)
        ((RingHom.id B : (a : B) → B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) : B)
        ((↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun x)
⊢ (↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun (m • x) =
    HSMul.hSMul (α := B) ((RingHom.id B : (a : B) → B) m : B) ((↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun x)

Tactic:
obtain ⟨m, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective m

Premises used: Algebra.IsPushout.equiv, AlgEquiv.surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
x : B ⊗[A] Ω[A⁄R]
m : A ⊗[R] S
dsimp :
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) x) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x : Ω[B⁄S])
⊢ (↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) x) =
    HSMul.hSMul (α := B)
      ((RingHom.id B : (a : B) → B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) m : B) : B)
      ((↑e₂ : B ⊗[A] Ω[A⁄R] →ₗ[R] Ω[B⁄S]).toFun x)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
x : B ⊗[A] Ω[A⁄R]
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 : B) x) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x : Ω[B⁄S])

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
x_1 : B ⊗[A] Ω[A⁄R]
x y : A ⊗[R] S
h_1 :
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x : B) x_1) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x_1 : Ω[B⁄S])
h_2 :
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) y : B) x_1) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) y : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x_1 : Ω[B⁄S])
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x + y) : B) x_1) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x + y) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x_1 : Ω[B⁄S])

Tactic:
simp only [add_smul, map_add, *]

Premises used: map_add, add_smul
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) 0) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
x y : B ⊗[A] Ω[A⁄R]
h_1 :
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) x) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) x : Ω[B⁄S])
h_2 :
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) y) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) y : Ω[B⁄S])
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) (x + y)) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) (x + y) : Ω[B⁄S])

Tactic:
simp only [smul_add, map_add, *]

Premises used: map_add, smul_add
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
x : B
y : Ω[A⁄R]
tmul :
  ∀ (x : A ⊗[R] S),
    (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
        (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
          ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
          ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x ⊗ₜ[A] y : B ⊗[A] Ω[A⁄R])) =
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x ⊗ₜ[A] y) :
          Ω[B⁄S])
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B) (x ⊗ₜ[A] y)) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) (x ⊗ₜ[A] y) : Ω[B⁄S])

Tactic:
obtain ⟨x, rfl⟩ := (Algebra.IsPushout.equiv R A S B).surjective x

Premises used: Algebra.IsPushout.equiv, AlgEquiv.surjective, rfl
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y : Ω[A⁄R]
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 ⊗ₜ[A] y : B ⊗[A] Ω[A⁄R])) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) 0 ⊗ₜ[A] y) : Ω[B⁄S])

Tactic:
simp
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y_1 : Ω[A⁄R]
x y : A ⊗[R] S
h_1 :
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x ⊗ₜ[A] y_1 : B ⊗[A] Ω[A⁄R])) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) x ⊗ₜ[A] y_1) :
        Ω[B⁄S])
h_2 :
  (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) y ⊗ₜ[A] y_1 : B ⊗[A] Ω[A⁄R])) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) y ⊗ₜ[A] y_1) :
        Ω[B⁄S])
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x + y) ⊗ₜ[A] y_1 : B ⊗[A] Ω[A⁄R])) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x + y) ⊗ₜ[A] y_1) :
        Ω[B⁄S])

Tactic:
simp only [smul_add, map_add, *, add_tmul]

Premises used: map_add, TensorProduct.add_tmul, smul_add
-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this_1 : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] TensorProduct.{u_1, u_3, u_2} R Ω[A⁄R] S :=
  (AlgebraTensorModule.congr (↑(AlgEquiv.symm (Algebra.IsPushout.equiv R A S B)) : B ≃ₗ[A] A ⊗[R] S)
          (LinearEquiv.refl A Ω[A⁄R]) :
        B ⊗[A] Ω[A⁄R] ≃ₗ[A] A ⊗[R] S ⊗[A] Ω[A⁄R]) ≪≫ₗ
      (TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] : A ⊗[R] S ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[A] (A ⊗[R] S)) ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y : Ω[A⁄R]
x : A
z : S
this :
  b •
      z •
        a •
          HSMul.hSMul (β := Ω[B⁄S]) x
            (((map R S A B : LinearMap.{u_3, u_3, u_3, u_4} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S]) y :
              Ω[B⁄S]) =
    HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap S B : (a : S) → B) b : B) •
      z •
        HSMul.hSMul (β := Ω[B⁄S]) x
          (((map R S A B : LinearMap.{u_3, u_3, u_3, u_4} (RingHom.id A) Ω[A⁄R] Ω[B⁄S]) : (a : Ω[A⁄R]) → Ω[B⁄S]) y :
            Ω[B⁄S])
⊢ (e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
      (HSMul.hSMul (α := B) (β := B ⊗[A] Ω[A⁄R])
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
        ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x ⊗ₜ[R] z) ⊗ₜ[A] y : B ⊗[A] Ω[A⁄R])) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (a ⊗ₜ[R] b) : B)
      ((e₂ : (a : B ⊗[A] Ω[A⁄R]) → Ω[B⁄S])
          ((Algebra.IsPushout.equiv R A S B : (a : A ⊗[R] S) → B) (x ⊗ₜ[R] z) ⊗ₜ[A] y) :
        Ω[B⁄S])

Tactic:
simpa [e₂, e₁, smul_tmul', Algebra.IsPushout.equiv_tmul, ← mul_smul,
      Algebra.IsPushout.equiv_symm_algebraMap_left, Algebra.IsPushout.equiv_symm_algebraMap_right]

Premises used: Algebra.IsPushout.equiv_symm_algebraMap_left, Algebra.IsPushout.equiv_tmul, TensorProduct.smul_tmul', Algebra.IsPushout.equiv_symm_algebraMap_right, SemigroupAction.mul_smul