Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁵⁰ : CommSemiring R
inst✝⁴⁹ : CommSemiring R₂
inst✝⁴⁸ : CommSemiring R₃
inst✝⁴⁷ : Monoid R'
inst✝⁴⁶ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A✝ : Type u_6
M✝ : Type u_7
N✝ : Type u_8
P : Type u_9
Q : Type u_10
S✝ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁵ : AddCommMonoid M✝
inst✝⁴⁴ : AddCommMonoid N✝
inst✝⁴³ : AddCommMonoid P
inst✝⁴² : AddCommMonoid Q
inst✝⁴¹ : AddCommMonoid S✝
inst✝⁴⁰ : AddCommMonoid P'
inst✝³⁹ : AddCommMonoid Q'
inst✝³⁸ : AddCommMonoid M₂
inst✝³⁷ : AddCommMonoid N₂
inst✝³⁶ : AddCommMonoid P₂
inst✝³⁵ : AddCommMonoid Q₂
inst✝³⁴ : AddCommMonoid M₃
inst✝³³ : AddCommMonoid N₃
inst✝³² : AddCommMonoid P₃
inst✝³¹ : AddCommMonoid Q₃
inst✝³⁰ : DistribMulAction R' M✝
inst✝²⁹ : Module R'' M✝
inst✝²⁸ : Module R M✝
inst✝²⁷ : Module R N✝
inst✝²⁶ : Module R S✝
inst✝²⁵ : Module R P'
inst✝²⁴ : Module R Q'
inst✝²³ : Module R₂ M₂
inst✝²² : Module R₂ N₂
inst✝²¹ : Module R₂ P₂
inst✝²⁰ : Module R₂ Q₂
inst✝¹⁹ : Module R₃ M₃
inst✝¹⁸ : Module R₃ N₃
inst✝¹⁷ : Module R₃ P₃
inst✝¹⁶ : Module R₃ Q₃
inst✝¹⁵ : Module R P
inst✝¹⁴ : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : CommSemiring A
inst✝⁸ : Module A M
inst✝⁷ : Module A N
inst✝⁶ : SMulCommClass R A M
inst✝⁵ : CommSemiring S
inst✝⁴ : Module S M
inst✝³ : SMulCommClass R S M
inst✝² : SMulCommClass A S M
inst✝¹ : CompatibleSMul R A M N
inst✝ : CompatibleSMul A R M N
x x✝¹ x✝ : M ⊗[R] N
h : (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) x✝¹) = x✝¹
h' : (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) x✝) = x✝
⊢ (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) (x✝¹ + x✝)) = x✝¹ + x✝

Tactic:
simpa using

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁵⁰ : CommSemiring R
inst✝⁴⁹ : CommSemiring R₂
inst✝⁴⁸ : CommSemiring R₃
inst✝⁴⁷ : Monoid R'
inst✝⁴⁶ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A✝ : Type u_6
M✝ : Type u_7
N✝ : Type u_8
P : Type u_9
Q : Type u_10
S✝ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁵ : AddCommMonoid M✝
inst✝⁴⁴ : AddCommMonoid N✝
inst✝⁴³ : AddCommMonoid P
inst✝⁴² : AddCommMonoid Q
inst✝⁴¹ : AddCommMonoid S✝
inst✝⁴⁰ : AddCommMonoid P'
inst✝³⁹ : AddCommMonoid Q'
inst✝³⁸ : AddCommMonoid M₂
inst✝³⁷ : AddCommMonoid N₂
inst✝³⁶ : AddCommMonoid P₂
inst✝³⁵ : AddCommMonoid Q₂
inst✝³⁴ : AddCommMonoid M₃
inst✝³³ : AddCommMonoid N₃
inst✝³² : AddCommMonoid P₃
inst✝³¹ : AddCommMonoid Q₃
inst✝³⁰ : DistribMulAction R' M✝
inst✝²⁹ : Module R'' M✝
inst✝²⁸ : Module R M✝
inst✝²⁷ : Module R N✝
inst✝²⁶ : Module R S✝
inst✝²⁵ : Module R P'
inst✝²⁴ : Module R Q'
inst✝²³ : Module R₂ M₂
inst✝²² : Module R₂ N₂
inst✝²¹ : Module R₂ P₂
inst✝²⁰ : Module R₂ Q₂
inst✝¹⁹ : Module R₃ M₃
inst✝¹⁸ : Module R₃ N₃
inst✝¹⁷ : Module R₃ P₃
inst✝¹⁶ : Module R₃ Q₃
inst✝¹⁵ : Module R P
inst✝¹⁴ : Module R Q
A : Type u_22
S : Type u_23
M : Type u_24
N : Type u_25
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : CommSemiring A
inst✝⁸ : Module A M
inst✝⁷ : Module A N
inst✝⁶ : SMulCommClass R A M
inst✝⁵ : CommSemiring S
inst✝⁴ : Module S M
inst✝³ : SMulCommClass R S M
inst✝² : SMulCommClass A S M
inst✝¹ : CompatibleSMul R A M N
inst✝ : CompatibleSMul A R M N
x x✝¹ x✝ : M ⊗[R] N
h : (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) x✝¹) = x✝¹
h' : (mapOfCompatibleSMul R A S M N).toFun ((mapOfCompatibleSMul A R S M N) x✝) = x✝
⊢ (mapOfCompatibleSMul R A S M N) ((mapOfCompatibleSMul A R S M N) x✝¹) +
      (mapOfCompatibleSMul R A S M N) ((mapOfCompatibleSMul A R S M N) x✝) =
    x✝¹ + x✝