case H.h.h
R : Type u_1
inst✝¹⁸ : CommSemiring R
R' : Type ?u.989827
inst✝¹⁷ : Monoid R'
R'' : Type ?u.989833
inst✝¹⁶ : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.989851
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : AddCommMonoid S
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : Module R P
inst✝⁷ : Module R Q
inst✝⁶ : Module R S
inst✝⁵ : DistribMulAction R' M
inst✝⁴ : Module R'' M
P' : Type ?u.990978
Q' : Type ?u.990981
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[R] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(compr₂ (mk R M N) (map f (g₁ + g₂))) x✝¹) x✝ = ↑(↑(compr₂ (mk R M N) (map f g₁ + map f g₂)) x✝¹) x✝
R : Type u_1
inst✝¹⁸ : CommSemiring R
R' : Type ?u.989827
inst✝¹⁷ : Monoid R'
R'' : Type ?u.989833
inst✝¹⁶ : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.989851
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : AddCommMonoid S
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : Module R P
inst✝⁷ : Module R Q
inst✝⁶ : Module R S
inst✝⁵ : DistribMulAction R' M
inst✝⁴ : Module R'' M
P' : Type ?u.990978
Q' : Type ?u.990981
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[R] P
g₁ g₂ : N →ₗ[R] Q
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂
ext
no goals
case H.h.h
R : Type u_1
inst✝¹⁸ : CommSemiring R
R' : Type ?u.989827
inst✝¹⁷ : Monoid R'
R'' : Type ?u.989833
inst✝¹⁶ : Semiring R''
M : Type u_2
N : Type u_4
P : Type u_3
Q : Type u_5
S : Type ?u.989851
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : AddCommMonoid S
inst✝¹⁰ : Module R M
inst✝⁹ : Module R N
inst✝⁸ : Module R P
inst✝⁷ : Module R Q
inst✝⁶ : Module R S
inst✝⁵ : DistribMulAction R' M
inst✝⁴ : Module R'' M
P' : Type ?u.990978
Q' : Type ?u.990981
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
f : M →ₗ[R] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(compr₂ (mk R M N) (map f (g₁ + g₂))) x✝¹) x✝ = ↑(↑(compr₂ (mk R M N) (map f g₁ + map f g₂)) x✝¹) x✝
simp only [tmul_add, compr₂_apply, mk_apply, map_tmul, add_apply]