L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
⊢ BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ)
      (fun x => ↑(Language.con L (↑(Equiv.sumEmpty α Empty) x))) default ↔
    M ⊨ φ
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
⊢ (Realize (↑equivSentence.symm φ) fun a => ↑(Language.con L a)) ↔ M ⊨ φ
simp only [equivSentence, Equiv.symm_symm, Equiv.coe_trans, Realize,
  BoundedFormula.realize_relabelEquiv, Function.comp]
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
⊢ BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ)
      (fun x => ↑(Language.con L (↑(Equiv.sumEmpty α Empty) x))) default ↔
    BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ) (Sum.elim (fun a => ↑(Language.con L a)) default)
      default
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
⊢ BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ)
      (fun x => ↑(Language.con L (↑(Equiv.sumEmpty α Empty) x))) default ↔
    M ⊨ φ
refine' _root_.trans _ BoundedFormula.realize_constantsVarsEquiv
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
⊢ BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ)
      (fun x => ↑(Language.con L (↑(Equiv.sumEmpty α Empty) x))) default =
    BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ) (Sum.elim (fun a => ↑(Language.con L a)) default)
      default
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
⊢ BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ)
      (fun x => ↑(Language.con L (↑(Equiv.sumEmpty α Empty) x))) default ↔
    BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ) (Sum.elim (fun a => ↑(Language.con L a)) default)
      default
rw [iff_iff_eq]
case e__v.h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
val✝ : α
⊢ ↑(Language.con L (↑(Equiv.sumEmpty α Empty) (Sum.inl val✝))) =
    Sum.elim (fun a => ↑(Language.con L a)) default (Sum.inl val✝)

case e__v.h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
a : Empty
⊢ ↑(Language.con L (↑(Equiv.sumEmpty α Empty) (Sum.inr a))) =
    Sum.elim (fun a => ↑(Language.con L a)) default (Sum.inr a)
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
⊢ BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ)
      (fun x => ↑(Language.con L (↑(Equiv.sumEmpty α Empty) x))) default =
    BoundedFormula.Realize (↑BoundedFormula.constantsVarsEquiv φ) (Sum.elim (fun a => ↑(Language.con L a)) default)
      default
congr with (_ | a)
case e__v.h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
a : Empty
⊢ ↑(Language.con L (↑(Equiv.sumEmpty α Empty) (Sum.inr a))) =
    Sum.elim (fun a => ↑(Language.con L a)) default (Sum.inr a)
case e__v.h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
val✝ : α
⊢ ↑(Language.con L (↑(Equiv.sumEmpty α Empty) (Sum.inl val✝))) =
    Sum.elim (fun a => ↑(Language.con L a)) default (Sum.inl val✝)

case e__v.h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
a : Empty
⊢ ↑(Language.con L (↑(Equiv.sumEmpty α Empty) (Sum.inr a))) =
    Sum.elim (fun a => ↑(Language.con L a)) default (Sum.inr a)
. simp
no goals
case e__v.h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
a : Empty
⊢ ↑(Language.con L (↑(Equiv.sumEmpty α Empty) (Sum.inr a))) =
    Sum.elim (fun a => ↑(Language.con L a)) default (Sum.inr a)
. cases a
no goals
case e__v.h.inl
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
val✝ : α
⊢ ↑(Language.con L (↑(Equiv.sumEmpty α Empty) (Sum.inl val✝))) =
    Sum.elim (fun a => ↑(Language.con L a)) default (Sum.inl val✝)
simp
no goals
case e__v.h.inr
L : Language
L' : Language
M : Type w
N : Type ?u.257040
P : Type ?u.257043
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Sentence (L[[α]])
a : Empty
⊢ ↑(Language.con L (↑(Equiv.sumEmpty α Empty) (Sum.inr a))) =
    Sum.elim (fun a => ↑(Language.con L a)) default (Sum.inr a)
cases a