no goals
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : LinearOrder ι
inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1
inst✝ : (i : ι) → PartialOrder (β i)
x y : (i : ι) → β i
i : ι
a : β i
⊢ ↑toLex x ≤ ↑toLex (update x i a) ↔ x i ≤ a
simp_rw [le_iff_lt_or_eq, lt_toLex_update_self_iff, toLex_inj, eq_update_self_iff]