internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case defeqDF
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e₁✝ e₂✝ : VExpr
h1 : defEq Γ✝ A✝ B✝ (sort u✝)
a✝ : IsDefEq1 env U hasType defEq Γ✝ e₁✝ e₂✝ A✝
ih : IsDefEq env U Γ✝ e₁✝ e₂✝ A✝
⊢ IsDefEq env U Γ✝ e₁✝ e₂✝ B✝
Tactic:
exact .defeqDF (hdf h1) ih
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case beta
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
h1 : hasType (A✝ :: Γ✝) e✝ B✝
h2 : hasType Γ✝ e'✝ A✝
⊢ IsDefEq env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
exact .beta (hty h1) (hty h2)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case eta
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
h : hasType Γ✝ e✝ (forallE A✝ B✝)
⊢ IsDefEq env U Γ✝ (lam A✝ (app (lift e✝) (bvar 0))) e✝ (forallE A✝ B✝)
Tactic:
exact .eta (hty h)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case proofIrrel
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
h1 : hasType Γ✝ p✝ (sort VLevel.zero)
h2 : hasType Γ✝ h✝ p✝
h3 : hasType Γ✝ h'✝ p✝
⊢ IsDefEq env U Γ✝ h✝ h'✝ p✝
Tactic:
exact .proofIrrel (hty h1) (hty h2) (hty h3)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case extra
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
⊢ IsDefEq env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
Tactic:
exact .extra h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_push
Proof state before:
a : Nat
arr : Array UFNode
⊢ parentD (Array.push arr { parent := Array.size arr, rank := 0 }) a = parentD arr a
Tactic:
simp [parentD]
Proof state after:
a : Nat
arr : Array UFNode
⊢ (if h : a < Array.size arr + 1 then (Array.push arr { parent := Array.size arr, rank := 0 })[a].parent else a) =
    if h : a < Array.size arr then arr[a].parent else a
Theorem: Lean4Lean.UnionFind.parentD_push
Proof state before:
a : Nat
arr : Array UFNode
⊢ (if h : a < Array.size arr + 1 then (Array.push arr { parent := Array.size arr, rank := 0 })[a].parent else a) =
    if h : a < Array.size arr then arr[a].parent else a
Tactic:
split <;> split <;> try simp [Array.get_push, *]
Proof state after:
case inl.inr
a : Nat
arr : Array UFNode
h✝¹ : a < Array.size arr + 1
h✝ : ¬a < Array.size arr
⊢ Array.size arr = a

case inr.inl
a : Nat
arr : Array UFNode
h✝¹ : ¬a < Array.size arr + 1
h✝ : a < Array.size arr
⊢ a = arr[a].parent
Theorem: Lean4Lean.UnionFind.parentD_push
Proof state before:
case inr.inr
a : Nat
arr : Array UFNode
h✝¹ : ¬a < Array.size arr + 1
h✝ : ¬a < Array.size arr
⊢ a = a
Tactic:
simp [Array.get_push, *]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_push
Proof state before:
case inl.inr
a : Nat
arr : Array UFNode
h✝¹ : a < Array.size arr + 1
h✝ : ¬a < Array.size arr
⊢ Array.size arr = a
Tactic:
next h1 h2 =>
simp [Nat.lt_succ] at h1 h2
exact Nat.le_antisymm h2 h1
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_push
Proof state before:
a : Nat
arr : Array UFNode
h1 : a < Array.size arr + 1
h2 : ¬a < Array.size arr
⊢ Array.size arr = a
Tactic:
simp [Nat.lt_succ] at h1 h2
Proof state after:
a : Nat
arr : Array UFNode
h1 : a ≤ Array.size arr
h2 : Array.size arr ≤ a
⊢ Array.size arr = a
Theorem: Lean4Lean.UnionFind.parentD_push
Proof state before:
a : Nat
arr : Array UFNode
h1 : a ≤ Array.size arr
h2 : Array.size arr ≤ a
⊢ Array.size arr = a
Tactic:
exact Nat.le_antisymm h2 h1
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_push
Proof state before:
case inr.inl
a : Nat
arr : Array UFNode
h✝¹ : ¬a < Array.size arr + 1
h✝ : a < Array.size arr
⊢ a = arr[a].parent
Tactic:
next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_push
Proof state before:
a : Nat
arr : Array UFNode
h1 : ¬a < Array.size arr + 1
h2 : a < Array.size arr
⊢ a = arr[a].parent
Tactic:
cases h1 (Nat.lt_succ_of_lt h2)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parent_push
Proof state before:
a : Nat
m : UnionFind
⊢ parent (push m) a = parent m a
Tactic:
simp [parent]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_push
Proof state before:
a : Nat
arr : Array UFNode
⊢ rankD (Array.push arr { parent := Array.size arr, rank := 0 }) a = rankD arr a
Tactic:
simp [rankD]
Proof state after:
a : Nat
arr : Array UFNode
⊢ (if h : a < Array.size arr + 1 then (Array.push arr { parent := Array.size arr, rank := 0 })[a].rank else 0) =
    if h : a < Array.size arr then arr[a].rank else 0
Theorem: Lean4Lean.UnionFind.rankD_push
Proof state before:
a : Nat
arr : Array UFNode
⊢ (if h : a < Array.size arr + 1 then (Array.push arr { parent := Array.size arr, rank := 0 })[a].rank else 0) =
    if h : a < Array.size arr then arr[a].rank else 0
Tactic:
split <;> split <;> try simp [Array.get_push, *]
Proof state after:
case inr.inl
a : Nat
arr : Array UFNode
h✝¹ : ¬a < Array.size arr + 1
h✝ : a < Array.size arr
⊢ 0 = arr[a].rank
Theorem: Lean4Lean.UnionFind.rankD_push
Proof state before:
case inr.inl
a : Nat
arr : Array UFNode
h✝¹ : ¬a < Array.size arr + 1
h✝ : a < Array.size arr
⊢ 0 = arr[a].rank
Tactic:
next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_push
Proof state before:
case inr.inr
a : Nat
arr : Array UFNode
h✝¹ : ¬a < Array.size arr + 1
h✝ : ¬a < Array.size arr
⊢ 0 = 0
Tactic:
simp [Array.get_push, *]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_push
Proof state before:
a : Nat
arr : Array UFNode
h1 : ¬a < Array.size arr + 1
h2 : a < Array.size arr
⊢ 0 = arr[a].rank
Tactic:
cases h1 (Nat.lt_succ_of_lt h2)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rank_push
Proof state before:
a : Nat
m : UnionFind
⊢ rank (push m) a = rank m a
Tactic:
simp [rank]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankMax_push
Proof state before:
m : UnionFind
⊢ rankMax (push m) = rankMax m
Tactic:
simp [rankMax]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_linkAux
Proof state before:
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
⊢ parentD (linkAux self x y) i =
    if ↑x = ↑y then parentD self i
    else
      if (Array.get self y).rank < (Array.get self x).rank then if ↑y = i then ↑x else parentD self i
      else if ↑x = i then ↑y else parentD self i
Tactic:
dsimp [linkAux]
Proof state after:
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
⊢ parentD
      (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 })
      i =
    if ↑x = ↑y then parentD self i
    else
      if (Array.get self y).rank < (Array.get self x).rank then if ↑y = i then ↑x else parentD self i
      else if ↑x = i then ↑y else parentD self i
Theorem: Lean4Lean.UnionFind.parentD_linkAux
Proof state before:
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
⊢ parentD
      (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 })
      i =
    if ↑x = ↑y then parentD self i
    else
      if (Array.get self y).rank < (Array.get self x).rank then if ↑y = i then ↑x else parentD self i
      else if ↑x = i then ↑y else parentD self i
Tactic:
split <;> [rfl; split] <;> [rw [parentD_set]; split] <;> rw [parentD_set]
Proof state after:
case inr.inr.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (if ↑{ val := ↑y, isLt := ⋯ } = i then
      { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }.parent
    else parentD (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) i) =
    if ↑x = i then ↑y else parentD self i
Theorem: Lean4Lean.UnionFind.parentD_linkAux
Proof state before:
case inr.inr.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (if ↑{ val := ↑y, isLt := ⋯ } = i then
      { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }.parent
    else parentD (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) i) =
    if ↑x = i then ↑y else parentD self i
Tactic:
simp
Proof state after:
case inr.inr.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (if ↑y = i then (Array.get self y).parent
    else parentD (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) i) =
    if ↑x = i then ↑y else parentD self i
Theorem: Lean4Lean.UnionFind.parentD_linkAux
Proof state before:
case inr.inr.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (if ↑y = i then (Array.get self y).parent
    else parentD (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) i) =
    if ↑x = i then ↑y else parentD self i
Tactic:
split <;> [(subst i; rwa [if_neg, parentD_eq]); rw [parentD_set]]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_linkAux
Proof state before:
case inr.inr.inl.inl
i : Nat
self : Array UFNode
x y : Fin (Array.size self)
h✝³ : ¬↑x = ↑y
h✝² : ¬(Array.get self y).rank < (Array.get self x).rank
h✝¹ : (Array.get self x).rank = (Array.get self y).rank
h✝ : ↑y = i
⊢ (Array.get self y).parent = if ↑x = i then ↑y else parentD self i
Tactic:
subst i
Proof state after:
case inr.inr.inl.inl
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (Array.get self y).parent = if ↑x = ↑y then ↑y else parentD self ↑y
Theorem: Lean4Lean.UnionFind.parentD_linkAux
Proof state before:
case inr.inr.inl.inl
self : Array UFNode
x y : Fin (Array.size self)
h✝² : ¬↑x = ↑y
h✝¹ : ¬(Array.get self y).rank < (Array.get self x).rank
h✝ : (Array.get self x).rank = (Array.get self y).rank
⊢ (Array.get self y).parent = if ↑x = ↑y then ↑y else parentD self ↑y
Tactic:
rwa [if_neg, parentD_eq]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parent_link
Proof state before:
self : UnionFind
x y : Fin (size self)
yroot : parent self ↑y = ↑y
i : Nat
⊢ parent (link self x y yroot) i =
    if ↑x = ↑y then parent self i
    else
      if rank self ↑y < rank self ↑x then if ↑y = i then ↑x else parent self i else if ↑x = i then ↑y else parent self i
Tactic:
simp [rankD_eq]
Proof state after:
self : UnionFind
x y : Fin (size self)
yroot : parent self ↑y = ↑y
i : Nat
⊢ parent (link self x y yroot) i =
    if ↑x = ↑y then parent self i
    else
      if (Array.get self.arr y).rank < (Array.get self.arr x).rank then if ↑y = i then ↑x else parent self i
      else if ↑x = i then ↑y else parent self i
Theorem: Lean4Lean.UnionFind.parent_link
Proof state before:
self : UnionFind
x y : Fin (size self)
yroot : parent self ↑y = ↑y
i : Nat
⊢ parent (link self x y yroot) i =
    if ↑x = ↑y then parent self i
    else
      if (Array.get self.arr y).rank < (Array.get self.arr x).rank then if ↑y = i then ↑x else parent self i
      else if ↑x = i then ↑y else parent self i
Tactic:
exact parentD_linkAux
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
⊢ ∃ r,
    (r = x ∨ r = y) ∧
      ∀ (i : Nat), root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
Tactic:
refine ⟨x, .inl rfl, fun i => ?_⟩
Proof state after:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [root_ext (m2 := self) (fun _ => by rw [parent_link, if_pos h])]
Proof state after:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ root self i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i : Nat
⊢ root self i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
split <;> [obtain _ | _ := ‹_› <;> simp [*]; rfl]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ↑x = ↑y
i x✝ : Nat
⊢ parent (link self x y yroot) x✝ = parent self x✝
Tactic:
rw [parent_link, if_pos h]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
h : ¬↑x = ↑y
this :
  ∀ {x y : Fin (size self)},
    parent self ↑x = ↑x →
      parent self ↑y = ↑y →
        ∀ {m : UnionFind},
          (∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i) →
            ∃ r,
              (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
⊢ ∃ r,
    (r = x ∨ r = y) ∧
      ∀ (i : Nat), root (link self x y yroot) i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
Tactic:
if hr : self.rank y < self.rank x then
  exact this xroot yroot fun i => by simp [parent_link, h, hr]
else
  simpa (config := {singlePass := true}) [or_comm] using
    this yroot xroot fun i => by simp [parent_link, h, hr]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
⊢ ∃ r, (r = x ∨ r = y) ∧ ∀ (i : Nat), root m i = if root self i = ↑x ∨ root self i = ↑y then ↑r else root self i
Tactic:
exact ⟨x, .inl rfl, go⟩
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : parent m i = i
⊢ root m i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [root_eq_self.2 h]
Proof state after:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : parent m i = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : parent m i = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [hm i] at h
Proof state after:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : (if ↑y = i then ↑x else parent self i) = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h : (if ↑y = i then ↑x else parent self i) = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
split at h
Proof state after:
case inl
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i

case inr
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
case inl
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [if_pos, h]
Proof state after:
case inl.hc
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ root self i = ↑x ∨ root self i = ↑y
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
case inl.hc
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ↑y = i
h : ↑x = i
⊢ root self i = ↑x ∨ root self i = ↑y
Tactic:
simp [← h, root_eq_self, xroot]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
case inr
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
⊢ i = if root self i = ↑x ∨ root self i = ↑y then ↑x else root self i
Tactic:
rw [root_eq_self.2 ‹_›]
Proof state after:
case inr
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
⊢ i = if i = ↑x ∨ i = ↑y then ↑x else i
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
case inr
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
⊢ i = if i = ↑x ∨ i = ↑y then ↑x else i
Tactic:
split <;> [skip; rfl]
Proof state after:
case inr.inl
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝² : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝¹ : ¬↑y = i
h : parent self i = i
h✝ : i = ↑x ∨ i = ↑y
⊢ i = ↑x
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
case inr.inl
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝² : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝¹ : ¬↑y = i
h : parent self i = i
h✝ : i = ↑x ∨ i = ↑y
⊢ i = ↑x
Tactic:
next h' => exact h'.resolve_right (Ne.symm ‹_›)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.root_link
Proof state before:
self : UnionFind
x✝ y✝ : Fin (size self)
xroot✝ : parent self ↑x✝ = ↑x✝
yroot✝ : parent self ↑y✝ = ↑y✝
h✝¹ : ¬↑x✝ = ↑y✝
x y : Fin (size self)
xroot : parent self ↑x = ↑x
yroot : parent self ↑y = ↑y
m : UnionFind
hm : ∀ (i : Nat), parent m i = if ↑y = i then ↑x else parent self i
i : Nat
h✝ : ¬↑y = i
h : parent self i = i
h' : i = ↑x ∨ i = ↑y
⊢ i = ↑x
Tactic:
exact h'.resolve_right (Ne.symm ‹_›)
Proof state after:
no goals