-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem find_root_1 (self : UnionFind) (x : Fin self.size) (i : Nat) :
    (self.find x).1.rootD i = self.rootD i

Proof state:
case inr
self : UnionFind
x : Fin self.size
i : Nat
h : self.parent i = i
h1 : (self.find x).fst.parent i = self.parent i
⊢ i = self.rootD i

Tactic:
rw [rootD_eq_self.2 h]

Result:
no goals

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h : (self.find x).fst.parent i = i
⊢ i = self.rootD i

Tactic:
obtain ⟨h1, _⟩ | h1 := find_parent_or self x i <;> rw [h1] at h

Result:
case inl.intro
self : UnionFind
x : Fin self.size
i : Nat
h : self.rootD i = i
h1 : (self.find x).fst.parent i = self.rootD i
right✝ : self.rootD i = self.rootD ↑x
⊢ i = self.rootD i

case inr
self : UnionFind
x : Fin self.size
i : Nat
h : self.parent i = i
h1 : (self.find x).fst.parent i = self.parent i
⊢ i = self.rootD i

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
⊢ (self.find x).fst.rootD i = self.rootD i

Tactic:
rw [← rootD_parent, find_root_1 self x ((self.find x).1.parent i)]

Result:
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
⊢ self.rootD ((self.find x).fst.parent i) = self.rootD i

Proof state:
case inr
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
h1 : (self.find x).fst.parent i = self.parent i
⊢ self.rootD ((self.find x).fst.parent i) = self.rootD i

Tactic:
rw [h1, rootD_parent]

Result:
no goals

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
⊢ (self.find x).fst.rootD i = self.rootD i

Tactic:
have := Nat.sub_lt_sub_left ((self.find x).1.lt_rankMax _) ((self.find x).1.rank_lt h)

Result:
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
⊢ (self.find x).fst.rootD i = self.rootD i

Proof state:
case inl.intro
self : UnionFind
x : Fin self.size
i : Nat
h : self.rootD i = i
h1 : (self.find x).fst.parent i = self.rootD i
right✝ : self.rootD i = self.rootD ↑x
⊢ i = self.rootD i

Tactic:
rw [h]

Result:
no goals

Proof state:
case inl.intro
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
h1 : (self.find x).fst.parent i = self.rootD i
right✝ : self.rootD i = self.rootD ↑x
⊢ self.rootD ((self.find x).fst.parent i) = self.rootD i

Tactic:
rw [h1, rootD_rootD]

Result:
no goals

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
⊢ self.rootD ((self.find x).fst.parent i) = self.rootD i

Tactic:
obtain ⟨h1, _⟩ | h1 := find_parent_or self x i

Result:
case inl.intro
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
h1 : (self.find x).fst.parent i = self.rootD i
right✝ : self.rootD i = self.rootD ↑x
⊢ self.rootD ((self.find x).fst.parent i) = self.rootD i

case inr
self : UnionFind
x : Fin self.size
i : Nat
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
h1 : (self.find x).fst.parent i = self.parent i
⊢ self.rootD ((self.find x).fst.parent i) = self.rootD i

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h : (self.find x).fst.parent i = i
⊢ (self.find x).fst.rootD i = self.rootD i

Tactic:
rw [rootD_eq_self.2 h]

Result:
self : UnionFind
x : Fin self.size
i : Nat
h : (self.find x).fst.parent i = i
⊢ i = self.rootD i

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
a✝ :
  ∀ (y : Nat),
    (invImage (fun x_1 => (self.find x).fst.rankMax - (self.find x).fst.rank x_1) instWellFoundedRelationOfSizeOf).1 y
        i →
      (self.find x).fst.rootD y = self.rootD y
h : ¬(self.find x).fst.parent i = i
this :
  (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i
⊢ (self.find x).fst.rankMax - (self.find x).fst.rank ((self.find x).fst.parent i) <
    (self.find x).fst.rankMax - (self.find x).fst.rank i

Tactic:
exact this

Result:
no goals