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

State before:
self : UnionFind
x : Fin (size self)
i : Nat
h : parent (find self x).fst i = i
⊢ root (find self x).fst i = root self i
Tactic:
rw [root_eq_self.2 h]
State after:
self : UnionFind
x : Fin (size self)
i : Nat
h : parent (find self x).fst i = i
⊢ i = root self i

State before:
self : UnionFind
x : Fin (size self)
i : Nat
h : parent (find self x).fst i = i
⊢ i = root self i
Tactic:
obtain ⟨h1, _⟩ | h1 := find_parent_or self x i <;> rw [h1] at h
State after:
case inl.intro
self : UnionFind
x : Fin (size self)
i : Nat
h : root self i = i
h1 : parent (find self x).fst i = root self i
right✝ : root self i = root self ↑x
⊢ i = root self i

case inr
self : UnionFind
x : Fin (size self)
i : Nat
h : parent self i = i
h1 : parent (find self x).fst i = parent self i
⊢ i = root self i

State before:
case inl.intro
self : UnionFind
x : Fin (size self)
i : Nat
h : root self i = i
h1 : parent (find self x).fst i = root self i
right✝ : root self i = root self ↑x
⊢ i = root self i
Tactic:
rw [h]
State after:
no goals

State before:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
h : parent self i = i
h1 : parent (find self x).fst i = parent self i
⊢ i = root self i
Tactic:
rw [root_eq_self.2 h]
State after:
no goals

State before:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
⊢ root (find self x).fst i = root self i
Tactic:
have := Nat.sub_lt_sub_left ((self.find x).1.lt_rankMax _) ((self.find x).1.rank_lt h)
State after:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ root (find self x).fst i = root self i

State before:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ root (find self x).fst i = root self i
Tactic:
rw [← root_parent, find_root_1 self x ((self.find x).1.parent i)]
State after:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ root self (parent (find self x).fst i) = root self i

State before:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ root self (parent (find self x).fst i) = root self i
Tactic:
obtain ⟨h1, _⟩ | h1 := find_parent_or self x i
State after:
case inl.intro
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
h1 : parent (find self x).fst i = root self i
right✝ : root self i = root self ↑x
⊢ root self (parent (find self x).fst i) = root self i

case inr
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
h1 : parent (find self x).fst i = parent self i
⊢ root self (parent (find self x).fst i) = root self i

State before:
case inl.intro
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
h1 : parent (find self x).fst i = root self i
right✝ : root self i = root self ↑x
⊢ root self (parent (find self x).fst i) = root self i
Tactic:
rw [h1, root_root]
State after:
no goals

State before:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
h1 : parent (find self x).fst i = parent self i
⊢ root self (parent (find self x).fst i) = root self i
Tactic:
rw [h1, root_parent]
State after:
no goals

State before:
self : UnionFind
x : Fin (size self)
i : Nat
a✝ :
  ∀ (y : Nat),
    (invImage (fun a => rankMax (find self x).fst - rank (find self x).fst a) instWellFoundedRelation).1 y i →
      root (find self x).fst y = root self y
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ (invImage (fun a => rankMax (find self x).fst - rank (find self x).fst a) instWellFoundedRelation).1
    (parent (find self x).fst i) i
Tactic:
exact this
State after:
no goals