-- Mathlib/ModelTheory/Complexity.lean
theorem realize_toPrenexImp {φ ψ : L.BoundedFormula α n} (hφ : IsPrenex φ) (hψ : IsPrenex ψ)
    {v : α → M} {xs : Fin n → M} : (φ.toPrenexImp ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ ψ : L.BoundedFormula α n
hφ : φ.IsPrenex
hψ : ψ.IsPrenex
v : α → M
xs : Fin n → M
⊢ (φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs

Tactic:
revert ψ

Result:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
hφ : φ.IsPrenex
v : α → M
xs : Fin n → M
⊢ ∀ {ψ : L.BoundedFormula α n}, ψ.IsPrenex → ((φ.toPrenexImp ψ).Realize v xs ↔ (φ ⟹ ψ).Realize v xs)

Proof state:
case ex
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
⊢ ∀ {ψ : L.BoundedFormula α n✝}, ψ.IsPrenex → (((∃'φ✝).toPrenexImp ψ).Realize v xs ↔ (∃'φ✝ ⟹ ψ).Realize v xs)

Tactic:
intro ψ hψ

Result:
case ex
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ ((∃'φ✝).toPrenexImp ψ).Realize v xs ↔ (∃'φ✝ ⟹ ψ).Realize v xs

Proof state:
case ex
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (∀ (a : M), (φ✝ ⟹ liftAt 1 n✝ ψ).Realize v (snoc xs a)) ↔ (∃'φ✝ ⟹ ψ).Realize v xs

Tactic:
simp

Result:
no goals

Proof state:
case all.refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
h' : (∀ (a : M), φ✝.Realize v (snoc xs a)) → ψ.Realize v xs
⊢ ∃ a, φ✝.Realize v (snoc xs a) → ψ.Realize v xs

Tactic:
by_cases h : ψ.Realize v xs

Result:
case pos
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
h' : (∀ (a : M), φ✝.Realize v (snoc xs a)) → ψ.Realize v xs
h : ψ.Realize v xs
⊢ ∃ a, φ✝.Realize v (snoc xs a) → ψ.Realize v xs

case neg
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
h' : (∀ (a : M), φ✝.Realize v (snoc xs a)) → ψ.Realize v xs
h : ¬ψ.Realize v xs
⊢ ∃ a, φ✝.Realize v (snoc xs a) → ψ.Realize v xs

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (∃'φ✝.toPrenexImp (liftAt 1 n✝ ψ)).Realize v xs ↔ (∀'φ✝ ⟹ ψ).Realize v xs

Tactic:
rw [realize_ex]

Result:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (∃ a, (φ✝.toPrenexImp (liftAt 1 n✝ ψ)).Realize v (snoc xs a)) ↔ (∀'φ✝ ⟹ ψ).Realize v xs

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
⊢ ∀ {ψ : L.BoundedFormula α n✝}, ψ.IsPrenex → (((∀'φ✝).toPrenexImp ψ).Realize v xs ↔ (∀'φ✝ ⟹ ψ).Realize v xs)

Tactic:
intro ψ hψ

Result:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ ((∀'φ✝).toPrenexImp ψ).Realize v xs ↔ (∀'φ✝ ⟹ ψ).Realize v xs

Proof state:
case of_isQF
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs

Tactic:
rw [hφ.toPrenexImp]

Result:
case of_isQF
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hφ : φ✝.IsQF
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (φ✝.toPrenexImpRight ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs

Proof state:
case neg
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
h' : (∀ (a : M), φ✝.Realize v (snoc xs a)) → ψ.Realize v xs
h : ¬ψ.Realize v xs
⊢ ∃ a, φ✝.Realize v (snoc xs a) → ψ.Realize v xs

Tactic:
obtain ⟨a, ha⟩ := not_forall.1 (h ∘ h')

Result:
case neg.intro
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
h' : (∀ (a : M), φ✝.Realize v (snoc xs a)) → ψ.Realize v xs
h : ¬ψ.Realize v xs
a : M
ha : ¬φ✝.Realize v (snoc xs a)
⊢ ∃ a, φ✝.Realize v (snoc xs a) → ψ.Realize v xs