-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem root_link {self : UnionFind} {x y : Fin self.size}
    (xroot : self.parent x = x) (yroot : self.parent y = y) :
    ∃ r, (r = x ∨ r = y) ∧ ∀ i,
      (link self x y yroot).rootD i =
      if self.rootD i = x ∨ self.rootD i = y then r.1 else self.rootD i

Proof state:
self : UnionFind
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
h : ↑x = ↑y
⊢ ∃ r,
    (r = x ∨ r = y) ∧
      ∀ (i : Nat), (self.link x y yroot).rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑r else self.rootD i

Tactic:
refine ⟨x, .inl rfl, fun i => ?_⟩

Result:
self : UnionFind
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ (self.link x y yroot).rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Proof state:
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i
i : Nat
h : m.parent i = i
⊢ i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Tactic:
rw [hm i] at h

Result:
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i
i : Nat
h : (if ↑y = i then ↑x else self.parent i) = i
⊢ i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Proof state:
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i
i : Nat
h : m.parent i = i
⊢ m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Tactic:
rw [rootD_eq_self.2 h]

Result:
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i
i : Nat
h : m.parent i = i
⊢ i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Proof state:
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i
i : Nat
h : (if ↑y = i then ↑x else self.parent i) = i
⊢ i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Tactic:
split at h

Result:
case isTrue
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

case isFalse
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i
i : Nat
h✝ : ¬↑y = i
h : self.parent i = i
⊢ i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i