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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m₁ m₂ : M
n : N
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m₁, n) + FreeAddMonoid.of (m₂, n)) =
    (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m₁ + m₂, n))

Tactic:
map_add,

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₃
f : M →+ N →+ P
hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
m₁ m₂ : M
n : N
⊢ (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m₁, n)) +
      (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m₂, n)) =
    (FreeAddMonoid.lift fun mn ↦ (f mn.1) mn.2) (FreeAddMonoid.of (m₁ + m₂, n))