[GOAL]
n : ℕ
m : UFModel n
k : ℕ
le : n ≤ k
i : Fin k
⊢ ↑((fun i =>
            if h : ↑i < n then
              match parent m { val := ↑i, isLt := h } with
              | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
            else i)
          i) ≠
      ↑i →
    (fun i => if i < n then rank m i else 0) ↑i <
      (fun i => if i < n then rank m i else 0)
        ↑((fun i =>
              if h : ↑i < n then
                match parent m { val := ↑i, isLt := h } with
                | { val := a, isLt := h' } => { val := a, isLt := (_ : a < k) }
              else i)
            i)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
m : UFModel n
k : ℕ
le : n ≤ k
i : Fin k
⊢ ¬↑(if h : ↑i < n then
            { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
          else i) =
        ↑i →
    (if ↑i < n then rank m ↑i else 0) <
      if
          ↑(if h : ↑i < n then
                { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
                  isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
              else i) <
            n then
        rank m
          ↑(if h : ↑i < n then
              { val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
                isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
            else i)
      else 0
[PROOFSTEP]
split
[GOAL]
case inl
n : ℕ
m : UFModel n
k : ℕ
le : n ≤ k
i : Fin k
h✝ : ↑i < n
⊢ ¬↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } =
        ↑i →
    rank m ↑i <
      if
          ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
                isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } <
            n then
        rank m
          ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
      else 0
[PROOFSTEP]
rename_i h
[GOAL]
case inr
n : ℕ
m : UFModel n
k : ℕ
le : n ≤ k
i : Fin k
h✝ : ¬↑i < n
⊢ ¬↑i = ↑i → 0 < 0
[PROOFSTEP]
rename_i h
[GOAL]
case inl
n : ℕ
m : UFModel n
k : ℕ
le : n ≤ k
i : Fin k
h : ↑i < n
⊢ ¬↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
            isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } =
        ↑i →
    rank m ↑i <
      if
          ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
                isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) } <
            n then
        rank m
          ↑{ val := ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }),
              isLt := (_ : ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) < k) }
      else 0
[PROOFSTEP]
simp [(m.parent ⟨i, h⟩).2, h]
[GOAL]
case inl
n : ℕ
m : UFModel n
k : ℕ
le : n ≤ k
i : Fin k
h : ↑i < n
⊢ ¬↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) }) = ↑i → rank m ↑i < rank m ↑(m.1 { val := ↑i, isLt := (_ : ↑i < n) })
[PROOFSTEP]
exact m.rank_lt _
[GOAL]
case inr
n : ℕ
m : UFModel n
k : ℕ
le : n ≤ k
i : Fin k
h : ¬↑i < n
⊢ ¬↑i = ↑i → 0 < 0
[PROOFSTEP]
intro .
[GOAL]
case inr
n : ℕ
m : UFModel n
k : ℕ
le : n ≤ k
i : Fin k
h : ¬↑i < n
⊢ ¬↑i = ↑i → 0 < 0
[PROOFSTEP]
intro.
[GOAL]
n : ℕ
m : UFModel n
x y : Fin n
h : rank m ↑x < rank m ↑y
i : Fin n
⊢ ↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
    rank m ↑i < rank m ↑((fun i => if ↑x = ↑i then y else parent m i) i)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
m : UFModel n
x y : Fin n
h : rank m ↑x < rank m ↑y
i : Fin n
⊢ ¬↑(if ↑x = ↑i then y else parent m i) = ↑i → rank m ↑i < rank m ↑(if ↑x = ↑i then y else parent m i)
[PROOFSTEP]
split
[GOAL]
case inl
n : ℕ
m : UFModel n
x y : Fin n
h : rank m ↑x < rank m ↑y
i : Fin n
h✝ : ↑x = ↑i
⊢ ¬↑y = ↑i → rank m ↑i < rank m ↑y
[PROOFSTEP]
rename_i h'
[GOAL]
case inr
n : ℕ
m : UFModel n
x y : Fin n
h : rank m ↑x < rank m ↑y
i : Fin n
h✝ : ¬↑x = ↑i
⊢ ¬↑(parent m i) = ↑i → rank m ↑i < rank m ↑(parent m i)
[PROOFSTEP]
rename_i h'
[GOAL]
case inl
n : ℕ
m : UFModel n
x y : Fin n
h : rank m ↑x < rank m ↑y
i : Fin n
h' : ↑x = ↑i
⊢ ¬↑y = ↑i → rank m ↑i < rank m ↑y
[PROOFSTEP]
rw [← h']
[GOAL]
case inl
n : ℕ
m : UFModel n
x y : Fin n
h : rank m ↑x < rank m ↑y
i : Fin n
h' : ↑x = ↑i
⊢ ¬↑y = ↑x → rank m ↑x < rank m ↑y
[PROOFSTEP]
exact fun _ ↦ h
[GOAL]
case inr
n : ℕ
m : UFModel n
x y : Fin n
h : rank m ↑x < rank m ↑y
i : Fin n
h' : ¬↑x = ↑i
⊢ ¬↑(parent m i) = ↑i → rank m ↑i < rank m ↑(parent m i)
[PROOFSTEP]
exact m.rank_lt i
[GOAL]
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
⊢ ↑((fun i => if ↑x = ↑i then y else parent m i) i) ≠ ↑i →
    (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i) ↑i <
      (fun i => if ↑y = i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m i)
        ↑((fun i => if ↑x = ↑i then y else parent m i) i)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
⊢ ¬↑(if ↑x = ↑i then y else parent m i) = ↑i →
    (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if ↑y = ↑(if ↑x = ↑i then y else parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1
      else rank m ↑(if ↑x = ↑i then y else parent m i)
[PROOFSTEP]
split
[GOAL]
case inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h✝ : ↑x = ↑i
⊢ ¬↑y = ↑i →
    (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if ↑y = ↑y ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
rename_i h₁
[GOAL]
case inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
⊢ ¬↑y = ↑i →
    (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if ↑y = ↑y ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
try simp [h₁]
[GOAL]
case inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
⊢ ¬↑y = ↑i →
    (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if ↑y = ↑y ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
simp [h₁]
[GOAL]
case inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
⊢ ¬↑y = ↑i →
    (if ↑y = ↑i ∧ rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
split
[GOAL]
case inl.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h✝ : ↑y = ↑i ∧ rank m ↑i = rank m ↑y
⊢ ¬↑y = ↑i → rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
rename_i h₂
[GOAL]
case inl.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h✝ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
⊢ ¬↑y = ↑i → rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
rename_i h₂
[GOAL]
case inl.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ↑y = ↑i ∧ rank m ↑i = rank m ↑y
⊢ ¬↑y = ↑i → rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
intro h
[GOAL]
case inl.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ↑y = ↑i ∧ rank m ↑i = rank m ↑y
h : ¬↑y = ↑i
⊢ rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
try simp [h] at h₂  <;> simp [h₁, h₂, h]
[GOAL]
case inl.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ↑y = ↑i ∧ rank m ↑i = rank m ↑y
h : ¬↑y = ↑i
⊢ rank m ↑y + 1 < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
simp [h] at h₂
[GOAL]
case inl.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
⊢ ¬↑y = ↑i → rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
intro h
[GOAL]
case inl.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
⊢ rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
try simp [h] at h₂  <;> simp [h₁, h₂, h]
[GOAL]
case inl.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
⊢ rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
simp [h] at h₂
[GOAL]
case inl.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h : ¬↑y = ↑i
h₂ : True
⊢ rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
simp [h₁, h₂, h]
[GOAL]
case inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h✝ : ¬↑x = ↑i
⊢ ¬↑(parent m i) = ↑i →
    (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
rename_i h₁
[GOAL]
case inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
⊢ ¬↑(parent m i) = ↑i →
    (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
try simp [h₁]
[GOAL]
case inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
⊢ ¬↑(parent m i) = ↑i →
    (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
simp [h₁]
[GOAL]
case inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
⊢ ¬↑(parent m i) = ↑i →
    (if ↑y = ↑i ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑i) <
      if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
split
[GOAL]
case inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h✝ : ↑y = ↑i ∧ rank m ↑x = rank m ↑y
⊢ ¬↑(parent m i) = ↑i →
    rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
rename_i h₂
[GOAL]
case inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h✝ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
⊢ ¬↑(parent m i) = ↑i →
    rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
rename_i h₂
[GOAL]
case inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ↑y = ↑i ∧ rank m ↑x = rank m ↑y
⊢ ¬↑(parent m i) = ↑i →
    rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
intro h
[GOAL]
case inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ↑y = ↑i ∧ rank m ↑x = rank m ↑y
h : ¬↑(parent m i) = ↑i
⊢ rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
try simp [h] at h₂  <;> simp [h₁, h₂, h]
[GOAL]
case inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ↑y = ↑i ∧ rank m ↑x = rank m ↑y
h : ¬↑(parent m i) = ↑i
⊢ rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
simp [h] at h₂
[GOAL]
case inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
⊢ ¬↑(parent m i) = ↑i →
    rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
intro h
[GOAL]
case inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
⊢ rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
try simp [h] at h₂  <;> simp [h₁, h₂, h]
[GOAL]
case inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
⊢ rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
simp [h] at h₂
[GOAL]
case inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h : ¬↑(parent m i) = ↑i
h₂ : ↑y = ↑i → ¬rank m ↑x = rank m ↑y
⊢ rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
simp [h₁, h₂, h]
[GOAL]
case inl.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
⊢ rank m ↑i < if rank m ↑i = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
simp [← h₁]
[GOAL]
case inl.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
⊢ rank m ↑x < if rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑y
[PROOFSTEP]
split
[GOAL]
case inl.inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
h✝ : rank m ↑x = rank m ↑y
⊢ rank m ↑x < rank m ↑y + 1
[PROOFSTEP]
rename_i h₃
[GOAL]
case inl.inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
h✝ : ¬rank m ↑x = rank m ↑y
⊢ rank m ↑x < rank m ↑y
[PROOFSTEP]
rename_i h₃
[GOAL]
case inl.inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
h₃ : rank m ↑x = rank m ↑y
⊢ rank m ↑x < rank m ↑y + 1
[PROOFSTEP]
rw [h₃]
[GOAL]
case inl.inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
h₃ : rank m ↑x = rank m ↑y
⊢ rank m ↑y < rank m ↑y + 1
[PROOFSTEP]
apply Nat.lt_succ_self
[GOAL]
case inl.inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑i = rank m ↑y)
h : ¬↑y = ↑i
h₃ : ¬rank m ↑x = rank m ↑y
⊢ rank m ↑x < rank m ↑y
[PROOFSTEP]
exact lt_of_le_of_ne H h₃
[GOAL]
case inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ↑y = ↑i ∧ rank m ↑x = rank m ↑y
h : ¬↑(parent m i) = ↑i
⊢ rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
have := Fin.eq_of_val_eq h₂.1
[GOAL]
case inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ↑y = ↑i ∧ rank m ↑x = rank m ↑y
h : ¬↑(parent m i) = ↑i
this : y = i
⊢ rank m ↑y + 1 < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
subst this
[GOAL]
case inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
h₁ : ¬↑x = ↑y
h₂ : ↑y = ↑y ∧ rank m ↑x = rank m ↑y
h : ¬↑(parent m y) = ↑y
⊢ rank m ↑y + 1 < if ↑y = ↑(parent m y) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m y)
[PROOFSTEP]
simp [hroot] at h
[GOAL]
case inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
⊢ rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
have := m.rank_lt i h
[GOAL]
case inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
this : rank m ↑i < rank m ↑(parent m i)
⊢ rank m ↑i < if ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y then rank m ↑y + 1 else rank m ↑(parent m i)
[PROOFSTEP]
split
[GOAL]
case inr.inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
this : rank m ↑i < rank m ↑(parent m i)
h✝ : ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y
⊢ rank m ↑i < rank m ↑y + 1
[PROOFSTEP]
rename_i h₃
[GOAL]
case inr.inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
this : rank m ↑i < rank m ↑(parent m i)
h✝ : ¬(↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y)
⊢ rank m ↑i < rank m ↑(parent m i)
[PROOFSTEP]
rename_i h₃
[GOAL]
case inr.inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
this : rank m ↑i < rank m ↑(parent m i)
h₃ : ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y
⊢ rank m ↑i < rank m ↑y + 1
[PROOFSTEP]
rw [h₃.1]
[GOAL]
case inr.inr.inl
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
this : rank m ↑i < rank m ↑(parent m i)
h₃ : ↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y
⊢ rank m ↑i < rank m ↑(parent m i) + 1
[PROOFSTEP]
exact Nat.lt_succ_of_lt this
[GOAL]
case inr.inr.inr
n : ℕ
m : UFModel n
x y : Fin n
H : rank m ↑x ≤ rank m ↑y
hroot : ↑(parent m y) = ↑y
i : Fin n
h₁ : ¬↑x = ↑i
h₂ : ¬(↑y = ↑i ∧ rank m ↑x = rank m ↑y)
h : ¬↑(parent m i) = ↑i
this : rank m ↑i < rank m ↑(parent m i)
h₃ : ¬(↑y = ↑(parent m i) ∧ rank m ↑x = rank m ↑y)
⊢ rank m ↑i < rank m ↑(parent m i)
[PROOFSTEP]
exact this
[GOAL]
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
n : ℕ
g : Fin n → β
e : n = Array.size arr
H :
  ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
    f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
⊢ Agrees arr f g
[PROOFSTEP]
cases e
[GOAL]
case refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
⊢ Agrees arr f g
[PROOFSTEP]
have : (fun i ↦ f (arr.get i)) = g := by funext ⟨i, h⟩; apply H
[GOAL]
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
⊢ (fun i => f (Array.get arr i)) = g
[PROOFSTEP]
funext ⟨i, h⟩
[GOAL]
case h
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
i : ℕ
h : i < Array.size arr
⊢ f (Array.get arr { val := i, isLt := h }) = g { val := i, isLt := h }
[PROOFSTEP]
apply H
[GOAL]
case refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
g : Fin (Array.size arr) → β
H : ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr), f (Array.get arr { val := i, isLt := h₁ }) = g { val := i, isLt := h₂ }
this : (fun i => f (Array.get arr i)) = g
⊢ Agrees arr f g
[PROOFSTEP]
cases this
[GOAL]
case refl.refl
α : Type u_1
β : Sort u_2
arr : Array α
f : α → β
H :
  ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr),
    f (Array.get arr { val := i, isLt := h₁ }) = (fun i => f (Array.get arr i)) { val := i, isLt := h₂ }
⊢ Agrees arr f fun i => f (Array.get arr i)
[PROOFSTEP]
constructor
[GOAL]
α : Type u_1
n : ℕ
β : Sort u_2
f : α → β
arr : Array α
m : Fin n → β
H : Agrees arr f m
⊢ n = Array.size arr
[PROOFSTEP]
cases H
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
⊢ Array.size arr = Array.size arr
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
n : ℕ
m : Fin n → β
H : Agrees arr f m
⊢ ∀ (i : ℕ) (h₁ : i < Array.size arr) (h₂ : i < n),
    f (Array.get arr { val := i, isLt := h₁ }) = m { val := i, isLt := h₂ }
[PROOFSTEP]
cases H
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
⊢ ∀ (i : ℕ) (h₁ h₂ : i < Array.size arr),
    f (Array.get arr { val := i, isLt := h₁ }) = (fun i => f (Array.get arr i)) { val := i, isLt := h₂ }
[PROOFSTEP]
exact fun i h _ ↦ rfl
[GOAL]
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
n : ℕ
m : Fin n → β
H : Agrees arr f m
k : ℕ
hk : k = n + 1
x : α
m' : Fin k → β
hm₁ : ∀ (i : Fin k) (h : ↑i < n), m' i = m { val := ↑i, isLt := h }
hm₂ : ∀ (h : n < k), f x = m' { val := n, isLt := h }
⊢ Agrees (Array.push arr x) f m'
[PROOFSTEP]
cases H
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
⊢ Agrees (Array.push arr x) f m'
[PROOFSTEP]
have : k = (arr.push x).size := by simp [hk]
[GOAL]
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
⊢ k = Array.size (Array.push arr x)
[PROOFSTEP]
simp [hk]
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
this : k = Array.size (Array.push arr x)
⊢ Agrees (Array.push arr x) f m'
[PROOFSTEP]
refine mk' this fun i h₁ h₂ ↦ ?_
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
⊢ f (Array.get (Array.push arr x) { val := i, isLt := h₁ }) = m' { val := i, isLt := h₂ }
[PROOFSTEP]
simp [Array.get_push]
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
⊢ f (if h : i < Array.size arr then arr[i] else x) = m' { val := i, isLt := h₂ }
[PROOFSTEP]
split
[GOAL]
case mk.inl
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h✝ : i < Array.size arr
⊢ f arr[i] = m' { val := i, isLt := h₂ }
[PROOFSTEP]
rename_i h
[GOAL]
case mk.inl
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h : i < Array.size arr
⊢ f arr[i] = m' { val := i, isLt := h₂ }
[PROOFSTEP]
simp at hm₁ ⊢
[GOAL]
case mk.inr
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h✝ : ¬i < Array.size arr
⊢ f x = m' { val := i, isLt := h₂ }
[PROOFSTEP]
rename_i h
[GOAL]
case mk.inr
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = (fun i => f (Array.get arr i)) { val := ↑i, isLt := h }
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h : ¬i < Array.size arr
⊢ f x = m' { val := i, isLt := h₂ }
[PROOFSTEP]
simp at hm₁ ⊢
[GOAL]
case mk.inl
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = f arr[↑i]
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h : i < Array.size arr
⊢ f arr[i] = m' { val := i, isLt := h₂ }
[PROOFSTEP]
rw [← hm₁ ⟨i, h₂⟩]
[GOAL]
case mk.inl
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = f arr[↑i]
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h : i < Array.size arr
⊢ ↑{ val := i, isLt := h₂ } < Array.size arr
[PROOFSTEP]
assumption
[GOAL]
case mk.inr
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = f arr[↑i]
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h : ¬i < Array.size arr
⊢ f x = m' { val := i, isLt := h₂ }
[PROOFSTEP]
cases show i = arr.size by apply le_antisymm <;> simp_all [Nat.lt_succ]
[GOAL]
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = f arr[↑i]
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h : ¬i < Array.size arr
⊢ i = Array.size arr
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = f arr[↑i]
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h : ¬i < Array.size arr
⊢ i ≤ Array.size arr
[PROOFSTEP]
simp_all [Nat.lt_succ]
[GOAL]
case a
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = f arr[↑i]
this : k = Array.size (Array.push arr x)
i : ℕ
h₁ : i < Array.size (Array.push arr x)
h₂ : i < k
h : ¬i < Array.size arr
⊢ Array.size arr ≤ i
[PROOFSTEP]
simp_all [Nat.lt_succ]
[GOAL]
case mk.inr.refl
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
k : ℕ
x : α
m' : Fin k → β
hk : k = Array.size arr + 1
hm₂ : ∀ (h : Array.size arr < k), f x = m' { val := Array.size arr, isLt := h }
hm₁ : ∀ (i : Fin k) (h : ↑i < Array.size arr), m' i = f arr[↑i]
this : k = Array.size (Array.push arr x)
h₁ : Array.size arr < Array.size (Array.push arr x)
h₂ : Array.size arr < k
h : ¬Array.size arr < Array.size arr
⊢ f x = m' { val := Array.size arr, isLt := h₂ }
[PROOFSTEP]
rw [hm₂]
[GOAL]
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
n : ℕ
m : Fin n → β
H : Agrees arr f m
i : Fin (Array.size arr)
x : α
m' : Fin n → β
hm₁ : ∀ (j : Fin n), ↑j ≠ ↑i → m' j = m j
hm₂ : ∀ (h : ↑i < n), f x = m' { val := ↑i, isLt := h }
⊢ Agrees (Array.set arr i x) f m'
[PROOFSTEP]
cases H
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
⊢ Agrees (Array.set arr i x) f m'
[PROOFSTEP]
refine mk' (by simp) fun j hj₁ hj₂ ↦ ?_
[GOAL]
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
⊢ Array.size arr = Array.size (Array.set arr i x)
[PROOFSTEP]
simp
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
⊢ f (Array.get (Array.set arr i x) { val := j, isLt := hj₁ }) = m' { val := j, isLt := hj₂ }
[PROOFSTEP]
suffices f (Array.set arr i x)[j] = m' ⟨j, hj₂⟩ by simp_all [Array.get_set]
[GOAL]
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
this : f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
⊢ f (Array.get (Array.set arr i x) { val := j, isLt := hj₁ }) = m' { val := j, isLt := hj₂ }
[PROOFSTEP]
simp_all [Array.get_set]
[GOAL]
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ↑i = j
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
hj₁ : ↑i < Array.size (Array.set arr i x)
hj₂ : ↑i < Array.size arr
⊢ f (Array.set arr i x)[↑i] = m' { val := ↑i, isLt := hj₂ }
[PROOFSTEP]
rw [Array.get_set_eq, ← hm₂]
[GOAL]
case neg
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
[PROOFSTEP]
rw [arr.get_set_ne _ _ _ h, hm₁ ⟨j, _⟩ (Ne.symm h)]
[GOAL]
case neg
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ f arr[j] = (fun i => f (Array.get arr i)) { val := j, isLt := hj₂ }
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ j < Array.size arr
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ j < Array.size arr
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
i : ℕ
h : i < Array.size arr
⊢ i < n
[PROOFSTEP]
rw [H.size_eq]
[GOAL]
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
i : ℕ
h : i < Array.size arr
⊢ i < Array.size arr
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
k : ℕ
hk : k = n + 1
x : α
⊢ Models (Array.push arr { parent := n, value := x, rank := 0 }) (UFModel.push m k (_ : n ≤ k))
[PROOFSTEP]
apply H.imp
[GOAL]
case f
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
k : ℕ
hk : k = n + 1
x : α
⊢ (Agrees arr (fun x => x.parent) fun i => ↑(parent m i)) →
    Agrees (Array.push arr { parent := n, value := x, rank := 0 }) (fun x => x.parent) fun i =>
      ↑(parent (UFModel.push m k (_ : n ≤ k)) i)
[PROOFSTEP]
intro H
[GOAL]
case f
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H✝ : Models arr m
k : ℕ
hk : k = n + 1
x : α
H : Agrees arr (fun x => x.parent) fun i => ↑(parent m i)
⊢ Agrees (Array.push arr { parent := n, value := x, rank := 0 }) (fun x => x.parent) fun i =>
    ↑(parent (UFModel.push m k (_ : n ≤ k)) i)
[PROOFSTEP]
refine H.push _ hk _ _ (fun i h ↦ ?_) (fun h ↦ ?_)
[GOAL]
case f.refine_1
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H✝ : Models arr m
k : ℕ
hk : k = n + 1
x : α
H : Agrees arr (fun x => x.parent) fun i => ↑(parent m i)
i : Fin k
h : ↑i < n
⊢ ↑(parent (UFModel.push m k (_ : n ≤ k)) i) = ↑(parent m { val := ↑i, isLt := h })
[PROOFSTEP]
simp [UFModel.push, h, lt_irrefl]
[GOAL]
case f.refine_2
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H✝ : Models arr m
k : ℕ
hk : k = n + 1
x : α
H : Agrees arr (fun x => x.parent) fun i => ↑(parent m i)
h : n < k
⊢ { parent := n, value := x, rank := 0 }.parent = ↑(parent (UFModel.push m k (_ : n ≤ k)) { val := n, isLt := h })
[PROOFSTEP]
simp [UFModel.push, h, lt_irrefl]
[GOAL]
case g
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
k : ℕ
hk : k = n + 1
x : α
⊢ (Agrees arr (fun x => x.rank) fun i => rank m ↑i) →
    Agrees (Array.push arr { parent := n, value := x, rank := 0 }) (fun x => x.rank) fun i =>
      rank (UFModel.push m k (_ : n ≤ k)) ↑i
[PROOFSTEP]
intro H
[GOAL]
case g
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H✝ : Models arr m
k : ℕ
hk : k = n + 1
x : α
H : Agrees arr (fun x => x.rank) fun i => rank m ↑i
⊢ Agrees (Array.push arr { parent := n, value := x, rank := 0 }) (fun x => x.rank) fun i =>
    rank (UFModel.push m k (_ : n ≤ k)) ↑i
[PROOFSTEP]
refine H.push _ hk _ _ (fun i h ↦ ?_) (fun h ↦ ?_)
[GOAL]
case g.refine_1
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H✝ : Models arr m
k : ℕ
hk : k = n + 1
x : α
H : Agrees arr (fun x => x.rank) fun i => rank m ↑i
i : Fin k
h : ↑i < n
⊢ rank (UFModel.push m k (_ : n ≤ k)) ↑i = rank m ↑{ val := ↑i, isLt := h }
[PROOFSTEP]
simp [UFModel.push, h, lt_irrefl]
[GOAL]
case g.refine_2
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H✝ : Models arr m
k : ℕ
hk : k = n + 1
x : α
H : Agrees arr (fun x => x.rank) fun i => rank m ↑i
h : n < k
⊢ { parent := n, value := x, rank := 0 }.rank = rank (UFModel.push m k (_ : n ≤ k)) ↑{ val := n, isLt := h }
[PROOFSTEP]
simp [UFModel.push, h, lt_irrefl]
[GOAL]
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
hm : Models arr m
i j : Fin n
H : rank m ↑i < rank m ↑j
hi : ↑i < Array.size arr
x : UFNode α
hp : x.parent = ↑j
hrk : x.rank = arr[i].rank
k : Fin n
h : ↑k ≠ ↑i
⊢ ↑(parent (UFModel.setParent m i j H) k) = ↑(parent m k)
[PROOFSTEP]
simp [UFModel.setParent, h.symm]
[GOAL]
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
hm : Models arr m
i j : Fin n
H : rank m ↑i < rank m ↑j
hi : ↑i < Array.size arr
x : UFNode α
hp : x.parent = ↑j
hrk : x.rank = arr[i].rank
h : ↑{ val := ↑i, isLt := hi } < n
⊢ x.parent = ↑(parent (UFModel.setParent m i j H) { val := ↑{ val := ↑i, isLt := hi }, isLt := h })
[PROOFSTEP]
simp [UFModel.setParent, hp]
[GOAL]
α : Type u_1
self : UnionFind α
⊢ ∃ m, UFModel.Models self.arr m
[PROOFSTEP]
let ⟨n, m, hm⟩ := self.model
[GOAL]
α : Type u_1
self : UnionFind α
n : ℕ
m : UFModel n
hm : UFModel.Models self.arr m
⊢ ∃ m, UFModel.Models self.arr m
[PROOFSTEP]
cases hm.size_eq
[GOAL]
case refl
α : Type u_1
self : UnionFind α
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ ∃ m, UFModel.Models self.arr m
[PROOFSTEP]
exact ⟨m, hm⟩
[GOAL]
α : Type ?u.46031
self : UnionFind α
i : ℕ
⊢ { k // ∀ (j : ℕ), j < i + 1 → ∀ (h : j < Array.size self.arr), (Array.get self.arr { val := j, isLt := h }).rank ≤ k }
[PROOFSTEP]
let ⟨k, H⟩ := rankMaxAux self i
[GOAL]
α : Type ?u.46031
self : UnionFind α
i k : ℕ
H : ∀ (j : ℕ), j < i → ∀ (h : j < Array.size self.arr), (Array.get self.arr { val := j, isLt := h }).rank ≤ k
⊢ { k // ∀ (j : ℕ), j < i + 1 → ∀ (h : j < Array.size self.arr), (Array.get self.arr { val := j, isLt := h }).rank ≤ k }
[PROOFSTEP]
refine ⟨max k (if h : _ then (self.arr.get ⟨i, h⟩).rank else 0), fun j hj h ↦ ?_⟩
[GOAL]
α : Type ?u.46031
self : UnionFind α
i k : ℕ
H : ∀ (j : ℕ), j < i → ∀ (h : j < Array.size self.arr), (Array.get self.arr { val := j, isLt := h }).rank ≤ k
j : ℕ
hj : j < i + 1
h : j < Array.size self.arr
⊢ (Array.get self.arr { val := j, isLt := h }).rank ≤
    max k (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0)
[PROOFSTEP]
match j, lt_or_eq_of_le (Nat.le_of_lt_succ hj) with
| j, Or.inl hj => exact le_trans (H _ hj h) (le_max_left _ _)
| _, Or.inr rfl => simp [h, le_max_right]
[GOAL]
α : Type ?u.46031
self : UnionFind α
i k : ℕ
H : ∀ (j : ℕ), j < i → ∀ (h : j < Array.size self.arr), (Array.get self.arr { val := j, isLt := h }).rank ≤ k
j✝ j : ℕ
hj : j < i
hj✝ : j < i + 1
h : j < Array.size self.arr
⊢ (Array.get self.arr { val := j, isLt := h }).rank ≤
    max k (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0)
[PROOFSTEP]
exact le_trans (H _ hj h) (le_max_left _ _)
[GOAL]
α : Type ?u.46031
self : UnionFind α
i k : ℕ
H : ∀ (j : ℕ), j < i → ∀ (h : j < Array.size self.arr), (Array.get self.arr { val := j, isLt := h }).rank ≤ k
j : ℕ
hj : i < i + 1
h : i < Array.size self.arr
⊢ (Array.get self.arr { val := i, isLt := h }).rank ≤
    max k (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0)
[PROOFSTEP]
simp [h, le_max_right]
[GOAL]
α : Type u_1
self : UnionFind α
i : ℕ
⊢ rank self i < rankMax self
[PROOFSTEP]
simp [rank]
[GOAL]
α : Type u_1
self : UnionFind α
i : ℕ
⊢ (if h : i < size self then self.arr[i].rank else 0) < rankMax self
[PROOFSTEP]
split
[GOAL]
case inl
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : i < size self
⊢ self.arr[i].rank < rankMax self
case inr α : Type u_1 self : UnionFind α i : ℕ h✝ : ¬i < size self ⊢ 0 < rankMax self
[PROOFSTEP]
{apply lt_rankMax'
}
[GOAL]
case inl
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : i < size self
⊢ self.arr[i].rank < rankMax self
[PROOFSTEP]
apply lt_rankMax'
[GOAL]
case inr
α : Type u_1
self : UnionFind α
i : ℕ
h✝ : ¬i < size self
⊢ 0 < rankMax self
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
α : Type u_1
self : UnionFind α
n : ℕ
m : UFModel n
H : UFModel.Models self.arr m
i : ℕ
h : i < size self
⊢ rank self i = UFModel.rank m i
[PROOFSTEP]
simp [rank, h, H.rank_eq]
[GOAL]
α : Type u_1
self : UnionFind α
i : ℕ
h : i < Array.size self.arr
⊢ self.arr[i].parent ≠ i → rank self i < rank self self.arr[i].parent
[PROOFSTEP]
let ⟨m, hm⟩ := self.model'
[GOAL]
α : Type u_1
self : UnionFind α
i : ℕ
h : i < Array.size self.arr
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ self.arr[i].parent ≠ i → rank self i < rank self self.arr[i].parent
[PROOFSTEP]
simpa [hm.parent_eq, hm.rank_eq, rank, size, h, (m.parent ⟨i, h⟩).2] using m.rank_lt ⟨i, h⟩
[GOAL]
α : Type u_1
self : UnionFind α
i : ℕ
h : i < Array.size self.arr
⊢ self.arr[i].parent < size self
[PROOFSTEP]
let ⟨m, hm⟩ := self.model'
[GOAL]
α : Type u_1
self : UnionFind α
i : ℕ
h : i < Array.size self.arr
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ self.arr[i].parent < size self
[PROOFSTEP]
simp [hm.parent_eq, size, (m.parent ⟨i, h⟩).2, h]
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
⊢ (s : Array (UFNode α)) ×'
    (root : Fin (Array.size s)) ×'
      ∃ n m m',
        UFModel.Models self.arr m ∧
          UFModel.Models s m' ∧
            m'.rank = m.rank ∧
              (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
                UFModel.rank m ↑x ≤ UFModel.rank m ↑root
[PROOFSTEP]
let y := self.arr[x].parent
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
⊢ (s : Array (UFNode α)) ×'
    (root : Fin (Array.size s)) ×'
      ∃ n m m',
        UFModel.Models self.arr m ∧
          UFModel.Models s m' ∧
            m'.rank = m.rank ∧
              (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
                UFModel.rank m ↑x ≤ UFModel.rank m ↑root
[PROOFSTEP]
refine
  if h : y = x then ⟨self.arr, x, ?a'⟩
  else
    have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt _ h)
    let ⟨arr₁, root, H⟩ := self.findAux ⟨y, self.parent_lt _ x.2⟩
    have hx := ?hx
    let arr₂ := arr₁.set ⟨x, hx⟩ { arr₁.get ⟨x, hx⟩ with parent := root }
    ⟨arr₂, ⟨root, by simp [root.2]⟩, ?b'⟩
      -- start proof
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
⊢ ↑root < Array.size arr₂
[PROOFSTEP]
simp [root.2]
[GOAL]
case a'
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : y = ↑x
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models self.arr m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑x, isLt := hr }) = ↑x) ∧ UFModel.rank m ↑x ≤ UFModel.rank m ↑x
case hx
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ↑x < Array.size arr₁
case b'
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root,
                            isLt :=
                              (_ :
                                ↑root <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
case a' =>
  -- FIXME: hygiene bug causes `case a` to fail
  let ⟨m, hm⟩ := self.model'
  exact ⟨_, m, m, hm, hm, rfl, ⟨x.2, by rwa [← hm.parent_eq]⟩, le_refl _⟩
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : y = ↑x
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models self.arr m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑x, isLt := hr }) = ↑x) ∧ UFModel.rank m ↑x ≤ UFModel.rank m ↑x
[PROOFSTEP]
case a' =>
  -- FIXME: hygiene bug causes `case a` to fail
  let ⟨m, hm⟩ := self.model'
  exact ⟨_, m, m, hm, hm, rfl, ⟨x.2, by rwa [← hm.parent_eq]⟩, le_refl _⟩
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : y = ↑x
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models self.arr m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑x, isLt := hr }) = ↑x) ∧ UFModel.rank m ↑x ≤ UFModel.rank m ↑x
[PROOFSTEP]
let ⟨m, hm⟩ := self.model'
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : y = ↑x
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models self.arr m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑x, isLt := hr }) = ↑x) ∧ UFModel.rank m ↑x ≤ UFModel.rank m ↑x
[PROOFSTEP]
exact ⟨_, m, m, hm, hm, rfl, ⟨x.2, by rwa [← hm.parent_eq]⟩, le_refl _⟩
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : y = ↑x
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ ↑(UFModel.parent m { val := ↑x, isLt := (_ : ↑x < size self) }) = ↑x
[PROOFSTEP]
rwa [← hm.parent_eq]
[GOAL]
case hx
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ↑x < Array.size arr₁
case b'
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root,
                            isLt :=
                              (_ :
                                ↑root <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
all_goals let ⟨n, m, m', hm, hm', e, ⟨_, hr⟩, le⟩ := H
[GOAL]
case hx
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ↑x < Array.size arr₁
[PROOFSTEP]
let ⟨n, m, m', hm, hm', e, ⟨_, hr⟩, le⟩ := H
[GOAL]
case b'
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root,
                            isLt :=
                              (_ :
                                ↑root <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
let ⟨n, m, m', hm, hm', e, ⟨_, hr⟩, le⟩ := H
[GOAL]
case hx
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ↑x < Array.size arr₁
case b'
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root,
                            isLt :=
                              (_ :
                                ↑root <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
case hx => exact hm'.size_eq ▸ hm.size_eq.symm ▸ x.2
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ↑x < Array.size arr₁
[PROOFSTEP]
case hx => exact hm'.size_eq ▸ hm.size_eq.symm ▸ x.2
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ↑x < Array.size arr₁
[PROOFSTEP]
exact hm'.size_eq ▸ hm.size_eq.symm ▸ x.2
[GOAL]
case b'
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root,
                            isLt :=
                              (_ :
                                ↑root <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
case b' =>
  let x' : Fin n := ⟨x, hm.size_eq ▸ x.2⟩
  let root : Fin n := ⟨root, hm'.size_eq.symm ▸ root.2⟩
  have hy : (UFModel.parent m x').1 = y := by rw [← hm.parent_eq x x.2 x'.2]; rfl
  have := m.rank_lt x'; rw [hy] at this
  have := lt_of_lt_of_le (this h) le
  refine ⟨n, m, _, hm, hm'.setParent x' root (by rw [e]; exact this) hx _ rfl rfl, e, ⟨root.2, ?_⟩, le_of_lt this⟩
  have : x.1 ≠ root := mt (congrArg _) (ne_of_lt this); dsimp only at this
  simp [UFModel.setParent, this, hr]
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root,
                            isLt :=
                              (_ :
                                ↑root <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
case b' =>
  let x' : Fin n := ⟨x, hm.size_eq ▸ x.2⟩
  let root : Fin n := ⟨root, hm'.size_eq.symm ▸ root.2⟩
  have hy : (UFModel.parent m x').1 = y := by rw [← hm.parent_eq x x.2 x'.2]; rfl
  have := m.rank_lt x'; rw [hy] at this
  have := lt_of_lt_of_le (this h) le
  refine ⟨n, m, _, hm, hm'.setParent x' root (by rw [e]; exact this) hx _ rfl rfl, e, ⟨root.2, ?_⟩, le_of_lt this⟩
  have : x.1 ≠ root := mt (congrArg _) (ne_of_lt this); dsimp only at this
  simp [UFModel.setParent, this, hr]
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root,
                            isLt :=
                              (_ :
                                ↑root <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
let x' : Fin n := ⟨x, hm.size_eq ▸ x.2⟩
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root,
                            isLt :=
                              (_ :
                                ↑root <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root,
                    isLt :=
                      (_ :
                        ↑root <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
let root : Fin n := ⟨root, hm'.size_eq.symm ▸ root.2⟩
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root✝,
                            isLt :=
                              (_ :
                                ↑root✝ <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
have hy : (UFModel.parent m x').1 = y := by rw [← hm.parent_eq x x.2 x'.2]; rfl
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
⊢ ↑(UFModel.parent m x') = y
[PROOFSTEP]
rw [← hm.parent_eq x x.2 x'.2]
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
⊢ self.arr[↑x].parent = y
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root✝,
                            isLt :=
                              (_ :
                                ↑root✝ <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
have := m.rank_lt x'
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this✝ : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
this : ↑(UFModel.parent m x') ≠ ↑x' → UFModel.rank m ↑x' < UFModel.rank m ↑(UFModel.parent m x')
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root✝,
                            isLt :=
                              (_ :
                                ↑root✝ <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
rw [hy] at this
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this✝ : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
this : y ≠ ↑x' → UFModel.rank m ↑x' < UFModel.rank m y
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root✝,
                            isLt :=
                              (_ :
                                ↑root✝ <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
have := lt_of_lt_of_le (this h) le
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this✝¹ : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
this✝ : y ≠ ↑x' → UFModel.rank m ↑x' < UFModel.rank m y
this : UFModel.rank m ↑x' < UFModel.rank m ↑root✝
⊢ ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₂ m' ∧
        m'.rank = m.rank ∧
          (∃ hr,
              ↑(UFModel.parent m'
                    {
                      val :=
                        ↑{ val := ↑root✝,
                            isLt :=
                              (_ :
                                ↑root✝ <
                                  Array.size
                                    (Array.set arr₁ { val := ↑x, isLt := hx }
                                      { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
                      isLt := hr }) =
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }) ∧
            UFModel.rank m ↑x ≤
              UFModel.rank m
                ↑{ val := ↑root✝,
                    isLt :=
                      (_ :
                        ↑root✝ <
                          Array.size
                            (Array.set arr₁ { val := ↑x, isLt := hx }
                              { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
refine ⟨n, m, _, hm, hm'.setParent x' root (by rw [e]; exact this) hx _ rfl rfl, e, ⟨root.2, ?_⟩, le_of_lt this⟩
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this✝¹ : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
this✝ : y ≠ ↑x' → UFModel.rank m ↑x' < UFModel.rank m y
this : UFModel.rank m ↑x' < UFModel.rank m ↑root✝
⊢ UFModel.rank m' ↑x' < UFModel.rank m' ↑root
[PROOFSTEP]
rw [e]
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this✝¹ : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
this✝ : y ≠ ↑x' → UFModel.rank m ↑x' < UFModel.rank m y
this : UFModel.rank m ↑x' < UFModel.rank m ↑root✝
⊢ UFModel.rank m ↑x' < UFModel.rank m ↑root
[PROOFSTEP]
exact this
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this✝¹ : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
this✝ : y ≠ ↑x' → UFModel.rank m ↑x' < UFModel.rank m y
this : UFModel.rank m ↑x' < UFModel.rank m ↑root✝
⊢ ↑(UFModel.parent (UFModel.setParent m' x' root (_ : UFModel.rank m' ↑x' < UFModel.rank m' ↑root))
        {
          val :=
            ↑{ val := ↑root✝,
                isLt :=
                  (_ :
                    ↑root✝ <
                      Array.size
                        (Array.set arr₁ { val := ↑x, isLt := hx }
                          { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
          isLt := (_ : ↑root < n) }) =
    ↑{ val := ↑root✝,
        isLt :=
          (_ :
            ↑root✝ <
              Array.size
                (Array.set arr₁ { val := ↑x, isLt := hx }
                  { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
have : x.1 ≠ root := mt (congrArg _) (ne_of_lt this)
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this✝² : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
this✝¹ : y ≠ ↑x' → UFModel.rank m ↑x' < UFModel.rank m y
this✝ : UFModel.rank m ↑x' < UFModel.rank m ↑root✝
this : ↑x ≠ ↑root
⊢ ↑(UFModel.parent (UFModel.setParent m' x' root (_ : UFModel.rank m' ↑x' < UFModel.rank m' ↑root))
        {
          val :=
            ↑{ val := ↑root✝,
                isLt :=
                  (_ :
                    ↑root✝ <
                      Array.size
                        (Array.set arr₁ { val := ↑x, isLt := hx }
                          { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
          isLt := (_ : ↑root < n) }) =
    ↑{ val := ↑root✝,
        isLt :=
          (_ :
            ↑root✝ <
              Array.size
                (Array.set arr₁ { val := ↑x, isLt := hx }
                  { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
dsimp only at this
[GOAL]
α : Type ?u.56700
self : UnionFind α
x : Fin (size self)
y : ℕ := self.arr[x].parent
h : ¬y = ↑x
this✝² : rankMax self - rank self self.arr[↑x].parent < rankMax self - rank self ↑x
arr₁ : Array (UFNode α)
root✝ : Fin (Array.size arr₁)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models arr₁ m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root✝, isLt := hr }) = ↑root✝) ∧
            UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
hx : ↑x < Array.size arr₁
arr₂ : Array (UFNode α) :=
  Array.set arr₁ { val := ↑x, isLt := hx }
    (let src := Array.get arr₁ { val := ↑x, isLt := hx };
    { parent := ↑root✝, value := src.value, rank := src.rank })
n : ℕ
m m' : UFModel n
hm : UFModel.Models self.arr m
hm' : UFModel.Models arr₁ m'
e : m'.rank = m.rank
w✝ : ↑root✝ < n
hr : ↑(UFModel.parent m' { val := ↑root✝, isLt := w✝ }) = ↑root✝
le : UFModel.rank m ↑{ val := y, isLt := (_ : self.arr[↑x].parent < size self) } ≤ UFModel.rank m ↑root✝
x' : Fin n := { val := ↑x, isLt := (_ : ↑x < n) }
root : Fin n := { val := ↑root✝, isLt := (_ : ↑root✝ < n) }
hy : ↑(UFModel.parent m x') = y
this✝¹ : y ≠ ↑x' → UFModel.rank m ↑x' < UFModel.rank m y
this✝ : UFModel.rank m ↑x' < UFModel.rank m ↑root✝
this : ↑x ≠ ↑root✝
⊢ ↑(UFModel.parent (UFModel.setParent m' x' root (_ : UFModel.rank m' ↑x' < UFModel.rank m' ↑root))
        {
          val :=
            ↑{ val := ↑root✝,
                isLt :=
                  (_ :
                    ↑root✝ <
                      Array.size
                        (Array.set arr₁ { val := ↑x, isLt := hx }
                          { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) },
          isLt := (_ : ↑root < n) }) =
    ↑{ val := ↑root✝,
        isLt :=
          (_ :
            ↑root✝ <
              Array.size
                (Array.set arr₁ { val := ↑x, isLt := hx }
                  { parent := ↑root✝, value := arr₁[↑x].value, rank := arr₁[↑x].rank })) }
[PROOFSTEP]
simp [UFModel.setParent, this, hr]
[GOAL]
α : Type ?u.79923
self : UnionFind α
x : Fin (size self)
s : Array (UFNode α)
root : Fin (Array.size s)
H :
  ∃ n m m',
    UFModel.Models self.arr m ∧
      UFModel.Models s m' ∧
        m'.rank = m.rank ∧
          (∃ hr, ↑(UFModel.parent m' { val := ↑root, isLt := hr }) = ↑root) ∧ UFModel.rank m ↑x ≤ UFModel.rank m ↑root
n : ℕ
w✝¹ m' : UFModel n
hm : UFModel.Models self.arr w✝¹
hm' : UFModel.Models s m'
left✝ : m'.rank = w✝¹.rank
w✝ : ↑root < n
hr : ↑(UFModel.parent m' { val := ↑root, isLt := w✝ }) = ↑root
right✝ : UFModel.rank w✝¹ ↑x ≤ UFModel.rank w✝¹ ↑root
⊢ s[↑root].parent = ↑root
[PROOFSTEP]
rwa [hm'.parent_eq]
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
⊢ UnionFind α
[PROOFSTEP]
refine
  if ne : x.1 = y then self
  else
    let nx := self.arr[x]
    let ny := self.arr[y]
    if h : ny.rank < nx.rank then ⟨self.arr.set y { ny with parent := x }, ?a⟩
    else
      let arr₁ := self.arr.set x { nx with parent := y }
      let arr₂ := if nx.rank = ny.rank then arr₁.set ⟨y, by simp; exact y.2⟩ { ny with rank := ny.rank + 1 } else arr₁
      ⟨arr₂, ?b⟩
        -- start proof
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
⊢ ↑y < Array.size arr₁
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
⊢ ↑y < Array.size self.arr
[PROOFSTEP]
exact y.2
[GOAL]
case a
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ny.rank < nx.rank
⊢ ∃ n m, UFModel.Models (Array.set self.arr y { parent := ↑x, value := ny.value, rank := ny.rank }) m
case b
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
⊢ ∃ n m, UFModel.Models arr₂ m
[PROOFSTEP]
case a =>
  let ⟨m, hm⟩ := self.model'
  exact ⟨_, _, hm.setParent y x (by simpa [hm.rank_eq] using h) _ _ rfl rfl⟩
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ny.rank < nx.rank
⊢ ∃ n m, UFModel.Models (Array.set self.arr y { parent := ↑x, value := ny.value, rank := ny.rank }) m
[PROOFSTEP]
case a =>
  let ⟨m, hm⟩ := self.model'
  exact ⟨_, _, hm.setParent y x (by simpa [hm.rank_eq] using h) _ _ rfl rfl⟩
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ny.rank < nx.rank
⊢ ∃ n m, UFModel.Models (Array.set self.arr y { parent := ↑x, value := ny.value, rank := ny.rank }) m
[PROOFSTEP]
let ⟨m, hm⟩ := self.model'
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ny.rank < nx.rank
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ ∃ n m, UFModel.Models (Array.set self.arr y { parent := ↑x, value := ny.value, rank := ny.rank }) m
[PROOFSTEP]
exact ⟨_, _, hm.setParent y x (by simpa [hm.rank_eq] using h) _ _ rfl rfl⟩
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ny.rank < nx.rank
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ UFModel.rank m ↑y < UFModel.rank m ↑x
[PROOFSTEP]
simpa [hm.rank_eq] using h
[GOAL]
case b
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
⊢ ∃ n m, UFModel.Models arr₂ m
[PROOFSTEP]
case b =>
  let ⟨m, hm⟩ := self.model'; let n := self.size
  refine ⟨_, m.setParentBump x y (by simpa [hm.rank_eq] using h) (by simpa [← hm.parent_eq'] using yroot), ?_⟩
  let parent (i : Fin n) := (if x.1 = i then y else m.parent i).1
  have : UFModel.Agrees arr₁ (·.parent) parent := hm.1.set (fun i h ↦ by simp; rw [if_neg h.symm]) (fun h ↦ by simp)
  have H1 : UFModel.Agrees arr₂ (·.parent) parent := by
    simp; split
    · exact this.set (fun i h ↦ by simp [h.symm]) (fun h ↦ by simp [ne, hm.parent_eq'])
    · exact this
  have : UFModel.Agrees arr₁ (·.rank) (fun i : Fin n ↦ m.rank i) :=
    hm.2.set (fun i _ ↦ by simp) (fun _ ↦ by simp [hm.rank_eq])
  let rank (i : Fin n) := if y.1 = i ∧ m.rank x = m.rank y then m.rank y + 1 else m.rank i
  have H2 : UFModel.Agrees arr₂ (·.rank) rank := by
    simp; split <;> (rename_i xy; simp [hm.rank_eq] at xy ; simp [xy])
    · exact this.set (fun i h ↦ by rw [if_neg h.symm]) (fun h ↦ by simp [hm.rank_eq])
    · exact this
  exact ⟨H1, H2⟩
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
⊢ ∃ n m, UFModel.Models arr₂ m
[PROOFSTEP]
case b =>
  let ⟨m, hm⟩ := self.model'; let n := self.size
  refine ⟨_, m.setParentBump x y (by simpa [hm.rank_eq] using h) (by simpa [← hm.parent_eq'] using yroot), ?_⟩
  let parent (i : Fin n) := (if x.1 = i then y else m.parent i).1
  have : UFModel.Agrees arr₁ (·.parent) parent := hm.1.set (fun i h ↦ by simp; rw [if_neg h.symm]) (fun h ↦ by simp)
  have H1 : UFModel.Agrees arr₂ (·.parent) parent := by
    simp; split
    · exact this.set (fun i h ↦ by simp [h.symm]) (fun h ↦ by simp [ne, hm.parent_eq'])
    · exact this
  have : UFModel.Agrees arr₁ (·.rank) (fun i : Fin n ↦ m.rank i) :=
    hm.2.set (fun i _ ↦ by simp) (fun _ ↦ by simp [hm.rank_eq])
  let rank (i : Fin n) := if y.1 = i ∧ m.rank x = m.rank y then m.rank y + 1 else m.rank i
  have H2 : UFModel.Agrees arr₂ (·.rank) rank := by
    simp; split <;> (rename_i xy; simp [hm.rank_eq] at xy ; simp [xy])
    · exact this.set (fun i h ↦ by rw [if_neg h.symm]) (fun h ↦ by simp [hm.rank_eq])
    · exact this
  exact ⟨H1, H2⟩
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
⊢ ∃ n m, UFModel.Models arr₂ m
[PROOFSTEP]
let ⟨m, hm⟩ := self.model'
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ ∃ n m, UFModel.Models arr₂ m
[PROOFSTEP]
let n := self.size
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
⊢ ∃ n m, UFModel.Models arr₂ m
[PROOFSTEP]
refine ⟨_, m.setParentBump x y (by simpa [hm.rank_eq] using h) (by simpa [← hm.parent_eq'] using yroot), ?_⟩
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
⊢ UFModel.rank m ↑x ≤ UFModel.rank m ↑y
[PROOFSTEP]
simpa [hm.rank_eq] using h
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
⊢ ↑(UFModel.parent m y) = ↑y
[PROOFSTEP]
simpa [← hm.parent_eq'] using yroot
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
⊢ UFModel.Models arr₂
    (UFModel.setParentBump m x y (_ : UFModel.rank m ↑x ≤ UFModel.rank m ↑y) (_ : ↑(UFModel.parent m y) = ↑y))
[PROOFSTEP]
let parent (i : Fin n) := (if x.1 = i then y else m.parent i).1
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
⊢ UFModel.Models arr₂
    (UFModel.setParentBump m x y (_ : UFModel.rank m ↑x ≤ UFModel.rank m ↑y) (_ : ↑(UFModel.parent m y) = ↑y))
[PROOFSTEP]
have : UFModel.Agrees arr₁ (·.parent) parent := hm.1.set (fun i h ↦ by simp; rw [if_neg h.symm]) (fun h ↦ by simp)
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h✝ : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
i : Fin (Array.size self.arr)
h : ↑i ≠ ↑x
⊢ parent i = ↑(UFModel.parent m i)
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h✝ : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
i : Fin (Array.size self.arr)
h : ↑i ≠ ↑x
⊢ ↑(if ↑x = ↑i then y else UFModel.parent m i) = ↑(UFModel.parent m i)
[PROOFSTEP]
rw [if_neg h.symm]
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h✝ : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
h : ↑x < Array.size self.arr
⊢ { parent := ↑y, value := nx.value, rank := nx.rank }.parent = parent { val := ↑x, isLt := h }
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
⊢ UFModel.Models arr₂
    (UFModel.setParentBump m x y (_ : UFModel.rank m ↑x ≤ UFModel.rank m ↑y) (_ : ↑(UFModel.parent m y) = ↑y))
[PROOFSTEP]
have H1 : UFModel.Agrees arr₂ (·.parent) parent := by
  simp; split
  · exact this.set (fun i h ↦ by simp [h.symm]) (fun h ↦ by simp [ne, hm.parent_eq'])
  · exact this
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
⊢ UFModel.Agrees arr₂ (fun x => x.parent) parent
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
⊢ UFModel.Agrees
    (if self.arr[↑x].rank = self.arr[↑y].rank then
      Array.set (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
        { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
        { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 }
    else Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
    (fun x => x.parent) fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
[PROOFSTEP]
split
[GOAL]
case inl
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
h✝ : self.arr[↑x].rank = self.arr[↑y].rank
⊢ UFModel.Agrees
    (Array.set (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
      { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 })
    (fun x => x.parent) fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
[PROOFSTEP]
exact this.set (fun i h ↦ by simp [h.symm]) (fun h ↦ by simp [ne, hm.parent_eq'])
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h✝¹ : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
h✝ : self.arr[↑x].rank = self.arr[↑y].rank
i : Fin n
h : ↑i ≠ ↑{ val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
⊢ ↑(if ↑x = ↑i then y else UFModel.parent m i) = parent i
[PROOFSTEP]
simp [h.symm]
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h✝¹ : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
h✝ : self.arr[↑x].rank = self.arr[↑y].rank
h : ↑{ val := ↑y, isLt := (_ : ↑y < Array.size arr₁) } < n
⊢ { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 }.parent =
    ↑(if ↑x = ↑{ val := ↑{ val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }, isLt := h } then y
      else UFModel.parent m { val := ↑{ val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }, isLt := h })
[PROOFSTEP]
simp [ne, hm.parent_eq']
[GOAL]
case inr
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
h✝ : ¬self.arr[↑x].rank = self.arr[↑y].rank
⊢ UFModel.Agrees (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
    (fun x => x.parent) fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
[PROOFSTEP]
exact this
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
⊢ UFModel.Models arr₂
    (UFModel.setParentBump m x y (_ : UFModel.rank m ↑x ≤ UFModel.rank m ↑y) (_ : ↑(UFModel.parent m y) = ↑y))
[PROOFSTEP]
have : UFModel.Agrees arr₁ (·.rank) (fun i : Fin n ↦ m.rank i) :=
  hm.2.set (fun i _ ↦ by simp) (fun _ ↦ by simp [hm.rank_eq])
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
i : Fin (Array.size self.arr)
x✝ : ↑i ≠ ↑x
⊢ UFModel.rank m ↑i = UFModel.rank m ↑i
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
x✝ : ↑x < Array.size self.arr
⊢ { parent := ↑y, value := nx.value, rank := nx.rank }.rank = UFModel.rank m ↑{ val := ↑x, isLt := x✝ }
[PROOFSTEP]
simp [hm.rank_eq]
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
⊢ UFModel.Models arr₂
    (UFModel.setParentBump m x y (_ : UFModel.rank m ↑x ≤ UFModel.rank m ↑y) (_ : ↑(UFModel.parent m y) = ↑y))
[PROOFSTEP]
let rank (i : Fin n) := if y.1 = i ∧ m.rank x = m.rank y then m.rank y + 1 else m.rank i
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
⊢ UFModel.Models arr₂
    (UFModel.setParentBump m x y (_ : UFModel.rank m ↑x ≤ UFModel.rank m ↑y) (_ : ↑(UFModel.parent m y) = ↑y))
[PROOFSTEP]
have H2 : UFModel.Agrees arr₂ (·.rank) rank := by
  simp; split <;> (rename_i xy; simp [hm.rank_eq] at xy ; simp [xy])
  · exact this.set (fun i h ↦ by rw [if_neg h.symm]) (fun h ↦ by simp [hm.rank_eq])
  · exact this
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
⊢ UFModel.Agrees arr₂ (fun x => x.rank) rank
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
⊢ UFModel.Agrees
    (if self.arr[↑x].rank = self.arr[↑y].rank then
      Array.set (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
        { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
        { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 }
    else Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
    (fun x => x.rank) fun i =>
    if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
[PROOFSTEP]
split
[GOAL]
case inl
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
h✝ : self.arr[↑x].rank = self.arr[↑y].rank
⊢ UFModel.Agrees
    (Array.set (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
      { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 })
    (fun x => x.rank) fun i =>
    if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
[PROOFSTEP]
rename_i xy
[GOAL]
case inl
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
xy : self.arr[↑x].rank = self.arr[↑y].rank
⊢ UFModel.Agrees
    (Array.set (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
      { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 })
    (fun x => x.rank) fun i =>
    if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
[PROOFSTEP]
simp [hm.rank_eq] at xy
[GOAL]
case inl
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
xy : UFModel.rank m ↑x = UFModel.rank m ↑y
⊢ UFModel.Agrees
    (Array.set (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
      { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 })
    (fun x => x.rank) fun i =>
    if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
[PROOFSTEP]
simp [xy]
[GOAL]
case inr
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
h✝ : ¬self.arr[↑x].rank = self.arr[↑y].rank
⊢ UFModel.Agrees (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
    (fun x => x.rank) fun i =>
    if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
[PROOFSTEP]
rename_i xy
[GOAL]
case inr
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
xy : ¬self.arr[↑x].rank = self.arr[↑y].rank
⊢ UFModel.Agrees (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
    (fun x => x.rank) fun i =>
    if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
[PROOFSTEP]
simp [hm.rank_eq] at xy
[GOAL]
case inr
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
xy : ¬UFModel.rank m ↑x = UFModel.rank m ↑y
⊢ UFModel.Agrees (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
    (fun x => x.rank) fun i =>
    if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
[PROOFSTEP]
simp [xy]
[GOAL]
case inl
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
xy : UFModel.rank m ↑x = UFModel.rank m ↑y
⊢ UFModel.Agrees
    (Array.set (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
      { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 })
    (fun x => x.rank) fun i => if ↑y = ↑i then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
[PROOFSTEP]
exact this.set (fun i h ↦ by rw [if_neg h.symm]) (fun h ↦ by simp [hm.rank_eq])
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h✝ : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
xy : UFModel.rank m ↑x = UFModel.rank m ↑y
i : Fin n
h : ↑i ≠ ↑{ val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
⊢ (if ↑y = ↑i then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i) = UFModel.rank m ↑i
[PROOFSTEP]
rw [if_neg h.symm]
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h✝ : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
xy : UFModel.rank m ↑x = UFModel.rank m ↑y
h : ↑{ val := ↑y, isLt := (_ : ↑y < Array.size arr₁) } < n
⊢ { parent := self.arr[↑y].parent, value := self.arr[↑y].value, rank := self.arr[↑y].rank + 1 }.rank =
    if ↑y = ↑{ val := ↑{ val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }, isLt := h } then UFModel.rank m ↑y + 1
    else UFModel.rank m ↑{ val := ↑{ val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }, isLt := h }
[PROOFSTEP]
simp [hm.rank_eq]
[GOAL]
case inr
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
xy : ¬UFModel.rank m ↑x = UFModel.rank m ↑y
⊢ UFModel.Agrees (Array.set self.arr x { parent := ↑y, value := self.arr[↑x].value, rank := self.arr[↑x].rank })
    (fun x => x.rank) fun i => UFModel.rank m ↑i
[PROOFSTEP]
exact this
[GOAL]
α : Type ?u.82096
self : UnionFind α
x y : Fin (size self)
yroot : (Array.get self.arr y).parent = ↑y
ne : ¬↑x = ↑y
nx : UFNode α := self.arr[x]
ny : UFNode α := self.arr[y]
h : ¬ny.rank < nx.rank
arr₁ : Array (UFNode α) := Array.set self.arr x { parent := ↑y, value := nx.value, rank := nx.rank }
arr₂ : Array (UFNode α) :=
  if nx.rank = ny.rank then
    Array.set arr₁ { val := ↑y, isLt := (_ : ↑y < Array.size arr₁) }
      { parent := ny.parent, value := ny.value, rank := ny.rank + 1 }
  else arr₁
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
n : ℕ := size self
parent : Fin n → ℕ := fun i => ↑(if ↑x = ↑i then y else UFModel.parent m i)
this✝ : UFModel.Agrees arr₁ (fun x => x.parent) parent
H1 : UFModel.Agrees arr₂ (fun x => x.parent) parent
this : UFModel.Agrees arr₁ (fun x => x.rank) fun i => UFModel.rank m ↑i
rank : Fin n → ℕ :=
  fun i => if ↑y = ↑i ∧ UFModel.rank m ↑x = UFModel.rank m ↑y then UFModel.rank m ↑y + 1 else UFModel.rank m ↑i
H2 : UFModel.Agrees arr₂ (fun x => x.rank) rank
⊢ UFModel.Models arr₂
    (UFModel.setParentBump m x y (_ : UFModel.rank m ↑x ≤ UFModel.rank m ↑y) (_ : ↑(UFModel.parent m y) = ↑y))
[PROOFSTEP]
exact ⟨H1, H2⟩
[GOAL]
α : Type ?u.99196
self : UnionFind α
x y : Fin (size self)
self₁ : UnionFind α
rx : Fin (size self₁)
e : size self₁ = size self
right✝ : (Array.get self₁.arr rx).parent = ↑rx
⊢ ↑y < size self₁
[PROOFSTEP]
rw [e]
[GOAL]
α : Type ?u.99196
self : UnionFind α
x y : Fin (size self)
self₁ : UnionFind α
rx : Fin (size self₁)
e : size self₁ = size self
right✝ : (Array.get self₁.arr rx).parent = ↑rx
⊢ ↑y < size self
[PROOFSTEP]
exact y.2
[GOAL]
α : Type ?u.99196
self : UnionFind α
x y : Fin (size self)
self₁ : UnionFind α
rx : Fin (size self₁)
e✝ : size self₁ = size self
right✝ : (Array.get self₁.arr rx).parent = ↑rx
self₂ : UnionFind α
ry : Fin (size self₂)
e : size self₂ = size self₁
hry : (Array.get self₂.arr ry).parent = ↑ry
⊢ ↑rx < size self₂
[PROOFSTEP]
rw [e]
[GOAL]
α : Type ?u.99196
self : UnionFind α
x y : Fin (size self)
self₁ : UnionFind α
rx : Fin (size self₁)
e✝ : size self₁ = size self
right✝ : (Array.get self₁.arr rx).parent = ↑rx
self₂ : UnionFind α
ry : Fin (size self₂)
e : size self₂ = size self₁
hry : (Array.get self₂.arr ry).parent = ↑ry
⊢ ↑rx < size self₁
[PROOFSTEP]
exact rx.2