Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.zero
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
a : A
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • 0) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) 0

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
a : A
x✝ : S
y✝ : Ω[A⁄R]
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • x✝ ⊗ₜ[R] y✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) (x✝ ⊗ₜ[R] y✝)

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
a : A
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • x✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) x✝
a✝ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • y✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) y✝
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • (x✝ + y✝)) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) (x✝ + y✝)

Tactic:
· simp only [smul_zero, map_zero]

Goal state after:
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
a : A
x✝ : S
y✝ : Ω[A⁄R]
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • x✝ ⊗ₜ[R] y✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) (x✝ ⊗ₜ[R] y✝)

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
a : A
x✝ y✝ : S ⊗[R] Ω[A⁄R]
a✝¹ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • x✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) x✝
a✝ :
  (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • y✝) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) y✝
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((IsScalarTower.toAlgHom R A B).toLinearMap a • (x✝ + y✝)) =
    (IsScalarTower.toAlgHom R A B).toLinearMap a • (LinearMap.liftBaseChange S (↑R (map R S A B))) (x✝ + y✝)