-- 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
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
⊢ ∃ 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:
exact this xroot yroot fun i => by 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 i = ↑x ∨ i = ↑y then ↑x else i

Tactic:
split <;> [skip; rfl]

Result:
case isFalse.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 : self.parent i = i
h✝ : i = ↑x ∨ i = ↑y
⊢ i = ↑x

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 (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

Tactic:
split <;> [subst i; rw [rootD_parent]]

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
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

Proof state:
case isFalse.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 : self.parent i = i
h✝ : i = ↑x ∨ i = ↑y
⊢ i = ↑x

Tactic:
next h' => exact h'.resolve_right (Ne.symm ‹_›)

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

Tactic:
rw [rootD_ext (m2 := self) (fun _ => by rw [parent_link, if_pos h])]

Result:
self : UnionFind
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ self.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
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 ↑x = i then ↑y else self.parent i

Tactic:
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
i : Nat
h✝ : ¬↑y = i
h : self.parent i = i
h' : i = ↑x ∨ i = ↑y
⊢ i = ↑x

Tactic:
exact h'.resolve_right (Ne.symm ‹_›)

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
⊢ ∃ 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:
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
i : Nat
⊢ self.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Tactic:
split <;> [obtain _ | _ := ‹_› <;> simp [*]; rfl]

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
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i

Tactic:
rw [if_pos, h]

Result:
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