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

State before:
self : UnionFind
x : Nat
⊢ rank self x < rank self (root self x) ↔ parent self x ≠ x
Tactic:
refine ⟨fun h h' => Nat.ne_of_lt h (by rw [root_eq_self.2 h']), fun h => ?_⟩
State after:
self : UnionFind
x : Nat
h : parent self x ≠ x
⊢ rank self x < rank self (root self x)

State before:
self : UnionFind
x : Nat
h : parent self x ≠ x
⊢ rank self x < rank self (root self x)
Tactic:
rw [← root_parent]
State after:
self : UnionFind
x : Nat
h : parent self x ≠ x
⊢ rank self x < rank self (root self (parent self x))

State before:
self : UnionFind
x : Nat
h : parent self x ≠ x
⊢ rank self x < rank self (root self (parent self x))
Tactic:
exact Nat.lt_of_lt_of_le (self.rank_lt h) le_rank_root
State after:
no goals

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