L : Language
M : Type ?u.318087
N : Type ?u.318090
inst✝ : Structure L M
e : M ≃ N
this : Structure L N := inducedStructure e
⊢ (a : N) → (fun x => M) a
L : Language
M : Type ?u.318087
N : Type ?u.318090
inst✝ : Structure L M
e : M ≃ N
⊢ (a : N) → (fun x => M) a
letI : L.Structure N := inducedStructure e
no goals
L : Language
M : Type ?u.318087
N : Type ?u.318090
inst✝ : Structure L M
e : M ≃ N
this : Structure L N := inducedStructure e
⊢ (a : N) → (fun x => M) a
exact FunLike.coe (@inducedStructureEquiv L M N _ e).symm