@[simp]

theorem Std.UnionFind.arr_empty : Std.UnionFind.empty.arr = #[]

@[simp]

theorem Std.UnionFind.parent_empty {a : Nat} : Std.UnionFind.parent Std.UnionFind.empty a = a

@[simp]

theorem Std.UnionFind.rank_empty {a : Nat} : Std.UnionFind.rank Std.UnionFind.empty a = 0

@[simp]

theorem Std.UnionFind.rootD_empty {a : Nat} : Std.UnionFind.rootD Std.UnionFind.empty a = a

@[simp]

theorem Std.UnionFind.arr_push {m : Std.UnionFind} : (Std.UnionFind.push m).arr = Array.push m.arr { parent := Array.size m.arr, rank := 0 }

@[simp]

theorem Std.UnionFind.parentD_push {a : Nat} {arr : Array Std.UFNode} : Std.UnionFind.parentD (Array.push arr { parent := Array.size arr, rank := 0 }) a = Std.UnionFind.parentD arr a

@[simp]

theorem Std.UnionFind.parent_push {a : Nat} {m : Std.UnionFind} : Std.UnionFind.parent (Std.UnionFind.push m) a = Std.UnionFind.parent m a

@[simp]

theorem Std.UnionFind.rankD_push {a : Nat} {arr : Array Std.UFNode} : Std.UnionFind.rankD (Array.push arr { parent := Array.size arr, rank := 0 }) a = Std.UnionFind.rankD arr a

@[simp]

theorem Std.UnionFind.rank_push {a : Nat} {m : Std.UnionFind} : Std.UnionFind.rank (Std.UnionFind.push m) a = Std.UnionFind.rank m a

@[simp]

theorem Std.UnionFind.rankMax_push {m : Std.UnionFind} : Std.UnionFind.rankMax (Std.UnionFind.push m) = Std.UnionFind.rankMax m

@[simp]

theorem Std.UnionFind.root_push {x : Nat} {self : Std.UnionFind} : Std.UnionFind.rootD (Std.UnionFind.push self) x = Std.UnionFind.rootD self x

@[simp]

theorem Std.UnionFind.arr_link {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} {y : Fin (Std.UnionFind.size self)} {yroot : Std.UnionFind.parent self ↑y = ↑y} : (Std.UnionFind.link self x y yroot).arr = Std.UnionFind.linkAux self.arr x y

theorem Std.UnionFind.parentD_linkAux {i : Nat} {self : Array Std.UFNode} {x : Fin (Array.size self)} {y : Fin (Array.size self)} : Std.UnionFind.parentD (Std.UnionFind.linkAux self x y) i = if ↑x = ↑y then Std.UnionFind.parentD self i else if (Array.get self y).rank < (Array.get self x).rank then if ↑y = i then ↑x else Std.UnionFind.parentD self i else if ↑x = i then ↑y else Std.UnionFind.parentD self i

theorem Std.UnionFind.parent_link {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} {y : Fin (Std.UnionFind.size self)} (yroot : Std.UnionFind.parent self ↑y = ↑y) {i : Nat} : Std.UnionFind.parent (Std.UnionFind.link self x y yroot) i = if ↑x = ↑y then Std.UnionFind.parent self i else if Std.UnionFind.rank self ↑y < Std.UnionFind.rank self ↑x then if ↑y = i then ↑x else Std.UnionFind.parent self i else if ↑x = i then ↑y else Std.UnionFind.parent self i

theorem Std.UnionFind.root_link {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} {y : Fin (Std.UnionFind.size self)} (xroot : Std.UnionFind.parent self ↑x = ↑x) (yroot : Std.UnionFind.parent self ↑y = ↑y) : ∃ (r : Fin (Std.UnionFind.size self)), (r = x ∨ r = y) ∧ ∀ (i : Nat), Std.UnionFind.rootD (Std.UnionFind.link self x y yroot) i = if Std.UnionFind.rootD self i = ↑x ∨ Std.UnionFind.rootD self i = ↑y then ↑r else Std.UnionFind.rootD self i

theorem Std.UnionFind.root_link.go {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} {y : Fin (Std.UnionFind.size self)} (xroot : Std.UnionFind.parent self ↑x = ↑x) (yroot : Std.UnionFind.parent self ↑y = ↑y) {m : Std.UnionFind} (hm : ∀ (i : Nat), Std.UnionFind.parent m i = if ↑y = i then ↑x else Std.UnionFind.parent self i) (i : Nat) : Std.UnionFind.rootD m i = if Std.UnionFind.rootD self i = ↑x ∨ Std.UnionFind.rootD self i = ↑y then ↑x else Std.UnionFind.rootD self i

theorem Std.UnionFind.Equiv.rfl {self : Std.UnionFind} {a : Nat} : Std.UnionFind.Equiv self a a

theorem Std.UnionFind.Equiv.symm {self : Std.UnionFind} {a : Nat} {b : Nat} : Std.UnionFind.Equiv self a b → Std.UnionFind.Equiv self b a

theorem Std.UnionFind.Equiv.trans {self : Std.UnionFind} {a : Nat} {b : Nat} {c : Nat} : Std.UnionFind.Equiv self a b → Std.UnionFind.Equiv self b c → Std.UnionFind.Equiv self a c

@[simp]

theorem Std.UnionFind.equiv_empty {a : Nat} {b : Nat} : Std.UnionFind.Equiv Std.UnionFind.empty a b ↔ a = b

@[simp]

theorem Std.UnionFind.equiv_push {a : Nat} {b : Nat} {self : Std.UnionFind} : Std.UnionFind.Equiv (Std.UnionFind.push self) a b ↔ Std.UnionFind.Equiv self a b

@[simp]

theorem Std.UnionFind.equiv_rootD {self : Std.UnionFind} {a : Nat} : Std.UnionFind.Equiv self (Std.UnionFind.rootD self a) a

@[simp]

theorem Std.UnionFind.equiv_rootD_l {self : Std.UnionFind} {a : Nat} {b : Nat} : Std.UnionFind.Equiv self (Std.UnionFind.rootD self a) b ↔ Std.UnionFind.Equiv self a b

@[simp]

theorem Std.UnionFind.equiv_rootD_r {self : Std.UnionFind} {a : Nat} {b : Nat} : Std.UnionFind.Equiv self a (Std.UnionFind.rootD self b) ↔ Std.UnionFind.Equiv self a b

theorem Std.UnionFind.equiv_find {a : Nat} {b : Nat} {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} : Std.UnionFind.Equiv (Std.UnionFind.find self x).fst a b ↔ Std.UnionFind.Equiv self a b

theorem Std.UnionFind.equiv_link {a : Nat} {b : Nat} {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} {y : Fin (Std.UnionFind.size self)} (xroot : Std.UnionFind.parent self ↑x = ↑x) (yroot : Std.UnionFind.parent self ↑y = ↑y) : Std.UnionFind.Equiv (Std.UnionFind.link self x y yroot) a b ↔ Std.UnionFind.Equiv self a b ∨ Std.UnionFind.Equiv self a ↑x ∧ Std.UnionFind.Equiv self (↑y) b ∨ Std.UnionFind.Equiv self a ↑y ∧ Std.UnionFind.Equiv self (↑x) b

theorem Std.UnionFind.equiv_union {a : Nat} {b : Nat} {self : Std.UnionFind} {x : Fin (Std.UnionFind.size self)} {y : Fin (Std.UnionFind.size self)} : Std.UnionFind.Equiv (Std.UnionFind.union self x y) a b ↔ Std.UnionFind.Equiv self a b ∨ Std.UnionFind.Equiv self a ↑x ∧ Std.UnionFind.Equiv self (↑y) b ∨ Std.UnionFind.Equiv self a ↑y ∧ Std.UnionFind.Equiv self (↑x) b