L : Language
M : Type u_4
N : Type ?u.371937
P : Type ?u.371940
Q : Type ?u.371943
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_1
φ : Formula L α
v : α → { x // x ∈ ⊤ }
⊢ Formula.Realize φ (↑topEquiv ∘ v) ↔ Formula.Realize φ (Subtype.val ∘ v)
L : Language
M : Type u_4
N : Type ?u.371937
P : Type ?u.371940
Q : Type ?u.371943
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_1
φ : Formula L α
v : α → { x // x ∈ ⊤ }
⊢ Formula.Realize φ v ↔ Formula.Realize φ (Subtype.val ∘ v)
rw [← Substructure.topEquiv.realize_formula φ]
no goals
L : Language
M : Type u_4
N : Type ?u.371937
P : Type ?u.371940
Q : Type ?u.371943
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
α : Type u_1
φ : Formula L α
v : α → { x // x ∈ ⊤ }
⊢ Formula.Realize φ (↑topEquiv ∘ v) ↔ Formula.Realize φ (Subtype.val ∘ v)
simp