-- Mathlib/ModelTheory/Semantics.lean
theorem realize_constantsVarsEquiv [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M]
    {n} {φ : L[[α]].BoundedFormula β n} {v : β → M} {xs : Fin n → M} :
    (constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) v) xs ↔ φ.Realize v xs

Proof state:
case a.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
xs : Fin n → M
R : (constantsOn α).Relations n
⊢ RelMap
      ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) (Sum.inr R)))
      xs ↔
    RelMap (Sum.inr R) xs

Tactic:
exact isEmptyElim R

Result:
no goals

Proof state:
case a
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) R)) xs ↔
    RelMap R xs

Tactic:
obtain - | R := R

Result:
case a.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
xs : Fin n → M
val✝ : L.Relations n
⊢ RelMap
      ((L.lhomWithConstants α).onRelation
        ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) (Sum.inl val✝)))
      xs ↔
    RelMap (Sum.inl val✝) xs

case a.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
xs : Fin n → M
R : (constantsOn α).Relations n
⊢ RelMap
      ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) (Sum.inr R)))
      xs ↔
    RelMap (Sum.inr R) xs

Proof state:
case a.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
xs : Fin n → M
val✝ : L.Relations n
⊢ RelMap
      ((L.lhomWithConstants α).onRelation
        ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) (Sum.inl val✝)))
      xs ↔
    RelMap (Sum.inl val✝) xs

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap (((fun x => Equiv.sumEmpty (L.Relations x) ((constantsOn α).Relations x)) n) R) xs = RelMap R xs

Tactic:
erw [← (lhomWithConstants L α).map_onRelation
    (Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n) R) xs]

Result:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) R)) xs =
    RelMap R xs

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
φ : L[[α]].BoundedFormula β n
v : β → M
xs : Fin n → M
⊢ (constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) v) xs ↔ φ.Realize v xs

Tactic:
refine realize_mapTermRel_id (fun n t xs => realize_constantsVarsEquivLeft) fun n R xs => ?_

Result:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap (((fun x => Equiv.sumEmpty (L.Relations x) ((constantsOn α).Relations x)) n) R) xs = RelMap R xs

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) R)) xs =
    RelMap R xs

Tactic:
rcongr

Result:
case a
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n✝ : ℕ
φ : L[[α]].BoundedFormula β n✝
v : β → M
xs✝ : Fin n✝ → M
n : ℕ
R : L[[α]].Relations n
xs : Fin n → M
⊢ RelMap ((L.lhomWithConstants α).onRelation ((Equiv.sumEmpty (L.Relations n) ((constantsOn α).Relations n)) R)) xs ↔
    RelMap R xs