awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hU : φ.IsUniversal
f : F
v : α → M
xs : Fin n → M
of_isQF :
  ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hQF : φ.IsQF) {xs : Fin n → M},
    Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ.Realize v xs
all :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsUniversal →
      ∀
        (ih :
          ∀ {xs : Fin (n + 1) → M},
            Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ.Realize v xs)
        {xs : Fin n → M},
        Realize.{u, v, u_2, u'} (M := N) (∀' φ) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → (∀' φ).Realize v xs
⊢ Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ.Realize v xs

Tactic:
induction hU with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | all _ ih =>
    simp only [realize_all, Nat.succ_eq_add_one]
    refine fun h a => ih ?_
    rw [Fin.comp_snoc]
    exact h (f a)

Premises used: Fin.comp_snoc, Nat.succ_eq_add_one, FirstOrder.Language.BoundedFormula.IsUniversal.all, FirstOrder.Language.BoundedFormula.IsUniversal.of_isQF, FirstOrder.Language.BoundedFormula.realize_all
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hQF : φ_1.IsQF
xs : Fin n_1 → M
⊢ φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)

Tactic:
simp [hQF.realize_embedding]

Premises used: FirstOrder.Language.BoundedFormula.IsQF.realize_embedding
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
ex :
  (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) →
    ∃ (a : N),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
⊢ (∃' φ_1).Realize v xs → Realize.{u, v, u_2, u'} (M := N) (∃' φ_1) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)

Tactic:
simp only [realize_ex, Nat.succ_eq_add_one]

Premises used: Nat.succ_eq_add_one, FirstOrder.Language.BoundedFormula.realize_ex
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
⊢ (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) →
    ∃ (a : N),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)

Tactic:
fun ⟨a, ha⟩ => ⟨f a, ?_⟩

Premises used: Function.comp, Exists, Fin.snoc, FirstOrder.Language.BoundedFormula.Realize, _private.0.FirstOrder.Language.BoundedFormula.IsExistential.realize_embedding.match_1, Exists.intro, DFunLike.coe
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
ex :
  (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) →
    ∀ (a : M) (ha : φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))
⊢ (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) →
    ∃ (a : N),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)

Tactic:
refine fun ⟨a, ha⟩ => ⟨f a, ?_⟩
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
h_1 : ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
a : M
ha : φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
ex :
  Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a))
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))

Tactic:
rw [← Fin.comp_snoc]

Premises used: Fin.comp_snoc
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
h_1 : ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
a : M
ha : φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a))

Tactic:
ih ha
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
h_1 : ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
a : M
ha : φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a))

Tactic:
exact ih ha
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hE : φ.IsExistential
f : F
v : α → M
xs : Fin n → M
of_isQF :
  ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hQF : φ.IsQF) {xs : Fin n → M},
    φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
ex :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsExistential →
      ∀
        (ih :
          ∀ {xs : Fin (n + 1) → M},
            φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs))
        {xs : Fin n → M},
        (∃' φ).Realize v xs → Realize.{u, v, u_2, u'} (M := N) (∃' φ) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
⊢ φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)

Tactic:
induction hE with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | ex _ ih =>
    simp only [realize_ex, Nat.succ_eq_add_one]
    refine fun ⟨a, ha⟩ => ⟨f a, ?_⟩
    rw [← Fin.comp_snoc]
    exact ih ha

Premises used: Fin.comp_snoc, Nat.succ_eq_add_one, FirstOrder.Language.BoundedFormula.realize_ex, FirstOrder.Language.BoundedFormula.IsExistential.ex, FirstOrder.Language.BoundedFormula.IsExistential.of_isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
simp : ∀ φ ∈ T, M ⊨ φ
⊢ M ⊨ T

Tactic:
simp only [model_iff]

Premises used: FirstOrder.Language.Theory.model_iff
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
⊢ ∀ φ ∈ T, M ⊨ φ

Tactic:
fun φ hφ => (hT.isUniversal_of_mem hφ).realize_embedding f (?_)

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding, FirstOrder.Language.Theory.IsUniversal.isUniversal_of_mem, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
refine :
  ∀ (φ : L.Sentence) (hφ : φ ∈ T),
    BoundedFormula.Realize.{u, v, u_1, 0} (M := N) φ
      (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑f : (a : M) → N) default)
      (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑f : (a : M) → N) default)
⊢ ∀ φ ∈ T, M ⊨ φ

Tactic:
refine fun φ hφ => (hT.isUniversal_of_mem hφ).realize_embedding f (?_)

Premises used: FirstOrder.Language.BoundedFormula.IsUniversal.realize_embedding, FirstOrder.Language.Theory.IsUniversal.isUniversal_of_mem
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
rw : BoundedFormula.Realize.{u, v, u_1, 0} (M := N) φ default default
⊢ BoundedFormula.Realize.{u, v, u_1, 0} (M := N) φ
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑f : (a : M) → N) default)
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑f : (a : M) → N) default)

Tactic:
rw [Subsingleton.elim (f ∘ default) default, Subsingleton.elim (f ∘ default) default]

Premises used: Inhabited.default, Function.comp, Subsingleton.elim, DFunLike.coe
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize.{u, v, u_1, 0} (M := N) φ default default

Tactic:
Theory.realize_sentence_of_mem T hφ

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.Theory.realize_sentence_of_mem, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize.{u, v, u_1, 0} (M := N) φ default default

Tactic:
exact Theory.realize_sentence_of_mem T hφ

Premises used: FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
n l : ℕ
φ : L.BoundedFormula α l
S : L.Substructure M
T : L.Theory
inst_1 : T.IsUniversal
inst_2 : M ⊨ T
⊢ Theory.Model.{u, v, w} (↥S) T

Tactic:
Theory.IsUniversal.models_of_embedding (Substructure.subtype S)

Premises used: FirstOrder.Language.Theory.IsUniversal.models_of_embedding, FirstOrder.Language.Substructure.subtype
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
simp : ∀ a ∈ T, BoundedFormula.IsUniversal a
⊢ ∀ ⦃φ_1 : L.Sentence⦄, φ_1 ∈ Insert.insert φ T → BoundedFormula.IsUniversal φ_1

Tactic:
simp only [Set.mem_insert_iff, forall_eq_or_imp, hφ, true_and]

Premises used: forall_eq_or_imp, Set.mem_insert_iff, true_and
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
⊢ ∀ a ∈ T, BoundedFormula.IsUniversal a

Tactic:
hT.isUniversal_of_mem

Premises used: FirstOrder.Language.Theory.IsUniversal.isUniversal_of_mem
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
⊢ ∀ a ∈ T, BoundedFormula.IsUniversal a

Tactic:
exact hT.isUniversal_of_mem

Premises used: FirstOrder.Language.Theory.IsUniversal.isUniversal_of_mem
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n l : ℕ
r : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
⊢ (r.boundedFormula ts).IsAtomic

Tactic:
IsAtomic.rel r ts

Premises used: FirstOrder.Language.BoundedFormula.IsAtomic.rel
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n l : ℕ
r : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
⊢ (r.boundedFormula ts).IsQF

Tactic:
(r.isAtomic ts).isQF

Premises used: FirstOrder.Language.Relations.isAtomic, FirstOrder.Language.BoundedFormula.IsAtomic.isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
r : L.Relations 2
⊢ IsUniversal r.reflexive

Tactic:
(r.isQF _).isUniversal.all

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isUniversal, FirstOrder.Language.BoundedFormula.IsUniversal.all, FirstOrder.Language.Relations.reflexive, FirstOrder.Language.Relations.isQF, FirstOrder.Language.Relations.boundedFormula₂
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
r : L.Relations 2
⊢ IsUniversal r.irreflexive

Tactic:
(r.isAtomic _).isQF.not.isUniversal.all

Premises used: FirstOrder.Language.Relations.isAtomic, FirstOrder.Language.BoundedFormula.IsQF.isUniversal, FirstOrder.Language.BoundedFormula.IsUniversal.all, FirstOrder.Language.BoundedFormula.IsQF.not, FirstOrder.Language.Relations.boundedFormula₂, FirstOrder.Language.Relations.irreflexive, FirstOrder.Language.BoundedFormula.IsAtomic.isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
r : L.Relations 2
⊢ IsUniversal r.symmetric

Tactic:
((r.isQF _).imp (r.isQF _)).isUniversal.all.all

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isUniversal, FirstOrder.Language.BoundedFormula.IsUniversal.all, FirstOrder.Language.Relations.isQF, FirstOrder.Language.Relations.boundedFormula₂, FirstOrder.Language.BoundedFormula.IsQF.imp, FirstOrder.Language.Relations.symmetric
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
r : L.Relations 2
⊢ IsUniversal r.antisymmetric

Tactic:
((r.isQF _).imp ((r.isQF _).imp (IsAtomic.equal _ _).isQF)).isUniversal.all.all

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isUniversal, FirstOrder.Language.BoundedFormula.IsUniversal.all, FirstOrder.Language.BoundedFormula.IsAtomic.equal, FirstOrder.Language.Relations.antisymmetric, FirstOrder.Language.Relations.isQF, FirstOrder.Language.Relations.boundedFormula₂, FirstOrder.Language.BoundedFormula.IsQF.imp, FirstOrder.Language.BoundedFormula.IsAtomic.isQF
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
r : L.Relations 2
⊢ IsUniversal r.transitive

Tactic:
((r.isQF _).imp ((r.isQF _).imp (r.isQF _))).isUniversal.all.all.all

Premises used: FirstOrder.Language.BoundedFormula.IsQF.isUniversal, FirstOrder.Language.BoundedFormula.IsUniversal.all, FirstOrder.Language.Relations.transitive, FirstOrder.Language.Relations.isQF, FirstOrder.Language.Relations.boundedFormula₂, FirstOrder.Language.BoundedFormula.IsQF.imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
r : L.Relations 2
⊢ IsUniversal r.total

Tactic:
((r.isQF _).sup (r.isQF _)).isUniversal.all.all

Premises used: FirstOrder.Language.Relations.total, FirstOrder.Language.BoundedFormula.IsQF.sup, FirstOrder.Language.BoundedFormula.IsQF.isUniversal, FirstOrder.Language.BoundedFormula.IsUniversal.all, FirstOrder.Language.Relations.isQF, FirstOrder.Language.Relations.boundedFormula₂
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
n : ℕ
f : L.Functions n
⊢ BoundedFormula.IsAtomic (graph f)

Tactic:
BoundedFormula.IsAtomic.equal _ _

Premises used: FirstOrder.Language.BoundedFormula.IsAtomic.equal, FirstOrder.Language.Term.equal, FirstOrder.Language.Formula.graph
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
L' : Language
inst_1 : L'.Structure M
h : A.Definable L s
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
obtain : ∀ (ψ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α), A.Definable L' (setOf ψ.Realize)
⊢ A.Definable L' 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₁
L' : Language
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
⊢ A.Definable L' (setOf ψ.Realize)

Tactic:
⟨(φ.addConstants A).onFormula ψ, ?_⟩

Premises used: Set.Definable, Set.Elem, FirstOrder.Language.LHom.addConstants, Exists.intro, FirstOrder.Language.LHom.onFormula
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
L' : Language
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
refine : Eq (α := Set (α → M)) (setOf ψ.Realize) (setOf (LHom.onFormula (LHom.addConstants (↑A : Type w) φ) ψ).Realize)
⊢ A.Definable L' (setOf ψ.Realize)

Tactic:
refine ⟨(φ.addConstants A).onFormula ψ, ?_⟩
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
L' : Language
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
h :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M)) (setOf ψ.Realize) x ↔
      Membership.mem (γ := Set (α → M)) (setOf (LHom.onFormula (LHom.addConstants (↑A : Type w) φ) ψ).Realize) x
⊢ Eq (α := Set (α → M)) (setOf ψ.Realize) (setOf (LHom.onFormula (LHom.addConstants (↑A : Type w) φ) ψ).Realize)

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
L' : Language
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
x : α → M
⊢ Membership.mem (γ := Set (α → M)) (setOf ψ.Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf (LHom.onFormula (LHom.addConstants (↑A : Type w) φ) ψ).Realize) x

Tactic:
simp only [mem_setOf_eq, LHom.realize_onFormula]

Premises used: FirstOrder.Language.LHom.realize_onFormula, Set.mem_setOf_eq
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
rw :
  (∃ (b : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0),
      s =
        setOf
          (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
            ((Equiv.symm BoundedFormula.constantsVarsEquiv :
                (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
              b))) ↔
    ∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
      s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
⊢ A.Definable L s ↔
    ∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
      s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}

Tactic:
rw [Definable, Equiv.exists_congr_left (BoundedFormula.constantsVarsEquiv)]

Premises used: Equiv.exists_congr_left, Set.Definable, FirstOrder.Language.BoundedFormula.constantsVarsEquiv
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ (b : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0),
      s =
        setOf
          (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
            ((Equiv.symm BoundedFormula.constantsVarsEquiv :
                (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
              b))) ↔
    ∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
      s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}

Tactic:
exists_congr (fun φ => iff_iff_eq.2 (congr_arg (s = ·) ?_))

Premises used: Iff.mpr, iff_iff_eq, congr_arg, exists_congr, Eq
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
refine :
  ∀ (φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0),
    Eq (α := Set (α → M))
      (setOf
        (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
          ((Equiv.symm BoundedFormula.constantsVarsEquiv :
              (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
            φ)))
      {v : α → M | Formula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
⊢ (∃ (b : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0),
      s =
        setOf
          (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
            ((Equiv.symm BoundedFormula.constantsVarsEquiv :
                (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
              b))) ↔
    ∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
      s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}

Tactic:
refine exists_congr (fun φ => iff_iff_eq.2 (congr_arg (s = ·) ?_))

Premises used: Iff.mpr, iff_iff_eq, congr_arg, exists_congr, Eq
-- Module: Mathlib.ModelTheory.Definability
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0
h :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M))
        (setOf
          (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
            ((Equiv.symm BoundedFormula.constantsVarsEquiv :
                (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
              φ)))
        x ↔
      Membership.mem (γ := Set (α → M))
        {v : α → M | Formula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)} x
⊢ Eq (α := Set (α → M))
    (setOf
      (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
        ((Equiv.symm BoundedFormula.constantsVarsEquiv :
            (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
          φ)))
    {v : α → M | Formula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}

Tactic:
ext