L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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φ : IsPrenex φ
v : α → M
xs : Fin n → M
⊢ ∀ {ψ : BoundedFormula L α n}, IsPrenex ψ → (Realize (toPrenexImp φ ψ) v xs ↔ Realize (φ ⟹ ψ) v xs)
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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φ : IsPrenex φ
hψ : IsPrenex ψ
v : α → M
xs : Fin n → M
⊢ Realize (toPrenexImp φ ψ) v xs ↔ Realize (φ ⟹ ψ) v xs
revert ψ
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs

case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (toPrenexImp (∀'φ✝) ψ) v xs ↔ Realize (∀'φ✝ ⟹ ψ) v xs

case ex
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (toPrenexImp (∃'φ✝) ψ) v xs ↔ Realize (∃'φ✝ ⟹ ψ) v xs
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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φ : IsPrenex φ
v : α → M
xs : Fin n → M
⊢ ∀ {ψ : BoundedFormula L α n}, IsPrenex ψ → (Realize (toPrenexImp φ ψ) v xs ↔ Realize (φ ⟹ ψ) v xs)
induction' hφ with _ _ hφ _ _ _hφ ih _ _ _hφ ih <;> intro ψ hψ
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (toPrenexImpRight φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs
rw [hφ.toPrenexImp]
no goals
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (toPrenexImpRight φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs
exact realize_toPrenexImpRight hφ hψ
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (∃'toPrenexImp φ✝ (liftAt 1 n✝ ψ)) v xs ↔ Realize (∀'φ✝ ⟹ ψ) v xs
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (toPrenexImp (∀'φ✝) ψ) v xs ↔ Realize (∀'φ✝ ⟹ ψ) v xs
unfold toPrenexImp
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∃ a, Realize (toPrenexImp φ✝ (liftAt 1 n✝ ψ)) v (snoc xs a)) ↔ Realize (∀'φ✝ ⟹ ψ) v xs
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (∃'toPrenexImp φ✝ (liftAt 1 n✝ ψ)) v xs ↔ Realize (∀'φ✝ ⟹ ψ) v xs
rw [realize_ex]
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∃ a, Realize (φ✝ ⟹ liftAt 1 n✝ ψ) v (snoc xs a)) ↔ Realize (∀'φ✝ ⟹ ψ) v xs
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∃ a, Realize (toPrenexImp φ✝ (liftAt 1 n✝ ψ)) v (snoc xs a)) ↔ Realize (∀'φ✝ ⟹ ψ) v xs
refine' _root_.trans (exists_congr fun _ => ih hψ.liftAt) _
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∃ a, Realize φ✝ v (snoc xs a) → Realize ψ v xs) ↔ (∀ (a : M), Realize φ✝ v (snoc xs a)) → Realize ψ v xs
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∃ a, Realize (φ✝ ⟹ liftAt 1 n✝ ψ) v (snoc xs a)) ↔ Realize (∀'φ✝ ⟹ ψ) v xs
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
case all.refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∃ a, Realize φ✝ v (snoc xs a) → Realize ψ v xs) → (∀ (a : M), Realize φ✝ v (snoc xs a)) → Realize ψ v xs

case all.refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
h' : (∀ (a : M), Realize φ✝ v (snoc xs a)) → Realize ψ v xs
⊢ ∃ a, Realize φ✝ v (snoc xs a) → Realize ψ v xs
case all
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∃ a, Realize φ✝ v (snoc xs a) → Realize ψ v xs) ↔ (∀ (a : M), Realize φ✝ v (snoc xs a)) → Realize ψ v xs
refine' ⟨_, fun h' => _⟩
case all.refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
a : M
ha : Realize φ✝ v (snoc xs a) → Realize ψ v xs
h : ∀ (a : M), Realize φ✝ v (snoc xs a)
⊢ Realize ψ v xs
case all.refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∃ a, Realize φ✝ v (snoc xs a) → Realize ψ v xs) → (∀ (a : M), Realize φ✝ v (snoc xs a)) → Realize ψ v xs
rintro ⟨a, ha⟩ h
no goals
case all.refine'_1.intro
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
a : M
ha : Realize φ✝ v (snoc xs a) → Realize ψ v xs
h : ∀ (a : M), Realize φ✝ v (snoc xs a)
⊢ Realize ψ v xs
exact ha (h a)
case pos
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α 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
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α 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 all.refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
h' : (∀ (a : M), Realize φ✝ v (snoc xs a)) → Realize ψ v xs
⊢ ∃ a, Realize φ✝ v (snoc xs a) → Realize ψ v xs
by_cases ψ.Realize v xs
case pos
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
h' : (∀ (a : M), Realize φ✝ v (snoc xs a)) → Realize ψ v xs
h : Realize ψ v xs
inhabited_h : Inhabited M
⊢ ∃ a, Realize φ✝ v (snoc xs a) → Realize ψ v xs
case pos
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α 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
inhabit M
no goals
case pos
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
h' : (∀ (a : M), Realize φ✝ v (snoc xs a)) → Realize ψ v xs
h : Realize ψ v xs
inhabited_h : Inhabited M
⊢ ∃ a, Realize φ✝ v (snoc xs a) → Realize ψ v xs
exact ⟨default, fun _h'' => h⟩
case neg.intro
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α 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
case neg
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α 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
obtain ⟨a, ha⟩ := not_forall.1 (h ∘ h')
no goals
case neg.intro
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α 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
exact ⟨a, fun h => (ha h).elim⟩
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∀ (a : M), Realize (φ✝ ⟹ liftAt 1 n✝ ψ) v (snoc xs a)) ↔ Realize (∃'φ✝ ⟹ ψ) v xs
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ Realize (toPrenexImp (∃'φ✝) ψ) v xs ↔ Realize (∃'φ✝ ⟹ ψ) v xs
refine' _root_.trans (forall_congr' fun _ => ih hψ.liftAt) _
no goals
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.197102
P : Type ?u.197105
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
v : α → M
xs✝ : Fin n → M
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
_hφ : IsPrenex φ✝
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : BoundedFormula L α (n✝ + 1)},
    IsPrenex ψ → (Realize (toPrenexImp φ✝ ψ) v xs ↔ Realize (φ✝ ⟹ ψ) v xs)
xs : Fin n✝ → M
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ (∀ (a : M), Realize (φ✝ ⟹ liftAt 1 n✝ ψ) v (snoc xs a)) ↔ Realize (∃'φ✝ ⟹ ψ) v xs
simp