Theorem: Lean4Lean.UnionFind.parentD_linkAux (Lean4Lean/Verify/UnionFind.lean)

State before:
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
⊢ parentD (linkAux self x y) i =
    if ↑x = ↑y then parentD self i
    else
      if (Array.get self y).rank < (Array.get 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 [linkAux]
State after:
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
⊢ parentD
      (if ↑x = ↑y then self
      else
        if (Array.get self y).rank < (Array.get self x).rank then
          Array.set self y { parent := ↑x, rank := (Array.get self y).rank }
        else
          if (Array.get self x).rank = (Array.get self y).rank then
            Array.set (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) { val := ↑y, isLt := ⋯ }
              { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }
          else Array.set self x { parent := ↑y, rank := (Array.get self x).rank })
      i =
    if ↑x = ↑y then parentD self i
    else
      if (Array.get self y).rank < (Array.get self x).rank then if ↑y = i then ↑x else parentD self i
      else if ↑x = i then ↑y else parentD self i

State before:
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
⊢ parentD
      (if ↑x = ↑y then self
      else
        if (Array.get self y).rank < (Array.get self x).rank then
          Array.set self y { parent := ↑x, rank := (Array.get self y).rank }
        else
          if (Array.get self x).rank = (Array.get self y).rank then
            Array.set (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) { val := ↑y, isLt := ⋯ }
              { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }
          else Array.set self x { parent := ↑y, rank := (Array.get self x).rank })
      i =
    if ↑x = ↑y then parentD self i
    else
      if (Array.get self y).rank < (Array.get 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]
State after:
case inr.inr.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (if ↑{ val := ↑y, isLt := ⋯ } = i then
      { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }.parent
    else parentD (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) i) =
    if ↑x = i then ↑y else parentD self i

State before:
case inr.inr.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (if ↑{ val := ↑y, isLt := ⋯ } = i then
      { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }.parent
    else parentD (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) i) =
    if ↑x = i then ↑y else parentD self i
Tactic:
simp
State after:
case inr.inr.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (if ↑y = i then (Array.get self y).parent
    else parentD (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) i) =
    if ↑x = i then ↑y else parentD self i

State before:
case inr.inr.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (if ↑y = i then (Array.get self y).parent
    else parentD (Array.set self x { parent := ↑y, rank := (Array.get 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]]
State after:
no goals

State before:
case inr.inr.inl.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝³ : ¬↑x = ↑y
h✝² : ¬(Array.get self y).rank < (Array.get self x).rank
h✝¹ : (Array.get self x).rank = (Array.get self y).rank
h✝ : ↑y = i
⊢ (Array.get self y).parent = if ↑x = i then ↑y else parentD self i
Tactic:
subst i
State after:
case inr.inr.inl.inl
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (Array.get self y).parent = if ↑x = ↑y then ↑y else parentD self ↑y

State before:
case inr.inr.inl.inl
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (Array.get self y).parent = if ↑x = ↑y then ↑y else parentD self ↑y
Tactic:
rwa [if_neg, parentD_eq]
State after:
no goals