case h.h
α : Type ?u.567819
M : Type u_4
N : Type u_5
P : Type ?u.567828
R : Type u_3
S : Type ?u.567834
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_1
κ : Type u_2
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
x✝ : κ →₀ N
a✝ : ι
⊢ ↑(↑(LinearEquiv.symm (lcongr e₁ e₂)) x✝) a✝ = ↑(↑(lcongr e₁.symm (LinearEquiv.symm e₂)) x✝) a✝
α : Type ?u.567819
M : Type u_4
N : Type u_5
P : Type ?u.567828
R : Type u_3
S : Type ?u.567834
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_1
κ : Type u_2
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
⊢ LinearEquiv.symm (lcongr e₁ e₂) = lcongr e₁.symm (LinearEquiv.symm e₂)
ext
no goals
case h.h
α : Type ?u.567819
M : Type u_4
N : Type u_5
P : Type ?u.567828
R : Type u_3
S : Type ?u.567834
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_1
κ : Type u_2
e₁ : ι ≃ κ
e₂ : M ≃ₗ[R] N
x✝ : κ →₀ N
a✝ : ι
⊢ ↑(↑(LinearEquiv.symm (lcongr e₁ e₂)) x✝) a✝ = ↑(↑(lcongr e₁.symm (LinearEquiv.symm e₂)) x✝) a✝
rfl