-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
    parentD (findAux self x).s i =
    if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt _ x.2⟩).s i

Proof state:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' :
  ¬i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ i = parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Tactic:
rw [parentD, dif_neg]

Result:
case isFalse.hnc
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' :
  ¬i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ ¬i < (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.size

Proof state:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' : i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank })[i].parent =
    if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Tactic:
rw [Array.getElem_modify (by simpa using h')]

Result:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' : i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ (if ↑x = i then { parent := self.rootD ↑x, rank := (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s[i].rank }
      else (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s[i]).parent =
    if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

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

Tactic:
rw [parentD]

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

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

Tactic:
simp [FindAux.size_eq]

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' : i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size

Tactic:
simpa using h'

Result:
no goals

Proof state:
case isTrue.isFalse
i : Nat
self : UnionFind
x : Fin self.size
h✝¹ : self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i =
    parentD
      (if self.arr[↑⟨self.arr[↑x].parent, ⋯⟩].parent = ↑⟨self.arr[↑x].parent, ⋯⟩ then self.arr
      else
        (self.findAux ⟨self.arr[↑⟨self.arr[↑x].parent, ⋯⟩].parent, ⋯⟩).s.modify ↑⟨self.arr[↑x].parent, ⋯⟩ fun s =>
          { parent := self.rootD ↑⟨self.arr[↑x].parent, ⋯⟩, rank := s.rank })
      i

Tactic:
simp [*, -Array.get_eq_getElem]

Result:
no goals

Proof state:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' : i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ (if ↑x = i then { parent := self.rootD ↑x, rank := (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s[i].rank }
      else (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s[i]).parent =
    if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Tactic:
simp only [Array.length_toList, @eq_comm _ i]

Result:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' : i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ (if ↑x = i then { parent := self.rootD ↑x, rank := (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s[i].rank }
      else (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s[i]).parent =
    if ↑x = i then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Proof state:
case isFalse.hnc
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' :
  ¬i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ ¬i < (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.size

Tactic:
simpa using h'

Result:
no goals

Proof state:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' :
  ¬i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ i = if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Tactic:
rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]

Result:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' :
  ¬i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ i = parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

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

Tactic:
split <;> rename_i h'

Result:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' : i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank })[i].parent =
    if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : ¬self.arr[↑x].parent = ↑x
h' :
  ¬i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size
⊢ i = if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i