L : Language
M : Type u_3
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
L : Language
M : Type u_3
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
change
  Quotient.lift (@RelMap L M ps.toStructure n r) Prestructure.rel_equiv (Quotient.finChoice _) ↔
    _
no goals
L : Language
M : Type u_3
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
rw [Quotient.finChoice_eq, Quotient.lift_mk]