[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
n : ℕ
f : Functions L n
x : Fin n → M
⊢ (funMap f fun i => Quotient.mk s (x i)) = Quotient.mk s (funMap f x)
[PROOFSTEP]
change Quotient.map (@funMap L M ps.toStructure n f) Prestructure.fun_equiv (Quotient.finChoice _) = _
[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
n : ℕ
f : Functions L n
x : Fin n → M
⊢ Quotient.map (funMap f) (_ : ∀ (x y : Fin n → M), x ≈ y → funMap f x ≈ funMap f y)
      (Quotient.finChoice fun i => Quotient.mk s (x i)) =
    Quotient.mk s (funMap f x)
[PROOFSTEP]
rw [Quotient.finChoice_eq, Quotient.map_mk]
[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
n : ℕ
r : Relations L n
x : Fin n → M
⊢ (RelMap r fun i => Quotient.mk s (x i)) ↔ RelMap r x
[PROOFSTEP]
change Quotient.lift (@RelMap L M ps.toStructure n r) Prestructure.rel_equiv (Quotient.finChoice _) ↔ _
[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
n : ℕ
r : Relations L n
x : Fin n → M
⊢ Quotient.lift (RelMap r) (_ : ∀ (x y : Fin n → M), x ≈ y → RelMap r x = RelMap r y)
      (Quotient.finChoice fun i => Quotient.mk s (x i)) ↔
    RelMap r x
[PROOFSTEP]
rw [Quotient.finChoice_eq, Quotient.lift_mk]
[GOAL]
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
β : Type u_2
t : Term L β
x : β → M
⊢ realize (fun i => Quotient.mk s (x i)) t = Quotient.mk s (realize x t)
[PROOFSTEP]
induction' t with _ _ _ _ ih
[GOAL]
case var
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
β : Type u_2
x : β → M
_a✝ : β
⊢ realize (fun i => Quotient.mk s (x i)) (var _a✝) = Quotient.mk s (realize x (var _a✝))
[PROOFSTEP]
rfl
[GOAL]
case func
L : Language
M : Type u_1
s : Setoid M
ps : Prestructure L s
β : Type u_2
x : β → M
l✝ : ℕ
_f✝ : Functions L l✝
_ts✝ : Fin l✝ → Term L β
ih : ∀ (a : Fin l✝), realize (fun i => Quotient.mk s (x i)) (_ts✝ a) = Quotient.mk s (realize x (_ts✝ a))
⊢ realize (fun i => Quotient.mk s (x i)) (func _f✝ _ts✝) = Quotient.mk s (realize x (func _f✝ _ts✝))
[PROOFSTEP]
simp only [ih, funMap_quotient_mk', Term.realize]
