Theorem: Lean4Lean.UnionFind.parentD_findAux (Lean4Lean/UnionFind.lean)

State before:
i : Nat
self : UnionFind
x : Fin (size self)
⊢ parentD (findAux self x).s i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [findAux_s]
State after:
i : Nat
self : UnionFind
x : Fin (size self)
⊢ parentD
      (if (Array.get self.arr x).parent = ↑x then self.arr
      else
        Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
      i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

State before:
i : Nat
self : UnionFind
x : Fin (size self)
⊢ parentD
      (if (Array.get self.arr x).parent = ↑x then self.arr
      else
        Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
      i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
split <;> [split; skip]
State after:
case inl.inl
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : i = ↑x
⊢ parentD self.arr i = root self ↑x

case inl.inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i = parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

case inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

State before:
case inl.inl
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : i = ↑x
⊢ parentD self.arr i = root self ↑x
Tactic:
subst i
State after:
case inl.inl
self : UnionFind
x : Fin (size self)
h✝ : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr ↑x = root self ↑x

State before:
case inl.inl
self : UnionFind
x : Fin (size self)
h✝ : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr ↑x = root self ↑x
Tactic:
rw [root_eq_self.2 _] <;> simp [parentD_eq, *]
State after:
no goals

State before:
case inl.inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i = parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [findAux_s]
State after:
case inl.inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i =
    parentD
      (if
          (Array.get self.arr { val := (Array.get self.arr x).parent, isLt := ⋯ }).parent =
            ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ } then
        self.arr
      else
        Array.modify
          (findAux self
              { val := (Array.get self.arr { val := (Array.get self.arr x).parent, isLt := ⋯ }).parent, isLt := ⋯ }).s
          ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ } fun s =>
          { parent := root self ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ }, rank := s.rank })
      i

State before:
case inl.inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i =
    parentD
      (if
          (Array.get self.arr { val := (Array.get self.arr x).parent, isLt := ⋯ }).parent =
            ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ } then
        self.arr
      else
        Array.modify
          (findAux self
              { val := (Array.get self.arr { val := (Array.get self.arr x).parent, isLt := ⋯ }).parent, isLt := ⋯ }).s
          ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ } fun s =>
          { parent := root self ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ }, rank := s.rank })
      i
Tactic:
simp [*]
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [parentD]
State after:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ (if h :
        i <
          Array.size
            (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
              { parent := root self ↑x, rank := s.rank }) then
      (Array.get
          (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
            { parent := root self ↑x, rank := s.rank })
          { val := i, isLt := h }).parent
    else i) =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ (if h :
        i <
          Array.size
            (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
              { parent := root self ↑x, rank := s.rank }) then
      (Array.get
          (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
            { parent := root self ↑x, rank := s.rank })
          { val := i, isLt := h }).parent
    else i) =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
split <;> rename_i h'
State after:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  i <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
⊢ (Array.get
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
        { val := i, isLt := h' }).parent =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ i = if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

State before:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  i <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
⊢ (Array.get
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
        { val := i, isLt := h' }).parent =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [Array.get_modify (by simpa using h')]
State after:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  i <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).parent =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

State before:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  i <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).parent =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
simp [@eq_comm _ i]
State after:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  i <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).parent =
    if ↑x = i then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

State before:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  i <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).parent =
    if ↑x = i then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
split <;> simp [← parentD_eq]
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  i <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
⊢ i < Array.size (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
Tactic:
simpa using h'
State after:
no goals

State before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ i = if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
State after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ i = parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

State before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ i = parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [parentD, dif_neg]
State after:
case inr.hnc
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ ¬i < Array.size (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s

State before:
case inr.hnc
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ ¬i < Array.size (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
Tactic:
simpa using h'
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ i = ↑x →
    i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
Tactic:
rintro rfl
State after:
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬↑x <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ ↑x <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })

State before:
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬↑x <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ ↑x <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
Tactic:
simp [FindAux.size_eq]
State after:
no goals