mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, (mapTermRel ft fr (fun x ↦ id) f₁✝).Realize v' xs ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, (mapTermRel ft fr (fun x ↦ id) f₂✝).Realize v' xs ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x ↦ id) (f₁✝ ⟹ f₂✝)).Realize v' xs ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
k : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (k + n))
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : {n : ℕ} → (Fin (k + n) → M) → α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs' : Fin (k + n) → M),
    realize (Sum.elim v' xs') (ft n t) = realize (Sum.elim (v xs') (xs' ∘ natAdd k)) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
hv : ∀ (n : ℕ) (xs : Fin (k + n) → M) (x : M), v (snoc xs x) = v xs
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (xs : Fin (k + n✝) → M),
    (mapTermRel ft fr (fun x ↦ castLE ⋯) f₁✝).Realize v' xs ↔ f₁✝.Realize (v xs) (xs ∘ natAdd k)
ih2 :
  ∀ (xs : Fin (k + n✝) → M),
    (mapTermRel ft fr (fun x ↦ castLE ⋯) f₂✝).Realize v' xs ↔ f₂✝.Realize (v xs) (xs ∘ natAdd k)
xs : Fin (k + n✝) → M
⊢ (mapTermRel ft fr (fun x ↦ castLE ⋯) (f₁✝ ⟹ f₂✝)).Realize v' xs ↔ (f₁✝ ⟹ f₂✝).Realize (v xs) (xs ∘ natAdd k)

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {xs : Fin (n✝ + n') → M},
    m ≤ n✝ →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f₁✝).Realize v xs ↔
        f₁✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
ih2 :
  ∀ {xs : Fin (n✝ + n') → M},
    m ≤ n✝ →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f₂✝).Realize v xs ↔
        f₂✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (n✝ + n') → M
hmn : m ≤ n✝
⊢ (mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) (f₁✝ ⟹ f₂✝)).Realize v xs ↔
    (f₁✝ ⟹ f₂✝).Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
f : ↥(rel R✝ ts✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(rel R✝ ts✝).freeVarFinset), v (f a) = v' ↑a
⊢ ((rel R✝ ts✝).restrictFreeVar f).Realize v xs ↔ (rel R✝ ts✝).Realize v' xs

Tactic:
simp only [Realize, restrictFreeVar]
    congr!
    rw [realize_restrictVarLeft v' (by simp [hv'])]
    simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ {f : ↥f₁✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₁✝.freeVarFinset), v (f a) = v' ↑a) → ((f₁✝.restrictFreeVar f).Realize v xs ↔ f₁✝.Realize v' xs)
ih2 :
  ∀ {f : ↥f₂✝.freeVarFinset → β} {xs : Fin n✝ → M},
    (∀ (a : ↥f₂✝.freeVarFinset), v (f a) = v' ↑a) → ((f₂✝.restrictFreeVar f).Realize v xs ↔ f₂✝.Realize v' xs)
f : ↥(f₁✝ ⟹ f₂✝).freeVarFinset → β
xs : Fin n✝ → M
hv' : ∀ (a : ↥(f₁✝ ⟹ f₂✝).freeVarFinset), v (f a) = v' ↑a
⊢ ((f₁✝ ⟹ f₂✝).restrictFreeVar f).Realize v xs ↔ (f₁✝ ⟹ f₂✝).Realize v' xs

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
n : ℕ
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, (φ.onBoundedFormula f₁✝).Realize v xs ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, (φ.onBoundedFormula f₂✝).Realize v xs ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ (φ.onBoundedFormula (f₁✝ ⟹ f₂✝)).Realize v xs ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
s : Set M
⊢ Small.{u, w} ↥⊥

Tactic:
← closure_empty

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
s : Set M
⊢ Small.{u, w} ↥((closure L).toFun ∅)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L.Formula α
⊢ Set.ofPred (φ.onFormula ψ).Realize = Set.ofPred ψ.Realize

Tactic:
ext

Goal state after:
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
ψ : L.Formula α
x✝ : α → M
⊢ x✝ ∈ Set.ofPred (φ.onFormula ψ).Realize ↔ x✝ ∈ Set.ofPred ψ.Realize
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case succ
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∃ xs a, φ.Realize v (snoc xs a)) ↔ ∃ xs, φ.Realize v xs

Tactic:
constructor

Goal state after:
case succ.mp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∃ xs a, φ.Realize v (snoc xs a)) → ∃ xs, φ.Realize v xs

case succ.mpr
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.exs.Realize v ↔ ∃ xs, φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∃ xs, φ.Realize v xs) → ∃ xs a, φ.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ ↑S
⊢ (L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) = S

Tactic:
ext

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
A : Set M
h : A ⊆ ↑S
x✝ : M
⊢ x✝ ∈ (L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) ↔ x✝ ∈ S
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ f.range = Substructure.map f ⊤

Tactic:
ext

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ Substructure.map f ⊤
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
⊢ ⇑f ∘ x = ⇑g ∘ x

Tactic:
ext

Goal state after:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S : L.Substructure M
f g : M →[L] N
n : ℕ
fn : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), x i ∈ {x | f x = g x}
x✝ : Fin n
⊢ (⇑f ∘ x) x✝ = (⇑g ∘ x) x✝
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
⊢ (Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype

Tactic:
ext

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
x✝ : ↥s
⊢ ((Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding) x✝ = (f.comp s.subtype) x✝
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
⊢ f.toHom.range.subtype.comp f.equivRange.toEmbedding = f

Tactic:
ext

Goal state after:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
x✝ : M
⊢ (f.toHom.range.subtype.comp f.equivRange.toEmbedding) x✝ = f x✝
Module: Mathlib.ModelTheory.Definability

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

Tactic:
ext

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ x✝ ∈ ofPred (Formula.Realize (BoundedFormula.constantsVarsEquiv.symm φ)) ↔
    x✝ ∈ {v | Formula.Realize φ (Sum.elim Subtype.val v)}
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
⊢ ∅ = ofPred ⊥.Realize

Tactic:
ext

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
x✝ : α → M
⊢ x✝ ∈ ∅ ↔ x✝ ∈ ofPred ⊥.Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
⊢ univ = ofPred ⊤.Realize

Tactic:
ext

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
x✝ : α → M
⊢ x✝ ∈ univ ↔ x✝ ∈ ofPred ⊤.Realize
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ (v : α ⊕ Fin n✝ → M), f₁✝.toFormula.Realize v ↔ f₁✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
ih2 : ∀ (v : α ⊕ Fin n✝ → M), f₂✝.toFormula.Realize v ↔ f₂✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
⊢ (f₁✝ ⟹ f₂✝).toFormula.Realize v ↔ (f₁✝ ⟹ f₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
⊢ ofPred φ.Realize ∩ ofPred θ.Realize = ofPred (φ ⊓ θ).Realize

Tactic:
ext

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ θ : L[[↑A]].Formula α
x✝ : α → M
⊢ x✝ ∈ ofPred φ.Realize ∩ ofPred θ.Realize ↔ x✝ ∈ ofPred (φ ⊓ θ).Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = ofPred φ.Realize
θ : L[[↑A]].Formula α
hθ : g = ofPred θ.Realize
⊢ f ∪ g = ofPred (φ ⊔ θ).Realize

Tactic:
ext

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = ofPred φ.Realize
θ : L[[↑A]].Formula α
hθ : g = ofPred θ.Realize
x✝ : α → M
⊢ x✝ ∈ f ∪ g ↔ x✝ ∈ ofPred (φ ⊔ θ).Realize
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
⊢ (fun g ↦ g ∘ f) ⁻¹' ofPred φ.Realize = ofPred (Formula.relabel f φ).Realize

Tactic:
ext

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
x✝ : β → M
⊢ x✝ ∈ (fun g ↦ g ∘ f) ⁻¹' ofPred φ.Realize ↔ x✝ ∈ ofPred (Formula.relabel f φ).Realize
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case imp
L : Language
α : Type u'
l : List ((n : ℕ) × L.BoundedFormula α n)
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝⟩ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₂✝⟩ :: listDecode l'
⊢ ∀ (l' : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (⟨n✝, f₁✝ ⟹ f₂✝⟩.snd.listEncode ++ l') = ⟨n✝, f₁✝ ⟹ f₂✝⟩ :: listDecode l'

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: 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

Goal state after:
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
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case mp
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

Goal state after:
case mp
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)}
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) ↔ ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)

Tactic:
constructor

Goal state after:
case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x) → ∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)

case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
m : ℕ
φ : L[[↑A]].Formula (α ⊕ Fin m)
x : α → M
⊢ (∃ xs, BoundedFormula.Realize φ (Sum.elim x xs) (xs ∘ Fin.natAdd m)) → ∃ x_1, φ.Realize x_1 ∧ x_1 ∘ Sum.inl = x
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols ∧ Countable (constantsOn α).Symbols

Tactic:
constructor

Goal state after:
case left
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols

case right
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable (constantsOn α).Symbols
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable α ∧ Countable L.Symbols

Tactic:
constructor

Goal state after:
case left
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable α

case right
L : Language
α : Type u'
inst✝¹ : Countable α
inst✝ : Countable L.Symbols
⊢ Countable L.Symbols
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ (∃ v, M ⊨ equivSentence φ) ↔ M ⊨ φ.exClosure

Tactic:
constructor

Goal state after:
case mp
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ (∃ v, M ⊨ equivSentence φ) → M ⊨ φ.exClosure

case mpr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : DecidableEq α
inst✝ : Nonempty M
φ : L.Formula α
⊢ M ⊨ φ.exClosure → ∃ v, M ⊨ equivSentence φ
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) ↔
    ∃ x_1 ∈ s, x_1 ∘ f = x

Tactic:
constructor

Goal state after:
case intro.intro.mp
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ ((∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))) →
    ∃ x_1 ∈ s, x_1 ∘ f = x

case intro.intro.mpr
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
⊢ (∃ x_1 ∈ s, x_1 ∘ f = x) →
    (∃ a ∈ s,
        ((a ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘
              ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
            Sum.inl =
          x ∘ rangeSplitting f) ∧
      ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case imp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : ∀ {xs : Fin n✝ → M}, f₁✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₁✝.Realize v xs
ih2 : ∀ {xs : Fin n✝ → M}, f₂✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f₂✝.Realize v xs
xs : Fin n✝ → M
⊢ (f₁✝ ⟹ f₂✝).Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ (f₁✝ ⟹ f₂✝).Realize v xs

Tactic:
| imp _ _ ih1 ih2 =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)) ↔ ∀ (x : M), f✝.Realize v (snoc xs x)

Tactic:
constructor

Goal state after:
case all.mp
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)) → ∀ (x : M), f✝.Realize v (snoc xs x)

case all.mpr
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
n : ℕ
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
v : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ {xs : Fin (n✝ + 1) → M}, f✝.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ f✝.Realize v xs
xs : Fin n✝ → M
⊢ (∀ (x : M), f✝.Realize v (snoc xs x)) → ∀ (x : N), f✝.Realize (⇑g ∘ v) (snoc (⇑g ∘ xs) x)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case intro.intro.mpr.refine_1
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ ((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
      Sum.inl =
    (y ∘ f) ∘ rangeSplitting f

Tactic:
ext

Goal state after:
case intro.intro.mpr.refine_1
M : Type w
A : Set M
L : Language
inst✝² : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h✝ : A.Definable L s
f : α → β
inst✝¹ : Finite α
inst✝ : Finite β
val✝¹ : Fintype α
val✝ : Fintype β
h :
  A.Definable L
    ((fun g ↦ g ∘ rangeSplitting f) ⁻¹'
      (fun g ↦ g ∘ Sum.inl) ''
        (fun g ↦ g ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ''
          (fun g ↦ g ∘ ⇑(Equiv.Set.sumCompl (range f))) '' s)
h' : A.Definable L {x | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
x✝ : ↑(range f)
⊢ (((y ∘ ⇑(Equiv.Set.sumCompl (range f))) ∘ ⇑((Equiv.refl ↑(range f)).sumCongr (Fintype.equivFin ↑(range f)ᶜ).symm)) ∘
        Sum.inl)
      x✝ =
    ((y ∘ f) ∘ rangeSplitting f) x✝
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L[[↑A]].Term α
⊢ (Function.tupleGraph fun v ↦ Term.realize v φ) = ofPred ((Term.relabel some φ).equal (var none)).Realize

Tactic:
ext

Goal state after:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L[[↑A]].Term α
x✝ : Option α → M
⊢ (x✝ ∈ Function.tupleGraph fun v ↦ Term.realize v φ) ↔ x✝ ∈ ofPred ((Term.relabel some φ).equal (var none)).Realize