awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
h₁ : f = f.comp (h.comp h.symm)
h₂ : f = f.comp (refl L N)
⊢ f = comp ((fun (f : N ≃[L] P) ↦ f.comp h) f) h.symm
have h₃ : f = f
Tactic: rw [comp_assoc, self_comp_symm, comp_refl]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
⊢ g = comp ((fun (f : N ≃[L] P) ↦ f.comp h) g) h.symm
have h₁ : g = g.comp (h.comp h.symm)
Tactic: rw [comp_assoc, self_comp_symm, comp_refl]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
h₁ : g = g.comp (h.comp h.symm)
⊢ g = comp ((fun (f : N ≃[L] P) ↦ f.comp h) g) h.symm
have h₂ : g = g.comp (refl L N)
Tactic: rw [comp_assoc, self_comp_symm, comp_refl]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : Eq (α := M ≃[L] P) ((fun (f : N ≃[L] P) ↦ f.comp h) f) ((fun (f : N ≃[L] P) ↦ f.comp h) g)
h₁ : g = g.comp (h.comp h.symm)
h₂ : g = g.comp (refl L N)
⊢ g = comp ((fun (f : N ≃[L] P) ↦ f.comp h) g) h.symm
have h₃ : g = g
Tactic: rw [comp_assoc, self_comp_symm, comp_refl]
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
a : Language.empty.Structure M
⊢ a = default
have funMap : ∀ (x : ℕ) (f : Language.empty.Functions x) (x_1 : Fin x → M), funMap f x_1 = funMap f x_1
Tactic: ext _ f
-- Lean 4 proof step from Mathlib.ModelTheory.Basic (goal)
Goal:
L : Language
L' : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
P : Type u_1
inst_2 : L.Structure P
Q : Type u_2
inst_3 : L.Structure Q
a : Language.empty.Structure M
funMap : ∀ (x : ℕ) (f : Language.empty.Functions x) (x_1 : Fin x → M), Structure.funMap f x_1 = Structure.funMap f x_1
⊢ a = default
have RelMap : ∀ (x : ℕ) (f : Language.empty.Relations x) (x_1 : Fin x → M), RelMap f x_1 ↔ RelMap f x_1
Tactic: ext _ f
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (hypothesis)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' φ).IsQF
⊢ False
have con₁ : (∀' φ).IsAtomic
Tactic: obtain - | con := con
Cleared hypotheses: con
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃' φ).IsQF
⊢ False
have of_isAtomic : ∀ (con : (∃' φ).IsAtomic), False
Tactic: obtain - | con | con := con
Cleared hypotheses: con
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃' φ).IsQF
of_isAtomic : ∀ (con : (∃' φ).IsAtomic), False
⊢ False
have imp : ∀ (con : (∀' ∼φ).IsQF), IsQF.{u, v, u'} (L := L) (α := α) (n := n) ⊥ → False
Tactic: obtain - | con | con := con
Cleared hypotheses: con
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n_1 : ℕ
φ_1 : L.BoundedFormula α n_1
hψ : φ_1.IsQF
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight φ_1).IsPrenex
have of_isQF : (φ ⟹ φ_1).IsPrenex
Tactic: rw [hψ.toPrenexImpRight]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsQF
hψ : ψ.IsPrenex
⊢ (φ.toPrenexImpRight ψ).IsPrenex
have of_isQF : ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hψ : φ.IsQF) {φ_1 : L.BoundedFormula α n} (hφ : φ_1.IsQF),
  (φ_1.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
Cleared hypotheses: φ, hφ, hψ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (φ.toPrenexImpRight ψ).IsPrenex
have 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
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
Cleared hypotheses: φ, hφ, hψ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (φ.toPrenexImpRight ψ).IsPrenex
have 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
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
Cleared hypotheses: φ, hφ, hψ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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.toPrenexImp ψ).IsPrenex
have of_isQF : (φ_1.toPrenexImpRight ψ).IsPrenex
Tactic: rw [hφ.toPrenexImp]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
φ ψ : L.BoundedFormula α n
hφ : φ.IsPrenex
hψ : ψ.IsPrenex
⊢ (φ.toPrenexImp ψ).IsPrenex
have of_isQF : ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hφ : φ.IsQF) {ψ : L.BoundedFormula α n} (hψ : ψ.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
Cleared hypotheses: ψ, hφ, hψ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (φ.toPrenexImp ψ).IsPrenex
have all : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
  φ.IsPrenex →
    ∀ (ih1 : ∀ {ψ : L.BoundedFormula α (n + 1)} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).IsPrenex)
      {ψ : L.BoundedFormula α n} (hψ : ψ.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
Cleared hypotheses: ψ, hφ, hψ
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
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
⊢ (φ.toPrenexImp ψ).IsPrenex
have ex : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
  φ.IsPrenex →
    ∀ (ih2 : ∀ {ψ : L.BoundedFormula α (n + 1)} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).IsPrenex)
      {ψ : L.BoundedFormula α n} (hψ : ψ.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
Cleared hypotheses: ψ, hφ, hψ
-- 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
φ : L.BoundedFormula α n_1
hφ : φ.IsQF
xs : Fin n_1 → M
⊢ (φ.toPrenexImpRight φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
have of_isQF : (φ ⟹ φ_1).Realize v xs ↔ (φ ⟹ φ_1).Realize v xs
Tactic: rw [hψ.toPrenexImpRight]
-- 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 :
  ∀ {φ : 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
have all : (∀ (a : M), (liftAt 1 n_1 φ ⟹ φ_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
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), (liftAt 1 n_1 φ ⟹ φ_1).Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) ↔
    (φ ⟹ ∀' φ_1).Realize v xs
have 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)
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 :
  ∀ {φ : 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 (liftAt 1 n_1 φ) φ_1).Realize v xs ↔ (φ ⟹ ∃' φ_1).Realize v xs
have 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
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 :
  ∀ {φ : 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
have ex : (∃ (a : M), (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) ?_
-- 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 :
  ∀ {φ : 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), (liftAt 1 n_1 φ ⟹ φ_1).Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)) ↔
    (φ ⟹ ∃' φ_1).Realize v xs
have 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)
Tactic: simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, 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 :
  ∀ {φ : 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)
have 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)
Tactic: refine ⟨?_, fun h' => ?_⟩
-- 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 :
  ∀ {φ : 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), φ.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)
have 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)
Tactic: refine ⟨?_, fun h' => ?_⟩
-- 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 :
  ∀ {φ : 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)
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
have pos : ∀ (h : φ.Realize v xs), ∃ (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
-- 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 :
  ∀ {φ : 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)
⊢ ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
have neg : ∀ (h : ¬φ.Realize v xs), ∃ (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
-- 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 : φ_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), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
have 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)
Tactic: obtain ⟨a, ha⟩ := h' h
-- 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 : φ_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), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
have neg : ∀ (inhabited_h : Inhabited M), ∃ (a : M), φ.Realize v xs → φ_1.Realize v (snoc (α := fun (a : Fin n_1.succ) ↦ M) xs a)
Tactic: inhabit M
-- 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φ : φ.IsQF
hψ : ψ.IsPrenex
v : α → M
xs : Fin n → M
⊢ (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
have 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
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⟩
Cleared hypotheses: φ, hφ, 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φ : φ.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
⊢ (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
have 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
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⟩
Cleared hypotheses: φ, hφ, 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φ : φ.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
⊢ (φ.toPrenexImpRight ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
have 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
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⟩
Cleared hypotheses: φ, hφ, 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
hψ : ψ.IsPrenex
v : α → M
xs : Fin n → M
⊢ (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
have revert : ∀ {ψ : L.BoundedFormula α n} (hψ : ψ.IsPrenex), (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs
Tactic: revert ψ
Cleared hypotheses: ψ, hψ