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
inst_11 : Algebra.IsPushout R S A B
x : S
x_1 y : A
H :
  HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x_1
      (x ⊗ₜ[R] (D R A : (a : A) → Ω[A⁄R]) y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    x ⊗ₜ[R] HSMul.hSMul (β := Ω[A⁄R]) x_1 ((D R A : (a : A) → Ω[A⁄R]) y : Ω[A⁄R])
⊢ x •
      HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x_1
        (1 ⊗ₜ[R] (D R A : (a : A) → Ω[A⁄R]) y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    x ⊗ₜ[R] HSMul.hSMul (β := Ω[A⁄R]) x_1 ((D R A : (a : A) → Ω[A⁄R]) y : Ω[A⁄R])

Tactic:
rw [smul_comm, TensorProduct.smul_tmul', smul_eq_mul, mul_one]

Premises used: TensorProduct.smul_tmul', smul_eq_mul, SMulCommClass.smul_comm, mul_one
-- 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
inst_11 : Algebra.IsPushout R S A B
x : S
x_1 y : A
⊢ HSMul.hSMul (β := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) x_1
      (x ⊗ₜ[R] (D R A : (a : A) → Ω[A⁄R]) y : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) =
    x ⊗ₜ[R] HSMul.hSMul (β := Ω[A⁄R]) x_1 ((D R A : (a : A) → Ω[A⁄R]) y : Ω[A⁄R])

Tactic:
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
x : Ω[B⁄S]
obtain :
  ∀ (x : B ⊗[S] B),
    Eq (α := Ω[B⁄S])
      (AddHom.toFun (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
        (LinearMap.toAddHom
          (LinearMap.liftBaseChange S
            ((↑R :
                {S M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (map R S A B))))
        (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                (derivationTensorProduct R S A B) :
              Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
            (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
          ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) x)))
      ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) x)
⊢ AddHom.toFun (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      (LinearMap.toAddHom
        (LinearMap.liftBaseChange S
          ((↑R :
              {S M : Type u_3} →
                {M₂ : Type u_4} →
                  [inst : Semiring R] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module R M] →
                            [inst_15 : Module R M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (map R S A B))))
      (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
              (derivationTensorProduct R S A B) :
            Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
          (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
        x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := tensorProductTo_surjective _ _ x

Premises used: KaehlerDifferential.tensorProductTo_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
⊢ Eq (α := Ω[B⁄S])
    ((LinearMap.liftBaseChange S
            ((↑R :
                {S M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (map R S A B)) :
          (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
        (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                (derivationTensorProduct R S A B) :
              Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
            (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
          ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) 0)) :
      Ω[B⁄S])
    ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) 0 : Ω[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
x y : B
tmul :
  HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
              ((↑R :
                  {S M : Type u_3} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (map R S A B)) :
            (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
          ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) y) :
        Ω[B⁄S]) =
    HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) y : Ω[B⁄S])
⊢ Eq.{u_4 + 1} (α := Ω[B⁄S])
    ((LinearMap.liftBaseChange S
            ((↑R :
                {S M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (map R S A B)) :
          (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
        (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                (derivationTensorProduct R S A B) :
              Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
            (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
          ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) (x ⊗ₜ[S] y))) :
      Ω[B⁄S])
    ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) (x ⊗ₜ[S] y) : Ω[B⁄S])

Tactic:
simp only [Derivation.tensorProductTo_tmul, LinearMap.map_smul,
        Derivation.liftKaehlerDifferential_comp_D, map_liftBaseChange_smul]

Premises used: Derivation.liftKaehlerDifferential_comp_D, LinearMap.map_smul, Derivation.tensorProductTo_tmul, KaehlerDifferential.map_liftBaseChange_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
x : B
⊢ HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
            ((↑R :
                {S M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (map R S A B)) :
          (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
        ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) 0)) =
    HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) 0 : Ω[B⁄S])

Tactic:
simp only [map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- 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
x : B
m : A
⊢ HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
              ((↑R :
                  {S M : Type u_3} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (map R S A B)) :
            (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
          ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R])
            ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → B) m)) :
        Ω[B⁄S]) =
    HSMul.hSMul (β := Ω[B⁄S]) x
      ((D S B : (a : B) → Ω[B⁄S]) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → B) m : B) : Ω[B⁄S])

Tactic:
simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom',
          derivationTensorProduct_algebraMap, LinearMap.liftBaseChange_tmul,
          LinearMap.coe_restrictScalars, map_D, one_smul]

Premises used: IsScalarTower.coe_toAlgHom', LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply, one_smul, LinearMap.liftBaseChange_tmul, KaehlerDifferential.derivationTensorProduct_algebraMap, KaehlerDifferential.map_D
-- 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
x : B
s : S
n : B
h_1 :
  HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
              ((↑R :
                  {S M : Type u_3} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (map R S A B)) :
            (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
          ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) n) :
        Ω[B⁄S]) =
    HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) n : Ω[B⁄S])
⊢ HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
              ((↑R :
                  {S M : Type u_3} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (map R S A B)) :
            (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
          ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) (s • n)) :
        Ω[B⁄S]) =
    HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) (s • n) : Ω[B⁄S])

Tactic:
simp only [Derivation.map_smul, LinearMap.map_smul, *, smul_comm x]

Premises used: LinearMap.map_smul, Derivation.map_smul, SMulCommClass.smul_comm
-- 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
inst_11 : Algebra.IsPushout R S A B
a : S
b : Ω[A⁄R]
⊢ (tensorKaehlerEquivBase R S A B : (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S]) (a ⊗ₜ[R] b) =
    HSMul.hSMul (β := Ω[B⁄S]) a
      (((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]) b : Ω[B⁄S])

Tactic:
LinearMap.liftBaseChange_tmul _ _ _ _

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.liftBaseChange_tmul
-- 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
⊢ IsBaseChange.{u_3, u_4, u_2, u_1} (M := Ω[A⁄R]) (N := Ω[B⁄S]) S
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑(tensorKaehlerEquivBase R S A B) : S ⊗[R] Ω[A⁄R] →ₗ[S] Ω[B⁄S]) ∘ₗ
      (mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1)

Tactic:
(TensorProduct.isBaseChange R Ω[A⁄R] S).comp
      (IsBaseChange.ofEquiv (tensorKaehlerEquivBase R S A B))

Premises used: KaehlerDifferential.tensorKaehlerEquivBase, TensorProduct.isBaseChange, IsBaseChange.ofEquiv, KaehlerDifferential, IsBaseChange.comp
-- 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
h₁ :
  Eq (α := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) Ω[A⁄R] Ω[B⁄S])
    ((↑R :
        {S M : Type u_3} →
          {M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_11 : Semiring S] →
                [inst_12 : AddCommMonoid M] →
                  [inst_13 : AddCommMonoid M₂] →
                    [inst_14 : Module R M] →
                      [inst_15 : Module R M₂] →
                        [inst_16 : Module S M] →
                          [inst_17 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (map R S A B))
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑(tensorKaehlerEquivBase R S A B) : S ⊗[R] Ω[A⁄R] →ₗ[S] Ω[B⁄S]) ∘ₗ
      (mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1)
⊢ IsBaseChange (M := Ω[A⁄R]) (N := Ω[B⁄S]) S
    ((↑R :
        {S M : Type u_3} →
          {M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_11 : Semiring S] →
                [inst_12 : AddCommMonoid M] →
                  [inst_13 : AddCommMonoid M₂] →
                    [inst_14 : Module R M] →
                      [inst_15 : Module R M₂] →
                        [inst_16 : Module S M] →
                          [inst_17 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (map R S A B))

Tactic:
convert!
    (TensorProduct.isBaseChange R Ω[A⁄R] S).comp
      (IsBaseChange.ofEquiv (tensorKaehlerEquivBase R S A B))

Premises used: KaehlerDifferential.tensorKaehlerEquivBase, TensorProduct.isBaseChange, IsBaseChange.ofEquiv, KaehlerDifferential, IsBaseChange.comp
-- 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
⊢ Eq (α := LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) Ω[A⁄R] Ω[B⁄S])
    ((↑R :
        {S M : Type u_3} →
          {M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_11 : Semiring S] →
                [inst_12 : AddCommMonoid M] →
                  [inst_13 : AddCommMonoid M₂] →
                    [inst_14 : Module R M] →
                      [inst_15 : Module R M₂] →
                        [inst_16 : Module S M] →
                          [inst_17 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (map R S A B))
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑(tensorKaehlerEquivBase R S A B) : S ⊗[R] Ω[A⁄R] →ₗ[S] Ω[B⁄S]) ∘ₗ
      (mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1)

Tactic:
LinearMap.ext fun x ↦ ?_

Premises used: LinearMap.ext
-- 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
x : Ω[A⁄R]
⊢ Eq.{u_4 + 1} (α := Ω[B⁄S])
    ((((↑R :
                {S M : Type u_3} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (map R S A B) :
            LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) Ω[A⁄R] Ω[B⁄S]) :
          (a : Ω[A⁄R]) → Ω[B⁄S])
        x :
      Ω[B⁄S])
    (((↑R :
                {S : Type u_2} →
                  {M : Type (max u_2 u_3)} →
                    {M₂ : Type u_4} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (↑(tensorKaehlerEquivBase R S A B) : S ⊗[R] Ω[A⁄R] →ₗ[S] Ω[B⁄S]) ∘ₗ
            (mk R S Ω[A⁄R] : (a : S) → Ω[A⁄R] →ₗ[R] S ⊗[R] Ω[A⁄R]) 1 :
          (a : Ω[A⁄R]) → Ω[B⁄S])
        x :
      Ω[B⁄S])

Tactic:
simp only [LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe,
    Function.comp_apply, mk_apply, tensorKaehlerEquivBase_tmul, one_smul]

Premises used: TensorProduct.mk_apply, LinearMap.coe_restrictScalars, KaehlerDifferential.tensorKaehlerEquivBase_tmul, one_smul, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe