internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
⊢ root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
have _ := Nat.sub_lt_sub_left (m.lt_rankMax i) (m.rank_lt h)
Proof state after:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [← root_parent, go (m.parent i)]
Proof state after:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ (if root self (parent m i) = ↑x ∨ root self (parent m i) = ↑y then ↑x else root self (parent m i)) =
    if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ (if root self (parent m i) = ↑x ∨ root self (parent m i) = ↑y then ↑x else root self (parent m i)) =
    if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [hm i]
Proof state after:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ (if root self (if ↑y = i then ↑x else parent self i) = ↑x ∨ root self (if ↑y = i then ↑x else parent self i) = ↑y then
      ↑x
    else root self (if ↑y = i then ↑x else parent self i)) =
    if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : ¬parent m i = i
x✝ : rankMax m - rank m (parent m i) < rankMax m - rank m i
⊢ (if root self (if ↑y = i then ↑x else parent self i) = ↑x ∨ root self (if ↑y = i then ↑x else parent self i) = ↑y then
      ↑x
    else root self (if ↑y = i then ↑x else parent self i)) =
    if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
split <;> [subst i; rw [root_parent]]
Proof state after:
case inl
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
h : ¬parent m ↑y = ↑y
x✝ : rankMax m - rank m (parent m ↑y) < rankMax m - rank m ↑y
⊢ (if root self ↑x = ↑x ∨ root self ↑x = ↑y then ↑x else root self ↑x) =
    if root self ↑y = ↑x ∨ root self ↑y = ↑y then ↑x else root self ↑y
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
case inl
self : UnionFind
x✝¹ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝¹ = ↑x✝¹
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝¹ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
h : ¬parent m ↑y = ↑y
x✝ : rankMax m - rank m (parent m ↑y) < rankMax m - rank m ↑y
⊢ (if root self ↑x = ↑x ∨ root self ↑x = ↑y then ↑x else root self ↑x) =
    if root self ↑y = ↑x ∨ root self ↑y = ↑y then ↑x else root self ↑y
Tactic:
simp [root_eq_self.2 xroot, root_eq_self.2 yroot]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
hr : rank self ↑y < rank self ↑x
⊢ ∃ r,
    (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
Tactic:
exact this xroot yroot fun i => by simp [parent_link, h, hr]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
hr : rank self ↑y < rank self ↑x
i : Nat
⊢ parent (link self x y yroot) i = if ↑y = i then ↑x else parent self i
Tactic:
simp [parent_link, h, hr]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
hr : ¬rank self ↑y < rank self ↑x
⊢ ∃ r,
    (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
Tactic:
simpa (config := {singlePass := true}) [or_comm] using
  this yroot xroot fun i => by simp [parent_link, h, hr]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
hr : ¬rank self ↑y < rank self ↑x
i : Nat
⊢ parent (link self x y yroot) i = if ↑x = i then ↑y else parent self i
Tactic:
simp [parent_link, h, hr]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_empty
Proof state before:
a b : Nat
⊢ Equiv empty a b ↔ a = b
Tactic:
simp [Equiv]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_push
Proof state before:
a b : Nat
self : UnionFind
⊢ Equiv (push self) a b ↔ Equiv self a b
Tactic:
simp [Equiv]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_root
Proof state before:
self : UnionFind
a : Nat
⊢ Equiv self (root self a) a
Tactic:
simp [Equiv, root_root]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_root_l
Proof state before:
self : UnionFind
a b : Nat
⊢ Equiv self (root self a) b ↔ Equiv self a b
Tactic:
simp [Equiv, root_root]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_root_r
Proof state before:
self : UnionFind
a b : Nat
⊢ Equiv self a (root self b) ↔ Equiv self a b
Tactic:
simp [Equiv, root_root]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_find
Proof state before:
a b : Nat
self : UnionFind
x : Fin (size self)
⊢ Equiv (find self x).fst a b ↔ Equiv self a b
Tactic:
simp [Equiv, find_root_1]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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
Proof 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
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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
Proof 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)
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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
Proof 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)
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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
Proof 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)
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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]
Proof 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
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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]
Proof 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
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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]
Proof 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
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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), *]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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), *]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_link
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_union
Proof state before:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv (union self x y) a b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b
Tactic:
simp [union]
Proof state after:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv
      (link (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst { val := root self ↑x, isLt := ⋯ }
        (find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val ⋯)
      a b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b