case h
R : Type u_1
R₁ : Type ?u.2212288
R₂ : Type ?u.2212291
R₃ : Type ?u.2212294
R₄ : Type ?u.2212297
S : Type ?u.2212300
K : Type ?u.2212303
K₂ : Type ?u.2212306
M : Type u_2
M' : Type ?u.2212312
M₁ : Type ?u.2212315
M₂ : Type u_3
M₃ : Type ?u.2212321
M₄ : Type ?u.2212324
N : Type ?u.2212327
N₂ : Type ?u.2212330
ι : Type ?u.2212333
V : Type ?u.2212336
V₂ : Type ?u.2212339
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₂
x✝ : M₂
⊢ ↑(↑(conj e) LinearMap.id) x✝ = ↑LinearMap.id x✝
R : Type u_1
R₁ : Type ?u.2212288
R₂ : Type ?u.2212291
R₃ : Type ?u.2212294
R₄ : Type ?u.2212297
S : Type ?u.2212300
K : Type ?u.2212303
K₂ : Type ?u.2212306
M : Type u_2
M' : Type ?u.2212312
M₁ : Type ?u.2212315
M₂ : Type u_3
M₃ : Type ?u.2212321
M₄ : Type ?u.2212324
N : Type ?u.2212327
N₂ : Type ?u.2212330
ι : Type ?u.2212333
V : Type ?u.2212336
V₂ : Type ?u.2212339
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₂
⊢ ↑(conj e) LinearMap.id = LinearMap.id
ext
no goals
case h
R : Type u_1
R₁ : Type ?u.2212288
R₂ : Type ?u.2212291
R₃ : Type ?u.2212294
R₄ : Type ?u.2212297
S : Type ?u.2212300
K : Type ?u.2212303
K₂ : Type ?u.2212306
M : Type u_2
M' : Type ?u.2212312
M₁ : Type ?u.2212315
M₂ : Type u_3
M₃ : Type ?u.2212321
M₄ : Type ?u.2212324
N : Type ?u.2212327
N₂ : Type ?u.2212330
ι : Type ?u.2212333
V : Type ?u.2212336
V₂ : Type ?u.2212339
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₂
x✝ : M₂
⊢ ↑(↑(conj e) LinearMap.id) x✝ = ↑LinearMap.id x✝
simp [conj_apply]