@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Batteries.UnionFind.parent_link {self : Batteries.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 Batteries.UnionFind.root_link {self : Batteries.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 Batteries.UnionFind.root_link.go {self : Batteries.UnionFind} {x : Fin self.size} {y : Fin self.size} (xroot : self.parent ↑x = ↑x) (yroot : self.parent ↑y = ↑y) {m : Batteries.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 Batteries.UnionFind.Equiv.rfl {self : Batteries.UnionFind} {a : Nat} : self.Equiv a a

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Batteries.UnionFind.equiv_link {a : Nat} {b : Nat} {self : Batteries.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 Batteries.UnionFind.equiv_union {a : Nat} {b : Nat} {self : Batteries.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