L : Language
L' : Language
M : Type w
N : Type ?u.123113
P : Type ?u.123116
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin (n + 1) → M
⊢ Realize φ v (xs ∘ fun i => if ↑i < n then ↑castSucc i else succ i) = Realize φ v (xs ∘ ↑castSucc)
L : Language
L' : Language
M : Type w
N : Type ?u.123113
P : Type ?u.123116
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin (n + 1) → M
⊢ Realize (liftAt 1 n φ) v xs ↔ Realize φ v (xs ∘ ↑castSucc)
rw [realize_liftAt_one (refl n), iff_eq_eq]
L : Language
L' : Language
M : Type w
N : Type ?u.123113
P : Type ?u.123116
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin (n + 1) → M
i : Fin n
⊢ (if ↑i < n then ↑castSucc i else succ i) = ↑castSucc i
L : Language
L' : Language
M : Type w
N : Type ?u.123113
P : Type ?u.123116
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin (n + 1) → M
⊢ Realize φ v (xs ∘ fun i => if ↑i < n then ↑castSucc i else succ i) = Realize φ v (xs ∘ ↑castSucc)
refine' congr rfl (congr rfl (funext fun i => _))
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.123113
P : Type ?u.123116
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
n : ℕ
φ : BoundedFormula L α n
v : α → M
xs : Fin (n + 1) → M
i : Fin n
⊢ (if ↑i < n then ↑castSucc i else succ i) = ↑castSucc i
rw [if_pos i.is_lt]