-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x

Proof state:
case isTrue.isFalse
self : UnionFind
x : Nat
h✝¹ : x < self.arr.size
h✝ : ¬self.arr[↑⟨x, ⋯⟩].parent = ↑⟨x, ⋯⟩
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) =
    ↑(let_fun this := ⋯;
      self.root ⟨self.arr[↑⟨x, ⋯⟩].parent, ⋯⟩)

Tactic:
simp

Result:
no goals

Proof state:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.arr.size
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) = ↑(self.root ⟨x, ⋯⟩)

Tactic:
conv => rhs; rw [root]

Result:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.arr.size
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) =
    ↑(if h : self.arr[↑⟨x, ⋯⟩].parent = ↑⟨x, ⋯⟩ then ⟨x, ⋯⟩
      else
        let_fun this := ⋯;
        self.root ⟨self.arr[↑⟨x, ⋯⟩].parent, ⋯⟩)

Proof state:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.arr.size
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) = ↑(self.root ⟨x, ⋯⟩)

Tactic:
(conv => rhs; rw [root])

Result:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.arr.size
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) =
    ↑(if h : self.arr[↑⟨x, ⋯⟩].parent = ↑⟨x, ⋯⟩ then ⟨x, ⋯⟩
      else
        let_fun this := ⋯;
        self.root ⟨self.arr[↑⟨x, ⋯⟩].parent, ⋯⟩)

Proof state:
self : UnionFind
x : Nat
⊢ (if h : x < self.arr.size then ↑(self.root ⟨self.parent x, ⋯⟩) else self.parent x) =
    if h : x < self.arr.size then ↑(self.root ⟨x, ⋯⟩) else x

Tactic:
split

Result:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.arr.size
⊢ ↑(self.root ⟨self.parent x, ⋯⟩) = ↑(self.root ⟨x, ⋯⟩)

case isFalse
self : UnionFind
x : Nat
h✝ : ¬x < self.arr.size
⊢ self.parent x = x

Proof state:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.arr.size
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) =
    ↑(if h : self.arr[↑⟨x, ⋯⟩].parent = ↑⟨x, ⋯⟩ then ⟨x, ⋯⟩
      else
        let_fun this := ⋯;
        self.root ⟨self.arr[↑⟨x, ⋯⟩].parent, ⋯⟩)

Tactic:
split

Result:
case isTrue.isTrue
self : UnionFind
x : Nat
h✝¹ : x < self.arr.size
h✝ : self.arr[↑⟨x, ⋯⟩].parent = ↑⟨x, ⋯⟩
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) = ↑⟨x, ⋯⟩

case isTrue.isFalse
self : UnionFind
x : Nat
h✝¹ : x < self.arr.size
h✝ : ¬self.arr[↑⟨x, ⋯⟩].parent = ↑⟨x, ⋯⟩
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) =
    ↑(let_fun this := ⋯;
      self.root ⟨self.arr[↑⟨x, ⋯⟩].parent, ⋯⟩)

Proof state:
self : UnionFind
x : Nat
⊢ self.rootD (self.parent x) = self.rootD x

Tactic:
simp only [rootD, Array.length_toList, parent_lt]

Result:
self : UnionFind
x : Nat
⊢ (if h : x < self.arr.size then ↑(self.root ⟨self.parent x, ⋯⟩) else self.parent x) =
    if h : x < self.arr.size then ↑(self.root ⟨x, ⋯⟩) else x

Proof state:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.arr.size
⊢ ↑(self.root ⟨self.parent x, ⋯⟩) = ↑(self.root ⟨x, ⋯⟩)

Tactic:
simp only [parentD, ↓reduceDIte, *]

Result:
case isTrue
self : UnionFind
x : Nat
h✝ : x < self.arr.size
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) = ↑(self.root ⟨x, ⋯⟩)

Proof state:
case isTrue.isTrue
self : UnionFind
x : Nat
h✝¹ : x < self.arr.size
h✝ : self.arr[↑⟨x, ⋯⟩].parent = ↑⟨x, ⋯⟩
⊢ ↑(self.root ⟨self.arr[x].parent, ⋯⟩) = ↑⟨x, ⋯⟩

Tactic:
rw [root, dif_pos] <;> simp_all

Result:
no goals

Proof state:
case isFalse
self : UnionFind
x : Nat
h✝ : ¬x < self.arr.size
⊢ self.parent x = x

Tactic:
simp only [not_false_eq_true, parentD_of_not_lt, *]

Result:
no goals