α : Type u_1
self : UnionFind α
i : ℕ
⊢ (if h : i < size self then self.arr[i].rank else 0) < rankMax self
α : Type u_1
self : UnionFind α
i : ℕ
⊢ rank self i < rankMax self
simp [rank]
case inl
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : i < size self
⊢ self.arr[i].rank < rankMax self

case inr
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : ¬i < size self
⊢ 0 < rankMax self
α : Type u_1
self : UnionFind α
i : ℕ
⊢ (if h : i < size self then self.arr[i].rank else 0) < rankMax self
split
case inr
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : ¬i < size self
⊢ 0 < rankMax self
case inl
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : i < size self
⊢ self.arr[i].rank < rankMax self

case inr
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : ¬i < size self
⊢ 0 < rankMax self
{apply lt_rankMax'}
no goals
case inr
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : ¬i < size self
⊢ 0 < rankMax self
apply Nat.succ_pos