@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Std.UnionFind.parentD_linkAux {i : Nat} {self : Array Std.UFNode} {x : Fin self.size} {y : Fin self.size} : Std.UnionFind.parentD (Std.UnionFind.linkAux self x y) i = if ↑x = ↑y then Std.UnionFind.parentD self i else if (self.get y).rank < (self.get 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 self.size} {y : Fin self.size} (yroot : self.parent ↑y = ↑y) {i : Nat} : (self.link x y yroot).parent i = if ↑x = ↑y then self.parent i else if self.rank ↑y < self.rank ↑x then if ↑y = i then ↑x else self.parent i else if ↑x = i then ↑y else self.parent i

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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