-- 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
b : B
x : TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]
zero :
  (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])
      (HSMul.hSMul (α := B) 0 x) =
    HSMul.hSMul (α := B) (β := Ω[B⁄S]) 0
      ((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])
          x :
        Ω[B⁄S])
smul :
  ∀ (s : S) (b : B)
    (e :
      (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])
          (b • x) =
        HSMul.hSMul (β := Ω[B⁄S]) b
          ((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])
              x :
            Ω[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])
        ((s • b) • x) =
      HSMul.hSMul (β := Ω[B⁄S]) (s • b)
        ((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])
            x :
          Ω[B⁄S])
add :
  ∀ (b₁ b₂ : B)
    (e₁ :
      (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])
          (b₁ • x) =
        HSMul.hSMul (β := Ω[B⁄S]) b₁
          ((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])
              x :
            Ω[B⁄S]))
    (e₂ :
      (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])
          (b₂ • x) =
        HSMul.hSMul (β := Ω[B⁄S]) b₂
          ((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])
              x :
            Ω[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])
        ((b₁ + b₂) • x) =
      HSMul.hSMul (β := Ω[B⁄S]) (b₁ + b₂)
        ((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])
            x :
          Ω[B⁄S])
tmul :
  ∀ (a : A),
    (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])
        (HSMul.hSMul (α := B) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → B) a : B) x) =
      HSMul.hSMul (α := B) (β := Ω[B⁄S]) ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A B) : (a : A) → B) a : B)
        ((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])
            x :
          Ω[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])
      (b • x) =
    HSMul.hSMul (β := Ω[B⁄S]) b
      ((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])
          x :
        Ω[B⁄S])

Tactic:
induction b using h.1.inductionOn with
  | zero => simp only [zero_smul, map_zero]
  | smul s b e => rw [smul_assoc, map_smul, e, smul_assoc]
  | add b₁ b₂ e₁ e₂ => simp only [map_add, e₁, e₂, add_smul]
  | tmul a =>
    induction x
    · simp only [smul_zero, map_zero]
    · simp [smul_comm]
    · simp only [map_add, smul_add, *]

Premises used: smul_assoc, smul_zero, map_zero, map_add, zero_smul, add_smul, TensorProduct.tmul, SMulCommClass.smul_comm, smul_add, map_smul