awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ ψ : L.BoundedFormula α n
hφ : φ.IsQF
hψ : ψ.IsPrenex
v : α → M
xs : Fin n → M
of_isQF :
  ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hψ : φ.IsQF) {φ_1 : L.BoundedFormula α n} (hφ : φ_1.IsQF) {xs : Fin n → M},
    (φ_1.toPrenexImpRight φ).Realize v xs ↔ (φ_1 ⟹ φ).Realize v xs
all :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsPrenex →
      ∀
        (ih :
          ∀ {φ_1 : L.BoundedFormula α (n + 1)} (hφ : φ_1.IsQF) {xs : Fin (n + 1) → M},
            (φ_1.toPrenexImpRight φ).Realize v xs ↔ (φ_1 ⟹ φ).Realize v xs)
        {φ_1 : L.BoundedFormula α n} (hφ : φ_1.IsQF) {xs : Fin n → M},
        (φ_1.toPrenexImpRight (∀' φ)).Realize v xs ↔ (φ_1 ⟹ ∀' φ).Realize v xs
ex :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsPrenex →
      ∀
        (ih :
          ∀ {φ_1 : L.BoundedFormula α (n + 1)} (hφ : φ_1.IsQF) {xs : Fin (n + 1) → M},
            (φ_1.toPrenexImpRight φ).Realize v xs ↔ (φ_1 ⟹ φ).Realize v xs)
        {φ_1 : L.BoundedFormula α n} (hφ : φ_1.IsQF) {xs : Fin n → M},
        (φ_1.toPrenexImpRight (∃' φ)).Realize v xs ↔ (φ_1 ⟹ ∃' φ).Realize v xs
⊢ (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs

Tactic:
induction hψ with
  | of_isQF hψ => rw [hψ.toPrenexImpRight]
  | all _ ih =>
    refine _root_.trans (forall_congr' fun _ => ih hφ.liftAt) ?_
    simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
    exact ⟨fun h1 a h2 => h1 h2 a, fun h1 h2 a => h1 a h2⟩
  | ex _ ih =>
    unfold toPrenexImpRight
    rw [realize_ex]
    refine _root_.trans (exists_congr fun _ => ih hφ.liftAt) ?_
    simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_ex]
    refine ⟨?_, fun h' => ?_⟩
    · rintro ⟨a, ha⟩ h
      exact ⟨a, ha h⟩
    · by_cases h : φ.Realize v xs
      · obtain ⟨a, ha⟩ := h' h
        exact ⟨a, fun _ => ha⟩
      · inhabit M
        exact ⟨default, fun h'' => (h h'').elim⟩

Premises used: FirstOrder.Language.BoundedFormula.realize_ex, Fin.snoc_comp_castSucc, FirstOrder.Language.BoundedFormula.toPrenexImpRight, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.BoundedFormula.realize_liftAt_one_self, FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.BoundedFormula.all
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ ψ : L.BoundedFormula α n
hφ : φ.IsPrenex
hψ : ψ.IsPrenex
v : α → M
xs : Fin n → M
revert : ∀ {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
⊢ (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs

Tactic:
revert ψ
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hφ : φ_1.IsQF
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
of_isQF : (φ_1.toPrenexImpRight ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
⊢ (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs

Tactic:
rw [hφ.toPrenexImp]

Premises used: FirstOrder.Language.BoundedFormula.IsQF.toPrenexImp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hφ : φ_1.IsQF
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ (φ_1.toPrenexImpRight ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs

Tactic:
realize_toPrenexImpRight hφ hψ

Premises used: FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hφ : φ_1.IsQF
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ (φ_1.toPrenexImpRight ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs

Tactic:
exact realize_toPrenexImpRight hφ hψ

Premises used: FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
all :
  (∃ (a : M), (φ_1.toPrenexImp (liftAt 1 n_1 ψ)).Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    (∀' φ_1 ⟹ ψ).Realize v xs
⊢ (∃' φ_1.toPrenexImp (liftAt 1 n_1 ψ)).Realize v xs ↔ (∀' φ_1 ⟹ ψ).Realize v xs

Tactic:
rw [realize_ex]

Premises used: FirstOrder.Language.BoundedFormula.realize_ex
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ (∃ (a : M), (φ_1.toPrenexImp (liftAt 1 n_1 ψ)).Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    (∀' φ_1 ⟹ ψ).Realize v xs

Tactic:
_root_.trans (exists_congr fun _ => ih hψ.liftAt) ?_

Premises used: trans, exists_congr, FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
all :
  (∃ (a : M), (φ_1 ⟹ liftAt 1 n_1 ψ).Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    (∀' φ_1 ⟹ ψ).Realize v xs
⊢ (∃ (a : M), (φ_1.toPrenexImp (liftAt 1 n_1 ψ)).Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    (∀' φ_1 ⟹ ψ).Realize v xs

Tactic:
refine _root_.trans (exists_congr fun _ => ih hψ.liftAt) ?_

Premises used: trans, exists_congr, FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
all :
  (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a) → ψ.Realize v xs) ↔
    (∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) → ψ.Realize v xs
⊢ (∃ (a : M), (φ_1 ⟹ liftAt 1 n_1 ψ).Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    (∀' φ_1 ⟹ ψ).Realize v xs

Tactic:
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]

Premises used: Fin.snoc_comp_castSucc, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.BoundedFormula.realize_liftAt_one_self, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a) → ψ.Realize v xs) ↔
    (∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) → ψ.Realize v xs

Tactic:
Iff.symm forall_imp_iff_exists_imp

Premises used: forall_imp_iff_exists_imp, Iff.symm
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a) → ψ.Realize v xs) ↔
    (∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) → ψ.Realize v xs

Tactic:
exact Iff.symm forall_imp_iff_exists_imp

Premises used: forall_imp_iff_exists_imp, Iff.symm
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ ((∃' φ_1).toPrenexImp ψ).Realize v xs ↔ (∃' φ_1 ⟹ ψ).Realize v xs

Tactic:
_root_.trans (forall_congr' fun _ => ih hψ.liftAt) ?_

Premises used: trans, forall_congr', FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
ex :
  (∀ (a : M), (φ_1 ⟹ liftAt 1 n_1 ψ).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) ↔
    (∃' φ_1 ⟹ ψ).Realize v xs
⊢ ((∃' φ_1).toPrenexImp ψ).Realize v xs ↔ (∃' φ_1 ⟹ ψ).Realize v xs

Tactic:
refine _root_.trans (forall_congr' fun _ => ih hψ.liftAt) ?_

Premises used: trans, forall_congr', FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {xs : Fin (n_1 + 1) → M} {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex),
    (φ_1.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
xs : Fin n_1 → M
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ (∀ (a : M), (φ_1 ⟹ liftAt 1 n_1 ψ).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) ↔
    (∃' φ_1 ⟹ ψ).Realize v xs

Tactic:
simp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
hφ : φ.IsPrenex
v : α → M
xs : Fin n → M
of_isQF :
  ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hφ : φ.IsQF) {xs : Fin n → M} {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex),
    (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
all :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsPrenex →
      ∀
        (ih :
          ∀ {xs : Fin (n + 1) → M} {ψ : L.BoundedFormula α (n + 1)} (hψ : ψ.IsPrenex),
            (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs)
        {xs : Fin n → M} {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex),
        ((∀' φ).toPrenexImp ψ).Realize v xs ↔ (∀' φ ⟹ ψ).Realize v xs
ex :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsPrenex →
      ∀
        (ih :
          ∀ {xs : Fin (n + 1) → M} {ψ : L.BoundedFormula α (n + 1)} (hψ : ψ.IsPrenex),
            (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs)
        {xs : Fin n → M} {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex),
        ((∃' φ).toPrenexImp ψ).Realize v xs ↔ (∃' φ ⟹ ψ).Realize v xs
⊢ ∀ {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs

Tactic:
induction hφ with
  | of_isQF hφ =>
    intro ψ hψ
    rw [hφ.toPrenexImp]
    exact realize_toPrenexImpRight hφ hψ
  | all _ ih =>
    intro ψ hψ
    unfold toPrenexImp
    rw [realize_ex]
    refine _root_.trans (exists_congr fun _ => ih hψ.liftAt) ?_
    simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
    exact Iff.symm forall_imp_iff_exists_imp
  | ex _ ih =>
    intro ψ hψ
    refine _root_.trans (forall_congr' fun _ => ih hψ.liftAt) ?_
    simp

Premises used: FirstOrder.Language.BoundedFormula.realize_ex, Fin.snoc_comp_castSucc, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.BoundedFormula.realize_liftAt_one_self, FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.toPrenexImp, forall_imp_iff_exists_imp, Iff.symm
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 : ℕ
xs : Fin n_1 → M
⊢ Realize.{u, v, w, u'} (L := L) (toPrenex falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) falsum v xs

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.BoundedFormula.toPrenex
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 : ℕ
⊢ ∀ {xs : Fin n_1 → M},
    Realize.{u, v, w, u'} (L := L) (toPrenex falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) falsum v xs

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ (equal t₁ t₂).toPrenex.Realize v xs ↔ (equal t₁ t₂).Realize v xs

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.Term.bdEqual, FirstOrder.Language.BoundedFormula.toPrenex
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ ∀ {xs : Fin n_1 → M}, (equal t₁ t₂).toPrenex.Realize v xs ↔ (equal t₁ t₂).Realize v xs

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ (rel R ts).toPrenex.Realize v xs ↔ (rel R ts).Realize v xs

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.BoundedFormula.toPrenex
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ ∀ {xs : Fin n_1 → M}, (rel R ts).toPrenex.Realize v xs ↔ (rel R ts).Realize v xs

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 : ℕ
f1 f2 : L.BoundedFormula α n_1
h1 : ∀ {xs : Fin n_1 → M}, f1.toPrenex.Realize v xs ↔ f1.Realize v xs
h2 : ∀ {xs : Fin n_1 → M}, f2.toPrenex.Realize v xs ↔ f2.Realize v xs
xs : Fin n_1 → M
imp : (f1.toPrenex.toPrenexImp f2.toPrenex).Realize v xs ↔ (f1 ⟹ f2).Realize v xs
imp₁ : (f1.toPrenex ⟹ f2.toPrenex).Realize v xs ↔ (f1 ⟹ f2).Realize v xs
imp₂ : f1.toPrenex.Realize v xs → f2.toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs
imp₃ : f1.toPrenex.Realize v xs → f2.toPrenex.Realize v xs ↔ f1.Realize v xs → f2.Realize v xs
imp₄ : f1.Realize v xs → f2.toPrenex.Realize v xs ↔ f1.Realize v xs → f2.Realize v xs
imp₅ imp₆ : f1.Realize v xs → f2.Realize v xs ↔ f1.Realize v xs → f2.Realize v xs
⊢ (f1 ⟹ f2).toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs

Tactic:
rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
      realize_imp, h1, h2]

Premises used: FirstOrder.Language.BoundedFormula.realize_toPrenexImp, FirstOrder.Language.BoundedFormula.toPrenex_isPrenex, FirstOrder.Language.BoundedFormula.toPrenex, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
h : ∀ {xs : Fin (n_1 + 1) → M}, f.toPrenex.Realize v xs ↔ f.Realize v xs
xs : Fin n_1 → M
all :
  (∀ (a : M), f.toPrenex.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    ∀ (a : M), f.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
⊢ (∀' f).toPrenex.Realize v xs ↔ (∀' f).Realize v xs

Tactic:
rw [realize_all, toPrenex, realize_all]

Premises used: FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.BoundedFormula.toPrenex
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
h : ∀ {xs : Fin (n_1 + 1) → M}, f.toPrenex.Realize v xs ↔ f.Realize v xs
xs : Fin n_1 → M
⊢ (∀ (a : M), f.toPrenex.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    ∀ (a : M), f.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
forall_congr' fun a => h

Premises used: forall_congr'
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
v : α → M
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
h : ∀ {xs : Fin (n_1 + 1) → M}, f.toPrenex.Realize v xs ↔ f.Realize v xs
xs : Fin n_1 → M
⊢ (∀ (a : M), f.toPrenex.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    ∀ (a : M), f.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
exact forall_congr' fun a => h

Premises used: forall_congr'
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
falsum :
  ∀ {n : ℕ} {xs : Fin n → M},
    Realize.{u, v, w, u'} (L := L) (toPrenex BoundedFormula.falsum) v xs ↔
      Realize.{u, v, w, u'} (L := L) BoundedFormula.falsum v xs
equal :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (BoundedFormula.equal t₁ t₂).toPrenex.Realize v xs ↔ (BoundedFormula.equal t₁ t₂).Realize v xs
rel :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
    (BoundedFormula.rel R ts).toPrenex.Realize v xs ↔ (BoundedFormula.rel R ts).Realize v xs
imp :
  ∀ {n : ℕ} (f1 f2 : L.BoundedFormula α n) (h1 : ∀ {xs : Fin n → M}, f1.toPrenex.Realize v xs ↔ f1.Realize v xs)
    (h2 : ∀ {xs : Fin n → M}, f2.toPrenex.Realize v xs ↔ f2.Realize v xs) {xs : Fin n → M},
    (f1 ⟹ f2).toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs
all :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1)) (h : ∀ {xs : Fin (n + 1) → M}, f.toPrenex.Realize v xs ↔ f.Realize v xs)
    {xs : Fin n → M}, (∀' f).toPrenex.Realize v xs ↔ (∀' f).Realize v xs
⊢ ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs

Tactic:
induction φ with
  | falsum => exact Iff.rfl
  | equal => exact Iff.rfl
  | rel => exact Iff.rfl
  | imp f1 f2 h1 h2 =>
    intros
    rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
      realize_imp, h1, h2]
  | all _ h =>
    intros
    rw [realize_all, toPrenex, realize_all]
    exact forall_congr' fun a => h

Premises used: FirstOrder.Language.BoundedFormula.imp, Iff.rfl, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, FirstOrder.Language.BoundedFormula.toPrenex, FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : L.BoundedFormula α n → Prop
φ : L.BoundedFormula α n
h : φ.IsQF
hf : P ⊥
ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ
hsup : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)
hnot : ∀ {φ : L.BoundedFormula α n}, P φ → P ∼φ
hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
⊢ P φ

Tactic:
IsQF.recOn h hf @ha fun {φ₁ φ₂} _ _ h1 h2 =>
    (hse (φ₁.imp_iff_not_sup φ₂)).2 (hsup (hnot h1) h2)

Premises used: FirstOrder.Language.BoundedFormula.IsQF.recOn
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : L.BoundedFormula α n → Prop
φ : L.BoundedFormula α n
h : φ.IsQF
hf : P ⊥
ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ
hinf : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)
hnot : ∀ {φ : L.BoundedFormula α n}, P φ → P ∼φ
hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
⊢ P φ

Tactic:
h.induction_on_sup_not hf ha
    (fun {φ₁ φ₂} h1 h2 =>
      (hse (φ₁.sup_iff_not_inf_not φ₂)).2 (hnot (hinf (hnot h1) (hnot h2))))
    (fun {_} => hnot) fun {_ _} => hse

Premises used: Iff.mpr, FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not, FirstOrder.Language.BoundedFormula.sup_iff_not_inf_not
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
M : Theory.ModelType (L := L) ∅
v : α → (↑M : Type (max (max u v) u'))
xs : Fin n → (↑M : Type (max (max u v) u'))
rw : φ.Realize v xs ↔ φ.toPrenex.Realize v xs
rw₁ rw₂ : φ.Realize v xs ↔ φ.Realize v xs
⊢ (φ ⇔ φ.toPrenex).Realize v xs

Tactic:
rw [realize_iff, realize_toPrenex]

Premises used: FirstOrder.Language.BoundedFormula.realize_toPrenex, FirstOrder.Language.BoundedFormula.realize_iff
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
suffices : ∀ {m : ℕ} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ
⊢ P φ

Tactic:
suffices h' : ∀ {m} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ from
    (hse φ.iff_toPrenex).2 (h' φ.toPrenex_isPrenex)
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ_1 : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
n_1 : ℕ
φ_2 : L.BoundedFormula α n_1
hφ : φ_2.IsQF
⊢ P φ_2

Tactic:
hqf hφ
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ_1 : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
n_1 : ℕ
φ_2 : L.BoundedFormula α n_1
hφ : φ_2.IsQF
⊢ P φ_2

Tactic:
exact hqf hφ
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ_1 : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : L.BoundedFormula α m
n_1 : ℕ
φ_2 : L.BoundedFormula α (n_1 + 1)
h : φ_2.IsPrenex
hφ : P φ_2
⊢ P (∀' φ_2)

Tactic:
hall hφ