Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x : M₂ ⊗[R] M₁
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • x) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun x

Tactic:
induction x

Goal state after:
case zero
R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • 0) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun 0

case tmul
R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x✝ : M₂
y✝ : M₁
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • x✝ ⊗ₜ[R] y✝) =
    (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun (x✝ ⊗ₜ[R] y✝)

case add
R✝ : Type u_1
inst✝³⁵ : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝³⁴ : AddCommMonoid M₁✝
inst✝³³ : AddCommMonoid M₂✝
inst✝³² : AddCommMonoid M
inst✝³¹ : AddCommMonoid M'
inst✝³⁰ : Module R✝ M₁✝
inst✝²⁹ : Module R✝ M₂✝
inst✝²⁸ : Module R✝ M
inst✝²⁷ : Module R✝ M'
f✝ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝²⁶ : AddCommMonoid N₁
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid N
inst✝²³ : Module R✝ N₁
inst✝²² : Module R✝ N₂
inst✝²¹ : Module R✝ N
g✝ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x✝ y✝ : M₂ ⊗[R] M₁
a✝¹ : (↑(TensorProduct.comm R M₂ M₁)).toFun (s • x✝) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun x✝
a✝ : (↑(TensorProduct.comm R M₂ M₁)).toFun (s • y✝) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun y✝
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • (x✝ + y✝)) =
    (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun (x✝ + y✝)