Theorem: Lean4Lean.UnionFind.rank'_lt_rankMax (Lean4Lean/UnionFind.lean)

State before:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).rank < rankMax self
Tactic:
simp [rankMax, Array.foldr_eq_foldr_data]
State after:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).rank < List.foldr (fun x => max x.rank) 0 self.arr.data + 1

State before:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).rank < List.foldr (fun x => max x.rank) 0 self.arr.data + 1
Tactic:
exact Nat.lt_succ.2 <| go (self.arr.data.get_mem i.1 i.2)
State after:
no goals

State before:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
⊢ a.rank ≤ List.foldr (fun x => max x.rank) 0 (a :: l)
Tactic:
dsimp
State after:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
⊢ a.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)

State before:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
⊢ a.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)
Tactic:
apply Nat.le_max_left
State after:
no goals

State before:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ List.foldr (fun x => max x.rank) 0 (a :: l)
Tactic:
dsimp
State after:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)

State before:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)
Tactic:
exact Nat.le_trans (go h) (Nat.le_max_right ..)
State after:
no goals