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

State before:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
⊢ root m1 x = root m2 x
Tactic:
if h : m2.parent x = x then
  rw [root_eq_self.2 h, root_eq_self.2 ((H _).trans h)]
else
  have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
  rw [← root_parent, H, root_ext H, root_parent]
State after:
no goals

State before:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
h : parent m2 x = x
⊢ root m1 x = root m2 x
Tactic:
rw [root_eq_self.2 h, root_eq_self.2 ((H _).trans h)]
State after:
no goals

State before:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
h : ¬parent m2 x = x
⊢ root m1 x = root m2 x
Tactic:
have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
State after:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
h : ¬parent m2 x = x
this : rankMax m2 - rank m2 (parent m2 x) < rankMax m2 - rank m2 x
⊢ root m1 x = root m2 x

State before:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
h : ¬parent m2 x = x
this : rankMax m2 - rank m2 (parent m2 x) < rankMax m2 - rank m2 x
⊢ root m1 x = root m2 x
Tactic:
rw [← root_parent, H, root_ext H, root_parent]
State after:
no goals