case H.h.h
R : Type u_3
inst✝¹⁸ : CommSemiring R
R' : Type ?u.944131
inst✝¹⁷ : Monoid R'
R'' : Type ?u.944137
inst✝¹⁶ : Semiring R''
M : Type u_1
N : Type u_2
P : Type ?u.944149
Q : Type ?u.944152
S : Type ?u.944155
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.945282
Q' : Type ?u.945285
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
x✝¹ : M
x✝ : N
⊢ ↑(↑(compr₂ (mk R M N) (map LinearMap.id LinearMap.id)) x✝¹) x✝ = ↑(↑(compr₂ (mk R M N) LinearMap.id) x✝¹) x✝
R : Type u_3
inst✝¹⁸ : CommSemiring R
R' : Type ?u.944131
inst✝¹⁷ : Monoid R'
R'' : Type ?u.944137
inst✝¹⁶ : Semiring R''
M : Type u_1
N : Type u_2
P : Type ?u.944149
Q : Type ?u.944152
S : Type ?u.944155
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.945282
Q' : Type ?u.945285
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
⊢ map LinearMap.id LinearMap.id = LinearMap.id
ext
no goals
case H.h.h
R : Type u_3
inst✝¹⁸ : CommSemiring R
R' : Type ?u.944131
inst✝¹⁷ : Monoid R'
R'' : Type ?u.944137
inst✝¹⁶ : Semiring R''
M : Type u_1
N : Type u_2
P : Type ?u.944149
Q : Type ?u.944152
S : Type ?u.944155
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.945282
Q' : Type ?u.945285
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
x✝¹ : M
x✝ : N
⊢ ↑(↑(compr₂ (mk R M N) (map LinearMap.id LinearMap.id)) x✝¹) x✝ = ↑(↑(compr₂ (mk R M N) LinearMap.id) x✝¹) x✝
simp only [mk_apply, id_coe, compr₂_apply, id.def, map_tmul]