Theorem: Lean4Lean.UnionFind.equiv_link (Lean4Lean/Verify/UnionFind.lean)

State before:
a b : Nat
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin (size self)},
    root self ↑x = ↑x →
      root self ↑y = ↑y →
        (∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i) →
          (Equiv m a b ↔ Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b)
⊢ 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
Tactic:
obtain ⟨r, ha, hr⟩ := root_link xroot yroot
State after:
case intro.intro
a b : Nat
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin (size self)},
    root self ↑x = ↑x →
      root self ↑y = ↑y →
        (∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i) →
          (Equiv m a b ↔ Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b)
r : Fin (size self)
ha : r = x ∨ r = y
hr : ∀ (i : Nat), root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
⊢ 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

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

State before:
case intro.intro
a b : Nat
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin (size self)},
    root self ↑x = ↑x →
      root self ↑y = ↑y →
        (∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i) →
          (Equiv m a b ↔ Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b)
r : Fin (size self)
ha : r = x ∨ r = y
⊢ (∀ (i : Nat), root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i) →
    (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)
Tactic:
rw [← root_eq_self] at xroot yroot
State after:
case intro.intro
a b : Nat
self : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot✝ : parent self ↑y = ↑y
yroot : root self ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin (size self)},
    root self ↑x = ↑x →
      root self ↑y = ↑y →
        (∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i) →
          (Equiv m a b ↔ Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b)
r : Fin (size self)
ha : r = x ∨ r = y
⊢ (∀ (i : Nat), root (link self x y yroot✝) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i) →
    (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)

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

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

State before:
a b : Nat
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
m : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot : root self ↑y = ↑y
hm : ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
⊢ Equiv m a b ↔ Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b
Tactic:
simp [Equiv, hm, xroot, yroot]
State after:
a b : Nat
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
m : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot : root self ↑y = ↑y
hm : ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
⊢ ((if root self a = ↑x ∨ root self a = ↑y then ↑x else root self a) =
      if root self b = ↑x ∨ root self b = ↑y then ↑x else root self b) ↔
    root self a = root self b ∨ root self a = ↑x ∧ ↑y = root self b ∨ root self a = ↑y ∧ ↑x = root self b

State before:
a b : Nat
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
m : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot : root self ↑y = ↑y
hm : ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
⊢ ((if root self a = ↑x ∨ root self a = ↑y then ↑x else root self a) =
      if root self b = ↑x ∨ root self b = ↑y then ↑x else root self b) ↔
    root self a = root self b ∨ root self a = ↑x ∧ ↑y = root self b ∨ root self a = ↑y ∧ ↑x = root self b
Tactic:
by_cases h1 : root self a = x <;> by_cases h2 : root self b = x <;>
  simp [h1, h2, imp_false, Decidable.not_not]
State after:
case neg
a b : Nat
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
m : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot : root self ↑y = ↑y
hm : ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
h1 : root self a = ↑x
h2 : ¬root self b = ↑x
⊢ (↑x = if root self b = ↑y then ↑x else root self b) ↔ ↑x = root self b ∨ ↑y = root self b ∨ ↑x = ↑y ∧ ↑x = root self b

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

State before:
case neg
a b : Nat
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
m : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot : root self ↑y = ↑y
hm : ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
h1 : root self a = ↑x
h2 : ¬root self b = ↑x
⊢ (↑x = if root self b = ↑y then ↑x else root self b) ↔ ↑x = root self b ∨ ↑y = root self b ∨ ↑x = ↑y ∧ ↑x = root self b
Tactic:
simp [h2, Ne.symm h2]
State after:
case neg
a b : Nat
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
m : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot : root self ↑y = ↑y
hm : ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
h1 : root self a = ↑x
h2 : ¬root self b = ↑x
⊢ (↑x = if root self b = ↑y then ↑x else root self b) ↔ ↑y = root self b

State before:
case neg
a b : Nat
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
m : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot : root self ↑y = ↑y
hm : ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
h1 : root self a = ↑x
h2 : ¬root self b = ↑x
⊢ (↑x = if root self b = ↑y then ↑x else root self b) ↔ ↑y = root self b
Tactic:
split <;> simp [@eq_comm _ _ (root self b), *]
State after:
no goals

State before:
case neg
a b : Nat
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
m : UnionFind
x y : Fin (size self)
xroot : root self ↑x = ↑x
yroot : root self ↑y = ↑y
hm : ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
h1 : ¬root self a = ↑x
h2 : ¬root self b = ↑x
⊢ ((if root self a = ↑y then ↑x else root self a) = if root self b = ↑y then ↑x else root self b) ↔
    root self a = root self b ∨ root self a = ↑y ∧ ↑x = root self b
Tactic:
by_cases h1 : root self a = y <;> by_cases h2 : root self b = y <;>
  simp [h1, h2, @eq_comm _ _ (root self b), *]
State after:
no goals

State before:
case intro.intro.inl
a b : Nat
self : UnionFind
y : Fin (size self)
yroot✝ : parent self ↑y = ↑y
yroot : root self ↑y = ↑y
this :
  ∀ {m : UnionFind} {x y : Fin (size self)},
    root self ↑x = ↑x →
      root self ↑y = ↑y →
        (∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i) →
          (Equiv m a b ↔ Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b)
r : Fin (size self)
xroot : root self ↑r = ↑r
⊢ (∀ (i : Nat), root (link self r y yroot✝) i = if root self i = ↑r ∨ root self i = ↑y then ↑r else root self i) →
    (Equiv (link self r y yroot✝) a b ↔
      Equiv self a b ∨ Equiv self a ↑r ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑r) b)
Tactic:
exact this xroot yroot
State after:
no goals

State before:
case intro.intro.inr
a b : Nat
self : UnionFind
x : Fin (size self)
xroot : root self ↑x = ↑x
this :
  ∀ {m : UnionFind} {x y : Fin (size self)},
    root self ↑x = ↑x →
      root self ↑y = ↑y →
        (∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i) →
          (Equiv m a b ↔ Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b)
r : Fin (size self)
yroot✝ : parent self ↑r = ↑r
yroot : root self ↑r = ↑r
⊢ (∀ (i : Nat), root (link self x r yroot✝) i = if root self i = ↑x ∨ root self i = ↑r then ↑r else root self i) →
    (Equiv (link self x r yroot✝) a b ↔
      Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑r) b ∨ Equiv self a ↑r ∧ Equiv self (↑x) b)
Tactic:
simpa [or_comm, and_comm] using this yroot xroot
State after:
no goals