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

State before:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv (union self x y) a b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b
Tactic:
simp [union]
State after:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv
      (link (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst { val := root self ↑x, isLt := ⋯ }
        (find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val ⋯)
      a b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b

State before:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv
      (link (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst { val := root self ↑x, isLt := ⋯ }
        (find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val ⋯)
      a b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b
Tactic:
rw [equiv_link (by simp [← root_eq_self, root_root])]
State after:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a b ∨
      Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a ↑{ val := root self ↑x, isLt := ⋯ } ∧
          Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst
            (↑(find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val) b ∨
        Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a
            ↑(find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val ∧
          Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst (↑{ val := root self ↑x, isLt := ⋯ }) b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b

State before:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a b ∨
      Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a ↑{ val := root self ↑x, isLt := ⋯ } ∧
          Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst
            (↑(find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val) b ∨
        Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a
            ↑(find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val ∧
          Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst (↑{ val := root self ↑x, isLt := ⋯ }) b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b
Tactic:
simp [equiv_find]
State after:
no goals

State before:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ parent (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst ↑{ val := root self ↑x, isLt := ⋯ } =
    ↑{ val := root self ↑x, isLt := ⋯ }
Tactic:
simp [← root_eq_self, root_root]
State after:
no goals