-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem parentD_linkAux {self} {x y : Fin self.size} :
    parentD (linkAux self x y) i =
    if x.1 = y then
      parentD self i
    else
      if self[y.1].rank < self[x.1].rank then
        if y = i then x else parentD self i
      else
        if x = i then y else parentD self i

Proof state:
i : Nat
self : Array UFNode
x y : Fin self.size
⊢ parentD (linkAux self x y) i =
    if ↑x = ↑y then parentD self i
    else
      if self[↑y].rank < self[↑x].rank then if ↑y = i then ↑x else parentD self i
      else if ↑x = i then ↑y else parentD self i

Tactic:
dsimp only [linkAux]

Result:
i : Nat
self : Array UFNode
x y : Fin self.size
⊢ parentD
      (if ↑x = ↑y then self
      else
        if self[↑y].rank < self[↑x].rank then self.set ↑y { parent := ↑x, rank := self[↑y].rank } ⋯
        else
          if self[↑x].rank = self[↑y].rank then
            (self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯).set ↑y
              { parent := self[↑y].parent, rank := self[↑y].rank + 1 } ⋯
          else self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯)
      i =
    if ↑x = ↑y then parentD self i
    else
      if self[↑y].rank < self[↑x].rank then if ↑y = i then ↑x else parentD self i
      else if ↑x = i then ↑y else parentD self i

Proof state:
i : Nat
self : Array UFNode
x y : Fin self.size
⊢ parentD
      (if ↑x = ↑y then self
      else
        if self[↑y].rank < self[↑x].rank then self.set ↑y { parent := ↑x, rank := self[↑y].rank } ⋯
        else
          if self[↑x].rank = self[↑y].rank then
            (self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯).set ↑y
              { parent := self[↑y].parent, rank := self[↑y].rank + 1 } ⋯
          else self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯)
      i =
    if ↑x = ↑y then parentD self i
    else
      if self[↑y].rank < self[↑x].rank then if ↑y = i then ↑x else parentD self i
      else if ↑x = i then ↑y else parentD self i

Tactic:
split <;> [rfl; split] <;> [rw [parentD_set]; split] <;> rw [parentD_set]

Result:
case isFalse.isFalse.isTrue
i : Nat
self : Array UFNode
x y : Fin self.size
h✝² : ¬↑x = ↑y
h✝¹ : ¬self[↑y].rank < self[↑x].rank
h✝ : self[↑x].rank = self[↑y].rank
⊢ (if ↑y = i then { parent := self[↑y].parent, rank := self[↑y].rank + 1 }.parent
    else parentD (self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯) i) =
    if ↑x = i then ↑y else parentD self i

Proof state:
case isFalse.isFalse.isTrue.isTrue
self : Array UFNode
x y : Fin self.size
h✝² : ¬↑x = ↑y
h✝¹ : ¬self[↑y].rank < self[↑x].rank
h✝ : self[↑x].rank = self[↑y].rank
⊢ { parent := self[↑y].parent, rank := self[↑y].rank + 1 }.parent = if ↑x = ↑y then ↑y else parentD self ↑y

Tactic:
rwa [if_neg, parentD_eq]

Result:
no goals

Proof state:
case isFalse.isFalse.isTrue
i : Nat
self : Array UFNode
x y : Fin self.size
h✝² : ¬↑x = ↑y
h✝¹ : ¬self[↑y].rank < self[↑x].rank
h✝ : self[↑x].rank = self[↑y].rank
⊢ (if ↑y = i then { parent := self[↑y].parent, rank := self[↑y].rank + 1 }.parent
    else parentD (self.set ↑x { parent := ↑y, rank := self[↑x].rank } ⋯) i) =
    if ↑x = i then ↑y else parentD self i

Tactic:
split <;> [(subst i; rwa [if_neg, parentD_eq]); rw [parentD_set]]

Result:
no goals

Proof state:
case isFalse.isFalse.isTrue.isTrue
i : Nat
self : Array UFNode
x y : Fin self.size
h✝³ : ¬↑x = ↑y
h✝² : ¬self[↑y].rank < self[↑x].rank
h✝¹ : self[↑x].rank = self[↑y].rank
h✝ : ↑y = i
⊢ { parent := self[↑y].parent, rank := self[↑y].rank + 1 }.parent = if ↑x = i then ↑y else parentD self i

Tactic:
subst i

Result:
case isFalse.isFalse.isTrue.isTrue
self : Array UFNode
x y : Fin self.size
h✝² : ¬↑x = ↑y
h✝¹ : ¬self[↑y].rank < self[↑x].rank
h✝ : self[↑x].rank = self[↑y].rank
⊢ { parent := self[↑y].parent, rank := self[↑y].rank + 1 }.parent = if ↑x = ↑y then ↑y else parentD self ↑y