internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inr.hnc
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ ¬i < Array.size (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
Tactic:
simpa using h'
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ i = ↑x →
    i <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
Tactic:
rintro rfl
Proof state after:
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬↑x <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ ↑x <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
h' :
  ¬↑x <
      Array.size
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
⊢ ↑x <
    Array.size
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
Tactic:
simp [FindAux.size_eq]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux_root
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ parentD (findAux self x).s (root self ↑x) = root self ↑x
Tactic:
rw [parentD_findAux]
Proof state after:
self : UnionFind
x : Fin (size self)
⊢ (if root self ↑x = ↑x then root self ↑x
    else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x)) =
    root self ↑x
Theorem: Lean4Lean.UnionFind.parentD_findAux_root
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (if root self ↑x = ↑x then root self ↑x
    else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x)) =
    root self ↑x
Tactic:
split <;> [rfl; rename_i h]
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
h : ¬root self ↑x = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
Theorem: Lean4Lean.UnionFind.parentD_findAux_root
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
h : ¬root self ↑x = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
Tactic:
rw [root_eq_self, parent, parentD_eq] at h
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
Theorem: Lean4Lean.UnionFind.parentD_findAux_root
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
Theorem: Lean4Lean.UnionFind.parentD_findAux_root
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
Tactic:
rw [← root_parent, parent, parentD_eq]
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
      (root self (Array.get self.arr x).parent) =
    root self (Array.get self.arr x).parent
Theorem: Lean4Lean.UnionFind.parentD_findAux_root
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
      (root self (Array.get self.arr x).parent) =
    root self (Array.get self.arr x).parent
Tactic:
exact parentD_findAux_root (x := ⟨_, self.parent'_lt x⟩)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux_lt
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
⊢ parentD (findAux self x).s i < size self
Tactic:
if h' : (self.arr.get x).parent = x then
  rw [findAux_s, if_pos h']; apply self.parentD_lt h
else
  rw [parentD_findAux]; split <;> [simp [root_lt]; skip]
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
  apply parentD_findAux_lt h
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux_lt
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self x).s i < size self
Tactic:
rw [findAux_s, if_pos h']
Proof state after:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i < size self
Theorem: Lean4Lean.UnionFind.parentD_findAux_lt
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i < size self
Tactic:
apply self.parentD_lt h
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux_lt
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self x).s i < size self
Tactic:
rw [parentD_findAux]
Proof state after:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ (if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i) <
    size self
Theorem: Lean4Lean.UnionFind.parentD_findAux_lt
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ (if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i) <
    size self
Tactic:
split <;> [simp [root_lt]; skip]
Proof state after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i < size self
Theorem: Lean4Lean.UnionFind.parentD_findAux_lt
Proof state before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i < size self
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
Proof state after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i < size self
Theorem: Lean4Lean.UnionFind.parentD_findAux_lt
Proof state before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i < size self
Tactic:
apply parentD_findAux_lt h
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux_or
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
⊢ parentD (findAux self x).s i = root self i ∧ root self i = root self ↑x ∨ parentD (findAux self x).s i = parent self i
Tactic:
if h' : (self.arr.get x).parent = x then
  rw [findAux_s, if_pos h']; exact .inr rfl
else
  rw [parentD_findAux]; split <;> [simp [*]; skip]
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
  exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
    simp [h, ← parentD_eq, root_parent]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux_or
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self x).s i = root self i ∧ root self i = root self ↑x ∨ parentD (findAux self x).s i = parent self i
Tactic:
rw [findAux_s, if_pos h']
Proof state after:
self : UnionFind
x : Fin (size self)
i : Nat
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i = root self i ∧ root self i = root self ↑x ∨ parentD self.arr i = parent self i
Theorem: Lean4Lean.UnionFind.parentD_findAux_or
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i = root self i ∧ root self i = root self ↑x ∨ parentD self.arr i = parent self i
Tactic:
exact .inr rfl
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux_or
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self x).s i = root self i ∧ root self i = root self ↑x ∨ parentD (findAux self x).s i = parent self i
Tactic:
rw [parentD_findAux]
Proof state after:
self : UnionFind
x : Fin (size self)
i : Nat
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ (if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i) =
        root self i ∧
      root self i = root self ↑x ∨
    (if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i) =
      parent self i
Theorem: Lean4Lean.UnionFind.parentD_findAux_or
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ (if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i) =
        root self i ∧
      root self i = root self ↑x ∨
    (if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i) =
      parent self i
Tactic:
split <;> [simp [*]; skip]
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = root self i ∧
      root self i = root self ↑x ∨
    parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = parent self i
Theorem: Lean4Lean.UnionFind.parentD_findAux_or
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = root self i ∧
      root self i = root self ↑x ∨
    parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = parent self i
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
Proof state after:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = root self i ∧
      root self i = root self ↑x ∨
    parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = parent self i
Theorem: Lean4Lean.UnionFind.parentD_findAux_or
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = root self i ∧
      root self i = root self ↑x ∨
    parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = parent self i
Tactic:
exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
  simp [h, ← parentD_eq, root_parent]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux_or
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
h : root self i = root self ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ }
⊢ root self i = root self ↑x
Tactic:
simp [h, ← parentD_eq, root_parent]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.lt_rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self x).s i ≠ i → rank self i < rank self (parentD (findAux self x).s i)
Tactic:
rw [findAux_s, if_pos h']
Proof state after:
i : Nat
self : UnionFind
x : Fin (size self)
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i ≠ i → rank self i < rank self (parentD self.arr i)
Theorem: Lean4Lean.UnionFind.lt_rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i ≠ i → rank self i < rank self (parentD self.arr i)
Tactic:
apply self.rank_lt
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.lt_rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self x).s i ≠ i → rank self i < rank self (parentD (findAux self x).s i)
Tactic:
rw [parentD_findAux]
Proof state after:
i : Nat
self : UnionFind
x : Fin (size self)
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ (if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i) ≠
      i →
    rank self i <
      rank self
        (if i = ↑x then root self ↑x
        else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i)
Theorem: Lean4Lean.UnionFind.lt_rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h' : ¬(Array.get self.arr x).parent = ↑x
⊢ (if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i) ≠
      i →
    rank self i <
      rank self
        (if i = ↑x then root self ↑x
        else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i)
Tactic:
split <;> rename_i h <;> intro h'
Proof state after:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : i = ↑x
h' : root self ↑x ≠ i
⊢ rank self i < rank self (root self ↑x)

case inr
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : ¬i = ↑x
h' : parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i ≠ i
⊢ rank self i < rank self (parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i)
Theorem: Lean4Lean.UnionFind.lt_rankD_findAux
Proof state before:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : i = ↑x
h' : root self ↑x ≠ i
⊢ rank self i < rank self (root self ↑x)
Tactic:
subst i
Proof state after:
case inl
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h' : root self ↑x ≠ ↑x
⊢ rank self ↑x < rank self (root self ↑x)
Theorem: Lean4Lean.UnionFind.lt_rankD_findAux
Proof state before:
case inl
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h' : root self ↑x ≠ ↑x
⊢ rank self ↑x < rank self (root self ↑x)
Tactic:
rwa [lt_rank_root, Ne, ← root_eq_self]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.lt_rankD_findAux
Proof state before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : ¬i = ↑x
h' : parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i ≠ i
⊢ rank self i < rank self (parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i)
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
Proof state after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : ¬i = ↑x
h' : parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i ≠ i
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ rank self i < rank self (parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i)
Theorem: Lean4Lean.UnionFind.lt_rankD_findAux
Proof state before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : ¬i = ↑x
h' : parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i ≠ i
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ rank self i < rank self (parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i)
Tactic:
apply lt_rankD_findAux h'
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.find_size
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ size (find self x).fst = size self
Tactic:
simp [find, size, FindAux.size_eq]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.find_root_2
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ ↑(find self x).snd.val = root self ↑x
Tactic:
simp [find, findAux_root, root]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.find_parent_1
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ parent (find self x).fst ↑x = root self ↑x
Tactic:
simp [find, parent]
Proof state after:
self : UnionFind
x : Fin (size self)
⊢ parentD (findAux self x).s ↑x = root self ↑x
Theorem: Lean4Lean.UnionFind.find_parent_1
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ parentD (findAux self x).s ↑x = root self ↑x
Tactic:
rw [parentD_findAux, if_pos rfl]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h : parent (find self x).fst i = i
⊢ root (find self x).fst i = root self i
Tactic:
rw [root_eq_self.2 h]
Proof state after:
self : UnionFind
x : Fin (size self)
i : Nat
h : parent (find self x).fst i = i
⊢ i = root self i
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h : parent (find self x).fst i = i
⊢ i = root self i
Tactic:
obtain ⟨h1, _⟩ | h1 := find_parent_or self x i <;> rw [h1] at h
Proof state after:
case inl.intro
self : UnionFind
x : Fin (size self)
i : Nat
h : root self i = i
h1 : parent (find self x).fst i = root self i
right✝ : root self i = root self ↑x
⊢ i = root self i

case inr
self : UnionFind
x : Fin (size self)
i : Nat
h : parent self i = i
h1 : parent (find self x).fst i = parent self i
⊢ i = root self i
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
case inl.intro
self : UnionFind
x : Fin (size self)
i : Nat
h : root self i = i
h1 : parent (find self x).fst i = root self i
right✝ : root self i = root self ↑x
⊢ i = root self i
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
h : parent self i = i
h1 : parent (find self x).fst i = parent self i
⊢ i = root self i
Tactic:
rw [root_eq_self.2 h]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
⊢ root (find self x).fst i = root self i
Tactic:
have := Nat.sub_lt_sub_left ((self.find x).1.lt_rankMax _) ((self.find x).1.rank_lt h)
Proof state after:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ root (find self x).fst i = root self i
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ root (find self x).fst i = root self i
Tactic:
rw [← root_parent, find_root_1 self x ((self.find x).1.parent i)]
Proof state after:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ root self (parent (find self x).fst i) = root self i
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ root self (parent (find self x).fst i) = root self i
Tactic:
obtain ⟨h1, _⟩ | h1 := find_parent_or self x i
Proof state after:
case inl.intro
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
h1 : parent (find self x).fst i = root self i
right✝ : root self i = root self ↑x
⊢ root self (parent (find self x).fst i) = root self i

case inr
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
h1 : parent (find self x).fst i = parent self i
⊢ root self (parent (find self x).fst i) = root self i
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
case inl.intro
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
h1 : parent (find self x).fst i = root self i
right✝ : root self i = root self ↑x
⊢ root self (parent (find self x).fst i) = root self i
Tactic:
rw [h1, root_root]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
h1 : parent (find self x).fst i = parent self i
⊢ root self (parent (find self x).fst i) = root self i
Tactic:
rw [h1, root_parent]
Proof state after:
no goals