Theorem: Lean4Lean.UnionFind.root_link (Lean4Lean/Verify/UnionFind.lean)

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
⊢ ∃ r,
    (r = x ∨ r = y) ∧
      ∀ (i : Nat), root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
Tactic:
refine ⟨x, .inl rfl, fun i => ?_⟩
State after:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [root_ext (m2 := self) (fun _ => by rw [parent_link, if_pos h])]
State after:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ root self i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ root self i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
split <;> [obtain _ | _ := ‹_› <;> simp [*]; rfl]
State after:
no goals

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i x✝ : Nat
⊢ parent (link self x y yroot) x✝ = parent self x✝
Tactic:
rw [parent_link, if_pos h]
State after:
no goals

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
⊢ ∃ r,
    (r = x ∨ r = y) ∧
      ∀ (i : Nat), root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
Tactic:
if hr : self.rank y < self.rank x then
  exact this xroot yroot fun i => by simp [parent_link, h, hr]
else
  simpa (config := {singlePass := true}) [or_comm] using
    this yroot xroot fun i => by simp [parent_link, h, hr]
State after:
no goals

State before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
⊢ ∃ r, (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
Tactic:
exact ⟨x, .inl rfl, go⟩
State after:
no goals

State before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : parent m i = i
⊢ root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [root_eq_self.2 h]
State after:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : parent m i = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

State before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : parent m i = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [hm i] at h
State after:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : (if ↑y = i then ↑x else parent self i) = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

State before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : (if ↑y = i then ↑x else parent self i) = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
split at h
State after:
case inl
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

case inr
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

State before:
case inl
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [if_pos, h]
State after:
case inl.hc
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ root self i = ↑x ∨ root self i = ↑y

State before:
case inl.hc
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ root self i = ↑x ∨ root self i = ↑y
Tactic:
simp [← h, root_eq_self, xroot]
State after:
no goals

State before:
case inr
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [root_eq_self.2 ‹_›]
State after:
case inr
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
⊢ i = if i = ↑x ∨ i = ↑y then ↑x else i

State before:
case inr
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
⊢ i = if i = ↑x ∨ i = ↑y then ↑x else i
Tactic:
split <;> [skip; rfl]
State after:
case inr.inl
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝² : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝¹ : ¬↑y = i
h : parent self i = i
h✝ : i = ↑x ∨ i = ↑y
⊢ i = ↑x

State before:
case inr.inl
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝² : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝¹ : ¬↑y = i
h : parent self i = i
h✝ : i = ↑x ∨ i = ↑y
⊢ i = ↑x
Tactic:
next h' => exact h'.resolve_right (Ne.symm ‹_›)
State after:
no goals

State before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
h' : i = ↑x ∨ i = ↑y
⊢ i = ↑x
Tactic:
exact h'.resolve_right (Ne.symm ‹_›)
State after:
no goals

State before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
⊢ root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
have _ := Nat.sub_lt_sub_left (m.lt_rankMax i) (m.rank_lt h)
State after:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

State before:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [← root_parent, go (m.parent i)]
State after:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ (if root self (parent m i) = ↑x ∨ root self (parent m i) = ↑y then ↑x else root self (parent m i)) =
    if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

State before:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ (if root self (parent m i) = ↑x ∨ root self (parent m i) = ↑y then ↑x else root self (parent m i)) =
    if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [hm i]
State after:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ (if root self (if ↑y = i then ↑x else parent self i) = ↑x ∨ root self (if ↑y = i then ↑x else parent self i) = ↑y then
      ↑x
    else root self (if ↑y = i then ↑x else parent self i)) =
    if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

State before:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ (if root self (if ↑y = i then ↑x else parent self i) = ↑x ∨ root self (if ↑y = i then ↑x else parent self i) = ↑y then
      ↑x
    else root self (if ↑y = i then ↑x else parent self i)) =
    if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
split <;> [subst i; rw [root_parent]]
State after:
case inl
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
h : ¬parent m ↑y = ↑y
x✝ : rankMax m - rank m (parent m ↑y) < rankMax m - rank m ↑y
⊢ (if root self ↑x = ↑x ∨ root self ↑x = ↑y then ↑x else root self ↑x) =
    if root self ↑y = ↑x ∨ root self ↑y = ↑y then ↑x else root self ↑y

State before:
case inl
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
h : ¬parent m ↑y = ↑y
x✝ : rankMax m - rank m (parent m ↑y) < rankMax m - rank m ↑y
⊢ (if root self ↑x = ↑x ∨ root self ↑x = ↑y then ↑x else root self ↑x) =
    if root self ↑y = ↑x ∨ root self ↑y = ↑y then ↑x else root self ↑y
Tactic:
simp [root_eq_self.2 xroot, root_eq_self.2 yroot]
State after:
no goals

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
hr : rank self ↑y < rank self ↑x
⊢ ∃ r,
    (r = x ∨ r = y) ∧
      ∀ (i : Nat), root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
Tactic:
exact this xroot yroot fun i => by simp [parent_link, h, hr]
State after:
no goals

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
hr : rank self ↑y < rank self ↑x
i : Nat
⊢ parent (link self x y yroot) i = if ↑y = i then ↑x else parent self i
Tactic:
simp [parent_link, h, hr]
State after:
no goals

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
hr : ¬rank self ↑y < rank self ↑x
⊢ ∃ r,
    (r = x ∨ r = y) ∧
      ∀ (i : Nat), root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
Tactic:
simpa (config := {singlePass := true}) [or_comm] using
  this yroot xroot fun i => by simp [parent_link, h, hr]
State after:
no goals

State before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
hr : ¬rank self ↑y < rank self ↑x
i : Nat
⊢ parent (link self x y yroot) i = if ↑x = i then ↑y else parent self i
Tactic:
simp [parent_link, h, hr]
State after:
no goals