L : Language
M : Type u_3
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)
L : Language
M : Type u_3
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)
change
  Quotient.map (@funMap L M ps.toStructure n f) Prestructure.fun_equiv (Quotient.finChoice _) =
    _
no goals
L : Language
M : Type u_3
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)
rw [Quotient.finChoice_eq, Quotient.map_mk]