-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem equiv_link {self : UnionFind} {x y : Fin self.size}
    (xroot : self.parent x = x) (yroot : self.parent y = y) :
    Equiv (link self x y yroot) a b ↔
    Equiv self a b ∨ Equiv self a x ∧ Equiv self y b ∨ Equiv self a y ∧ Equiv self x b

Proof state:
case intro.intro
a b : Nat
self : UnionFind
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin self.size},
    self.rootD ↑x = ↑x →
      self.rootD ↑y = ↑y →
        (∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i) →
          (m.Equiv a b ↔ self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b)
r : Fin self.size
ha : 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) →
    ((self.link x y yroot).Equiv a b ↔
      self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b)

Tactic:
rw [← rootD_eq_self] at xroot yroot

Result:
case intro.intro
a b : Nat
self : UnionFind
x y : Fin self.size
xroot : self.rootD ↑x = ↑x
yroot✝ : self.parent ↑y = ↑y
yroot : self.rootD ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin self.size},
    self.rootD ↑x = ↑x →
      self.rootD ↑y = ↑y →
        (∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i) →
          (m.Equiv a b ↔ self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b)
r : Fin self.size
ha : 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) →
    ((self.link x y yroot✝).Equiv a b ↔
      self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b)

Proof state:
case neg
a b : Nat
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
m : UnionFind
x y : Fin self.size
xroot : self.rootD ↑x = ↑x
yroot : self.rootD ↑y = ↑y
hm : ∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i
h1 : self.rootD a = ↑x
h2 : ¬self.rootD b = ↑x
⊢ (↑x = if self.rootD b = ↑y then ↑x else self.rootD b) ↔
    ↑x = self.rootD b ∨ ↑y = self.rootD b ∨ ↑x = ↑y ∧ ↑x = self.rootD b

Tactic:
simp [h2, Ne.symm h2]

Result:
case neg
a b : Nat
self : UnionFind
x✝ y✝ : Fin self.size
xroot✝ : self.parent ↑x✝ = ↑x✝
yroot✝ : self.parent ↑y✝ = ↑y✝
m : UnionFind
x y : Fin self.size
xroot : self.rootD ↑x = ↑x
yroot : self.rootD ↑y = ↑y
hm : ∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i
h1 : self.rootD a = ↑x
h2 : ¬self.rootD b = ↑x
⊢ (↑x = if self.rootD b = ↑y then ↑x else self.rootD b) ↔ ↑y = self.rootD b

Proof state:
a b : Nat
self : UnionFind
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin self.size},
    self.rootD ↑x = ↑x →
      self.rootD ↑y = ↑y →
        (∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i) →
          (m.Equiv a b ↔ self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b)
⊢ (self.link x y yroot).Equiv a b ↔
    self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b

Tactic:
obtain ⟨r, ha, hr⟩ := root_link xroot yroot

Result:
case intro.intro
a b : Nat
self : UnionFind
x y : Fin self.size
xroot : self.parent ↑x = ↑x
yroot : self.parent ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin self.size},
    self.rootD ↑x = ↑x →
      self.rootD ↑y = ↑y →
        (∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i) →
          (m.Equiv a b ↔ self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b)
r : Fin self.size
ha : r = x ∨ r = y
hr : ∀ (i : Nat), (self.link x y yroot).rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑r else self.rootD i
⊢ (self.link x y yroot).Equiv a b ↔
    self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b

Proof state:
case intro.intro.inr
a b : Nat
self : UnionFind
x : Fin self.size
xroot : self.rootD ↑x = ↑x
this :
  ∀ {m : UnionFind} {x y : Fin self.size},
    self.rootD ↑x = ↑x →
      self.rootD ↑y = ↑y →
        (∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i) →
          (m.Equiv a b ↔ self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b)
r : Fin self.size
yroot✝ : self.parent ↑r = ↑r
yroot : self.rootD ↑r = ↑r
⊢ (∀ (i : Nat), (self.link x r yroot✝).rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑r then ↑r else self.rootD i) →
    ((self.link x r yroot✝).Equiv a b ↔
      self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑r) b ∨ self.Equiv a ↑r ∧ self.Equiv (↑x) b)

Tactic:
simpa [or_comm, and_comm] using this yroot xroot

Result:
no goals

Proof state:
case intro.intro.inl
a b : Nat
self : UnionFind
y : Fin self.size
yroot✝ : self.parent ↑y = ↑y
yroot : self.rootD ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin self.size},
    self.rootD ↑x = ↑x →
      self.rootD ↑y = ↑y →
        (∀ (i : Nat), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i) →
          (m.Equiv a b ↔ self.Equiv a b ∨ self.Equiv a ↑x ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑x) b)
r : Fin self.size
xroot : self.rootD ↑r = ↑r
⊢ (∀ (i : Nat), (self.link r y yroot✝).rootD i = if self.rootD i = ↑r ∨ self.rootD i = ↑y then ↑r else self.rootD i) →
    ((self.link r y yroot✝).Equiv a b ↔
      self.Equiv a b ∨ self.Equiv a ↑r ∧ self.Equiv (↑y) b ∨ self.Equiv a ↑y ∧ self.Equiv (↑r) b)

Tactic:
exact this xroot yroot

Result:
no goals

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

Tactic:
simp [Equiv, hm, xroot, yroot]

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