awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
t : L.Term α
⊢ ∃ (φ : Formula.{u_4, u_5, u_2} L (Option α)),
    Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t) (setOf φ.Realize)

Tactic:
⟨(t.relabel some).equal (Term.var none), ?_⟩

Premises used: FirstOrder.Language.Term.relabel, Option.some, FirstOrder.Language.Term.equal, Option.none, FirstOrder.Language.Term.var, Exists.intro
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
t : L.Term α
refine :
  Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t)
    (setOf ((Term.relabel some t).equal (var none)).Realize)
⊢ ∃ (φ : Formula.{u_4, u_5, u_2} L (Option α)),
    Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t) (setOf φ.Realize)

Tactic:
refine ⟨(t.relabel some).equal (Term.var none), ?_⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
t : L.Term α
h :
  ∀ (v : Option α → M),
    Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t) v ↔
      Membership.mem (γ := Set (Option α → M)) (setOf ((Term.relabel some t).equal (var none)).Realize) v
⊢ Eq (α := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t)
    (setOf ((Term.relabel some t).equal (var none)).Realize)

Tactic:
ext v
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
t : L.Term α
v : Option α → M
⊢ Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ Term.realize v t) v ↔
    Membership.mem (γ := Set (Option α → M)) (setOf ((Term.relabel some t).equal (var none)).Realize) v

Tactic:
simp [tupleGraph]

Premises used: Function.tupleGraph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
n : ℕ
f : L.Functions n
⊢ DefinableFun.{u_1, 0, u_4, u_5} (M := M) L ∅ (Structure.funMap f)

Tactic:
(Term.func f Term.var).definableFun_realize

Premises used: FirstOrder.Language.Term.definableFun_realize, FirstOrder.Language.Term.func, FirstOrder.Language.Term.var, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
i : α
⊢ DefinableFun.{u_1, u_2, u_4, u_5} (M := M) L (α := α) ∅ fun (v : α → M) ↦ v i

Tactic:
(Term.var i).definableFun_realize

Premises used: FirstOrder.Language.Term.definableFun_realize, FirstOrder.Language.Term.var, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
i : α
⊢ DefinableFun.{u_1, u_2, u_4, u_5} L (α := α) A fun (v : α → M) ↦ v i

Tactic:
of_empty <| L.definableFun_var i

Premises used: Set.DefinableFun.of_empty, FirstOrder.Language.definableFun_var
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
rw : DefinableFun (M := M) (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)) (α := γ) ∅ fun (x : γ → M) ↦ a
⊢ DefinableFun.{u_1, u_4, u_5, u_6} L (α := γ) A fun (x : γ → M) ↦ a

Tactic:
rw [definableFun_iff_empty_definableFun_with_params]

Premises used: Set.definableFun_iff_empty_definableFun_with_params
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
⊢ DefinableFun (M := M) (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)) (α := γ) ∅ fun (x : γ → M) ↦ a

Tactic:
((L.con (⟨a,ha⟩ : ↑A)).term).definableFun_realize

Premises used: FirstOrder.Language.Constants.term, FirstOrder.Language.Term.definableFun_realize, Subtype.mk, FirstOrder.Language.con, FirstOrder.Language.Term.realize, Sum.elim
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
a : M
γ : Type u_4
ha : a ∈ A
⊢ DefinableFun (M := M) (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)) (α := γ) ∅ fun (x : γ → M) ↦ a

Tactic:
exact ((L.con (⟨a,ha⟩ : ↑A)).term).definableFun_realize

Premises used: FirstOrder.Language.Constants.term, FirstOrder.Language.Term.definableFun_realize, Subtype.mk, FirstOrder.Language.con
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
rw : A.Definable L (α := α ⊕ β) (⋂ (i : β), {x : α ⊕ β → M | F (x ∘ Sum.inl) i = x (Sum.inr i)})
⊢ A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}

Tactic:
rw [setOf_forall]

Premises used: Set.setOf_forall
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
⊢ A.Definable L (α := α ⊕ β) (⋂ (i : β), {x : α ⊕ β → M | F (x ∘ Sum.inl) i = x (Sum.inr i)})

Tactic:
definable_iInter_of_finite fun i => ?_

Premises used: Set.definable_iInter_of_finite
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
refine : ∀ (i : β), A.Definable L (α := α ⊕ β) {x : α ⊕ β → M | F (x ∘ Sum.inl) i = x (Sum.inr i)}
⊢ A.Definable L (α := α ⊕ β) (⋂ (i : β), {x : α ⊕ β → M | F (x ∘ Sum.inl) i = x (Sum.inr i)})

Tactic:
refine definable_iInter_of_finite fun i => ?_

Premises used: Set.definable_iInter_of_finite
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
i : β
⊢ A.Definable L (α := α ⊕ β) {x : α ⊕ β → M | F (x ∘ Sum.inl) i = x (Sum.inr i)}

Tactic:
simpa [tupleGraph] using
      (hF i).preimage_comp (fun | none => Sum.inr i | some j => Sum.inl j)

Premises used: Set.Definable.preimage_comp, Function.tupleGraph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
⊢ A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}

Tactic:
have h_graph : A.Definable L { w : α ⊕ β → M | ∀ i, F (w ∘ Sum.inl) i = w (Sum.inr i) } := by
    rw [setOf_forall]
    refine definable_iInter_of_finite fun i => ?_
    simpa [tupleGraph] using
      (hF i).preimage_comp (fun | none => Sum.inr i | some j => Sum.inl j)
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
⊢ A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | w ∘ Sum.inr ∈ S}

Tactic:
have h_cyl : A.Definable L { w : α ⊕ β → M | w ∘ Sum.inr ∈ S } :=
    hS.preimage_comp Sum.inr
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | w ∘ Sum.inr ∈ S}
⊢ Definable.{u_6, u_7, u_1, u_4} A L (α := α)
    {v : α → M |
      ∃ (u : β → M),
        Membership.mem (γ := Set (α ⊕ β → M))
          ({w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w : α ⊕ β → M | w ∘ Sum.inr ∈ S})
          (Sum.elim v u)}

Tactic:
Definable.exists_of_finite (Definable.inter h_graph h_cyl)

Premises used: Set.Definable.inter, Set.Definable.exists_of_finite
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | w ∘ Sum.inr ∈ S}
h :
  F ⁻¹' S =
    {v : α → M |
      ∃ (u : β → M),
        Membership.mem (γ := Set (α ⊕ β → M))
          ({w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w : α ⊕ β → M | w ∘ Sum.inr ∈ S})
          (Sum.elim v u)}
⊢ A.Definable L (F ⁻¹' S)

Tactic:
convert! Definable.exists_of_finite (Definable.inter h_graph h_cyl) using 1

Premises used: Set.Definable.inter, Set.Definable.exists_of_finite
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | w ∘ Sum.inr ∈ S}
h :
  ∀ (v : α → M),
    v ∈ F ⁻¹' S ↔
      Membership.mem (γ := Set (α → M))
        {v : α → M |
          ∃ (u : β → M),
            Membership.mem (γ := Set (α ⊕ β → M))
              ({w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w : α ⊕ β → M | w ∘ Sum.inr ∈ S})
              (Sum.elim v u)}
        v
⊢ F ⁻¹' S =
    {v : α → M |
      ∃ (u : β → M),
        Membership.mem (γ := Set (α ⊕ β → M))
          ({w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w : α ⊕ β → M | w ∘ Sum.inr ∈ S})
          (Sum.elim v u)}

Tactic:
ext v
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
A : Set M
α : Type u_4
β : Type u_5
inst_1 : Finite β
F : (α → M) → β → M
hF : DefinableMap L A F
S : Set (β → M)
hS : A.Definable L S
h_graph : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)}
h_cyl : A.Definable L (α := α ⊕ β) {w : α ⊕ β → M | w ∘ Sum.inr ∈ S}
v : α → M
⊢ v ∈ F ⁻¹' S ↔
    Membership.mem (γ := Set (α → M))
      {v : α → M |
        ∃ (u : β → M),
          Membership.mem (γ := Set (α ⊕ β → M))
            ({w : α ⊕ β → M | ∀ (i : β), F (w ∘ Sum.inl) i = w (Sum.inr i)} ∩ {w : α ⊕ β → M | w ∘ Sum.inr ∈ S})
            (Sum.elim v u)}
      v

Tactic:
simp [← funext_iff]

Premises used: funext_iff
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst_1 : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun (w : Option β → M) (j : Option α) ↦
    match (motive := Option α → M) j with
    | none => w none
    | some i => g (w ∘ some) i
⊢ DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x none

Tactic:
fun_prop
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst_1 : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun (w : Option β → M) (j : Option α) ↦
    match (motive := Option α → M) j with
    | none => w none
    | some i => g (w ∘ some) i
j : α
⊢ DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x (some j)

Tactic:
simpa [tupleGraph] using
        ((hg j).preimage_comp fun | none => none | some i => some (some i))

Premises used: Set.Definable.preimage_comp, Function.tupleGraph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst_1 : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun (w : Option β → M) (j : Option α) ↦
    match (motive := Option α → M) j with
    | Option.none => w Option.none
    | Option.some i => g (w ∘ Option.some) i
i : Option α
none : DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x Option.none
some : ∀ (j : α), DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x (Option.some j)
⊢ DefinableFun.{u_1, u_3, u_4, u_5} L (α := Option β) A fun (x : Option β → M) ↦ G x i

Tactic:
cases i with
    | none => fun_prop
    | some j =>
      simpa [tupleGraph] using
        ((hg j).preimage_comp fun | none => none | some i => some (some i))

Premises used: Option.some, Option.none, Function.tupleGraph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst_1 : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun (w : Option β → M) (j : Option α) ↦
    match (motive := Option α → M) j with
    | none => w none
    | some i => g (w ∘ some) i
⊢ DefinableMap L A G

Tactic:
have hG : A.DefinableMap L G := by
    intro i
    cases i with
    | none => fun_prop
    | some j =>
      simpa [tupleGraph] using
        ((hg j).preimage_comp fun | none => none | some i => some (some i))
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst_1 : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun (w : Option β → M) (j : Option α) ↦
    match (motive := Option α → M) j with
    | none => w none
    | some i => g (w ∘ some) i
hG : DefinableMap L A G
⊢ DefinableFun.{u_1, u_3, u_4, u_5} L (α := β) A fun (v : β → M) ↦ f (g v)

Tactic:
simpa [DefinableFun, G, tupleGraph] using hf.preimage_map hG

Premises used: Function.tupleGraph, Set.Definable.preimage_map, 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
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
⊢ A.Definable L P

Tactic:
have hP : A.Definable L P := hp.preimage_comp some
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
⊢ A.Definable L (P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g)

Tactic:
(hP.inter hf).union (hP.compl.inter hg)

Premises used: Set.Definable.inter, Set.Definable.union, Set.Definable.compl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
h : (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) = P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
⊢ Definable.{u_4, u_5, u_1, u_2} A L (α := Option α) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v)

Tactic:
convert! (hP.inter hf).union (hP.compl.inter hg)

Premises used: Set.Definable.inter, Set.Definable.union, Set.Definable.compl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
h :
  ∀ (w : Option α → M),
    Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
      w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
⊢ (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) = P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

Tactic:
ext w
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
pos :
  ∀ (h : p (w ∘ some)),
    Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
      w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
neg :
  ∀ (h : ¬p (w ∘ some)),
    Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
      w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g
⊢ Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
    w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

Tactic:
by_cases h : p (w ∘ some)

Premises used: Option.some, Function.comp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
h : p (w ∘ some)
⊢ Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
    w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

Tactic:
simp [tupleGraph, P, h]

Premises used: Function.tupleGraph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
p : (α → M) → Prop
g : (α → M) → M
inst_1 : DecidablePred p
hp : A.Definable L (setOf p)
hf : DefinableFun L A f
hg : DefinableFun L A g
P : Set (Option α → M) := {w : Option α → M | p (w ∘ some)}
hP : A.Definable L P
w : Option α → M
h : ¬p (w ∘ some)
⊢ Membership.mem (γ := Set (Option α → M)) (tupleGraph fun (v : α → M) ↦ if p v then f v else g v) w ↔
    w ∈ P ∩ tupleGraph f ∪ Pᶜ ∩ tupleGraph g

Tactic:
simp [tupleGraph, P, h]

Premises used: Function.tupleGraph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f g : (α → M) → M
hf : DefinableFun L A f
hg : DefinableFun L A g
⊢ DefinableMap.{u_1, u_2, 0, u_4, u_5} L (α := α) (β := Fin (Nat.succ 0).succ) A fun (v : α → M) ↦ ![f v, g v]

Tactic:
simp [DefinableMap, *]

Premises used: Set.DefinableMap
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f g : (α → M) → M
hf : DefinableFun L A f
hg : DefinableFun L A g
⊢ DefinableMap.{u_1, u_2, 0, u_4, u_5} L (α := α) (β := Fin (Nat.succ 0).succ) A fun (v : α → M) ↦ ![f v, g v]

Tactic:
have hF : A.DefinableMap L (fun v => ![f v, g v]) := by
    simp [DefinableMap, *]
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f g : (α → M) → M
hf : DefinableFun L A f
hg : DefinableFun L A g
hF : DefinableMap.{u_1, u_2, 0, u_4, u_5} L (α := α) (β := Fin (Nat.succ 0).succ) A fun (v : α → M) ↦ ![f v, g v]
⊢ Definable.{u_4, u_5, u_1, u_2} A L (α := α) {v : α → M | f v = g v}

Tactic:
(Definable.diagonal L A).preimage_map hF

Premises used: Eq.mpr, Set.Mem, setOf, Fin.cons, Fin.induction.go, Set.diagonal, Fin.induction, Set.preimage, Fin.cases, Matrix.vecCons, Set.Definable.diagonal, Set.Definable.preimage_map
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f g : (α → M) → M
hf : DefinableFun L A f
hg : DefinableFun L A g
hF : DefinableMap.{u_1, u_2, 0, u_4, u_5} L (α := α) (β := Fin (Nat.succ 0).succ) A fun (v : α → M) ↦ ![f v, g v]
⊢ Definable.{u_4, u_5, u_1, u_2} A L (α := α) {v : α → M | f v = g v}

Tactic:
exact (Definable.diagonal L A).preimage_map hF

Premises used: Set.Definable.diagonal, Set.Definable.preimage_map
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type u_1
L : Language
inst : L.Structure M
α : Type u_2
A : Set M
f : (α → M) → M
hf : DefinableFun L A f
a : M
ha : a ∈ A
⊢ Definable.{u_4, u_5, u_1, u_2} A L (α := α) {v : α → M | f v = a}

Tactic:
hf.setOf_eq (L.definableFun_const α ha)

Premises used: FirstOrder.Language.definableFun_const, Set.DefinableFun.setOf_eq
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f : (α → M) → M
h : A.TermDefinable L f
obtain :
  ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α),
    Definable.{u, v, w, u₁} A L (α := Option α) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ)
⊢ A.Definable L (Function.tupleGraph f)

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₁
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
h :
  Eq (α := Set (Option α → M)) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ)
    (setOf ((Term.relabel some φ).equal (var none)).Realize)
⊢ Definable.{u, v, w, u₁} A L (α := Option α) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ)

Tactic:
use (φ.relabel some).equal (Term.var none)

Premises used: FirstOrder.Language.Term.relabel, Option.some, FirstOrder.Language.Term.equal, Option.none, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
h :
  ∀ (x : Option α → M),
    Membership.mem (γ := Set (Option α → M)) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ) x ↔
      Membership.mem (γ := Set (Option α → M)) (setOf ((Term.relabel some φ).equal (var none)).Realize) x
⊢ Eq (α := Set (Option α → M)) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ)
    (setOf ((Term.relabel some φ).equal (var none)).Realize)

Tactic:
ext
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
x : Option α → M
⊢ Membership.mem (γ := Set (Option α → M)) (Function.tupleGraph fun (v : α → M) ↦ Term.realize v φ) x ↔
    Membership.mem (γ := Set (Option α → M)) (setOf ((Term.relabel some φ).equal (var none)).Realize) x

Tactic:
simp [Function.tupleGraph]

Premises used: Function.tupleGraph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
α : Type u₁
f : (α → M) → M
h : A.TermDefinable L f
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
obtain :
  ∀ (ψ : (withConstants.{u, v, w} L (↑A : Type w)).Term α),
    TermDefinable.{u_2, u_3, w, u₁} A L' (α := α) fun (v : α → M) ↦ Term.realize v ψ
⊢ A.TermDefinable L' f

Tactic:
obtain ⟨ψ, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
α : Type u₁
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
h :
  Eq (α := (α → M) → M) (fun (v : α → M) ↦ Term.realize v ψ) fun (v : α → M) ↦
    Term.realize v (LHom.onTerm (LHom.addConstants (↑A : Type w) φ) ψ)
⊢ TermDefinable.{u_2, u_3, w, u₁} A L' (α := α) fun (v : α → M) ↦ Term.realize v ψ

Tactic:
use (φ.addConstants A).onTerm ψ

Premises used: FirstOrder.Language.LHom.onTerm, Set.Elem, FirstOrder.Language.LHom.addConstants
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
L' : Language
inst : L.Structure M
inst_1 : L'.Structure M
α : Type u₁
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
⊢ Eq (α := (α → M) → M) (fun (v : α → M) ↦ Term.realize v ψ) fun (v : α → M) ↦
    Term.realize v (LHom.onTerm (LHom.addConstants (↑A : Type w) φ) ψ)

Tactic:
simp