awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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.toPrenexImp ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
have of_isQF : (φ_1.toPrenexImpRight ψ).Realize v xs ↔ (φ_1 ⟹ ψ).Realize v xs
Tactic: rw [hφ.toPrenexImp]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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 (liftAt 1 n_1 ψ)).Realize v xs ↔ (∀' φ_1 ⟹ ψ).Realize v xs
have 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
Tactic: rw [realize_ex]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
have all : (∃ (a : M), (φ_1 ⟹ 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) ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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.succ) ↦ M) xs a)) ↔
    (∀' φ_1 ⟹ ψ).Realize v xs
have 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
Tactic: simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
have ex : (∀ (a : M), (φ_1 ⟹ liftAt 1 n_1 ψ).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) ↔ (∃' φ_1 ⟹ ψ).Realize v xs
Tactic: refine _root_.trans (forall_congr' fun _ => ih hψ.liftAt) ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ ∀ {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
have of_isQF : ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hφ : φ.IsQF) {xs : Fin n → M} {ψ : 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
Cleared hypotheses: hφ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ ∀ {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
have 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
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
Cleared hypotheses: hφ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ ∀ {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
have 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
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
Cleared hypotheses: hφ, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (f1 ⟹ f2).toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs
have imp : (f1.toPrenex.toPrenexImp 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]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (f1 ⟹ f2).toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs
have imp₁ : (f1.toPrenex ⟹ 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]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (f1 ⟹ f2).toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs
have imp₂ : f1.toPrenex.Realize v xs → 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]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (f1 ⟹ f2).toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs
have imp₃ : f1.toPrenex.Realize v xs → f2.toPrenex.Realize v xs ↔ f1.Realize v xs → f2.Realize v xs
Tactic: rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
      realize_imp, h1, h2]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (f1 ⟹ f2).toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs
have imp₄ : f1.Realize v xs → f2.toPrenex.Realize v xs ↔ f1.Realize v xs → f2.Realize v xs
Tactic: rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
      realize_imp, h1, h2]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (f1 ⟹ f2).toPrenex.Realize v xs ↔ (f1 ⟹ f2).Realize v xs
have imp₅ : f1.Realize v xs → f2.Realize v xs ↔ f1.Realize v xs → f2.Realize v xs
Tactic: rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
      realize_imp, h1, h2]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (∀' f).toPrenex.Realize v xs ↔ (∀' f).Realize v xs
have 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)
Tactic: rw [realize_all, toPrenex, realize_all]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
inst_1 : Nonempty M
φ : L.BoundedFormula α n
v : α → M
⊢ ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs
have falsum : ∀ {n : ℕ} {xs : Fin n → M},
  Realize.{u, v, w, u'} (L := L) (toPrenex falsum) v xs ↔ Realize.{u, v, w, u'} (L := L) falsum 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
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs
have equal : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
  (equal t₁ t₂).toPrenex.Realize v xs ↔ (equal t₁ t₂).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
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs
have rel : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)) {xs : Fin n → M},
  (rel R ts).toPrenex.Realize v xs ↔ (rel R ts).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
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs
have 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
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
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs
have 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
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
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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'))
⊢ (φ ⇔ φ.toPrenex).Realize v xs
have rw : φ.Realize v xs ↔ φ.toPrenex.Realize v xs
Tactic: rw [realize_iff, realize_toPrenex]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (φ ⇔ φ.toPrenex).Realize v xs
have rw₁ : φ.Realize v xs ↔ φ.Realize v xs
Tactic: rw [realize_iff, realize_toPrenex]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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 φ₂)
⊢ P φ
have suffices : ∀ {m : ℕ} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ
Tactic: suffices h' : ∀ {m} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ from
    (hse φ.iff_toPrenex).2 (h' φ.toPrenex_isPrenex)
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
hφ : φ.IsPrenex
of_isQF : ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hφ : φ.IsQF), P φ
⊢ P φ
have all : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → ∀ (hφ : P φ), P (∀' φ)
Tactic: induction hφ with
  | of_isQF hφ => exact hqf hφ
  | all _ hφ => exact hall hφ
  | ex _ hφ => exact hex hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
hφ : φ.IsPrenex
of_isQF : ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hφ : φ.IsQF), P φ
all : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → ∀ (hφ : P φ), P (∀' φ)
⊢ P φ
have ex : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsPrenex → ∀ (hφ : P φ), P (∃' φ)
Tactic: induction hφ with
  | of_isQF hφ => exact hqf hφ
  | all _ hφ => exact hall hφ
  | ex _ hφ => exact hex hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
φ : L.BoundedFormula α n
inst_3 : L.HomClass F M N
f : F
hInj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
v : α → M
xs : Fin n → M
l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
⊢ (R.boundedFormula ts).Realize v xs →
    Realize.{u, v, u_2, u'} (M := N) (R.boundedFormula ts) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
have rel : (RelMap.{u, v, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)) →
  RelMap.{u, v, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))
Tactic: simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
φ : L.BoundedFormula α n
hA : φ.IsAtomic
inst_3 : L.HomClass F M N
f : F
hInj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
v : α → M
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)
have equal : ∀ (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
  (t₁ =' t₂).Realize v xs →
    Realize.{u, v, u_2, u'} (M := N) (t₁ =' t₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
Tactic: induction hA with
  | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff,
    imp_self]
  | rel R ts =>
    simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
    exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
Cleared hypotheses: hA