-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem findAux_root {self : UnionFind} {x : Fin self.size} :
    (findAux self x).root = self.root x

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
h✝ : ¬self.arr[↑x].parent = ↑x
⊢ (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root = self.root ⟨self.arr[↑x].parent, ⋯⟩

Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)

Result:
case isFalse
self : UnionFind
x : Fin self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root = self.root ⟨self.arr[↑x].parent, ⋯⟩

Proof state:
self : UnionFind
x : Fin self.size
⊢ (if self.arr[↑x].parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        {
          s :=
            (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s =>
              { parent := ↑(self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root, rank := s.rank },
          root := (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root, size_eq := ⋯ }).root =
    if self.arr[↑x].parent = ↑x then x else self.root ⟨self.arr[↑x].parent, ⋯⟩

Tactic:
split <;> simp only

Result:
case isFalse
self : UnionFind
x : Fin self.size
h✝ : ¬self.arr[↑x].parent = ↑x
⊢ (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root = self.root ⟨self.arr[↑x].parent, ⋯⟩

Proof state:
self : UnionFind
x : Fin self.size
⊢ (self.findAux x).root = self.root x

Tactic:
rw [findAux, root]

Result:
self : UnionFind
x : Fin self.size
⊢ (if h : self.arr[↑x].parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        let_fun this := ⋯;
        match self.findAux ⟨self.arr[↑x].parent, ⋯⟩ with
        | { s := arr₁, root := root, size_eq := H } =>
          { s := arr₁.modify ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }).root =
    if h : self.arr[↑x].parent = ↑x then x
    else
      let_fun this := ⋯;
      self.root ⟨self.arr[↑x].parent, ⋯⟩

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root = self.root ⟨self.arr[↑x].parent, ⋯⟩

Tactic:
exact findAux_root

Result:
no goals

Proof state:
self : UnionFind
x : Fin self.size
⊢ (if h : self.arr[↑x].parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        let_fun this := ⋯;
        match self.findAux ⟨self.arr[↑x].parent, ⋯⟩ with
        | { s := arr₁, root := root, size_eq := H } =>
          { s := arr₁.modify ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }).root =
    if h : self.arr[↑x].parent = ↑x then x
    else
      let_fun this := ⋯;
      self.root ⟨self.arr[↑x].parent, ⋯⟩

Tactic:
simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite]

Result:
self : UnionFind
x : Fin self.size
⊢ (if self.arr[↑x].parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        {
          s :=
            (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s =>
              { parent := ↑(self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root, rank := s.rank },
          root := (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root, size_eq := ⋯ }).root =
    if self.arr[↑x].parent = ↑x then x else self.root ⟨self.arr[↑x].parent, ⋯⟩