@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Batteries.UnionFind.parent_link {self : UnionFind} {x 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 : UnionFind} {x 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

@[irreducible]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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