-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
    rankD (findAux self x).s i = self.rank i

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
⊢ rankD (self.findAux x).s i = self.rank i

Tactic:
rw [findAux_s]

Result:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
⊢ rankD
      (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 =
    self.rank i

Proof state:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this✝ : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
this : ↑x < self.arr.size
⊢ rankD ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }) i =
    self.rank i

Tactic:
rw [rankD_eq (by simp [FindAux.size_eq, h]), Array.getElem_modify]

Result:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this✝ : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
this : ↑x < self.arr.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]).rank =
    self.rank i

Proof state:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this✝ : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
this : ↑x < self.arr.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]).rank =
    self.rank i

Tactic:
split <;>
  simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem]

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : ¬i < self.size
⊢ (if h : i < (self.findAux x).s.size then (self.findAux x).s[i].rank else 0) =
    if h : i < self.arr.size then self.arr[i].rank else 0

Tactic:
rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]

Result:
no goals

Proof state:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
⊢ rankD ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }) i =
    self.rank i

Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)

Result:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ rankD ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }) i =
    self.rank i

Proof state:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ rankD ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }) i =
    self.rank i

Tactic:
have := lt_of_parentD (by rwa [parentD_eq])

Result:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this✝ : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
this : ↑x < self.arr.size
⊢ rankD ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }) i =
    self.rank i

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : ¬i < self.size
⊢ ¬i < (self.findAux x).s.size

Tactic:
rwa [FindAux.size_eq]

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this✝ : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
this : ↑x < self.arr.size
⊢ i < ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }).size

Tactic:
simp [FindAux.size_eq, h]

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
⊢ rankD
      (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 =
    self.rank i

Tactic:
split <;> [rfl; skip]

Result:
case isFalse
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
⊢ rankD ((self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s.modify ↑x fun s => { parent := self.rootD ↑x, rank := s.rank }) i =
    self.rank i

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : ¬i < self.size
⊢ rankD (self.findAux x).s i = self.rank i

Tactic:
simp only [rankD, Array.length_toList, Array.get_eq_getElem, rank]

Result:
i : Nat
self : UnionFind
x : Fin self.size
h : ¬i < self.size
⊢ (if h : i < (self.findAux x).s.size then (self.findAux x).s[i].rank else 0) =
    if h : i < self.arr.size then self.arr[i].rank else 0

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
⊢ rankD (self.findAux x).s i = self.rank 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.getElem_modify]
  split <;>
    simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem]
else
  simp only [rankD, Array.length_toList, Array.get_eq_getElem, rank]
  rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h : i < self.size
h✝ : ¬self.arr[↑x].parent = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD ?m.56140 ?m.56141 ≠ ?m.56141

Tactic:
rwa [parentD_eq]

Result:
no goals