L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs : Fin k → M
⊢ Realize
      (mapTermRel (fun n => ↑(Term.relabelEquiv (Equiv.sumCongr g (_root_.Equiv.refl (Fin n))))) (fun n => id)
        (fun x => id) φ)
      v xs ↔
    Realize φ (v ∘ ↑g) xs
L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs : Fin k → M
⊢ Realize (↑(relabelEquiv g) φ) v xs ↔ Realize φ (v ∘ ↑g) xs
simp only [relabelEquiv, mapTermRelEquiv_apply, Equiv.coe_refl]
L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : Term L (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs) (↑(Term.relabelEquiv (Equiv.sumCongr g (_root_.Equiv.refl (Fin n)))) t) =
    realize (Sum.elim (v ∘ ↑g) xs) t
L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs : Fin k → M
⊢ Realize
      (mapTermRel (fun n => ↑(Term.relabelEquiv (Equiv.sumCongr g (_root_.Equiv.refl (Fin n))))) (fun n => id)
        (fun x => id) φ)
      v xs ↔
    Realize φ (v ∘ ↑g) xs
refine' realize_mapTermRel_id (fun n t xs => _) fun _ _ _ => rfl
L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : Term L (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs ∘ ↑(Equiv.sumCongr g (_root_.Equiv.refl (Fin n)))) t = realize (Sum.elim (v ∘ ↑g) xs) t
L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : Term L (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs) (↑(Term.relabelEquiv (Equiv.sumCongr g (_root_.Equiv.refl (Fin n)))) t) =
    realize (Sum.elim (v ∘ ↑g) xs) t
simp only [relabelEquiv_apply, Term.realize_relabel]
L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : Term L (α ⊕ Fin n)
xs : Fin n → M
⊢ Sum.elim v xs ∘ ↑(Equiv.sumCongr g (_root_.Equiv.refl (Fin n))) = Sum.elim (v ∘ ↑g) xs
L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : Term L (α ⊕ Fin n)
xs : Fin n → M
⊢ realize (Sum.elim v xs ∘ ↑(Equiv.sumCongr g (_root_.Equiv.refl (Fin n)))) t = realize (Sum.elim (v ∘ ↑g) xs) t
refine' congr (congr rfl _) rfl
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.163438
P : Type ?u.163441
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
g : α ≃ β
k : ℕ
φ : BoundedFormula L α k
v : β → M
xs✝ : Fin k → M
n : ℕ
t : Term L (α ⊕ Fin n)
xs : Fin n → M
⊢ Sum.elim v xs ∘ ↑(Equiv.sumCongr g (_root_.Equiv.refl (Fin n))) = Sum.elim (v ∘ ↑g) xs
ext (i | i) <;> rfl