-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem findAux_s {self : UnionFind} {x : Fin self.size} :
    (findAux self x).s = if self.arr[x.1].parent = x then self.arr else
      (self.findAux ⟨_, self.parent'_lt x x.2⟩).s.modify x fun s =>
        { s with parent := self.rootD x }

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

Tactic:
rw [findAux]

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 := ⋯ }).s =
    if self.arr[↑x].parent = ↑x then self.arr
    else
      (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s =>
        { parent := ↑(self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root, rank := s.rank }

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

Tactic:
rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x x.2⟩).root from _]

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

self : UnionFind
x : Fin self.size
⊢ self.rootD ↑x = ↑(self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root

Proof state:
self : UnionFind
x : Fin self.size
⊢ (if h : self.arr[↑x].parent < self.arr.size then ↑(self.root ⟨self.arr[↑x].parent, ⋯⟩) else self.arr[↑x].parent) =
    ↑(self.root ⟨self.arr[↑x].parent, ⋯⟩)

self : UnionFind
x : Fin self.size
⊢ ↑x < self.arr.size

Tactic:
apply dif_pos

Result:
case hc
self : UnionFind
x : Fin self.size
⊢ self.arr[↑x].parent < self.arr.size

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 := ⋯ }).s =
    if self.arr[↑x].parent = ↑x then self.arr
    else
      (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s =>
        { parent := ↑(self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root, rank := s.rank }

Tactic:
split <;> rfl

Result:
no goals

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

self : UnionFind
x : Fin self.size
⊢ ↑x < self.arr.size

Tactic:
simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root]

Result:
self : UnionFind
x : Fin self.size
⊢ (if h : self.arr[↑x].parent < self.arr.size then ↑(self.root ⟨self.arr[↑x].parent, ⋯⟩) else self.arr[↑x].parent) =
    ↑(self.root ⟨self.arr[↑x].parent, ⋯⟩)

self : UnionFind
x : Fin self.size
⊢ ↑x < self.arr.size

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

Tactic:
rw [← rootD_parent, parent, parentD_eq]

Result:
self : UnionFind
x : Fin self.size
⊢ self.rootD self.arr[↑x].parent = ↑(self.findAux ⟨self.arr[↑x].parent, ⋯⟩).root

self : UnionFind
x : Fin self.size
⊢ ↑x < self.arr.size

Proof state:
case hc
self : UnionFind
x : Fin self.size
⊢ self.arr[↑x].parent < self.arr.size

Tactic:
exact parent'_lt ..

Result:
no goals