Theorem: Lean4Lean.UnionFind.le_rank_root (Lean4Lean/UnionFind.lean)

State before:
self : UnionFind
x : Nat
⊢ rank self x ≤ rank self (root self x)
Tactic:
if h : self.parent x = x then
  rw [root_eq_self.2 h]
else
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
  rw [← root_parent]
  exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root
State after:
no goals

State before:
self : UnionFind
x : Nat
h : parent self x = x
⊢ rank self x ≤ rank self (root self x)
Tactic:
rw [root_eq_self.2 h]
State after:
no goals

State before:
self : UnionFind
x : Nat
h : ¬parent self x = x
⊢ rank self x ≤ rank self (root self x)
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
State after:
self : UnionFind
x : Nat
h : ¬parent self x = x
this : rankMax self - rank self (parent self x) < rankMax self - rank self x
⊢ rank self x ≤ rank self (root self x)

State before:
self : UnionFind
x : Nat
h : ¬parent self x = x
this : rankMax self - rank self (parent self x) < rankMax self - rank self x
⊢ rank self x ≤ rank self (root self x)
Tactic:
rw [← root_parent]
State after:
self : UnionFind
x : Nat
h : ¬parent self x = x
this : rankMax self - rank self (parent self x) < rankMax self - rank self x
⊢ rank self x ≤ rank self (root self (parent self x))

State before:
self : UnionFind
x : Nat
h : ¬parent self x = x
this : rankMax self - rank self (parent self x) < rankMax self - rank self x
⊢ rank self x ≤ rank self (root self (parent self x))
Tactic:
exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root
State after:
no goals