internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.UnionFind.find_root_1
Proof state before:
self : UnionFind
x : Fin (size self)
i : Nat
a✝ :
  ∀ (y : Nat),
    (invImage (fun a => rankMax (find self x).fst - rank (find self x).fst a) instWellFoundedRelation).1 y i →
      root (find self x).fst y = root self y
h : ¬parent (find self x).fst i = i
this :
  rankMax (find self x).fst - rank (find self x).fst (parent (find self x).fst i) <
    rankMax (find self x).fst - rank (find self x).fst i
⊢ (invImage (fun a => rankMax (find self x).fst - rank (find self x).fst a) instWellFoundedRelation).1
    (parent (find self x).fst i) i
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)
hP : parentD arr' i = if ↑x = i then ↑y else parentD arr i
hR :
  ∀ {i : Nat},
    rankD arr' i =
      if ↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr i
⊢ ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i)
Tactic:
simp [hP, hR] at *
Proof state after:
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
⊢ ¬(if ↑x = i then ↑y else parentD arr i) = i →
    (if ↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr i) <
      if (↑y = if ↑x = i then ↑y else parentD arr i) ∧ (Array.get arr x).rank = (Array.get arr y).rank then
        (Array.get arr y).rank + 1
      else rankD arr (if ↑x = i then ↑y else parentD arr i)
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
⊢ ¬(if ↑x = i then ↑y else parentD arr i) = i →
    (if ↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr i) <
      if (↑y = if ↑x = i then ↑y else parentD arr i) ∧ (Array.get arr x).rank = (Array.get arr y).rank then
        (Array.get arr y).rank + 1
      else rankD arr (if ↑x = i then ↑y else parentD arr i)
Tactic:
split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
split <;> rename_i h₂ <;> intro h
Proof state after:
case inl.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬↑y = ↑x
⊢ (Array.get arr y).rank + 1 <
    if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr ↑y

case inl.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
⊢ rankD arr ↑x < if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr ↑y

case inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr i = i
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)

case inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
⊢ rankD arr i <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inl.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬↑y = ↑x
⊢ (Array.get arr y).rank + 1 <
    if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr ↑y
Tactic:
simp [h₂] at h
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inl.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
⊢ rankD arr ↑x < if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr ↑y
Tactic:
simp [rankD_eq]
Proof state after:
case inl.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
⊢ (Array.get arr x).rank <
    if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else (Array.get arr y).rank
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inl.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
⊢ (Array.get arr x).rank <
    if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else (Array.get arr y).rank
Tactic:
split <;> rename_i h₃
Proof state after:
case inl.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : (Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr y).rank + 1

case inl.inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : ¬(Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr y).rank
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inl.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : (Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr y).rank + 1
Tactic:
rw [← h₃]
Proof state after:
case inl.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : (Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr x).rank + 1
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inl.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : (Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr x).rank + 1
Tactic:
apply Nat.lt_succ_self
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inl.inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : ¬(Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr y).rank
Tactic:
exact Nat.lt_of_le_of_ne H h₃
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr i = i
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)
Tactic:
cases h₂.1
Proof state after:
case inr.inl.refl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
hP hR : True
rankD_lt : ¬parentD arr ↑y = ↑y → rankD arr ↑y < rankD arr (parentD arr ↑y)
h₁ : ¬↑x = ↑y
h₂ : ↑y = ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr ↑y = ↑y
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr ↑y)
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inr.inl.refl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
hP hR : True
rankD_lt : ¬parentD arr ↑y = ↑y → rankD arr ↑y < rankD arr (parentD arr ↑y)
h₁ : ¬↑x = ↑y
h₂ : ↑y = ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr ↑y = ↑y
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr ↑y)
Tactic:
simp [h₂.2] at hroot
Proof state after:
case inr.inl.refl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
hP hR : True
rankD_lt : ¬parentD arr ↑y = ↑y → rankD arr ↑y < rankD arr (parentD arr ↑y)
h₁ : ¬↑x = ↑y
h₂ : ↑y = ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr ↑y = ↑y
hroot : (Array.get arr y).parent = ↑y
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr ↑y)
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inr.inl.refl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
hP hR : True
rankD_lt : ¬parentD arr ↑y = ↑y → rankD arr ↑y < rankD arr (parentD arr ↑y)
h₁ : ¬↑x = ↑y
h₂ : ↑y = ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr ↑y = ↑y
hroot : (Array.get arr y).parent = ↑y
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr ↑y)
Tactic:
simp [hroot, parentD_eq] at h
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
⊢ rankD arr i <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)
Tactic:
have := rankD_lt h
Proof state after:
case inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
⊢ rankD arr i <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
⊢ rankD arr i <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)
Tactic:
split <;> rename_i h₃
Proof state after:
case inr.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank
⊢ rankD arr i < (Array.get arr y).rank + 1

case inr.inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ¬(↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
⊢ rankD arr i < rankD arr (parentD arr i)
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inr.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank
⊢ rankD arr i < (Array.get arr y).rank + 1
Tactic:
rw [← rankD_eq, h₃.1]
Proof state after:
case inr.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank
⊢ rankD arr i < rankD arr (parentD arr i) + 1
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inr.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank
⊢ rankD arr i < rankD arr (parentD arr i) + 1
Tactic:
exact Nat.lt_succ_of_lt this
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.setParentBump_rankD_lt
Proof state before:
case inr.inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get arr y).rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ¬(↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
⊢ rankD arr i < rankD arr (parentD arr i)
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.setParent_rankD_lt
Proof state before:
arr : Array UFNode
x y : Fin (Array.size arr)
h : (Array.get arr x).rank < (Array.get arr y).rank
i : Nat
rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)
⊢ ∀ {i : Nat},
    rankD (Array.set arr x { parent := ↑y, rank := (Array.get arr x).rank }) i =
      if ↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr i
Tactic:
simp [rankD_set, Nat.ne_of_lt h, rankD_eq]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.linkAux_size
Proof state before:
self : Array UFNode
x y : Fin (Array.size self)
⊢ Array.size (linkAux self x y) = Array.size self
Tactic:
simp [linkAux]
Proof state after:
self : Array UFNode
x y : Fin (Array.size self)
⊢ Array.size
      (if ↑x = ↑y then self
      else
        if (Array.get self y).rank < (Array.get self x).rank then
          Array.set self y { parent := ↑x, rank := (Array.get self y).rank }
        else
          if (Array.get self x).rank = (Array.get self y).rank then
            Array.set (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) { val := ↑y, isLt := ⋯ }
              { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }
          else Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) =
    Array.size self
Theorem: Lean4Lean.UnionFind.linkAux_size
Proof state before:
self : Array UFNode
x y : Fin (Array.size self)
⊢ Array.size
      (if ↑x = ↑y then self
      else
        if (Array.get self y).rank < (Array.get self x).rank then
          Array.set self y { parent := ↑x, rank := (Array.get self y).rank }
        else
          if (Array.get self x).rank = (Array.get self y).rank then
            Array.set (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) { val := ↑y, isLt := ⋯ }
              { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }
          else Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) =
    Array.size self
Tactic:
split <;> [rfl; split] <;> [skip; split] <;> simp
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.isDefEq_iff
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
⊢ IsDefEq env U Γ e₁ e₂ A ↔ HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
Tactic:
refine ⟨fun h => ⟨h.hasType.1, h.hasType.2, _, h⟩, fun ⟨_, h2, _, h3⟩ => ?_⟩
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
x✝ : HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
left✝ : HasType env U Γ e₁ A
h2 : HasType env U Γ e₂ A
w✝ : VExpr
h3 : IsDefEq env U Γ e₁ e₂ w✝
⊢ IsDefEq env U Γ e₁ e₂ A
Theorem: Lean4Lean.VEnv.isDefEq_iff
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
x✝ : HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
left✝ : HasType env U Γ e₁ A
h2 : HasType env U Γ e₂ A
w✝ : VExpr
h3 : IsDefEq env U Γ e₁ e₂ w✝
⊢ IsDefEq env U Γ e₁ e₂ A
Tactic:
have ⟨_, h⟩ := h3.uniq henv hΓ h2
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
x✝ : HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
left✝ : HasType env U Γ e₁ A
h2 : HasType env U Γ e₂ A
w✝¹ : VExpr
h3 : IsDefEq env U Γ e₁ e₂ w✝¹
w✝ : VLevel
h : IsDefEq env U Γ w✝¹ A (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₂ A
Theorem: Lean4Lean.VEnv.isDefEq_iff
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
x✝ : HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
left✝ : HasType env U Γ e₁ A
h2 : HasType env U Γ e₂ A
w✝¹ : VExpr
h3 : IsDefEq env U Γ e₁ e₂ w✝¹
w✝ : VLevel
h : IsDefEq env U Γ w✝¹ A (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₂ A
Tactic:
exact h.defeqDF h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.trans_r
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
⊢ IsDefEq env U Γ e₁ e₃ B
Tactic:
have ⟨_, h⟩ := h₁.uniq henv hΓ h₂
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
w✝ : VLevel
h : IsDefEq env U Γ A B (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₃ B