awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s_1 : Finset ι
i : ι
s : Finset ι
h_1 : i ∉ s
h : A.Definable L (s.sup f)
rw : A.Definable L (f i ⊔ s.sup f)
⊢ A.Definable L ((insert i s).sup f)

Tactic:
rw [Finset.sup_insert]

Premises used: Finset.sup_insert
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s_1 : Finset ι
i : ι
s : Finset ι
h_1 : i ∉ s
h : A.Definable L (s.sup f)
⊢ A.Definable L (f i ⊔ s.sup f)

Tactic:
(hf i).union h

Premises used: Set.Definable.union
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s_1 : Finset ι
i : ι
s : Finset ι
h_1 : i ∉ s
h : A.Definable L (s.sup f)
⊢ A.Definable L (f i ⊔ s.sup f)

Tactic:
exact (hf i).union h

Premises used: Set.Definable.union
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
refine : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.sup f)), A.Definable L ((insert i s).sup f)
refine₁ : ∀ (i : ι) (s : Finset ι), i ∉ s → ∀ (h : A.Definable L (s.sup f)), A.Definable L (f i ⊔ s.sup f)
⊢ A.Definable L (s.sup f)

Tactic:
classical
    refine Finset.induction definable_empty (fun i s _ h => ?_) s
    rw [Finset.sup_insert]
    exact (hf i).union h

Premises used: Finset.sup_insert
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
rw : A.Definable L (s.inf f)
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋂ i ∈ s, f i)

Tactic:
rw [← Finset.inf_set_eq_iInter]

Premises used: Finset.inf_set_eq_iInter
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
definable_finset_inf hf s

Premises used: Set.definable_finset_inf
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
exact definable_finset_inf hf s

Premises used: Set.definable_finset_inf
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
rw : A.Definable L (s.sup f)
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋃ i ∈ s, f i)

Tactic:
rw [← Finset.sup_set_eq_biUnion]

Premises used: Finset.sup_set_eq_biUnion
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)

Tactic:
definable_finset_sup hf s

Premises used: Set.definable_finset_sup
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.sup f)

Tactic:
exact definable_finset_sup hf s

Premises used: Set.definable_finset_sup
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
haveI : ∀ (this : Fintype ι), Definable.{u, v, w, u₁} A L (α := α) (⋂ (i : ι), f i)
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋂ (i : ι), f i)

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
⊢ A.Definable L (Finset.inf Finset.univ f)

Tactic:
definable_finset_inf hf Finset.univ

Premises used: Finset.univ, Set.definable_finset_inf
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
h : ⋂ (i : ι), f i = Finset.inf Finset.univ f
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋂ (i : ι), f i)

Tactic:
convert! definable_finset_inf hf Finset.univ using 1

Premises used: Finset.univ, Set.definable_finset_inf
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
⊢ ⋂ (i : ι), f i = Finset.inf Finset.univ f

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
haveI : ∀ (this : Fintype ι), Definable.{u, v, w, u₁} A L (α := α) (⋃ (i : ι), f i)
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋃ (i : ι), f i)

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
⊢ A.Definable L (Finset.sup Finset.univ f)

Tactic:
definable_finset_sup hf Finset.univ

Premises used: Finset.univ, Set.definable_finset_sup
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
h : ⋃ (i : ι), f i = Finset.sup Finset.univ f
⊢ Definable.{u, v, w, u₁} A L (α := α) (⋃ (i : ι), f i)

Tactic:
convert! definable_finset_sup hf Finset.univ using 1

Premises used: Finset.univ, Set.definable_finset_sup
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
ι : Type u_2
inst_1 : Finite ι
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
this : Fintype ι
⊢ ⋃ (i : ι), f i = Finset.sup Finset.univ f

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
hf : A.Definable L s
rcases : ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α) (hφ : s = setOf φ.Realize), A.Definable L sᶜ
⊢ A.Definable L sᶜ

Tactic:
rcases hf with ⟨φ, hφ⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
⊢ A.Definable L sᶜ

Tactic:
⟨φ.not, ?_⟩

Premises used: Set.Definable, FirstOrder.Language.Formula.not, Exists.intro
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
refine : sᶜ = setOf φ.not.Realize
⊢ A.Definable L sᶜ

Tactic:
refine ⟨φ.not, ?_⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
h : ∀ (v : α → M), v ∈ sᶜ ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
⊢ sᶜ = setOf φ.not.Realize

Tactic:
ext v
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
hφ : s = setOf φ.Realize
v : α → M
h : Membership.mem (γ := Set (α → M)) (setOf φ.Realize)ᶜ v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₁ :
  Membership.mem (γ := Set (α → M)) {a : α → M | ¬φ.Realize a} v ↔
    Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₂ : ¬φ.Realize v ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v
h₃ : ¬φ.Realize v ↔ φ.not.Realize v
h₄ h₅ : ¬φ.Realize v ↔ ¬φ.Realize v
⊢ v ∈ sᶜ ↔ Membership.mem (γ := Set (α → M)) (setOf φ.not.Realize) v

Tactic:
rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]

Premises used: Set.mem_setOf, FirstOrder.Language.Formula.realize_not, Set.compl_setOf
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (s \ t)

Tactic:
hs.inter ht.compl

Premises used: Set.Definable.inter, Set.Definable.compl, Set.Mem, Set.diff, setOf, Not
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
rw : A.Definable L (t ⊔ sᶜ)
⊢ A.Definable L (s ⇨ t)

Tactic:
rw [himp_eq]

Premises used: himp_eq
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (t ⊔ sᶜ)

Tactic:
ht.union hs.compl

Premises used: Set.Definable.union, Set.Definable.compl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s t : Set (α → M)
hs : A.Definable L s
ht : A.Definable L t
⊢ A.Definable L (t ⊔ sᶜ)

Tactic:
exact ht.union hs.compl

Premises used: Set.Definable.union, Set.Definable.compl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
s : Set (α → M)
h : A.Definable L s
obtain :
  ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α),
    Definable.{u, v, w, u_1} A L (α := β) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))
⊢ Definable.{u, v, w, u_1} A L (α := β) ((fun (g : β → M) ↦ g ∘ f) ⁻¹' s)

Tactic:
obtain ⟨φ, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
⊢ Definable.{u, v, w, u_1} A L (α := β) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))

Tactic:
⟨φ.relabel f, ?_⟩

Premises used: Set.Definable, FirstOrder.Language.Formula.relabel, Exists.intro
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
refine :
  Eq (α := Set (β → M)) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))
    (setOf (Formula.relabel f φ).Realize)
⊢ Definable.{u, v, w, u_1} A L (α := β) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))

Tactic:
refine ⟨φ.relabel f, ?_⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
h :
  ∀ (x : β → M),
    Membership.mem (γ := Set (β → M)) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize)) x ↔
      Membership.mem (γ := Set (β → M)) (setOf (Formula.relabel f φ).Realize) x
⊢ Eq (α := Set (β → M)) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize))
    (setOf (Formula.relabel f φ).Realize)

Tactic:
ext
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
x : β → M
⊢ Membership.mem (γ := Set (β → M)) (preimage (β := α → M) (fun (g : β → M) ↦ g ∘ f) (setOf φ.Realize)) x ↔
    Membership.mem (γ := Set (β → M)) (setOf (Formula.relabel f φ).Realize) x

Tactic:
simp only [Set.preimage_setOf_eq, mem_setOf_eq, Formula.realize_relabel]

Premises used: Set.mem_setOf_eq, FirstOrder.Language.Formula.realize_relabel, Set.preimage_setOf_eq
-- Module: Mathlib.ModelTheory.Definability
Goal:
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 : α ≃ β
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)

Tactic:
(congr rfl ?_).mp (h.preimage_comp f.symm)

Premises used: Set.Definable.preimage_comp, Eq.mp, congr, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
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 : α ≃ β
refine :
  Eq (α := Set (α → M)) ((fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) ⁻¹' s)
    ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)
⊢ Definable.{u, v, w, u₁} A L (α := α) ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)

Tactic:
refine (congr rfl ?_).mp (h.preimage_comp f.symm)

Premises used: Set.Definable.preimage_comp, Eq.mp, congr, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
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 : α ≃ β
h₁ : Function.LeftInverse (fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)
h₂ : Function.RightInverse (fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)
⊢ Eq (α := Set (α → M)) ((fun (g : α → M) ↦ g ∘ (⇑f.symm : (a : β) → α)) ⁻¹' s)
    ((fun (g : β → M) ↦ g ∘ (⇑f : (a : α) → β)) '' s)

Tactic:
rw [image_eq_preimage_of_inverse]

Premises used: Set.image_eq_preimage_of_inverse
-- Module: Mathlib.ModelTheory.Definability
Goal:
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 : α ≃ β
i : β → M
h₁ :
  ∀ (b : β),
    (fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) ((fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) i)
        b =
      i b
⊢ (fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) ((fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) i) = i

Tactic:
ext b
-- Module: Mathlib.ModelTheory.Definability
Goal:
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 : α ≃ β
i : β → M
b : β
⊢ (fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) ((fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) i) b =
    i b

Tactic:
simp only [Function.comp_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Function.comp_apply
-- Module: Mathlib.ModelTheory.Definability
Goal:
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 : α ≃ β
i : α → M
h₂ :
  ∀ (a : α),
    (fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) ((fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) i)
        a =
      i a
⊢ (fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) ((fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) i) = i

Tactic:
ext a
-- Module: Mathlib.ModelTheory.Definability
Goal:
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 : α ≃ β
i : α → M
a : α
⊢ (fun (g : β → M) ↦ (g ∘ (⇑f : (a : α) → β) : α → M)) ((fun (g : α → M) ↦ (g ∘ (⇑f.symm : (a : β) → α) : β → M)) i) a =
    i a

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
mp : A.Definable L s → ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s
mpr : (∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s) → A.Definable L s
⊢ A.Definable L s ↔ ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
mp :
  (∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
      s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}) →
    ∃ (A0 : Finset M),
      (↑A0 : Set M) ⊆ A ∧
        ∃ (φ : L.Formula (Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)),
          s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
⊢ A.Definable L s → ∃ (A0 : Finset M), (↑A0 : Set M) ⊆ A ∧ (↑A0 : Set M).Definable L s

Tactic:
simp only [definable_iff_exists_formula_sum]

Premises used: Set.definable_iff_exists_formula_sum
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
⊢ (↑A0 : Set M) ⊆ A

Tactic:
simp [A0]
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
x_1 : ↥(BoundedFormula.freeVarFinset φ)
x : (↑A : Type w)
hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ
⊢ (↑x : M) ∈ (↑A0 : Set M)

Tactic:
simp [A0, hx]
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
mp :
  Eq (α := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
    {v : α → M |
      Formula.Realize (α := Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)
        (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
          Sum.casesOn (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
            x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α) (↑x : (↑A : Type w) ⊕ α)
            (fun (x : (↑A : Type w)) (hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ) ↦
              Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑x : M) ⋯))
            (fun (x : α) (x_1 : Sum.inr x ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr x) ⋯)
        (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
⊢ ∃ (A0 : Finset M),
    (↑A0 : Set M) ⊆ A ∧
      ∃ (φ_1 : L.Formula (Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)),
        Eq (α := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
          {v : α → M | φ_1.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) 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), ?_⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
mp :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)} x ↔
      Membership.mem (γ := Set (α → M))
        {v : α → M |
          Formula.Realize (α := Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)
            (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
              Sum.casesOn (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
                x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α) (↑x : (↑A : Type w) ⊕ α)
                (fun (x : (↑A : Type w)) (hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ) ↦
                  Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑x : M) ⋯))
                (fun (x : α) (x_1 : Sum.inr x ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr x) ⋯)
            (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
        x
⊢ Eq (α := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
    {v : α → M |
      Formula.Realize (α := Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)
        (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
          Sum.casesOn (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
            x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α) (↑x : (↑A : Type w) ⊕ α)
            (fun (x : (↑A : Type w)) (hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ) ↦
              Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑x : M) ⋯))
            (fun (x : α) (x_1 : Sum.inr x ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr x) ⋯)
        (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}

Tactic:
ext
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
x : α → M
mp :
  BoundedFormula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x) default ↔
    BoundedFormula.Realize (α := Sum.{w, u₁} (↥A0) α)
      (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
        Sum.rec (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
          x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↥A0) α)
          (fun (val : (↑A : Type w)) (hx : Sum.inl val ∈ BoundedFormula.freeVarFinset φ) ↦
            Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑val : M) ⋯))
          (fun (val : α) (x : Sum.inr val ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr val) (↑x : (↑A : Type w) ⊕ α) ⋯)
      (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) x) default
⊢ Membership.mem (γ := Set (α → M)) {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)} x ↔
    Membership.mem (γ := Set (α → M))
      {v : α → M |
        Formula.Realize (α := Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α)
          (BoundedFormula.restrictFreeVar φ fun (x : ↥(BoundedFormula.freeVarFinset φ)) ↦
            Sum.casesOn (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
              x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↑(↑A0 : Set M) : Type w) α) (↑x : (↑A : Type w) ⊕ α)
              (fun (x : (↑A : Type w)) (hx : Sum.inl x ∈ BoundedFormula.freeVarFinset φ) ↦
                Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑x : M) ⋯))
              (fun (x : α) (x_1 : Sum.inr x ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr x) ⋯)
          (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) v)}
      x

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

Premises used: Finset.coe_sort_coe, Set.mem_setOf_eq, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)
A0 : Finset M := Finset.image (Subtype.val (p := fun (x : M) ↦ x ∈ A)) (BoundedFormula.freeVarFinset φ).toLeft
x : α → M
⊢ ∀ (a : ↥(BoundedFormula.freeVarFinset φ)),
    Sum.elim (α := ↥A0) (Subtype.val (p := fun (x : M) ↦ x ∈ (↑A0 : Set M))) x
        (Sum.rec (motive := fun (x : Sum.{w, u₁} (↑A : Type w) α) ↦
          x ∈ BoundedFormula.freeVarFinset φ → Sum.{w, u₁} (↥A0) α)
          (fun (val : (↑A : Type w)) (hx : Sum.inl val ∈ BoundedFormula.freeVarFinset φ) ↦
            Sum.inl (Subtype.mk (p := fun (x : M) ↦ x ∈ (↑A0 : Set M)) (↑val : M) ⋯))
          (fun (val : α) (x : Sum.inr val ∈ BoundedFormula.freeVarFinset φ) ↦ Sum.inr val) (↑a : (↑A : Type w) ⊕ α) ⋯) =
      Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) x (↑a : (↑A : Type w) ⊕ α)

Tactic:
simp