-- Mathlib/ModelTheory/Definability.lean
theorem definable_iff_exists_formula_sum :
    A.Definable L s ↔ ∃ φ : L.Formula (A ⊕ α), s = {v | φ.Realize (Sum.elim (↑) v)}

Proof state:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ ∀ (n : ℕ) (t : L.Term ((↑A ⊕ α) ⊕ Fin n)) (xs : Fin n → M),
    Term.realize (Sum.elim x✝ xs) (Term.constantsVarsEquivLeft.symm t) =
      Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs) t

Tactic:
intros

Result:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Term.realize (Sum.elim x✝ xs✝) (Term.constantsVarsEquivLeft.symm t✝) =
    Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝

Proof state:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Term.realize (Sum.elim (fun a => ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) t✝ =
    Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝

Tactic:
congr

Result:
case h.e_v
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Sum.elim (fun a => ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝)) = Sum.elim (Sum.elim Subtype.val x✝) xs✝

Proof state:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ (BoundedFormula.mapTermRel (fun n => ⇑Term.constantsVarsEquivLeft.symm)
          (fun n => ⇑(Equiv.sumEmpty (L.Relations n) Empty).symm) (fun x => id) φ).Realize
      x✝ default ↔
    φ.Realize (Sum.elim Subtype.val x✝) default

Tactic:
refine BoundedFormula.realize_mapTermRel_id ?_ (fun _ _ _ => rfl)

Result:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ ∀ (n : ℕ) (t : L.Term ((↑A ⊕ α) ⊕ Fin n)) (xs : Fin n → M),
    Term.realize (Sum.elim x✝ xs) (Term.constantsVarsEquivLeft.symm t) =
      Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs) t

Proof state:
case h.e_v
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Sum.elim (fun a => ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝)) = Sum.elim (Sum.elim Subtype.val x✝) xs✝

Tactic:
ext a

Result:
case h.e_v.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
a : (↑A ⊕ α) ⊕ Fin n✝
⊢ (Sum.elim (fun a => ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) a =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ a

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
⊢ setOf (Formula.Realize (BoundedFormula.constantsVarsEquiv.symm φ)) = {v | Formula.Realize φ (Sum.elim Subtype.val v)}

Tactic:
ext

Result:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ x✝ ∈ setOf (Formula.Realize (BoundedFormula.constantsVarsEquiv.symm φ)) ↔
    x✝ ∈ {v | Formula.Realize φ (Sum.elim Subtype.val v)}

Proof state:
case h.e_v.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
a : (↑A ⊕ α) ⊕ Fin n✝
⊢ (Sum.elim (fun a => ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) a =
    Sum.elim (Sum.elim Subtype.val x✝) xs✝ a

Tactic:
rcases a with (_ | _) | _ <;> rfl

Result:
no goals

Proof state:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ x✝ ∈ setOf (Formula.Realize (BoundedFormula.constantsVarsEquiv.symm φ)) ↔
    x✝ ∈ {v | Formula.Realize φ (Sum.elim Subtype.val v)}

Tactic:
simp only [BoundedFormula.constantsVarsEquiv, constantsOn,
  BoundedFormula.mapTermRelEquiv_symm_apply, mem_setOf_eq, Formula.Realize]

Result:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ (BoundedFormula.mapTermRel (fun n => ⇑Term.constantsVarsEquivLeft.symm)
          (fun n => ⇑(Equiv.sumEmpty (L.Relations n) Empty).symm) (fun x => id) φ).Realize
      x✝ default ↔
    φ.Realize (Sum.elim Subtype.val x✝) default

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ A.Definable L s ↔ ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}

Tactic:
rw [Definable, Equiv.exists_congr_left (BoundedFormula.constantsVarsEquiv)]

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ b, s = setOf (Formula.Realize (BoundedFormula.constantsVarsEquiv.symm b))) ↔
    ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}

Proof state:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Term.realize (Sum.elim x✝ xs✝) (Term.constantsVarsEquivLeft.symm t✝) =
    Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝

Tactic:
simp only [Term.constantsVarsEquivLeft_symm_apply, Term.realize_varsToConstants,
  coe_con, Term.realize_relabel]

Result:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
n✝ : ℕ
t✝ : L.Term ((↑A ⊕ α) ⊕ Fin n✝)
xs✝ : Fin n✝ → M
⊢ Term.realize (Sum.elim (fun a => ↑a) (Sum.elim x✝ xs✝) ∘ ⇑(Equiv.sumAssoc (↑A) α (Fin n✝))) t✝ =
    Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs✝) t✝