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

State before:
i : Nat
self : UnionFind
x : Fin (size self)
⊢ rankD (findAux self x).s i = rank self i
Tactic:
if h : i < self.size then
  rw [findAux_s]; split <;> [rfl; skip]
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
  have := lt_of_parentD (by rwa [parentD_eq])
  rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify (by rwa [FindAux.size_eq])]
  split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩)]
else
  simp [rank, rankD]; rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
⊢ rankD (findAux self x).s i = rank self i
Tactic:
rw [findAux_s]
State after:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
⊢ rankD
      (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 =
    rank self i

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
⊢ rankD
      (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 =
    rank self i
Tactic:
split <;> [rfl; skip]
State after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i

State before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
State after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i

State before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Tactic:
have := lt_of_parentD (by rwa [parentD_eq])
State after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i

State before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Tactic:
rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify (by rwa [FindAux.size_eq])]
State after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ (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 := ⋯ }).rank =
    rank self i

State before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ (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 := ⋯ }).rank =
    rank self i
Tactic:
split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩)]
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD ?m.115685 ?m.115686 ≠ ?m.115686
Tactic:
rwa [parentD_eq]
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ 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:
simp [FindAux.size_eq, h]
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h✝ : ¬(Array.get self.arr x).parent = ↑x
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ i < Array.size (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
Tactic:
rwa [FindAux.size_eq]
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬i < size self
⊢ rankD (findAux self x).s i = rank self i
Tactic:
simp [rank, rankD]
State after:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬i < size self
⊢ (if h : i < Array.size (findAux self x).s then (Array.get (findAux self x).s { val := i, isLt := h }).rank else 0) =
    if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬i < size self
⊢ (if h : i < Array.size (findAux self x).s then (Array.get (findAux self x).s { val := i, isLt := h }).rank else 0) =
    if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0
Tactic:
rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬i < size self
⊢ ¬i < Array.size (findAux self x).s
Tactic:
rwa [FindAux.size_eq]
State after:
no goals