internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.UnionFind.rank'_lt_rankMax
Proof state before:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ List.foldr (fun x => max x.rank) 0 (a :: l)
Tactic:
dsimp
Proof state after:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)
Theorem: Lean4Lean.UnionFind.rank'_lt_rankMax
Proof state before:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)
Tactic:
exact Nat.le_trans (go h) (Nat.le_max_right ..)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_lt_rankMax
Proof state before:
self : UnionFind
i : Nat
⊢ rankD self.arr i < rankMax self
Tactic:
simp [rankD]
Proof state after:
self : UnionFind
i : Nat
⊢ (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0) < rankMax self
Theorem: Lean4Lean.UnionFind.rankD_lt_rankMax
Proof state before:
self : UnionFind
i : Nat
⊢ (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0) < rankMax self
Tactic:
split <;> [apply rank'_lt_rankMax; apply Nat.succ_pos]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.push_rankD
Proof state before:
i : Nat
arr : Array UFNode
⊢ rankD (Array.push arr { parent := Array.size arr, rank := 0 }) i = rankD arr i
Tactic:
simp [rankD, Array.get_eq_getElem, Array.get_push]
Proof state after:
i : Nat
arr : Array UFNode
⊢ (if i < Array.size arr + 1 then
      (if h : i < Array.size arr then arr[i] else { parent := Array.size arr, rank := 0 }).rank
    else 0) =
    if h : i < Array.size arr then arr[i].rank else 0
Theorem: Lean4Lean.UnionFind.push_rankD
Proof state before:
i : Nat
arr : Array UFNode
⊢ (if i < Array.size arr + 1 then
      (if h : i < Array.size arr then arr[i] else { parent := Array.size arr, rank := 0 }).rank
    else 0) =
    if h : i < Array.size arr then arr[i].rank else 0
Tactic:
split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.push_rankD
Proof state before:
case inr.inr
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : ¬i < Array.size arr
⊢ 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.push_rankD
Proof state before:
case inr.inl
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : i < Array.size arr
⊢ 0 = arr[i].rank
Tactic:
cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.push_parentD
Proof state before:
i : Nat
arr : Array UFNode
⊢ parentD (Array.push arr { parent := Array.size arr, rank := 0 }) i = parentD arr i
Tactic:
simp [parentD, Array.get_eq_getElem, Array.get_push]
Proof state after:
i : Nat
arr : Array UFNode
⊢ (if i < Array.size arr + 1 then
      (if h : i < Array.size arr then arr[i] else { parent := Array.size arr, rank := 0 }).parent
    else i) =
    if h : i < Array.size arr then arr[i].parent else i
Theorem: Lean4Lean.UnionFind.push_parentD
Proof state before:
i : Nat
arr : Array UFNode
⊢ (if i < Array.size arr + 1 then
      (if h : i < Array.size arr then arr[i] else { parent := Array.size arr, rank := 0 }).parent
    else i) =
    if h : i < Array.size arr then arr[i].parent else i
Tactic:
split <;> split <;> try simp
Proof state after:
case inl.inr
i : Nat
arr : Array UFNode
h✝¹ : i < Array.size arr + 1
h✝ : ¬i < Array.size arr
⊢ Array.size arr = i

case inr.inl
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : i < Array.size arr
⊢ i = arr[i].parent
Theorem: Lean4Lean.UnionFind.push_parentD
Proof state before:
case inr.inr
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : ¬i < Array.size arr
⊢ i = i
Tactic:
simp
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.push_parentD
Proof state before:
case inl.inr
i : Nat
arr : Array UFNode
h✝¹ : i < Array.size arr + 1
h✝ : ¬i < Array.size arr
⊢ Array.size arr = i
Tactic:
exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.push_parentD
Proof state before:
case inr.inl
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : i < Array.size arr
⊢ i = arr[i].parent
Tactic:
cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parent'_root'
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (Array.get self.arr (root' self x)).parent = ↑(root' self x)
Tactic:
rw [root']
Proof state after:
self : UnionFind
x : Fin (size self)
⊢ (Array.get self.arr
        (if h : (Array.get self.arr x).parent = ↑x then x
        else
          let_fun this := ⋯;
          root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(if h : (Array.get self.arr x).parent = ↑x then x
      else
        let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })
Theorem: Lean4Lean.UnionFind.parent'_root'
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (Array.get self.arr
        (if h : (Array.get self.arr x).parent = ↑x then x
        else
          let_fun this := ⋯;
          root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(if h : (Array.get self.arr x).parent = ↑x then x
      else
        let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })
Tactic:
split <;> [assumption; skip]
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ (Array.get self.arr
        (let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })
Theorem: Lean4Lean.UnionFind.parent'_root'
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ (Array.get self.arr
        (let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ (Array.get self.arr
        (let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })
Theorem: Lean4Lean.UnionFind.parent'_root'
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ (Array.get self.arr
        (let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })
Tactic:
apply parent'_root'
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parent_root
Proof state before:
self : UnionFind
x : Nat
⊢ parent self (root self x) = root self x
Tactic:
rw [root]
Proof state after:
self : UnionFind
x : Nat
⊢ parent self (if h : x < size self then ↑(root' self { val := x, isLt := h }) else x) =
    if h : x < size self then ↑(root' self { val := x, isLt := h }) else x
Theorem: Lean4Lean.UnionFind.parent_root
Proof state before:
self : UnionFind
x : Nat
⊢ parent self (if h : x < size self then ↑(root' self { val := x, isLt := h }) else x) =
    if h : x < size self then ↑(root' self { val := x, isLt := h }) else x
Tactic:
split <;> [simp [parentD, parent'_root']; simp [parentD_of_not_lt, *]]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_parent
Proof state before:
self : UnionFind
x : Nat
⊢ root self (parent self x) = root self x
Tactic:
simp [root, parent_lt]
Proof state after:
self : UnionFind
x : Nat
⊢ (if h : x < Array.size self.arr then ↑(root' self { val := parent self x, isLt := ⋯ }) else parent self x) =
    if h : x < Array.size self.arr then ↑(root' self { val := x, isLt := ⋯ }) else x
Theorem: Lean4Lean.UnionFind.root_parent
Proof state before:
self : UnionFind
x : Nat
⊢ (if h : x < Array.size self.arr then ↑(root' self { val := parent self x, isLt := ⋯ }) else parent self x) =
    if h : x < Array.size self.arr then ↑(root' self { val := x, isLt := ⋯ }) else x
Tactic:
split <;> simp [parentD, parentD_of_not_lt, *]
Proof state after:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(root' self { val := x, isLt := ⋯ })
Theorem: Lean4Lean.UnionFind.root_parent
Proof state before:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(root' self { val := x, isLt := ⋯ })
Tactic:
(conv => rhs; rw [root'])
Proof state after:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(if h : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ } then { val := x, isLt := ⋯ }
      else
        let_fun this := ⋯;
        root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })
Theorem: Lean4Lean.UnionFind.root_parent
Proof state before:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(if h : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ } then { val := x, isLt := ⋯ }
      else
        let_fun this := ⋯;
        root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })
Tactic:
split
Proof state after:
case inl.inl
self : UnionFind
x : Nat
h✝¹ : x < Array.size self.arr
h✝ : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ }
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) = ↑{ val := x, isLt := ⋯ }

case inl.inr
self : UnionFind
x : Nat
h✝¹ : x < Array.size self.arr
h✝ : ¬(Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ }
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })
Theorem: Lean4Lean.UnionFind.root_parent
Proof state before:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(root' self { val := x, isLt := ⋯ })
Tactic:
conv => rhs; rw [root']
Proof state after:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(if h : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ } then { val := x, isLt := ⋯ }
      else
        let_fun this := ⋯;
        root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })
Theorem: Lean4Lean.UnionFind.root_parent
Proof state before:
case inl.inl
self : UnionFind
x : Nat
h✝¹ : x < Array.size self.arr
h✝ : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ }
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) = ↑{ val := x, isLt := ⋯ }
Tactic:
rw [root', dif_pos] <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_parent
Proof state before:
case inl.inr
self : UnionFind
x : Nat
h✝¹ : x < Array.size self.arr
h✝ : ¬(Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ }
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })
Tactic:
simp
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_lt
Proof state before:
self : UnionFind
x : Nat
⊢ root self x < size self ↔ x < size self
Tactic:
simp [root]
Proof state after:
self : UnionFind
x : Nat
⊢ (if h : x < Array.size self.arr then ↑(root' self { val := x, isLt := ⋯ }) else x) < Array.size self.arr ↔
    x < Array.size self.arr
Theorem: Lean4Lean.UnionFind.root_lt
Proof state before:
self : UnionFind
x : Nat
⊢ (if h : x < Array.size self.arr then ↑(root' self { val := x, isLt := ⋯ }) else x) < Array.size self.arr ↔
    x < Array.size self.arr
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_eq_self
Proof state before:
self : UnionFind
x : Nat
⊢ root self x = x ↔ parent self x = x
Tactic:
refine ⟨fun h => by rw [← h, parent_root], fun h => ?_⟩
Proof state after:
self : UnionFind
x : Nat
h : parent self x = x
⊢ root self x = x
Theorem: Lean4Lean.UnionFind.root_eq_self
Proof state before:
self : UnionFind
x : Nat
h : parent self x = x
⊢ root self x = x
Tactic:
rw [root]
Proof state after:
self : UnionFind
x : Nat
h : parent self x = x
⊢ (if h : x < size self then ↑(root' self { val := x, isLt := h }) else x) = x
Theorem: Lean4Lean.UnionFind.root_eq_self
Proof state before:
self : UnionFind
x : Nat
h : parent self x = x
⊢ (if h : x < size self then ↑(root' self { val := x, isLt := h }) else x) = x
Tactic:
split <;> [rw [root', dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_eq_self
Proof state before:
self : UnionFind
x : Nat
h : root self x = x
⊢ parent self x = x
Tactic:
rw [← h, parent_root]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_eq_self
Proof state before:
self : UnionFind
x : Nat
h : parent self x = x
h✝ : x < size self
⊢ (Array.get self.arr { val := x, isLt := h✝ }).parent = ↑{ val := x, isLt := h✝ }
Tactic:
rwa [parent, parentD_eq' ‹_›] at h
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_ext
Proof state before:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
⊢ root m1 x = root m2 x
Tactic:
if h : m2.parent x = x then
  rw [root_eq_self.2 h, root_eq_self.2 ((H _).trans h)]
else
  have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
  rw [← root_parent, H, root_ext H, root_parent]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_ext
Proof state before:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
h : parent m2 x = x
⊢ root m1 x = root m2 x
Tactic:
rw [root_eq_self.2 h, root_eq_self.2 ((H _).trans h)]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_ext
Proof state before:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
h : ¬parent m2 x = x
⊢ root m1 x = root m2 x
Tactic:
have := Nat.sub_lt_sub_left (m2.lt_rankMax x) (m2.rank_lt h)
Proof state after:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
h : ¬parent m2 x = x
this : rankMax m2 - rank m2 (parent m2 x) < rankMax m2 - rank m2 x
⊢ root m1 x = root m2 x
Theorem: Lean4Lean.UnionFind.root_ext
Proof state before:
m1 m2 : UnionFind
H : ∀ (x : Nat), parent m1 x = parent m2 x
x : Nat
h : ¬parent m2 x = x
this : rankMax m2 - rank m2 (parent m2 x) < rankMax m2 - rank m2 x
⊢ root m1 x = root m2 x
Tactic:
rw [← root_parent, H, root_ext H, root_parent]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.le_rank_root
Proof state before:
self : UnionFind
x : Nat
⊢ rank self x ≤ rank self (root self x)
Tactic:
if h : self.parent x = x then
  rw [root_eq_self.2 h]
else
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
  rw [← root_parent]
  exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.le_rank_root
Proof state before:
self : UnionFind
x : Nat
h : parent self x = x
⊢ rank self x ≤ rank self (root self x)
Tactic:
rw [root_eq_self.2 h]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.le_rank_root
Proof state before:
self : UnionFind
x : Nat
h : ¬parent self x = x
⊢ rank self x ≤ rank self (root self x)
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
Proof state after:
self : UnionFind
x : Nat
h : ¬parent self x = x
this : rankMax self - rank self (parent self x) < rankMax self - rank self x
⊢ rank self x ≤ rank self (root self x)
Theorem: Lean4Lean.UnionFind.le_rank_root
Proof state before:
self : UnionFind
x : Nat
h : ¬parent self x = x
this : rankMax self - rank self (parent self x) < rankMax self - rank self x
⊢ rank self x ≤ rank self (root self x)
Tactic:
rw [← root_parent]
Proof state after:
self : UnionFind
x : Nat
h : ¬parent self x = x
this : rankMax self - rank self (parent self x) < rankMax self - rank self x
⊢ rank self x ≤ rank self (root self (parent self x))
Theorem: Lean4Lean.UnionFind.le_rank_root
Proof state before:
self : UnionFind
x : Nat
h : ¬parent self x = x
this : rankMax self - rank self (parent self x) < rankMax self - rank self x
⊢ rank self x ≤ rank self (root self (parent self x))
Tactic:
exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.lt_rank_root
Proof state before:
self : UnionFind
x : Nat
⊢ rank self x < rank self (root self x) ↔ parent self x ≠ x
Tactic:
refine ⟨fun h h' => Nat.ne_of_lt h (by rw [root_eq_self.2 h']), fun h => ?_⟩
Proof state after:
self : UnionFind
x : Nat
h : parent self x ≠ x
⊢ rank self x < rank self (root self x)
Theorem: Lean4Lean.UnionFind.lt_rank_root
Proof state before:
self : UnionFind
x : Nat
h : parent self x ≠ x
⊢ rank self x < rank self (root self x)
Tactic:
rw [← root_parent]
Proof state after:
self : UnionFind
x : Nat
h : parent self x ≠ x
⊢ rank self x < rank self (root self (parent self x))
Theorem: Lean4Lean.UnionFind.lt_rank_root
Proof state before:
self : UnionFind
x : Nat
h : parent self x ≠ x
⊢ rank self x < rank self (root self (parent self x))
Tactic:
exact Nat.lt_of_lt_of_le (self.rank_lt h) le_rank_root
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.lt_rank_root
Proof state before:
self : UnionFind
x : Nat
h : rank self x < rank self (root self x)
h' : parent self x = x
⊢ rank self x = rank self (root self x)
Tactic:
rw [root_eq_self.2 h']
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.findAux_root
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (findAux self x).root = root' self x
Tactic:
rw [findAux, root']
Proof state after:
self : UnionFind
x : Fin (size self)
⊢ (if h : (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        let_fun this := ⋯;
        match findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ } with
        | { s := arr₁, root := root, size_eq := H } =>
          { s := Array.modify arr₁ ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }).root =
    if h : (Array.get self.arr x).parent = ↑x then x
    else
      let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Theorem: Lean4Lean.UnionFind.findAux_root
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (if h : (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        let_fun this := ⋯;
        match findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ } with
        | { s := arr₁, root := root, size_eq := H } =>
          { s := Array.modify arr₁ ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }).root =
    if h : (Array.get self.arr x).parent = ↑x then x
    else
      let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Tactic:
simp
Proof state after:
self : UnionFind
x : Fin (size self)
⊢ (if (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        {
          s :=
            Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
              { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank },
          root := (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, size_eq := ⋯ }).root =
    if (Array.get self.arr x).parent = ↑x then x else root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Theorem: Lean4Lean.UnionFind.findAux_root
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (if (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        {
          s :=
            Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
              { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank },
          root := (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, size_eq := ⋯ }).root =
    if (Array.get self.arr x).parent = ↑x then x else root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Tactic:
split <;> simp
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root =
    root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Theorem: Lean4Lean.UnionFind.findAux_root
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root =
    root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root =
    root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Theorem: Lean4Lean.UnionFind.findAux_root
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root =
    root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Tactic:
exact findAux_root
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.findAux_s
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (findAux self x).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank }
Tactic:
rw [show self.root _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
Proof state after:
self : UnionFind
x : Fin (size self)
⊢ (findAux self x).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank }

self : UnionFind
x : Fin (size self)
⊢ root self ↑x = ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root