Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ ⊗ₜ[R] y✝)) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ ⊗ₜ[R] y✝))

pp: case add
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A ⊗[R] A
a✝¹ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo x✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo x✝)
a✝ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo y✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo y✝)
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝)) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝))

Tactic:
· simp only [LinearMap.restrictScalars_comp, Derivation.tensorProductTo_tmul, LinearMap.coe_comp,
      LinearMap.coe_restrictScalars, Function.comp_apply, LinearMap.liftBaseChange_tmul, map_smul,
      map_D, LinearMap.map_smul_of_tower, Derivation.liftKaehlerDifferential_comp_D,
      LinearMap.id_coe, id_eq, derivationTensorProduct_algebraMap]
    rw [smul_comm, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
    rfl

Goal state after:
case add
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
x : S
x✝ y✝ : A ⊗[R] A
a✝¹ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo x✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo x✝)
a✝ :
  (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo y✝) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo y✝)
⊢ (↑R (↑S (derivationTensorProduct R S A B).liftKaehlerDifferential ∘ₗ LinearMap.liftBaseChange S (↑R (map R S A B))))
      (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝)) =
    (↑R LinearMap.id) (x ⊗ₜ[R] (D R A).tensorProductTo (x✝ + y✝))