L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
⊢ Realize (∀'liftAt 1 n φ) v xs ↔ Realize φ v xs
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
⊢ Realize (∀'liftAt 1 n φ) v xs ↔ Realize φ v xs
inhabit M
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
⊢ (∀ (a : M), Realize φ v (snoc xs a ∘ ↑castSucc)) ↔ Realize φ v xs
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
⊢ Realize (∀'liftAt 1 n φ) v xs ↔ Realize φ v xs
simp only [realize_all, realize_liftAt_one_self]
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : ∀ (a : M), Realize φ v (snoc xs a ∘ ↑castSucc)
⊢ Realize φ v xs

case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : Realize φ v xs
a : M
⊢ Realize φ v (snoc xs a ∘ ↑castSucc)
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
⊢ (∀ (a : M), Realize φ v (snoc xs a ∘ ↑castSucc)) ↔ Realize φ v xs
refine' ⟨fun h => _, fun h a => _⟩
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : ∀ (a : M), Realize φ v (snoc xs a ∘ ↑castSucc)
i : Fin n
⊢ (snoc xs default ∘ ↑castSucc) i = xs i
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : ∀ (a : M), Realize φ v (snoc xs a ∘ ↑castSucc)
⊢ Realize φ v xs
refine' (congr rfl (funext fun i => _)).mp (h default)
no goals
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : ∀ (a : M), Realize φ v (snoc xs a ∘ ↑castSucc)
i : Fin n
⊢ (snoc xs default ∘ ↑castSucc) i = xs i
simp
case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : Realize φ v xs
a : M
i : Fin n
⊢ xs i = (snoc xs a ∘ ↑castSucc) i
case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : Realize φ v xs
a : M
⊢ Realize φ v (snoc xs a ∘ ↑castSucc)
refine' (congr rfl (funext fun i => _)).mp h
no goals
case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.165049
P : Type ?u.165052
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin n → M
inhabited_h : Inhabited M
h : Realize φ v xs
a : M
i : Fin n
⊢ xs i = (snoc xs a ∘ ↑castSucc) i
simp