-- 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✝
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
x✝ : m.rankMax - m.rank (m.parent i) < m.rankMax - m.rank i
⊢ m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Tactic:
rw [← rootD_parent, go (m.parent i)]

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
x✝ : m.rankMax - m.rank (m.parent i) < m.rankMax - m.rank i
⊢ (if self.rootD (m.parent i) = ↑x ∨ self.rootD (m.parent i) = ↑y then ↑x else self.rootD (m.parent 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
this :
  ∀ {x y : Fin self.size},
    self.parent ↑x = ↑x →
      self.parent ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i) →
            ∃ r,
              (r = x ∨ r = y) ∧
                ∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑r else self.rootD i
⊢ ∃ 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:
if hr : self.rank y < self.rank x then
  exact this xroot yroot fun i => by simp [parent_link, h, hr]
else
  simpa (config := {singlePass := true}) [or_comm] using
    this yroot xroot fun i => by simp [parent_link, h, hr]

Result:
no goals

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
⊢ ∃ r, (r = x ∨ r = y) ∧ ∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑r else self.rootD i

Tactic:
exact ⟨x, .inl rfl, go⟩

Result:
no goals

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
x✝ : m.rankMax - m.rank (m.parent i) < m.rankMax - m.rank i
⊢ (if self.rootD (m.parent i) = ↑x ∨ self.rootD (m.parent i) = ↑y then ↑x else self.rootD (m.parent i)) =
    if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Tactic:
rw [hm i]

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
x✝ : m.rankMax - m.rank (m.parent i) < m.rankMax - m.rank i
⊢ (if
        self.rootD (if ↑y = i then ↑x else self.parent i) = ↑x ∨
          self.rootD (if ↑y = i then ↑x else self.parent i) = ↑y then
      ↑x
    else self.rootD (if ↑y = i then ↑x else self.parent 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
i x✝ : Nat
⊢ (self.link x y yroot).parent x✝ = self.parent x✝

Tactic:
rw [parent_link, if_pos h]

Result:
no goals

Proof state:
self : UnionFind
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin self.size},
    self.parent ↑x = ↑x →
      self.parent ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), m.parent i = if ↑y = i then ↑x else self.parent i) →
            ∃ r,
              (r = x ∨ r = y) ∧
                ∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑r else self.rootD i
hr : self.rank ↑y < self.rank ↑x
i : Nat
⊢ (self.link x y yroot).parent i = if ↑y = i then ↑x else self.parent i

Tactic:
simp [parent_link, h, hr]

Result:
no goals

Proof state:
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

Tactic:
rw [rootD_eq_self.2 ‹_›]

Result:
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 i = ↑x ∨ i = ↑y then ↑x else 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:
have _ := Nat.sub_lt_sub_left (m.lt_rankMax i) (m.rank_lt 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
x✝ : m.rankMax - m.rank (m.parent i) < m.rankMax - m.rank i
⊢ m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Proof state:
case isTrue.hc
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
⊢ self.rootD i = ↑x ∨ self.rootD i = ↑y

Tactic:
simp [← h, rootD_eq_self, xroot]

Result:
no goals

Proof state:
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
h : ¬m.parent ↑y = ↑y
x✝ : m.rankMax - m.rank (m.parent ↑y) < m.rankMax - m.rank ↑y
⊢ (if self.rootD ↑x = ↑x ∨ self.rootD ↑x = ↑y then ↑x else self.rootD ↑x) =
    if self.rootD ↑y = ↑x ∨ self.rootD ↑y = ↑y then ↑x else self.rootD ↑y

Tactic:
simp [rootD_eq_self.2 xroot, rootD_eq_self.2 yroot]

Result:
no goals