awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih2 : ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF), (φ.toPrenexImpRight φ_1).IsPrenex
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight (∃' φ_1)).IsPrenex

Tactic:
exact (ih2 hφ.liftAt).ex

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.ex, FirstOrder.Language.BoundedFormula.IsQF.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsQF
hψ : ψ.IsPrenex
of_isQF :
  ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hψ : φ.IsQF) {φ_1 : L.BoundedFormula α n} (hφ : φ_1.IsQF),
    (φ_1.toPrenexImpRight φ).IsPrenex
all :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsPrenex →
      ∀ (ih1 : ∀ {φ_1 : L.BoundedFormula α (n + 1)} (hφ : φ_1.IsQF), (φ_1.toPrenexImpRight φ).IsPrenex)
        {φ_1 : L.BoundedFormula α n} (hφ : φ_1.IsQF), (φ_1.toPrenexImpRight (∀' φ)).IsPrenex
ex :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsPrenex →
      ∀ (ih2 : ∀ {φ_1 : L.BoundedFormula α (n + 1)} (hφ : φ_1.IsQF), (φ_1.toPrenexImpRight φ).IsPrenex)
        {φ_1 : L.BoundedFormula α n} (hφ : φ_1.IsQF), (φ_1.toPrenexImpRight (∃' φ)).IsPrenex
⊢ (φ.toPrenexImpRight ψ).IsPrenex

Tactic:
induction hψ with
  | of_isQF hψ => rw [hψ.toPrenexImpRight]; exact (hφ.imp hψ).isPrenex
  | all _ ih1 => exact (ih1 hφ.liftAt).all
  | ex _ ih2 => exact (ih2 hφ.liftAt).ex

Premises used: FirstOrder.Language.BoundedFormula.all
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hφ : φ_1.IsQF
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
of_isQF : (φ_1.toPrenexImpRight ψ).IsPrenex
⊢ (φ_1.toPrenexImp ψ).IsPrenex

Tactic:
rw [hφ.toPrenexImp]

Premises used: FirstOrder.Language.BoundedFormula.IsQF.toPrenexImp
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hφ : φ_1.IsQF
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ (φ_1.toPrenexImpRight ψ).IsPrenex

Tactic:
isPrenex_toPrenexImpRight hφ hψ

Premises used: FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hφ : φ_1.IsQF
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ (φ_1.toPrenexImpRight ψ).IsPrenex

Tactic:
exact isPrenex_toPrenexImpRight hφ hψ

Premises used: FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih1 : ∀ {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex), (φ_1.toPrenexImp ψ).IsPrenex
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ ((∀' φ_1).toPrenexImp ψ).IsPrenex

Tactic:
(ih1 hψ.liftAt).ex

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.ex, FirstOrder.Language.BoundedFormula.toPrenexImp, FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih1 : ∀ {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex), (φ_1.toPrenexImp ψ).IsPrenex
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ ((∀' φ_1).toPrenexImp ψ).IsPrenex

Tactic:
exact (ih1 hψ.liftAt).ex

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.ex, FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih2 : ∀ {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex), (φ_1.toPrenexImp ψ).IsPrenex
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ ((∃' φ_1).toPrenexImp ψ).IsPrenex

Tactic:
(ih2 hψ.liftAt).all

Premises used: FirstOrder.Language.BoundedFormula.not, FirstOrder.Language.BoundedFormula.IsPrenex.all, FirstOrder.Language.BoundedFormula.ex, FirstOrder.Language.BoundedFormula.toPrenexImp, FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih2 : ∀ {ψ : L.BoundedFormula α (n_1 + 1)} (hψ : ψ.IsPrenex), (φ_1.toPrenexImp ψ).IsPrenex
ψ : L.BoundedFormula α n_1
hψ : ψ.IsPrenex
⊢ ((∃' φ_1).toPrenexImp ψ).IsPrenex

Tactic:
exact (ih2 hψ.liftAt).all

Premises used: FirstOrder.Language.BoundedFormula.IsPrenex.all, FirstOrder.Language.BoundedFormula.IsPrenex.liftAt
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsPrenex
hψ : ψ.IsPrenex
of_isQF :
  ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hφ : φ.IsQF) {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex),
    (φ.toPrenexImp ψ).IsPrenex
all :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsPrenex →
      ∀ (ih1 : ∀ {ψ : L.BoundedFormula α (n + 1)} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).IsPrenex)
        {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex), ((∀' φ).toPrenexImp ψ).IsPrenex
ex :
  ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
    φ.IsPrenex →
      ∀ (ih2 : ∀ {ψ : L.BoundedFormula α (n + 1)} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).IsPrenex)
        {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex), ((∃' φ).toPrenexImp ψ).IsPrenex
⊢ (φ.toPrenexImp ψ).IsPrenex

Tactic:
induction hφ with
  | of_isQF hφ => rw [hφ.toPrenexImp]; exact isPrenex_toPrenexImpRight hφ hψ
  | all _ ih1 => exact (ih1 hψ.liftAt).ex
  | ex _ ih2 => exact (ih2 hψ.liftAt).all

Premises used: FirstOrder.Language.BoundedFormula.all
-- Module: Mathlib.ModelTheory.Complexity
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
⊢ φ.toPrenex.IsPrenex

Tactic:
BoundedFormula.recOn φ isQF_bot.isPrenex (fun _ _ => (IsAtomic.equal _ _).isPrenex)
    (fun _ _ => (IsAtomic.rel _ _).isPrenex) (fun _ _ h1 h2 => isPrenex_toPrenexImp h1 h2)
    fun _ => IsPrenex.all

Premises used: FirstOrder.Language.BoundedFormula.recOn
-- 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
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
of_isQF of_isQF₁ : (φ ⟹ φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
⊢ (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs

Tactic:
rw [hψ.toPrenexImpRight]

Premises used: FirstOrder.Language.BoundedFormula.IsQF.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 :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
⊢ (φ.toPrenexImpRight (∀' φ_1)).Realize v xs ↔ (φ ⟹ ∀' φ_1).Realize v xs

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

Premises used: trans, FirstOrder.Language.BoundedFormula.IsQF.liftAt, 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
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
all :
  (∀ (a : M), (liftAt 1 n_1 φ ⟹ φ_1).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) ↔
    (φ ⟹ ∀' φ_1).Realize v xs
⊢ (φ.toPrenexImpRight (∀' φ_1)).Realize v xs ↔ (φ ⟹ ∀' φ_1).Realize v xs

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

Premises used: trans, FirstOrder.Language.BoundedFormula.IsQF.liftAt, 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
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
all :
  (∀ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) ↔
    φ.Realize v xs → ∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
⊢ (∀ (a : M), (liftAt 1 n_1 φ ⟹ φ_1).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ 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 :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
⊢ (∀ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) ↔
    φ.Realize v xs → ∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
⟨fun h1 a h2 => h1 h2 a, fun h1 h2 a => h1 a h2⟩

Premises used: Iff.intro
-- 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 :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
⊢ (∀ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) ↔
    φ.Realize v xs → ∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
exact ⟨fun h1 a h2 => h1 h2 a, fun h1 h2 a => h1 a h2⟩
-- 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 :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
ex :
  (∃ (a : M), (toPrenexImpRight (liftAt 1 n_1 φ) φ_1).Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    (φ ⟹ ∃' φ_1).Realize v xs
⊢ (∃' toPrenexImpRight (liftAt 1 n_1 φ) φ_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 :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
⊢ (∃ (a : M), (toPrenexImpRight (liftAt 1 n_1 φ) φ_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, FirstOrder.Language.BoundedFormula.IsQF.liftAt, exists_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
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
ex :
  (∃ (a : M), (liftAt 1 n_1 φ ⟹ φ_1).Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    (φ ⟹ ∃' φ_1).Realize v xs
⊢ (∃ (a : M), (toPrenexImpRight (liftAt 1 n_1 φ) φ_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, FirstOrder.Language.BoundedFormula.IsQF.liftAt, exists_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
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
ex :
  (∃ (a : M), φ.Realize v xs → φ_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)
⊢ (∃ (a : M), (liftAt 1 n_1 φ ⟹ φ_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_ex]

Premises used: FirstOrder.Language.BoundedFormula.realize_ex, Fin.snoc_comp_castSucc, 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 :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
⊢ (∃ (a : M), φ.Realize v xs → φ_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)

Tactic:
⟨?_, fun h' => ?_⟩

Premises used: Iff.intro
-- 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 :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
ex :
  (∃ (a : M), φ.Realize v xs → φ_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)
ex₁ :
  ∀ (h' : φ.Realize v xs → ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)),
    ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
⊢ (∃ (a : M), φ.Realize v xs → φ_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)

Tactic:
refine ⟨?_, fun h' => ?_⟩
-- 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 : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
a : M
ha : φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
h : φ.Realize v xs
⊢ ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
⟨a, ha h⟩

Premises used: Exists.intro
-- 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 : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
a : M
ha : φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
h : φ.Realize v xs
⊢ ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
exact ⟨a, ha h⟩
-- 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 :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
h' : φ.Realize v xs → ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
pos : ∀ (h : φ.Realize v xs), ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
neg : ∀ (h : ¬φ.Realize v xs), ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
by_cases h : φ.Realize v xs

Premises used: FirstOrder.Language.BoundedFormula.Realize
-- 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 : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
h' : φ.Realize v xs → ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
h : φ.Realize v xs
pos :
  ∀ (a : M) (ha : φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)),
    ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
obtain ⟨a, ha⟩ := h' h
-- 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 : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
h' : φ.Realize v xs → ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
h : φ.Realize v xs
a : M
ha : φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
⟨a, fun _ => ha⟩

Premises used: Exists.intro
-- 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 : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
h' : φ.Realize v xs → ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
h : φ.Realize v xs
a : M
ha : φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
exact ⟨a, fun _ => ha⟩
-- 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 : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
h' : φ.Realize v xs → ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
h : ¬φ.Realize v xs
neg :
  ∀ (inhabited_h : Inhabited M), ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
inhabit M
-- 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 : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
h' : φ.Realize v xs → ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
h : ¬φ.Realize v xs
inhabited_h : Inhabited M
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
⟨default, fun h'' => (h h'').elim⟩

Premises used: Inhabited.default, False.elim, Exists.intro
-- 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 : φ_1.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n_1 + 1)} (hφ : φ.IsQF) {xs : Fin (n_1 + 1) → M},
    (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
h' : φ.Realize v xs → ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
h : ¬φ.Realize v xs
inhabited_h : Inhabited M
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)

Tactic:
exact ⟨default, fun h'' => (h h'').elim⟩