case h
L : Language
L' : Language
M : Type w
N : Type ?u.247641
P : Type ?u.247644
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
ψ : Formula L α
x✝ : α → M
⊢ x✝ ∈ setOf (Formula.Realize (onFormula φ ψ)) ↔ x✝ ∈ setOf (Formula.Realize ψ)
L : Language
L' : Language
M : Type w
N : Type ?u.247641
P : Type ?u.247644
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
ψ : Formula L α
⊢ setOf (Formula.Realize (onFormula φ ψ)) = setOf (Formula.Realize ψ)
ext
no goals
case h
L : Language
L' : Language
M : Type w
N : Type ?u.247641
P : Type ?u.247644
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
ψ : Formula L α
x✝ : α → M
⊢ x✝ ∈ setOf (Formula.Realize (onFormula φ ψ)) ↔ x✝ ∈ setOf (Formula.Realize ψ)
simp