-- Mathlib/ModelTheory/Complexity.lean
theorem realize_toPrenex (φ : L.BoundedFormula α n) {v : α → M} :
    ∀ {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
⊢ ∀ {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

Result:
no goals

Proof state:
case rel
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ∀ {xs : Fin n✝ → M}, (rel R✝ ts✝).toPrenex.Realize v xs ↔ (rel R✝ ts✝).Realize v xs

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
case falsum
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
⊢ ∀ {xs : Fin n✝ → M}, falsum.toPrenex.Realize v xs ↔ falsum.Realize v xs

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
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:
rw [toPrenex, realize_toPrenexImp f1.toPrenex_isPrenex f2.toPrenex_isPrenex, realize_imp,
  realize_imp, h1, h2]

Result:
no goals

Proof state:
case equal
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ ∀ {xs : Fin n✝ → M}, (equal t₁✝ t₂✝).toPrenex.Realize v xs ↔ (equal t₁✝ t₂✝).Realize v xs

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
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:
intros

Result:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
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✝

Proof state:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
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:
intros

Result:
case imp
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
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✝

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
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
⊢ (∀ (a : M), f✝.toPrenex.Realize v (snoc xs✝ a)) ↔ ∀ (a : M), f✝.Realize v (snoc xs✝ a)

Tactic:
exact forall_congr' fun a => h

Result:
no goals

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
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:
rw [realize_all, toPrenex, realize_all]

Result:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
v : α → M
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
⊢ (∀ (a : M), f✝.toPrenex.Realize v (snoc xs✝ a)) ↔ ∀ (a : M), f✝.Realize v (snoc xs✝ a)