case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hψ : IsQF φ✝
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs

case all
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ Realize (toPrenexImpRight φ (∀'φ✝)) v xs ↔ Realize (φ ⟹ ∀'φ✝) v xs

case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ Realize (toPrenexImpRight φ (∃'φ✝)) v xs ↔ Realize (φ ⟹ ∃'φ✝) v xs
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝ ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝ : Fin l → M
inst✝ : Nonempty M
φ ψ : BoundedFormula L α n
hφ : IsQF φ
hψ : IsPrenex ψ
v : α → M
xs : Fin n → M
⊢ Realize (toPrenexImpRight φ ψ) v xs ↔ Realize (φ ⟹ ψ) v xs
induction' hψ with _ _ hψ _ _ _hψ ih _ _ _hψ ih
no goals
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hψ : IsQF φ✝
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
rw [hψ.toPrenexImpRight]
case all
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∀ (a : M), Realize (liftAt 1 n✝ φ ⟹ φ✝) v (snoc xs a)) ↔ Realize (φ ⟹ ∀'φ✝) v xs
case all
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ Realize (toPrenexImpRight φ (∀'φ✝)) v xs ↔ Realize (φ ⟹ ∀'φ✝) v xs
refine' _root_.trans (forall_congr' fun _ => ih hφ.liftAt) _
case all
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∀ (a : M), Realize φ v xs → Realize φ✝ v (snoc xs a)) ↔ Realize φ v xs → ∀ (a : M), Realize φ✝ v (snoc xs a)
case all
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∀ (a : M), Realize (liftAt 1 n✝ φ ⟹ φ✝) v (snoc xs a)) ↔ Realize (φ ⟹ ∀'φ✝) v xs
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
no goals
case all
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∀ (a : M), Realize φ v xs → Realize φ✝ v (snoc xs a)) ↔ Realize φ v xs → ∀ (a : M), Realize φ✝ v (snoc xs a)
exact ⟨fun h1 a h2 => h1 h2 a, fun h1 h2 a => h1 a h2⟩
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ Realize (∃'toPrenexImpRight (liftAt 1 n✝ φ) φ✝) v xs ↔ Realize (φ ⟹ ∃'φ✝) v xs
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ Realize (toPrenexImpRight φ (∃'φ✝)) v xs ↔ Realize (φ ⟹ ∃'φ✝) v xs
unfold toPrenexImpRight
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∃ a, Realize (toPrenexImpRight (liftAt 1 n✝ φ) φ✝) v (snoc xs a)) ↔ Realize (φ ⟹ ∃'φ✝) v xs
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ Realize (∃'toPrenexImpRight (liftAt 1 n✝ φ) φ✝) v xs ↔ Realize (φ ⟹ ∃'φ✝) v xs
rw [realize_ex]
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∃ a, Realize (liftAt 1 n✝ φ ⟹ φ✝) v (snoc xs a)) ↔ Realize (φ ⟹ ∃'φ✝) v xs
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∃ a, Realize (toPrenexImpRight (liftAt 1 n✝ φ) φ✝) v (snoc xs a)) ↔ Realize (φ ⟹ ∃'φ✝) v xs
refine' _root_.trans (exists_congr fun _ => ih hφ.liftAt) _
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)) ↔ Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∃ a, Realize (liftAt 1 n✝ φ ⟹ φ✝) v (snoc xs a)) ↔ Realize (φ ⟹ ∃'φ✝) v xs
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_ex]
case ex.refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)) → Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)

case ex.refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)) ↔ Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
refine' ⟨_, fun h' => _⟩
case ex.refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
a : M
ha : Realize φ v xs → Realize φ✝ v (snoc xs a)
h : Realize φ v xs
⊢ ∃ a, Realize φ✝ v (snoc xs a)
case ex.refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
⊢ (∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)) → Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
rintro ⟨a, ha⟩ h
no goals
case ex.refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
a : M
ha : Realize φ v xs → Realize φ✝ v (snoc xs a)
h : Realize φ v xs
⊢ ∃ a, Realize φ✝ v (snoc xs a)
exact ⟨a, ha h⟩
case pos
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
h : Realize φ v xs
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)

case neg
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
h : ¬Realize φ v xs
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
case ex.refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
by_cases φ.Realize v xs
case pos.intro
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
h : Realize φ v xs
a : M
ha : Realize φ✝ v (snoc xs a)
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
case pos
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
h : Realize φ v xs
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
obtain ⟨a, ha⟩ := h' h
no goals
case pos.intro
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
h : Realize φ v xs
a : M
ha : Realize φ✝ v (snoc xs a)
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
exact ⟨a, fun _ => ha⟩
case neg
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
h : ¬Realize φ v xs
inhabited_h : Inhabited M
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
case neg
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
h : ¬Realize φ v xs
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
inhabit M
no goals
case neg
L : Language
L' : Language
M : Type w
N : Type ?u.166214
P : Type ?u.166217
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v✝ : α → M
xs✝¹ : Fin l → M
inst✝ : Nonempty M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hψ : IsPrenex φ✝
ih :
  ∀ {φ : BoundedFormula L α (n✝ + 1)},
    IsQF φ → ∀ {xs : Fin (n✝ + 1) → M}, Realize (toPrenexImpRight φ φ✝) v xs ↔ Realize (φ ⟹ φ✝) v xs
φ : BoundedFormula L α n✝
hφ : IsQF φ
xs : Fin n✝ → M
h' : Realize φ v xs → ∃ a, Realize φ✝ v (snoc xs a)
h : ¬Realize φ v xs
inhabited_h : Inhabited M
⊢ ∃ a, Realize φ v xs → Realize φ✝ v (snoc xs a)
exact ⟨default, fun h'' => (h h'').elim⟩