-- 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:
i : Nat
self : UnionFind
x : Fin self.size
⊢ parentD
      (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 })
      i =
    if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Tactic:
split <;> [split; skip]

Result:
case isTrue.isTrue
i : Nat
self : UnionFind
x : Fin self.size
h✝¹ : self.arr[↑x].parent = ↑x
h✝ : i = ↑x
⊢ parentD self.arr i = self.rootD ↑x

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 (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

case isFalse
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

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 (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Tactic:
rw [findAux_s]

Result:
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

Proof state:
case isTrue.isTrue
i : Nat
self : UnionFind
x : Fin self.size
h✝¹ : self.arr[↑x].parent = ↑x
h✝ : i = ↑x
⊢ parentD self.arr i = self.rootD ↑x

Tactic:
subst i

Result:
case isTrue.isTrue
self : UnionFind
x : Fin self.size
h✝ : self.arr[↑x].parent = ↑x
⊢ parentD self.arr ↑x = self.rootD ↑x

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
⊢ parentD (self.findAux x).s i = if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Tactic:
rw [findAux_s]

Result:
i : Nat
self : UnionFind
x : Fin self.size
⊢ parentD
      (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 })
      i =
    if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

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 ↑x = i then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i

Tactic:
split <;> simp [← parentD_eq, -Array.get_eq_getElem]

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 = ↑x →
    i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size

Tactic:
rintro rfl

Result:
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

Proof state:
case isTrue.isTrue
self : UnionFind
x : Fin self.size
h✝ : self.arr[↑x].parent = ↑x
⊢ parentD self.arr ↑x = self.rootD ↑x

Tactic:
rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem]

Result:
no goals