case h.h
R : Type u_1
R₁ : Type ?u.2210347
R₂ : Type ?u.2210350
R₃ : Type ?u.2210353
R₄ : Type ?u.2210356
S : Type ?u.2210359
K : Type ?u.2210362
K₂ : Type ?u.2210365
M : Type u_2
M' : Type ?u.2210371
M₁ : Type ?u.2210374
M₂ : Type u_3
M₃ : Type u_4
M₄ : Type ?u.2210383
N : Type ?u.2210386
N₂ : Type ?u.2210389
ι : Type ?u.2210392
V : Type ?u.2210395
V₂ : Type ?u.2210398
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁ : M ≃ₗ[R] M₂
e₂ : M₂ ≃ₗ[R] M₃
f : Module.End R M
x : M₃
⊢ ↑(↑(trans (conj e₁) (conj e₂)) f) x = ↑(↑(conj (trans e₁ e₂)) f) x
R : Type u_1
R₁ : Type ?u.2210347
R₂ : Type ?u.2210350
R₃ : Type ?u.2210353
R₄ : Type ?u.2210356
S : Type ?u.2210359
K : Type ?u.2210362
K₂ : Type ?u.2210365
M : Type u_2
M' : Type ?u.2210371
M₁ : Type ?u.2210374
M₂ : Type u_3
M₃ : Type u_4
M₄ : Type ?u.2210383
N : Type ?u.2210386
N₂ : Type ?u.2210389
ι : Type ?u.2210392
V : Type ?u.2210395
V₂ : Type ?u.2210398
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁ : M ≃ₗ[R] M₂
e₂ : M₂ ≃ₗ[R] M₃
⊢ trans (conj e₁) (conj e₂) = conj (trans e₁ e₂)
ext (f x)
no goals
case h.h
R : Type u_1
R₁ : Type ?u.2210347
R₂ : Type ?u.2210350
R₃ : Type ?u.2210353
R₄ : Type ?u.2210356
S : Type ?u.2210359
K : Type ?u.2210362
K₂ : Type ?u.2210365
M : Type u_2
M' : Type ?u.2210371
M₁ : Type ?u.2210374
M₂ : Type u_3
M₃ : Type u_4
M₄ : Type ?u.2210383
N : Type ?u.2210386
N₂ : Type ?u.2210389
ι : Type ?u.2210392
V : Type ?u.2210395
V₂ : Type ?u.2210398
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁ : M ≃ₗ[R] M₂
e₂ : M₂ ≃ₗ[R] M₃
f : Module.End R M
x : M₃
⊢ ↑(↑(trans (conj e₁) (conj e₂)) f) x = ↑(↑(conj (trans e₁ e₂)) f) x
rfl