internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.UnionFind.findAux_s
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (findAux self x).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank }
Tactic:
rw [findAux]
Proof state after:
self : UnionFind
x : Fin (size self)
⊢ (if h : (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        let_fun this := ⋯;
        match findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ } with
        | { s := arr₁, root := root, size_eq := H } =>
          { s := Array.modify arr₁ ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank }
Theorem: Lean4Lean.UnionFind.findAux_s
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ (if h : (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        let_fun this := ⋯;
        match findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ } with
        | { s := arr₁, root := root, size_eq := H } =>
          { s := Array.modify arr₁ ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank }
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.findAux_s
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ root self ↑x = ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root
Tactic:
rw [← root_parent, parent, parentD_eq]
Proof state after:
self : UnionFind
x : Fin (size self)
⊢ root self (Array.get self.arr x).parent = ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root
Theorem: Lean4Lean.UnionFind.findAux_s
Proof state before:
self : UnionFind
x : Fin (size self)
⊢ root self (Array.get self.arr x).parent = ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root
Tactic:
simp [findAux_root, root, parent'_lt]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
⊢ rankD (findAux self x).s i = rank self i
Tactic:
if h : i < self.size then
  rw [findAux_s]; split <;> [rfl; skip]
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
  have := lt_of_parentD (by rwa [parentD_eq])
  rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify (by rwa [FindAux.size_eq])]
  split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩)]
else
  simp [rank, rankD]; rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
⊢ rankD (findAux self x).s i = rank self i
Tactic:
rw [findAux_s]
Proof state after:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
⊢ rankD
      (if (Array.get self.arr x).parent = ↑x then self.arr
      else
        Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
⊢ rankD
      (if (Array.get self.arr x).parent = ↑x then self.arr
      else
        Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Tactic:
split <;> [rfl; 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
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Theorem: Lean4Lean.UnionFind.rankD_findAux
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
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self 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 : i < 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
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Theorem: Lean4Lean.UnionFind.rankD_findAux
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
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Tactic:
have := lt_of_parentD (by rwa [parentD_eq])
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
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Theorem: Lean4Lean.UnionFind.rankD_findAux
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
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ rankD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    rank self i
Tactic:
rw [rankD_eq' (by simp [FindAux.size_eq, h]), Array.get_modify (by rwa [FindAux.size_eq])]
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
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).rank =
    rank self i
Theorem: Lean4Lean.UnionFind.rankD_findAux
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
this✝ : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
this : ↑x < Array.size self.arr
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).rank =
    rank self i
Tactic:
split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt x⟩)]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < 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 ?m.115685 ?m.115686 ≠ ?m.115686
Tactic:
rwa [parentD_eq]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < 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
this : ↑x < Array.size self.arr
⊢ 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:
simp [FindAux.size_eq, h]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < 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
this : ↑x < Array.size self.arr
⊢ i < Array.size (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
Tactic:
rwa [FindAux.size_eq]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬i < size self
⊢ rankD (findAux self x).s i = rank self i
Tactic:
simp [rank, rankD]
Proof state after:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬i < size self
⊢ (if h : i < Array.size (findAux self x).s then (Array.get (findAux self x).s { val := i, isLt := h }).rank else 0) =
    if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬i < size self
⊢ (if h : i < Array.size (findAux self x).s then (Array.get (findAux self x).s { val := i, isLt := h }).rank else 0) =
    if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0
Tactic:
rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬i < size self
⊢ ¬i < Array.size (findAux self x).s
Tactic:
rwa [FindAux.size_eq]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
⊢ parentD (findAux self x).s i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [findAux_s]
Proof state after:
i : Nat
self : UnionFind
x : Fin (size self)
⊢ parentD
      (if (Array.get self.arr x).parent = ↑x then self.arr
      else
        Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
      i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
⊢ parentD
      (if (Array.get self.arr x).parent = ↑x then self.arr
      else
        Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
      i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
split <;> [split; skip]
Proof state after:
case inl.inl
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : i = ↑x
⊢ parentD self.arr i = root self ↑x

case inl.inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i = parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

case inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inl.inl
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : i = ↑x
⊢ parentD self.arr i = root self ↑x
Tactic:
subst i
Proof state after:
case inl.inl
self : UnionFind
x : Fin (size self)
h✝ : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr ↑x = root self ↑x
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inl.inl
self : UnionFind
x : Fin (size self)
h✝ : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr ↑x = root self ↑x
Tactic:
rw [root_eq_self.2 _] <;> simp [parentD_eq, *]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inl.inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i = parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [findAux_s]
Proof state after:
case inl.inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i =
    parentD
      (if
          (Array.get self.arr { val := (Array.get self.arr x).parent, isLt := ⋯ }).parent =
            ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ } then
        self.arr
      else
        Array.modify
          (findAux self
              { val := (Array.get self.arr { val := (Array.get self.arr x).parent, isLt := ⋯ }).parent, isLt := ⋯ }).s
          ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ } fun s =>
          { parent := root self ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ }, rank := s.rank })
      i
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inl.inr
i : Nat
self : UnionFind
x : Fin (size self)
h✝¹ : (Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD self.arr i =
    parentD
      (if
          (Array.get self.arr { val := (Array.get self.arr x).parent, isLt := ⋯ }).parent =
            ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ } then
        self.arr
      else
        Array.modify
          (findAux self
              { val := (Array.get self.arr { val := (Array.get self.arr x).parent, isLt := ⋯ }).parent, isLt := ⋯ }).s
          ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ } fun s =>
          { parent := root self ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ }, rank := s.rank })
      i
Tactic:
simp [*]
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
⊢ parentD
      (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank })
      i =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [parentD]
Proof state after:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ (if 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 }) then
      (Array.get
          (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
            { parent := root self ↑x, rank := s.rank })
          { val := i, isLt := h }).parent
    else i) =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
i : Nat
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ (if 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 }) then
      (Array.get
          (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
            { parent := root self ↑x, rank := s.rank })
          { val := i, isLt := h }).parent
    else i) =
    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'
Proof state after:
case inl
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 })
⊢ (Array.get
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
        { val := i, isLt := h' }).parent =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i

case inr
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 = if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inl
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 })
⊢ (Array.get
        (Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
          { parent := root self ↑x, rank := s.rank })
        { val := i, isLt := h' }).parent =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [Array.get_modify (by simpa using h')]
Proof state after:
case inl
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 })
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).parent =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inl
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 })
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).parent =
    if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
simp [@eq_comm _ i]
Proof state after:
case inl
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 })
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).parent =
    if ↑x = i then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inl
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 })
⊢ (if ↑x = i then
        { parent := root self ↑x,
          rank :=
            (Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
                { val := i, isLt := ⋯ }).rank }
      else
        Array.get (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s { val := i, isLt := ⋯ }).parent =
    if ↑x = i then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
split <;> simp [← parentD_eq]
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 < 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:
case inr
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 = if i = ↑x then root self ↑x else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
Proof state after:
case inr
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 = parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Theorem: Lean4Lean.UnionFind.parentD_findAux
Proof state before:
case inr
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 = parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i
Tactic:
rw [parentD, dif_neg]
Proof state after:
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