-- Mathlib/RingTheory/Kaehler/TensorProduct.lean
lemma map_liftBaseChange_smul [h : Algebra.IsPushout R S A B] (b : B) (x) :
    ((map R S A B).restrictScalars R).liftBaseChange S (b • x) =
    b • ((map R S A B).restrictScalars R).liftBaseChange S x

Proof state:
case h₁
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 : S ⊗[R] Ω[A⁄R]
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) (0 • x) = 0 • (LinearMap.liftBaseChange S (↑R (map R S A B))) x

Tactic:
simp only [zero_smul, map_zero]

Result:
no goals

Proof state:
case h₂.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

Tactic:
simp only [smul_zero, map_zero]

Result:
no goals

Proof state:
case h₂
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 : S ⊗[R] Ω[A⁄R]
a : 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

Tactic:
induction x

Result:
case h₂.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

case h₂.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 h₂.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✝)

Proof state:
case h₂.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✝)

Tactic:
simp [smul_comm]

Result:
no goals

Proof state:
case h₂.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 [map_add, smul_add, *]

Result:
no goals

Proof state:
case h₃
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 : S ⊗[R] Ω[A⁄R]
s : S
b : B
e : (LinearMap.liftBaseChange S (↑R (map R S A B))) (b • x) = b • (LinearMap.liftBaseChange S (↑R (map R S A B))) x
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((s • b) • x) =
    (s • b) • (LinearMap.liftBaseChange S (↑R (map R S A B))) x

Tactic:
rw [smul_assoc, map_smul, e, smul_assoc]

Result:
no goals

Proof state:
case h₄
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 : S ⊗[R] Ω[A⁄R]
b₁ b₂ : B
e₁ : (LinearMap.liftBaseChange S (↑R (map R S A B))) (b₁ • x) = b₁ • (LinearMap.liftBaseChange S (↑R (map R S A B))) x
e₂ : (LinearMap.liftBaseChange S (↑R (map R S A B))) (b₂ • x) = b₂ • (LinearMap.liftBaseChange S (↑R (map R S A B))) x
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((b₁ + b₂) • x) =
    (b₁ + b₂) • (LinearMap.liftBaseChange S (↑R (map R S A B))) x

Tactic:
simp only [map_add, e₁, e₂, add_smul]

Result:
no goals