α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
i : ℕ
h : i < Array.size arr
⊢ i < Array.size arr
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
i : ℕ
h : i < Array.size arr
⊢ i < n
rw [H.size_eq]
no goals
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
i : ℕ
h : i < Array.size arr
⊢ i < Array.size arr
exact h