case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type ?u.417
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
⊢ Definable A L' (setOf (Formula.Realize ψ))
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type ?u.417
B : Set M
s : Set (α → M)
L' : Language
inst✝¹ : Structure L' M
h : Definable A L s
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
⊢ Definable A L' s
obtain ⟨ψ, rfl⟩ := h
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type ?u.417
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
⊢ setOf (Formula.Realize ψ) = setOf (Formula.Realize (LHom.onFormula (LHom.addConstants (↑A) φ) ψ))
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type ?u.417
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
⊢ Definable A L' (setOf (Formula.Realize ψ))
refine' ⟨(φ.addConstants A).onFormula ψ, _⟩
case intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type ?u.417
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
x : α → M
⊢ x ∈ setOf (Formula.Realize ψ) ↔ x ∈ setOf (Formula.Realize (LHom.onFormula (LHom.addConstants (↑A) φ) ψ))
case intro
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type ?u.417
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
⊢ setOf (Formula.Realize ψ) = setOf (Formula.Realize (LHom.onFormula (LHom.addConstants (↑A) φ) ψ))
ext x
no goals
case intro.h
M : Type w
A : Set M
L : Language
inst✝² : Structure L M
α : Type u₁
β : Type ?u.417
B : Set M
L' : Language
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : LHom.IsExpansionOn φ M
ψ : Formula (L[[↑A]]) α
x : α → M
⊢ x ∈ setOf (Formula.Realize ψ) ↔ x ∈ setOf (Formula.Realize (LHom.onFormula (LHom.addConstants (↑A) φ) ψ))
simp only [mem_setOf_eq, LHom.realize_onFormula]