no goals
α : Type ?u.541821
M : Type u_4
N : Type u_5
P : Type ?u.541830
R : Type u_3
S : Type ?u.541836
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
i : ι
m : M
⊢ ↑(lcongr e₁ e₂) (single i m) = single (↑e₁ i) (↑e₂ m)
simp [lcongr]