α : Type u_1
self : UnionFind α
n : ℕ
m : UFModel n
hm : UFModel.Models self.arr m
⊢ ∃ m, UFModel.Models self.arr m
α : Type u_1
self : UnionFind α
⊢ ∃ m, UFModel.Models self.arr m
let ⟨n, m, hm⟩ := self.model
case refl
α : Type u_1
self : UnionFind α
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ ∃ m, UFModel.Models self.arr m
α : Type u_1
self : UnionFind α
n : ℕ
m : UFModel n
hm : UFModel.Models self.arr m
⊢ ∃ m, UFModel.Models self.arr m
cases hm.size_eq
no goals
case refl
α : Type u_1
self : UnionFind α
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ ∃ m, UFModel.Models self.arr m
exact ⟨m, hm⟩