-- Mathlib/ModelTheory/Definability.lean
theorem definable_iff_finitely_definable :
    A.Definable L s ↔ ∃ (A0 : Finset M), (A0 : Set M) ⊆ A ∧
      (A0 : Set M).Definable L s

Proof state:
case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s) → A.Definable L s

Tactic:
rintro ⟨A0, hA0, hd⟩

Result:
case mpr.intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
A0 : Finset M
hA0 : ↑A0 ⊆ A
hd : (↑A0).Definable L s
⊢ A.Definable L s

Proof state:
case mp.intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ x✝ ∈ {v | φ.Realize (Sum.elim Subtype.val v)} ↔
    x✝ ∈
      {v |
        Formula.Realize
          (BoundedFormula.restrictFreeVar φ fun x =>
            Sum.casesOn (motive := fun x => x ∈ BoundedFormula.freeVarFinset φ → ↑↑A0 ⊕ α) (↑x)
              (fun x hx => Sum.inl ⟨↑x, ⋯⟩) (fun x x_1 => Sum.inr x) ⋯)
          (Sum.elim Subtype.val v)}

Tactic:
simp only [Formula.Realize, mem_setOf_eq, Finset.coe_sort_coe]

Result:
case mp.intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ BoundedFormula.Realize φ (Sum.elim Subtype.val x✝) default ↔
    (BoundedFormula.restrictFreeVar φ fun x =>
          Sum.rec (motive := fun x => x ∈ BoundedFormula.freeVarFinset φ → { x // x ∈ A0 } ⊕ α)
            (fun val hx => Sum.inl ⟨↑val, ⋯⟩) (fun val x => Sum.inr val) ↑x ⋯).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 ↔ ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s

Tactic:
constructor

Result:
case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ A.Definable L s → ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s

case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s) → A.Definable L s

Proof state:
case mp.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
⊢ {v | φ.Realize (Sum.elim Subtype.val v)} =
    {v |
      Formula.Realize
        (BoundedFormula.restrictFreeVar φ fun x =>
          Sum.casesOn (motive := fun x => x ∈ BoundedFormula.freeVarFinset φ → ↑↑A0 ⊕ α) (↑x)
            (fun x hx => Sum.inl ⟨↑x, ⋯⟩) (fun x x_1 => Sum.inr x) ⋯)
        (Sum.elim Subtype.val v)}

Tactic:
ext

Result:
case mp.intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ x✝ ∈ {v | φ.Realize (Sum.elim Subtype.val v)} ↔
    x✝ ∈
      {v |
        Formula.Realize
          (BoundedFormula.restrictFreeVar φ fun x =>
            Sum.casesOn (motive := fun x => x ∈ BoundedFormula.freeVarFinset φ → ↑↑A0 ⊕ α) (↑x)
              (fun x hx => Sum.inl ⟨↑x, ⋯⟩) (fun x x_1 => Sum.inr x) ⋯)
          (Sum.elim Subtype.val v)}

Proof state:
case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ A.Definable L s → ∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s

Tactic:
simp only [definable_iff_exists_formula_sum]

Result:
case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}) →
    ∃ A0, ↑A0 ⊆ A ∧ ∃ φ, s = {v | φ.Realize (Sum.elim Subtype.val v)}

Proof state:
case mp.intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ BoundedFormula.Realize φ (Sum.elim Subtype.val x✝) default ↔
    (BoundedFormula.restrictFreeVar φ fun x =>
          Sum.rec (motive := fun x => x ∈ BoundedFormula.freeVarFinset φ → { x // x ∈ A0 } ⊕ α)
            (fun val hx => Sum.inl ⟨↑val, ⋯⟩) (fun val x => Sum.inr val) ↑x ⋯).Realize
      (Sum.elim Subtype.val x✝) default

Tactic:
exact iff_comm.1 <| BoundedFormula.realize_restrictFreeVar _ (by simp)

Result:
no goals

Proof state:
case mpr.intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
A0 : Finset M
hA0 : ↑A0 ⊆ A
hd : (↑A0).Definable L s
⊢ A.Definable L s

Tactic:
exact Definable.mono hd hA0

Result:
no goals

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

Tactic:
rintro ⟨φ, rfl⟩

Result:
case mp.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
⊢ ∃ A0, ↑A0 ⊆ A ∧ ∃ φ_1, {v | φ.Realize (Sum.elim Subtype.val v)} = {v | φ_1.Realize (Sum.elim Subtype.val v)}

Proof state:
case mp.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
⊢ ∃ A0, ↑A0 ⊆ A ∧ ∃ φ_1, {v | φ.Realize (Sum.elim Subtype.val v)} = {v | φ_1.Realize (Sum.elim Subtype.val v)}

Tactic:
refine ⟨A0, by simp [A0], (φ.restrictFreeVar <| fun x => Sum.casesOn x.1
    (fun x hx => Sum.inl ⟨x, by simp [A0, hx]⟩) (fun x _ => Sum.inr x) x.2), ?_⟩

Result:
case mp.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
⊢ {v | φ.Realize (Sum.elim Subtype.val v)} =
    {v |
      Formula.Realize
        (BoundedFormula.restrictFreeVar φ fun x =>
          Sum.casesOn (motive := fun x => x ∈ BoundedFormula.freeVarFinset φ → ↑↑A0 ⊕ α) (↑x)
            (fun x hx => Sum.inl ⟨↑x, ⋯⟩) (fun x x_1 => Sum.inr x) ⋯)
        (Sum.elim Subtype.val v)}

Proof state:
case mp.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
⊢ ∃ A0, ↑A0 ⊆ A ∧ ∃ φ_1, {v | φ.Realize (Sum.elim Subtype.val v)} = {v | φ_1.Realize (Sum.elim Subtype.val v)}

Tactic:
let A0 := (φ.freeVarFinset.toLeft).image Subtype.val

Result:
case mp.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
⊢ ∃ A0, ↑A0 ⊆ A ∧ ∃ φ_1, {v | φ.Realize (Sum.elim Subtype.val v)} = {v | φ_1.Realize (Sum.elim Subtype.val v)}

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
⊢ ↑A0 ⊆ A

Tactic:
simp [A0]

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ ∀ (a : { x // x ∈ BoundedFormula.freeVarFinset φ }),
    Sum.elim Subtype.val x✝
        (Sum.rec (motive := fun x => x ∈ BoundedFormula.freeVarFinset φ → { x // x ∈ A0 } ⊕ α)
          (fun val hx => Sum.inl ⟨↑val, ⋯⟩) (fun val x => Sum.inr val) ↑a ⋯) =
      Sum.elim Subtype.val x✝ ↑a

Tactic:
simp

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : { x // x ∈ BoundedFormula.freeVarFinset φ }
x : ↑A
hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ
⊢ ↑x ∈ ↑A0

Tactic:
simp [A0, hx]

Result:
no goals