Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.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
h : Algebra.IsPushout R S A B
x : B
m✝ : A
⊢ x •
      (LinearMap.liftBaseChange S (↑R (map R S A B)))
        ((derivationTensorProduct R S A B) ((IsScalarTower.toAlgHom R A B).toLinearMap m✝)) =
    x • (D S B) ((IsScalarTower.toAlgHom R A B).toLinearMap m✝)

pp: case tmul.smul
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
h : Algebra.IsPushout R S A B
x : B
s✝ : S
n✝ : B
a✝ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n✝) = x • (D S B) n✝
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) (s✝ • n✝)) =
    x • (D S B) (s✝ • n✝)

pp: case tmul.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
h : Algebra.IsPushout R S A B
x n₁✝ n₂✝ : B
a✝¹ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₁✝) = x • (D S B) n₁✝
a✝ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₂✝) = x • (D S B) n₂✝
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) (n₁✝ + n₂✝)) =
    x • (D S B) (n₁✝ + n₂✝)

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

Goal state after:
case tmul.smul
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
h : Algebra.IsPushout R S A B
x : B
s✝ : S
n✝ : B
a✝ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n✝) = x • (D S B) n✝
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) (s✝ • n✝)) =
    x • (D S B) (s✝ • n✝)

case tmul.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
h : Algebra.IsPushout R S A B
x n₁✝ n₂✝ : B
a✝¹ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₁✝) = x • (D S B) n₁✝
a✝ : x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) n₂✝) = x • (D S B) n₂✝
⊢ x • (LinearMap.liftBaseChange S (↑R (map R S A B))) ((derivationTensorProduct R S A B) (n₁✝ + n₂✝)) =
    x • (D S B) (n₁✝ + n₂✝)