-- 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
y : A ⊗[R] A
H :
  Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    ((((↑R :
                {S : Type u_2} →
                  {M M₂ : Type (max u_2 u_3)} →
                    [inst : Semiring R] →
                      [inst_12 : Semiring S] →
                        [inst_13 : AddCommMonoid M] →
                          [inst_14 : AddCommMonoid M₂] →
                            [inst_15 : Module R M] →
                              [inst_16 : Module R M₂] →
                                [inst_17 : Module S M] →
                                  [inst_18 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              ((↑S :
                    {S_1 M : Type u_4} →
                      {M₂ : Type (max u_2 u_3)} →
                        [inst : Semiring S] →
                          [inst_12 : Semiring S_1] →
                            [inst_13 : AddCommMonoid M] →
                              [inst_14 : AddCommMonoid M₂] →
                                [inst_15 : Module S M] →
                                  [inst_16 : Module S M₂] →
                                    [inst_17 : Module S_1 M] →
                                      [inst_18 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  (Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                    (derivationTensorProduct R S A B)) ∘ₗ
                LinearMap.liftBaseChange S
                  ((↑R :
                      {S M : Type u_3} →
                        {M₂ : Type u_4} →
                          [inst : Semiring R] →
                            [inst_12 : Semiring S] →
                              [inst_13 : AddCommMonoid M] →
                                [inst_14 : AddCommMonoid M₂] →
                                  [inst_15 : Module R M] →
                                    [inst_16 : Module R M₂] →
                                      [inst_17 : Module S M] →
                                        [inst_18 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (map R S A B))) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
          (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
        (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) 0) :
      TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    (((↑R :
              {S : Type u_2} →
                {M M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring R] →
                    [inst_12 : Semiring S] →
                      [inst_13 : AddCommMonoid M] →
                        [inst_14 : AddCommMonoid M₂] →
                          [inst_15 : Module R M] →
                            [inst_16 : Module R M₂] →
                              [inst_17 : Module S M] →
                                [inst_18 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) LinearMap.id :
          (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
        (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) 0) :
      TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
H₁ :
  ∀ (x_1 y : A),
    Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      ((((↑R :
                  {S : Type u_2} →
                    {M M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring R] →
                        [inst_12 : Semiring S] →
                          [inst_13 : AddCommMonoid M] →
                            [inst_14 : AddCommMonoid M₂] →
                              [inst_15 : Module R M] →
                                [inst_16 : Module R M₂] →
                                  [inst_17 : Module S M] →
                                    [inst_18 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                ((↑S :
                      {S_1 M : Type u_4} →
                        {M₂ : Type (max u_2 u_3)} →
                          [inst : Semiring S] →
                            [inst_12 : Semiring S_1] →
                              [inst_13 : AddCommMonoid M] →
                                [inst_14 : AddCommMonoid M₂] →
                                  [inst_15 : Module S M] →
                                    [inst_16 : Module S M₂] →
                                      [inst_17 : Module S_1 M] →
                                        [inst_18 : Module S_1 M₂] →
                                          [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                    (Derivation.liftKaehlerDifferential (R := S) (S := B) (M :=
                      TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (derivationTensorProduct R S A B)) ∘ₗ
                  LinearMap.liftBaseChange S
                    ((↑R :
                        {S M : Type u_3} →
                          {M₂ : Type u_4} →
                            [inst : Semiring R] →
                              [inst_12 : Semiring S] →
                                [inst_13 : AddCommMonoid M] →
                                  [inst_14 : AddCommMonoid M₂] →
                                    [inst_15 : Module R M] →
                                      [inst_16 : Module R M₂] →
                                        [inst_17 : Module S M] →
                                          [inst_18 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      (map R S A B))) :
              TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
            (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
          (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) (x_1 ⊗ₜ[R] y)) :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
      (((↑R :
                {S : Type u_2} →
                  {M M₂ : Type (max u_2 u_3)} →
                    [inst : Semiring R] →
                      [inst_12 : Semiring S] →
                        [inst_13 : AddCommMonoid M] →
                          [inst_14 : AddCommMonoid M₂] →
                            [inst_15 : Module R M] →
                              [inst_16 : Module R M₂] →
                                [inst_17 : Module S M] →
                                  [inst_18 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (S := S) LinearMap.id :
            (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
          (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) (x_1 ⊗ₜ[R] y)) :
        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
H₂ :
  ∀ (x_1 y : A ⊗[R] A),
    Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
        ((((↑R :
                    {S : Type u_2} →
                      {M M₂ : Type (max u_2 u_3)} →
                        [inst : Semiring R] →
                          [inst_12 : Semiring S] →
                            [inst_13 : AddCommMonoid M] →
                              [inst_14 : AddCommMonoid M₂] →
                                [inst_15 : Module R M] →
                                  [inst_16 : Module R M₂] →
                                    [inst_17 : Module S M] →
                                      [inst_18 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  ((↑S :
                        {S_1 M : Type u_4} →
                          {M₂ : Type (max u_2 u_3)} →
                            [inst : Semiring S] →
                              [inst_12 : Semiring S_1] →
                                [inst_13 : AddCommMonoid M] →
                                  [inst_14 : AddCommMonoid M₂] →
                                    [inst_15 : Module S M] →
                                      [inst_16 : Module S M₂] →
                                        [inst_17 : Module S_1 M] →
                                          [inst_18 : Module S_1 M₂] →
                                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                      (Derivation.liftKaehlerDifferential (R := S) (S := B) (M :=
                        TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (derivationTensorProduct R S A B)) ∘ₗ
                    LinearMap.liftBaseChange S
                      ((↑R :
                          {S M : Type u_3} →
                            {M₂ : Type u_4} →
                              [inst : Semiring R] →
                                [inst_12 : Semiring S] →
                                  [inst_13 : AddCommMonoid M] →
                                    [inst_14 : AddCommMonoid M₂] →
                                      [inst_15 : Module R M] →
                                        [inst_16 : Module R M₂] →
                                          [inst_17 : Module S M] →
                                            [inst_18 : Module S M₂] →
                                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        (map R S A B))) :
                TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
              (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
            (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) x_1) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
        (((↑R :
                  {S : Type u_2} →
                    {M M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring R] →
                        [inst_12 : Semiring S] →
                          [inst_13 : AddCommMonoid M] →
                            [inst_14 : AddCommMonoid M₂] →
                              [inst_15 : Module R M] →
                                [inst_16 : Module R M₂] →
                                  [inst_17 : Module S M] →
                                    [inst_18 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (S := S) LinearMap.id :
              (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
            (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) x_1) :
          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) →
      Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
          ((((↑R :
                      {S : Type u_2} →
                        {M M₂ : Type (max u_2 u_3)} →
                          [inst : Semiring R] →
                            [inst_12 : Semiring S] →
                              [inst_13 : AddCommMonoid M] →
                                [inst_14 : AddCommMonoid M₂] →
                                  [inst_15 : Module R M] →
                                    [inst_16 : Module R M₂] →
                                      [inst_17 : Module S M] →
                                        [inst_18 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    ((↑S :
                          {S_1 M : Type u_4} →
                            {M₂ : Type (max u_2 u_3)} →
                              [inst : Semiring S] →
                                [inst_12 : Semiring S_1] →
                                  [inst_13 : AddCommMonoid M] →
                                    [inst_14 : AddCommMonoid M₂] →
                                      [inst_15 : Module S M] →
                                        [inst_16 : Module S M₂] →
                                          [inst_17 : Module S_1 M] →
                                            [inst_18 : Module S_1 M₂] →
                                              [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                        (Derivation.liftKaehlerDifferential (R := S) (S := B) (M :=
                          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (derivationTensorProduct R S A B)) ∘ₗ
                      LinearMap.liftBaseChange S
                        ((↑R :
                            {S M : Type u_3} →
                              {M₂ : Type u_4} →
                                [inst : Semiring R] →
                                  [inst_12 : Semiring S] →
                                    [inst_13 : AddCommMonoid M] →
                                      [inst_14 : AddCommMonoid M₂] →
                                        [inst_15 : Module R M] →
                                          [inst_16 : Module R M₂] →
                                            [inst_17 : Module S M] →
                                              [inst_18 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          (map R S A B))) :
                  TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
                (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
              (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) y) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
          (((↑R :
                    {S : Type u_2} →
                      {M M₂ : Type (max u_2 u_3)} →
                        [inst : Semiring R] →
                          [inst_12 : Semiring S] →
                            [inst_13 : AddCommMonoid M] →
                              [inst_14 : AddCommMonoid M₂] →
                                [inst_15 : Module R M] →
                                  [inst_16 : Module R M₂] →
                                    [inst_17 : Module S M] →
                                      [inst_18 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (S := S) LinearMap.id :
                (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
              (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) y) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) →
        Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
          ((((↑R :
                      {S : Type u_2} →
                        {M M₂ : Type (max u_2 u_3)} →
                          [inst : Semiring R] →
                            [inst_12 : Semiring S] →
                              [inst_13 : AddCommMonoid M] →
                                [inst_14 : AddCommMonoid M₂] →
                                  [inst_15 : Module R M] →
                                    [inst_16 : Module R M₂] →
                                      [inst_17 : Module S M] →
                                        [inst_18 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    ((↑S :
                          {S_1 M : Type u_4} →
                            {M₂ : Type (max u_2 u_3)} →
                              [inst : Semiring S] →
                                [inst_12 : Semiring S_1] →
                                  [inst_13 : AddCommMonoid M] →
                                    [inst_14 : AddCommMonoid M₂] →
                                      [inst_15 : Module S M] →
                                        [inst_16 : Module S M₂] →
                                          [inst_17 : Module S_1 M] →
                                            [inst_18 : Module S_1 M₂] →
                                              [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                        (Derivation.liftKaehlerDifferential (R := S) (S := B) (M :=
                          TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) (derivationTensorProduct R S A B)) ∘ₗ
                      LinearMap.liftBaseChange S
                        ((↑R :
                            {S M : Type u_3} →
                              {M₂ : Type u_4} →
                                [inst : Semiring R] →
                                  [inst_12 : Semiring S] →
                                    [inst_13 : AddCommMonoid M] →
                                      [inst_14 : AddCommMonoid M₂] →
                                        [inst_15 : Module R M] →
                                          [inst_16 : Module R M₂] →
                                            [inst_17 : Module S M] →
                                              [inst_18 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          (map R S A B))) :
                  TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
                (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
              (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) (x_1 + y)) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
          (((↑R :
                    {S : Type u_2} →
                      {M M₂ : Type (max u_2 u_3)} →
                        [inst : Semiring R] →
                          [inst_12 : Semiring S] →
                            [inst_13 : AddCommMonoid M] →
                              [inst_14 : AddCommMonoid M₂] →
                                [inst_15 : Module R M] →
                                  [inst_16 : Module R M₂] →
                                    [inst_17 : Module S M] →
                                      [inst_18 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (S := S) LinearMap.id :
                (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
              (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) (x_1 + y)) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    ((((↑R :
                {S : Type u_2} →
                  {M M₂ : Type (max u_2 u_3)} →
                    [inst : Semiring R] →
                      [inst_12 : Semiring S] →
                        [inst_13 : AddCommMonoid M] →
                          [inst_14 : AddCommMonoid M₂] →
                            [inst_15 : Module R M] →
                              [inst_16 : Module R M₂] →
                                [inst_17 : Module S M] →
                                  [inst_18 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              ((↑S :
                    {S_1 M : Type u_4} →
                      {M₂ : Type (max u_2 u_3)} →
                        [inst : Semiring S] →
                          [inst_12 : Semiring S_1] →
                            [inst_13 : AddCommMonoid M] →
                              [inst_14 : AddCommMonoid M₂] →
                                [inst_15 : Module S M] →
                                  [inst_16 : Module S M₂] →
                                    [inst_17 : Module S_1 M] →
                                      [inst_18 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  (Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                    (derivationTensorProduct R S A B)) ∘ₗ
                LinearMap.liftBaseChange S
                  ((↑R :
                      {S M : Type u_3} →
                        {M₂ : Type u_4} →
                          [inst : Semiring R] →
                            [inst_12 : Semiring S] →
                              [inst_13 : AddCommMonoid M] →
                                [inst_14 : AddCommMonoid M₂] →
                                  [inst_15 : Module R M] →
                                    [inst_16 : Module R M₂] →
                                      [inst_17 : Module S M] →
                                        [inst_18 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (map R S A B))) :
            TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R] →ₗ[R] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
          (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
        (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) y) :
      TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
    (((↑R :
              {S : Type u_2} →
                {M M₂ : Type (max u_2 u_3)} →
                  [inst : Semiring R] →
                    [inst_12 : Semiring S] →
                      [inst_13 : AddCommMonoid M] →
                        [inst_14 : AddCommMonoid M₂] →
                          [inst_15 : Module R M] →
                            [inst_16 : Module R M₂] →
                              [inst_17 : Module S M] →
                                [inst_18 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S) LinearMap.id :
          (a : S ⊗[R] Ω[A⁄R]) → S ⊗[R] Ω[A⁄R])
        (x ⊗ₜ[R] (Derivation.tensorProductTo (D R A) : (a : A ⊗[R] A) → Ω[A⁄R]) y) :
      TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])

Tactic:
induction y