awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
L : Language
inst : L.Structure M
α : Type u₁
f : (α → M) → M
rw :
  (∃ (φ : (withConstants.{u, v, w} L (↑∅ : Type w)).Term α), f = fun (v : α → M) ↦ Term.realize v φ) ↔
    ∃ (b : (withConstants.{u, v, w} L (↑∅ : Type w)).Term α),
      f = fun (v : α → M) ↦
        Term.realize.{u, v, w, u₁} (L := L) v
          ((Equiv.symm (LEquiv.onTerm (LEquiv.addEmptyConstants L (↑∅ : Type w))) :
              (a : L[[(↑∅ : Type w)]].Term α) → L.Term α)
            b)
⊢ TermDefinable ∅ L f ↔ ∃ (φ : L.Term α), f = fun (v : α → M) ↦ Term.realize v φ

Tactic:
rw [TermDefinable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onTerm]

Premises used: Equiv.exists_congr_left, FirstOrder.Language.LEquiv.onTerm, Set.Elem, Set.TermDefinable, FirstOrder.Language.LEquiv.addEmptyConstants, EmptyCollection.emptyCollection
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
L : Language
inst : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ (∃ (φ : (withConstants.{u, v, w} L (↑∅ : Type w)).Term α), f = fun (v : α → M) ↦ Term.realize v φ) ↔
    ∃ (b : (withConstants.{u, v, w} L (↑∅ : Type w)).Term α),
      f = fun (v : α → M) ↦
        Term.realize.{u, v, w, u₁} (L := L) v
          ((Equiv.symm (LEquiv.onTerm (LEquiv.addEmptyConstants L (↑∅ : Type w))) :
              (a : L[[(↑∅ : Type w)]].Term α) → L.Term α)
            b)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ TermDefinable ∅ (withConstants.{u, v, w} L (↑A : Type w)) f ↔ A.TermDefinable L f

Tactic:
termDefinable_empty_iff

Premises used: Set.TermDefinable, Set.termDefinable_empty_iff
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
B : Set M
f : (α → M) → M
h : A.TermDefinable L f
hAB : A ⊆ B
rw :
  ∀ (h : TermDefinable ∅ (withConstants.{u, v, w} L (↑A : Type w)) f) (hAB : A ⊆ B),
    TermDefinable ∅ (withConstants.{u, v, w} L (↑B : Type w)) f
⊢ B.TermDefinable L f

Tactic:
rw [← termDefinable_empty_withConstants_iff] at h ⊢

Premises used: Set.termDefinable_empty_withConstants_iff
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
B : Set M
f : (α → M) → M
h : TermDefinable ∅ (withConstants.{u, v, w} L (↑A : Type w)) f
hAB : A ⊆ B
⊢ TermDefinable ∅ (withConstants.{u, v, w} L (↑B : Type w)) f

Tactic:
h.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))

Premises used: Set.TermDefinable.map_expansion, FirstOrder.Language.lhomWithConstantsMap, Set.inclusion
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
B : Set M
f : (α → M) → M
h : TermDefinable ∅ (withConstants.{u, v, w} L (↑A : Type w)) f
hAB : A ⊆ B
⊢ TermDefinable ∅ (withConstants.{u, v, w} L (↑B : Type w)) f

Tactic:
exact h.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))

Premises used: Set.TermDefinable.map_expansion, FirstOrder.Language.lhomWithConstantsMap, Set.inclusion
-- 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_1
f : (β → M) → M
h₁ : A.TermDefinable L f
h₂ :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n),
    A.TermDefinable L' (α := Fin n) fun (v : Fin n → M) ↦ Term.realize v g.term
obtain :
  ∀ (x : (withConstants.{u, v, w} L (↑A : Type w)).Term β),
    TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x
⊢ A.TermDefinable L' f

Tactic:
obtain ⟨x, 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_1
h₂ :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n),
    A.TermDefinable L' (α := Fin n) fun (v : Fin n → M) ↦ Term.realize v g.term
x : (withConstants.{u, v, w} L (↑A : Type w)).Term β
choose :
  ∀
    (c :
      {n : ℕ} →
        (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) →
          (withConstants.{u_2, u_3, w} L' (↑A : Type w)).Term (Fin n))
    (hc :
      ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n),
        Eq.{w + 1} (α := (Fin n → M) → M) (fun (v : Fin n → M) ↦ Term.realize v g.term) fun (v : Fin n → M) ↦
          Term.realize v (c g)),
    TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x
⊢ TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x

Tactic:
choose c hc using @h₂
-- 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_1
x : (withConstants.{u, v, w} L (↑A : Type w)).Term β
c :
  {n : ℕ} →
    (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) →
      (withConstants.{u_2, u_3, w} L' (↑A : Type w)).Term (Fin n)
hc :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n),
    Eq.{w + 1} (α := (Fin n → M) → M) (fun (v : Fin n → M) ↦ Term.realize v g.term) fun (v : Fin n → M) ↦
      Term.realize v (c g)
⊢ ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) (x : Fin n → M),
    Term.realize x g.term = Term.realize x (c g)

Tactic:
simp only [funext_iff] at hc

Premises used: funext_iff
-- 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_1
x : (withConstants.{u, v, w} L (↑A : Type w)).Term β
c :
  {n : ℕ} →
    (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) →
      (withConstants.{u_2, u_3, w} L' (↑A : Type w)).Term (Fin n)
hc :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) (x : Fin n → M),
    Term.realize x g.term = Term.realize x (c g)
h :
  Eq (α := (β → M) → M) (fun (v : β → M) ↦ Term.realize v x) fun (v : β → M) ↦
    Term.realize (L := withConstants.{u_2, u_3, w} L' (↑A : Type w)) v (x.substFunc fun {n : ℕ} ↦ c)
⊢ TermDefinable.{u_2, u_3, w, u_1} A L' (α := β) fun (v : β → M) ↦ Term.realize v x

Tactic:
use x.substFunc c

Premises used: FirstOrder.Language.Term.substFunc
-- 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_1
x : (withConstants.{u, v, w} L (↑A : Type w)).Term β
c :
  {n : ℕ} →
    (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) →
      (withConstants.{u_2, u_3, w} L' (↑A : Type w)).Term (Fin n)
hc :
  ∀ {n : ℕ} (g : (withConstants.{u, v, w} L (↑A : Type w)).Functions n) (x : Fin n → M),
    Term.realize x g.term = Term.realize x (c g)
⊢ Eq (α := (β → M) → M) (fun (v : β → M) ↦ Term.realize v x) fun (v : β → M) ↦
    Term.realize (L := withConstants.{u_2, u_3, w} L' (↑A : Type w)) v (x.substFunc fun {n : ℕ} ↦ c)

Tactic:
simp_rw [Term.realize_substFunc hc]

Premises used: FirstOrder.Language.Term.realize_substFunc
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
⊢ TermDefinable₁ (A := A) L f ↔ A.TermDefinable L (α := Unit) fun (v : Unit → M) ↦ f (v ())

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
⊢ TermDefinable₁ (A := A) L f ↔
    ∃ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit),
      f = (fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit

Tactic:
exists_congr fun φ ↦ ?_

Premises used: Set.TermDefinable₁, Set.TermDefinable, exists_congr
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
refine :
  ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit),
    (Eq.{w + 1} (α := (Unit → M) → M) (fun (x : Unit → M) ↦ f (x ())) fun (v : Unit → M) ↦ Term.realize v φ) ↔
      f = (fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit
⊢ TermDefinable₁ (A := A) L f ↔
    ∃ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit),
      f = (fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit

Tactic:
refine exists_congr fun φ ↦ ?_

Premises used: exists_congr
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit
rw :
  ∀ (b : M),
    f (((Equiv.funUnique Unit M).symm : (a : M) → Unit → M) b ()) =
        Term.realize (((Equiv.funUnique Unit M).symm : (a : M) → Unit → M) b) φ ↔
      f b = ((fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit) b
⊢ (Eq.{w + 1} (α := (Unit → M) → M) (fun (x : Unit → M) ↦ f (x ())) fun (v : Unit → M) ↦ Term.realize v φ) ↔
    f = (fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit

Tactic:
rw [funext_iff, funext_iff, (Equiv.funUnique Unit M).forall_congr']

Premises used: funext_iff, Equiv.forall_congr', Unit, Equiv.funUnique
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit
simp :
  ∀ (b : M),
    f b = Term.realize (uniqueElim (α := fun (a : Unit) ↦ M) b) φ ↔ f b = Term.realize (Function.const Unit b) φ
⊢ ∀ (b : M),
    f (((Equiv.funUnique Unit M).symm : (a : M) → Unit → M) b ()) =
        Term.realize (((Equiv.funUnique Unit M).symm : (a : M) → Unit → M) b) φ ↔
      f b = ((fun (v : Unit → M) ↦ Term.realize v φ) ∘ Function.const Unit) b

Tactic:
simp only [Equiv.funUnique_symm_apply, uniqueElim_const, Function.comp_apply]

Premises used: uniqueElim_const, Function.comp_apply, Equiv.funUnique_symm_apply
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term Unit
⊢ ∀ (b : M),
    f b = Term.realize (uniqueElim (α := fun (a : Unit) ↦ M) b) φ ↔ f b = Term.realize (Function.const Unit b) φ

Tactic:
congr!
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h : TermDefinable₁ (A := A) L f
obtain :
  ∀ (t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit))
    (h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)),
    A.Definable₂ L (Function.graph f)
⊢ A.Definable₂ L (Function.graph f)

Tactic:
obtain ⟨t, h⟩ := h.termDefinable.definable_tupleGraph A L

Premises used: Set.TermDefinable₁.termDefinable, Set.TermDefinable.definable_tupleGraph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h_1 : TermDefinable₁ (A := A) L f
t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit)
h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)
h₁ :
  Eq.{w + 1} (α := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Function.graph f}
    (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t)))
⊢ A.Definable₂ L (Function.graph f)

Tactic:
use t.relabel (Option.elim · 1 (fun _ ↦ 0))

Premises used: FirstOrder.Language.Formula.relabel, OfNat.ofNat, Option.elim
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h_1 : TermDefinable₁ (A := A) L f
t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit)
h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)
h₁ :
  ∀ (v : Fin 2 → M),
    Membership.mem (γ := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Function.graph f} v ↔
      Membership.mem (γ := Set (Fin 2 → M))
        (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t))) v
⊢ Eq.{w + 1} (α := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Function.graph f}
    (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t)))

Tactic:
ext v
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h_1 : TermDefinable₁ (A := A) L f
t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit)
h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)
v : Fin 2 → M
⊢ Membership.mem (γ := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ()))
      (v ∘ fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) ↔
    Membership.mem (γ := Set (Option Unit → M)) (setOf t.Realize)
      (v ∘ fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0)

Tactic:
Set.ext_iff.1 h (v ∘ (Option.elim · 1 (fun _ ↦ 0)))

Premises used: Function.comp, Iff.mp, Set.ext_iff, OfNat.ofNat, Option.elim
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h_1 : TermDefinable₁ (A := A) L f
t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit)
h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)
v : Fin 2 → M
h₁ :
  Membership.mem (γ := Set (Fin 2 → M))
      (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t))) v ↔
    Membership.mem (γ := Set (Option Unit → M)) (setOf t.Realize)
      (v ∘ fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0)
⊢ Membership.mem (γ := Set (Fin 2 → M)) {x : Fin 2 → M | (x 0, x 1) ∈ Function.graph f} v ↔
    Membership.mem (γ := Set (Fin 2 → M))
      (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t))) v

Tactic:
convert! Set.ext_iff.1 h (v ∘ (Option.elim · 1 (fun _ ↦ 0)))

Premises used: Function.comp, Iff.mp, Set.ext_iff, OfNat.ofNat, Option.elim
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f : M → M
h_1 : TermDefinable₁ (A := A) L f
t : (withConstants.{u, v, w} L (↑A : Type w)).Formula (Option Unit)
h : Eq.{w + 1} (α := Set (Option Unit → M)) (Function.tupleGraph fun (v : Unit → M) ↦ f (v ())) (setOf t.Realize)
v : Fin 2 → M
⊢ Membership.mem (γ := Set (Fin 2 → M))
      (setOf (Formula.Realize (Formula.relabel (fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0) t))) v ↔
    Membership.mem (γ := Set (Option Unit → M)) (setOf t.Realize)
      (v ∘ fun (x : Option Unit) ↦ x.elim 1 fun (x : Unit) ↦ 0)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
⊢ TermDefinable₁ (A := A) L _root_.id

Tactic:
⟨Term.var (), rfl⟩

Premises used: Set.TermDefinable₁, Unit.unit, Set.TermDefinable, FirstOrder.Language.Term.var, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
C : (withConstants.{u, v, w} L (↑A : Type w)).Constants
simp : Eq (α := (α → M) → M) (Function.const (α → M) (↑C : M)) fun (v : α → M) ↦ (↑C : M)
⊢ Eq (α := (α → M) → M) (Function.const (α → M) (↑C : M)) fun (v : α → M) ↦ Term.realize v C.term

Tactic:
simp only [Term.realize_constants]

Premises used: FirstOrder.Language.Term.realize_constants
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
C : (withConstants.{u, v, w} L (↑A : Type w)).Constants
⊢ Eq (α := (α → M) → M) (Function.const (α → M) (↑C : M)) fun (v : α → M) ↦ (↑C : M)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
C : (withConstants.{u, v, w} L (↑A : Type w)).Constants
⊢ TermDefinable₁ (A := A) L (Function.const M (↑C : M))

Tactic:
(TermDefinable.const C).termDefinable₁

Premises used: Set.TermDefinable.termDefinable₁
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
f : (α → M) → M
g : α → (β → M) → M
hf : A.TermDefinable L f
hg : ∀ (i : α), A.TermDefinable L (g i)
obtain :
  ∀ (φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α),
    TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b
⊢ TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ f fun (x : α) ↦ g x b

Tactic:
obtain ⟨φ, rfl⟩ := hf

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
g : α → (β → M) → M
hg : ∀ (i : α), A.TermDefinable L (g i)
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
choose :
  ∀ (ψ : (i : α) → (withConstants.{u, v, w} L (↑A : Type w)).Term β)
    (hψ : ∀ (i : α), g i = fun (v : β → M) ↦ Term.realize v (ψ i)),
    TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b
⊢ TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b

Tactic:
choose ψ hψ using hg
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
g : α → (β → M) → M
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
ψ : (i : α) → (withConstants.{u, v, w} L (↑A : Type w)).Term β
hψ : ∀ (i : α), g i = fun (v : β → M) ↦ Term.realize v (ψ i)
h :
  Eq (α := (β → M) → M) (fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b) fun (v : β → M) ↦
    Term.realize v (φ.subst ψ)
⊢ TermDefinable.{u, v, w, u_1} A L (α := β) fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b

Tactic:
use φ.subst ψ

Premises used: FirstOrder.Language.Term.subst
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
β : Type u_1
g : α → (β → M) → M
φ : (withConstants.{u, v, w} L (↑A : Type w)).Term α
ψ : (i : α) → (withConstants.{u, v, w} L (↑A : Type w)).Term β
hψ : ∀ (i : α), g i = fun (v : β → M) ↦ Term.realize v (ψ i)
⊢ Eq (α := (β → M) → M) (fun (b : β → M) ↦ (fun (v : α → M) ↦ Term.realize v φ) fun (x : α) ↦ g x b) fun (v : β → M) ↦
    Term.realize v (φ.subst ψ)

Tactic:
simp [hψ]
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
f g : M → M
hf : TermDefinable₁ (A := A) L f
hg : TermDefinable₁ (A := A) L g
⊢ TermDefinable₁ (A := A) L (f ∘ g)

Tactic:
(hf.termDefinable.comp fun _ ↦ hg.termDefinable).termDefinable₁

Premises used: Set.TermDefinable.termDefinable₁
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
f : M → M
g : (α → M) → M
hf : TermDefinable₁ (A := A) L f
hg : A.TermDefinable L g
⊢ A.TermDefinable L (f ∘ g)

Tactic:
hf.termDefinable.comp fun _ ↦ hg

Premises used: Set.TermDefinable₁.termDefinable, Set.TermDefinable.comp
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m n : ℕ
h : m ≤ n
obtain :
  ∀ (k : ℕ) (h : m ≤ m + k),
    Eq (α := (a : G' m) → G' (m + k)) (⇑(natLERec (G' := G') f' m (m + k) h) : (a : G' m) → G' (m + k)) fun (a : G' m) ↦
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) a
⊢ Eq (α := (a : G' m) → G' n) (⇑(natLERec (G' := G') f' m n h) : (a : G' m) → G' n) fun (a : G' m) ↦
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) a

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
h₁ :
  ∀ (x : G' m),
    (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
⊢ Eq (α := (a : G' m) → G' (m + k)) (⇑(natLERec (G' := G') f' m (m + k) h) : (a : G' m) → G' (m + k)) fun (a : G' m) ↦
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) a

Tactic:
ext x
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m : ℕ
x : G' m
h : m ≤ m + 0
⊢ (natLERec (G' := G') f' m (m + 0) h : (a : G' m) → G' (m + 0)) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x

Tactic:
simp [natLERec, Nat.leRecOn_self]

Premises used: FirstOrder.Language.DirectedSystem.natLERec, Nat.leRecOn_self
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
G' : ℕ → Type w
inst : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
x : G' m
h₁ :
  ∀ (h : m ≤ m + 0),
    (natLERec (G' := G') f' m (m + 0) h : (a : G' m) → G' (m + 0)) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
h₂ :
  ∀ (k : ℕ)
    (ih :
      ∀ (h : m ≤ m + k),
        (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
          Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x)
    (h : m ≤ m + (k + 1)),
    (natLERec (G' := G') f' m (m + (k + 1)) h : (a : G' m) → G' (m + (k + 1))) x =
      Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x
⊢ (natLERec (G' := G') f' m (m + k) h : (a : G' m) → G' (m + k)) x =
    Nat.leRecOn (C := G') h (fun (k : ℕ) ↦ (⇑(f' k) : (a : G' k) → G' (k + 1))) x

Tactic:
induction k with
  | zero => simp [natLERec, Nat.leRecOn_self]
  | succ k ih =>
    rw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,
      Embedding.comp_apply, ih]

Premises used: Nat.leRecOn_succ, FirstOrder.Language.DirectedSystem.natLERec, Nat.leRecOn_self, FirstOrder.Language.Embedding.comp_apply, le_self_add
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_1, u_2, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
G' : ℕ → Type w
inst_2 : (i : ℕ) → Structure.{u_1, u_2, w} L (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
x x_1 x_2 : ℕ
hij : x_2 ≤ x_1
hjk : x_1 ≤ x
⊢ ∀ (x_3 : G' x_2),
    Eq (α := G' x)
      ((natLERec (G' := G') f' x_1 x hjk : (a : G' x_1) → G' x)
          ((natLERec (G' := G') f' x_2 x_1 hij : (a : G' x_2) → G' x_1) x_3 : G' x_1) :
        G' x)
      ((natLERec (G' := G') f' x_2 x ⋯ : (a : G' x_2) → G' x) x_3 : G' x)

Tactic:
simp [Nat.leRecOn_trans hij hjk]

Premises used: Nat.leRecOn_trans
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
α : Type u_1
i : ι
x : α → G i
h : ∀ (a : α), unify (G := G) f (fun (a : α) ↦ Structure.Sigma.mk (G := G) f i (x a)) i ⋯ a = x a
⊢ unify (G := G) f (fun (a : α) ↦ Structure.Sigma.mk (G := G) f i (x a)) i ⋯ = x

Tactic:
ext a
-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
α : Type u_1
i : ι
x : α → G i
a : α
h :
  ((f ((Structure.Sigma.mk (G := G) f i (x a)).fst (β := fun (i : ι) ↦ G i)) i ⋯ :
          G ((Structure.Sigma.mk (G := G) f i (x a)).fst (β := fun (i : ι) ↦ G i)) ↪[L] G i) :
        (a : G (Structure.Sigma.mk f i (x a)).fst) → G i)
      ((Structure.Sigma.mk (G := G) f i (x a)).snd (β := fun (i : ι) ↦ G i)) =
    x a
⊢ unify (G := G) f (fun (a : α) ↦ Structure.Sigma.mk (G := G) f i (x a)) i ⋯ a = x a

Tactic:
rw [unify]

Premises used: FirstOrder.Language.DirectLimit.unify