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_1
s : Set (β → M)
h_1 : A.Definable L s
f : α → β
inst_1 : Finite α
inst_2 : Finite β
val : Fintype α
val_1 : Fintype β
h :
  Definable.{u, v, w, u₁} A L (α := α)
    (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
      ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
        (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
            g ∘
              (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                    (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                  (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
          (fun (g : β → M) ↦
              g ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
            s))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
x : α → M
hx : ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))
y : β → M
ys : y ∈ s
hy :
  Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
      (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
        (y ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
        (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
              (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
          (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
            (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
      Sum.inl =
    x ∘ rangeSplitting f
a : α
⊢ (y ∘ f) a =
    Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
      (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
        (y ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
        (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
              (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
          (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
            (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
      Sum.inl (rangeFactorization f a)

Tactic:
simp
-- 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_1 : A.Definable L s
f : α → β
inst_1 : Finite α
inst_2 : Finite β
val : Fintype α
val_1 : Fintype β
h :
  Definable.{u, v, w, u₁} A L (α := α)
    (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
      ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
        (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
            g ∘
              (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                    (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                  (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
          (fun (g : β → M) ↦
              g ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
            s))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
⊢ (∃ a ∈ s,
      Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
          (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
            (a ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
            (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                  (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
              (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
          Sum.inl =
        (y ∘ f) ∘ rangeSplitting f) ∧
    ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))

Tactic:
⟨⟨y, ys, ?_⟩, fun a => ?_⟩

Premises used: And.intro, Exists.intro
-- 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_1 : A.Definable L s
f : α → β
inst_1 : Finite α
inst_2 : Finite β
val : Fintype α
val_1 : Fintype β
h :
  Definable.{u, v, w, u₁} A L (α := α)
    (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
      ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
        (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
            g ∘
              (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                    (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                  (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
          (fun (g : β → M) ↦
              g ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
            s))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
intro :
  Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
      (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
        (y ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
        (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
              (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
          (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
            (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
      Sum.inl =
    (y ∘ f) ∘ rangeSplitting f
intro₁ : ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
⊢ (∃ a ∈ s,
      Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
          (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
            (a ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
            (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                  (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
              (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
          Sum.inl =
        (y ∘ f) ∘ rangeSplitting f) ∧
    ∀ (a : α), (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))

Tactic:
refine ⟨⟨y, ys, ?_⟩, fun 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_1 : A.Definable L s
f : α → β
inst_1 : Finite α
inst_2 : Finite β
val : Fintype α
val_1 : Fintype β
h :
  Definable.{u, v, w, u₁} A L (α := α)
    (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
      ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
        (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
            g ∘
              (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                    (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                  (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
          (fun (g : β → M) ↦
              g ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
            s))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
intro :
  ∀ (x : (↑(range f) : Type u_1)),
    Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
        (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
          (y ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
          (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
            (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
              (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
        Sum.inl x =
      ((y ∘ f) ∘ rangeSplitting f) x
⊢ Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
      (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
        (y ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
        (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
              (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
          (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
            (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
      Sum.inl =
    (y ∘ f) ∘ rangeSplitting f

Tactic:
ext
-- 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_1 : A.Definable L s
f : α → β
inst_1 : Finite α
inst_2 : Finite β
val : Fintype α
val_1 : Fintype β
h :
  Definable.{u, v, w, u₁} A L (α := α)
    (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
      ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
        (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
            g ∘
              (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                    (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                  (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
          (fun (g : β → M) ↦
              g ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
            s))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
x : (↑(range f) : Type u_1)
⊢ Function.comp (β := (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)))
      (Function.comp (β := (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))
        (y ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β))
        (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
              (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
          (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
            (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)))
      Sum.inl x =
    ((y ∘ f) ∘ rangeSplitting f) x

Tactic:
simp [Set.apply_rangeSplitting f]

Premises used: Set.apply_rangeSplitting
-- 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_1 : A.Definable L s
f : α → β
inst_1 : Finite α
inst_2 : Finite β
val : Fintype α
val_1 : Fintype β
h :
  Definable.{u, v, w, u₁} A L (α := α)
    (preimage (β := (↑(range f) : Type u_1) → M) (fun (g : α → M) ↦ g ∘ rangeSplitting f)
      ((fun (g : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card.{u_1} (↑(range f)ᶜ : Type u_1)) → M) ↦ g ∘ Sum.inl) ''
        (fun (g : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1) → M) ↦
            g ∘
              (⇑(Equiv.sumCongr (Equiv.refl (↑(range f) : Type u_1))
                    (Equiv.symm (Fintype.equivFin (↑(range f)ᶜ : Type u_1)))) :
                (a : (↑(range f) : Type u_1) ⊕ Fin (Fintype.card (↑(range f)ᶜ : Type u_1))) →
                  (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1))) ''
          (fun (g : β → M) ↦
              g ∘ (⇑(Equiv.Set.sumCompl (range f)) : (a : (↑(range f) : Type u_1) ⊕ (↑(range f)ᶜ : Type u_1)) → β)) ''
            s))
h' : Definable.{u, v, w, u₁} A L (α := α) {x : α → M | ∀ (a : α), x a = x (rangeSplitting f (rangeFactorization f a))}
y : β → M
ys : y ∈ s
a : α
intro : y (f a) = (y ∘ f) (rangeSplitting f (rangeFactorization f a))
intro₁ : y (f a) = y (f (rangeSplitting f (rangeFactorization f a)))
intro₂ : y (f a) = y (↑(rangeFactorization f a) : β)
intro₃ intro₄ : y (f a) = y (f a)
⊢ (y ∘ f) a = (y ∘ f) (rangeSplitting f (rangeFactorization f a))

Tactic:
rw [Function.comp_apply, Function.comp_apply, apply_rangeSplitting f,
          rangeFactorization_coe]

Premises used: Set.rangeFactorization_coe, Function.comp_apply, Set.apply_rangeSplitting
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
inst_1 : Finite β
S : Set (α ⊕ β → M)
hS : A.Definable L S
obtain :
  ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)) (hφ : S = setOf φ.Realize),
    Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S}
⊢ Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S}

Tactic:
obtain ⟨φ, hφ⟩ := hS
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
exists : Eq (α := Set (α → M)) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S} (setOf (Formula.iExs β φ).Realize)
⊢ Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S}

Tactic:
exists φ.iExs β

Premises used: FirstOrder.Language.Formula.iExs
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
h :
  ∀ (v : α → M),
    Membership.mem (γ := Set (α → M)) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S} v ↔
      Membership.mem (γ := Set (α → M)) (setOf (Formula.iExs β φ).Realize) v
⊢ Eq (α := Set (α → M)) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S} (setOf (Formula.iExs β φ).Realize)

Tactic:
ext v
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
v : α → M
⊢ Membership.mem (γ := Set (α → M)) {v : α → M | ∃ (u : β → M), Sum.elim v u ∈ S} v ↔
    Membership.mem (γ := Set (α → M)) (setOf (Formula.iExs β φ).Realize) v

Tactic:
simp [hφ]
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
inst_1 : Finite β
S : Set (α ⊕ β → M)
hS : A.Definable L S
obtain :
  ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)) (hφ : S = setOf φ.Realize),
    Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S}
⊢ Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S}

Tactic:
obtain ⟨φ, hφ⟩ := hS
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
exists : Eq (α := Set (α → M)) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S} (setOf (Formula.iAlls β φ).Realize)
⊢ Definable.{u, v, w, u₁} A L (α := α) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S}

Tactic:
exists φ.iAlls β

Premises used: FirstOrder.Language.Formula.iAlls
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
h :
  ∀ (v : α → M),
    Membership.mem (γ := Set (α → M)) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S} v ↔
      Membership.mem (γ := Set (α → M)) (setOf (Formula.iAlls β φ).Realize) v
⊢ Eq (α := Set (α → M)) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S} (setOf (Formula.iAlls β φ).Realize)

Tactic:
ext v
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
inst_1 : Finite β
S : Set (α ⊕ β → M)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Formula (α ⊕ β)
hφ : S = setOf φ.Realize
v : α → M
⊢ Membership.mem (γ := Set (α → M)) {v : α → M | ∀ (u : β → M), Sum.elim v u ∈ S} v ↔
    Membership.mem (γ := Set (α → M)) (setOf (Formula.iAlls β φ).Realize) v

Tactic:
simp [hφ]
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
L : Language
inst : L.Structure M
a : M
exists exists₁ :
  Eq.{w + 1} (α := Set (Fin 1 → M)) {x : Fin 1 → M | Membership.mem (γ := Set M) {a} (x 0)}
    (setOf
      (Formula.Realize
        (Term.equal (var 0) (L.con (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Set M) {a} x) a ⋯)).term)))
⊢ Definable₁ (M := M) {a} L {a}

Tactic:
exists (Term.var 0).equal (L.con (⟨a, rfl⟩ : ↑({a} : Set M))).term

Premises used: FirstOrder.Language.Constants.term, FirstOrder.Language.Term.equal, Subtype.mk, FirstOrder.Language.con, FirstOrder.Language.Term.var, OfNat.ofNat, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
L : Language
inst : L.Structure M
a : M
A : Set M
ha : a ∈ A
⊢ A.Definable₁ L {a}

Tactic:
(Definable.singleton L a).mono (Set.singleton_subset_iff.mpr ha)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.Definable.singleton, Set.Definable₁, Set.Definable.mono
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
L : Language
inst : L.Structure M
A : Set M
exists exists₁ :
  Eq.{w + 1} (α := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Set.diagonal M}
    (setOf (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w)) (Term.equal (var 0) (var 1))))
⊢ A.Definable₂ L (Set.diagonal M)

Tactic:
exists (Term.var 0).equal (Term.var 1)

Premises used: FirstOrder.Language.Term.equal, FirstOrder.Language.Term.var, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s t : L.DefinableSet A α
⊢ s ≤ t ↔ (↑s : Set (α → M)) ≤ (↑t : Set (α → M))

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
x : α → M
⊢ Membership.mem (γ := L.DefinableSet A α) ⊤ x

Tactic:
mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
x : α → M
⊢ x ∉ ⊥

Tactic:
notMem_empty x

Premises used: Set.Mem, Set.notMem_empty
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s t : L.DefinableSet A α
x : α → M
⊢ x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t

Tactic:
Iff.rfl

Premises used: Set.union, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s t : L.DefinableSet A α
x : α → M
⊢ x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s : L.DefinableSet A α
x : α → M
⊢ x ∈ sᶜ ↔ x ∉ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s t : L.DefinableSet A α
x : α → M
⊢ x ∈ s \ t ↔ x ∈ s ∧ x ∉ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Set.diff, Iff.rfl, setOf
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
⊢ (↑⊤ : Set (α → M)) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
⊢ (↑⊥ : Set (α → M)) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s t : L.DefinableSet A α
⊢ (↑(s ⊔ t) : Set (α → M)) = (↑s : Set (α → M)) ∪ (↑t : Set (α → M))

Tactic:
rfl

Premises used: Set.union, setOf, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s t : L.DefinableSet A α
⊢ (↑(s ⊓ t) : Set (α → M)) = (↑s : Set (α → M)) ∩ (↑t : Set (α → M))

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s : L.DefinableSet A α
⊢ (↑sᶜ : Set (α → M)) = (↑s : Set (α → M))ᶜ

Tactic:
rfl

Premises used: setOf, Not, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s t : L.DefinableSet A α
⊢ (↑(s \ t) : Set (α → M)) = (↑s : Set (α → M)) \ (↑t : Set (α → M))

Tactic:
rfl

Premises used: Set.diff, setOf, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
L : Language
M : Type w
inst : L.Structure M
A : Set M
α : Type u₁
s t : L.DefinableSet A α
⊢ (↑(s ⇨ t) : Set (α → M)) = (↑s : Set (α → M)) ⇨ (↑t : Set (α → M))

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
B : Set M
hAs : DefinableFun L A f
hAB : A ⊆ B
⊢ DefinableFun L B f

Tactic:
Set.Definable.mono hAs hAB

Premises used: Set.Definable.mono, Set.DefinableFun
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
hAs : DefinableFun L ∅ f
⊢ DefinableFun L A f

Tactic:
Set.Definable.mono hAs (empty_subset A)

Premises used: Set.empty_subset, Set.Definable.mono, Set.DefinableFun
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
f : (α → M) → M
⊢ DefinableFun L ∅ f ↔ ∃ (φ : Formula.{u_4, u_5, u_2} L (Option α)), tupleGraph f = setOf φ.Realize

Tactic:
simp [DefinableFun, Set.empty_definable_iff]

Premises used: Set.empty_definable_iff, Set.DefinableFun
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
⊢ DefinableFun L A f ↔ DefinableFun (withConstants.{u_4, u_5, u_1} L (↑A : Type u_1)) ∅ f

Tactic:
empty_definable_iff.symm

Premises used: Set.empty_definable_iff, Set.Definable, setOf, Iff.symm, Set.DefinableFun
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
t : L.Term α
rw :
  ∃ (φ : Formula.{u_4, u_5, u_2} L (Option α)),
    Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t) (setOf φ.Realize)
⊢ DefinableFun.{u_1, u_2, u_4, u_5} (M := M) L (α := α) ∅ fun (v : α → M) ↦ Term.realize v t

Tactic:
rw [empty_definableFun_iff]

Premises used: Set.empty_definableFun_iff