internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastVar.go_eq_eval_getLsb
Proof state before:
case inr
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ ⟦{
        aig :=
          (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯).aig,
        ref :=
          (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
                  ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯).stream.getRef
            idx hidx1 },
      assign.toAIGAssignment⟧ =
    (eval assign (var a)).getLsb idx
Tactic:
dsimp
Proof state after:
case inr
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ ⟦{
        aig :=
          (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯).aig,
        ref :=
          (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
                  ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯).stream.getRef
            idx hidx1 },
      assign.toAIGAssignment⟧ =
    (BitVec.truncate w (assign.getD a).bv).getLsb idx
Theorem: BVExpr.bitblast.blastVar.go_eq_eval_getLsb
Proof state before:
case inr
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ ⟦{
        aig :=
          (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
              ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯).aig,
        ref :=
          (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
                  ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯).stream.getRef
            idx hidx1 },
      assign.toAIGAssignment⟧ =
    (BitVec.truncate w (assign.getD a).bv).getLsb idx
Tactic:
rw [go_eq_eval_getLsb]
Proof state after:
case inr
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ (eval assign (var a)).getLsb idx = (BitVec.truncate w (assign.getD a).bv).getLsb idx

case inr.a
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ curr + 1 ≤ idx
Theorem: BVExpr.bitblast.blastVar.go_eq_eval_getLsb
Proof state before:
case inr
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ (eval assign (var a)).getLsb idx = (BitVec.truncate w (assign.getD a).bv).getLsb idx

case inr.a
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ curr + 1 ≤ idx
Tactic:
. simp
Proof state after:
case inr.a
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ curr + 1 ≤ idx
Theorem: BVExpr.bitblast.blastVar.go_eq_eval_getLsb
Proof state before:
case inr.a
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ curr + 1 ≤ idx
Tactic:
. omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_eq_eval_getLsb
Proof state before:
case inr
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ (eval assign (var a)).getLsb idx = (BitVec.truncate w (assign.getD a).bv).getLsb idx
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_eq_eval_getLsb
Proof state before:
case inr.a
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
hlt : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, hlt⟩)).ref) a ⋯ =
    res
h✝ : curr < idx
⊢ curr + 1 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar.go_eq_eval_getLsb
Proof state before:
case isFalse
w : Nat
aig : AIG BVBit
a : Nat
assign : Assignment
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx1 : idx < w
hidx2 : curr ≤ idx
res : RefStreamEntry BVBit w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx1 }, assign.toAIGAssignment⟧ = (eval assign (var a)).getLsb idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastVar_eq_eval_getLsb
Proof state before:
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := (blastVar aig var).aig, ref := (blastVar aig var).stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
      (eval assign (BVExpr.var var.ident)).getLsb idx
Tactic:
intros
Proof state after:
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastVar aig var).aig, ref := (blastVar aig var).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign (BVExpr.var var.ident)).getLsb idx✝
Theorem: BVExpr.bitblast.blastVar_eq_eval_getLsb
Proof state before:
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦{ aig := (blastVar aig var).aig, ref := (blastVar aig var).stream.getRef idx✝ hidx✝ }, assign.toAIGAssignment⟧ =
    (eval assign (BVExpr.var var.ident)).getLsb idx✝
Tactic:
apply blastVar.go_eq_eval_getLsb
Proof state after:
case a
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Theorem: BVExpr.bitblast.blastVar_eq_eval_getLsb
Proof state before:
case a
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝
Tactic:
omega
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2
Proof state before:
⊢ ∀ (x C1 C : BitVec 64), x ^^^ C1 ||| C = (x ||| C) ^^^ C1 &&& ~~~C
Tactic:
intros
Proof state after:
x✝ C1✝ C✝ : BitVec 64
⊢ x✝ ^^^ C1✝ ||| C✝ = (x✝ ||| C✝) ^^^ C1✝ &&& ~~~C✝
Theorem: bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2
Proof state before:
x✝ C1✝ C✝ : BitVec 64
⊢ x✝ ^^^ C1✝ ||| C✝ = (x✝ ||| C✝) ^^^ C1✝ &&& ~~~C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2284
Proof state before:
⊢ ∀ (A B : BitVec 64), A ||| (A ||| B) ^^^ -1 = A ||| B ^^^ -1
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ A✝ ||| (A✝ ||| B✝) ^^^ -1 = A✝ ||| B✝ ^^^ -1
Theorem: bitvec_AndOrXor_2284
Proof state before:
A✝ B✝ : BitVec 64
⊢ A✝ ||| (A✝ ||| B✝) ^^^ -1 = A✝ ||| B✝ ^^^ -1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2113___A__B__A___A__B
Proof state before:
⊢ ∀ (A B : BitVec 64), (A ^^^ -1) &&& B ||| A = A ||| B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ (A✝ ^^^ -1) &&& B✝ ||| A✝ = A✝ ||| B✝
Theorem: bitvec_AndOrXor_2113___A__B__A___A__B
Proof state before:
A✝ B✝ : BitVec 64
⊢ (A✝ ^^^ -1) &&& B✝ ||| A✝ = A✝ ||| B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__422_2
Proof state before:
⊢ ∀ (Y X C : BitVec 31), (Y + X.sshiftRight C.toNat) <<< C = Y <<< C + X &&& (-1) <<< C
Tactic:
intros
Proof state after:
Y✝ X✝ C✝ : BitVec 31
⊢ (Y✝ + X✝.sshiftRight C✝.toNat) <<< C✝ = Y✝ <<< C✝ + X✝ &&& (-1) <<< C✝
Theorem: bitvec_InstCombineShift__422_2
Proof state before:
Y✝ X✝ C✝ : BitVec 31
⊢ (Y✝ + X✝.sshiftRight C✝.toNat) <<< C✝ = Y✝ <<< C✝ + X✝ &&& (-1) <<< C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
⊢ s.fst = s'.fst → s = s'
Tactic:
intro keys_eq
Proof state after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
⊢ s = s'
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
⊢ s = s'
Tactic:
have goal_rw : (s = s') = (s.1 = s'.1 ∧ s.2 = s'.2) := by
  have s_rw : s = (s.1, s.2) := rfl
  have s'_rw : s' = (s'.1, s'.2) := rfl
  rw [s_rw, s'_rw]
  simp only [Prod.mk.injEq]
Proof state after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s = s'
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s = s'
Tactic:
rw [goal_rw]
Proof state after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst ∧ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst ∧ s.snd = s'.snd
Tactic:
constructor
Proof state after:
case left
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst

case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case left
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst

case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd
Tactic:
. exact keys_eq
Proof state after:
case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd
Tactic:
. induction l with
  | nil => exact False.elim $ List.not_mem_nil s h
  | cons hd tl ih =>
    rw [List.Nodupkeys, List.Nodup, List.Pairwise_iff] at nd
    simp only [List.map_eq_nil, ne_eq] at nd
    rcases nd with l_eq_nil | ⟨a, l', nd⟩
    . exact False.elim l_eq_nil
    . rw [List.Nodupkeys, List.Nodup] at ih
      rcases nd with ⟨nd1, nd2, nd3⟩
      rw [List.map_cons] at nd3
      simp only [List.cons.injEq] at nd3
      rcases nd3 with ⟨hd_fst_eq_a, nd3⟩
      rw [← nd3] at nd2
      specialize ih nd2
      rw [List.mem_cons] at h h'
      rcases h with s_eq_hd | s_in_tl
      . rcases h' with s'_eq_hd | s'_in_tl
        . rw [s_eq_hd, s'_eq_hd]
        . rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
          specialize nd1 s'.1
          simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
            forall_exists_index] at nd1
          specialize nd1 s'.2 s'_in_tl
          exfalso
          exact nd1 keys_eq
      . rcases h' with s'_eq_hd | s'_in_tl
        . rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
          specialize nd1 s.1
          simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
            forall_exists_index] at nd1
          specialize nd1 s.2 s_in_tl
          exfalso
          exact nd1 keys_eq.symm
        . exact ih s_in_tl s'_in_tl
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
Tactic:
have s_rw : s = (s.1, s.2) := rfl
Proof state after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
Tactic:
have s'_rw : s' = (s'.1, s'.2) := rfl
Proof state after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
s'_rw : s' = (s'.fst, s'.snd)
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
s'_rw : s' = (s'.fst, s'.snd)
⊢ (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
Tactic:
rw [s_rw, s'_rw]
Proof state after:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
s'_rw : s' = (s'.fst, s'.snd)
⊢ ((s.fst, s.snd) = (s'.fst, s'.snd)) =
    ((s.fst, s.snd).fst = (s'.fst, s'.snd).fst ∧ (s.fst, s.snd).snd = (s'.fst, s'.snd).snd)
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
s_rw : s = (s.fst, s.snd)
s'_rw : s' = (s'.fst, s'.snd)
⊢ ((s.fst, s.snd) = (s'.fst, s'.snd)) =
    ((s.fst, s.snd).fst = (s'.fst, s'.snd).fst ∧ (s.fst, s.snd).snd = (s'.fst, s'.snd).snd)
Tactic:
simp only [Prod.mk.injEq]
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case left
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.fst = s'.fst
Tactic:
exact keys_eq
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right
α : Type u_1
β : Type u_2
l : List (α × β)
nd : l.Nodupkeys
s s' : α × β
h : s ∈ l
h' : s' ∈ l
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
⊢ s.snd = s'.snd
Tactic:
induction l with
| nil => exact False.elim $ List.not_mem_nil s h
| cons hd tl ih =>
  rw [List.Nodupkeys, List.Nodup, List.Pairwise_iff] at nd
  simp only [List.map_eq_nil, ne_eq] at nd
  rcases nd with l_eq_nil | ⟨a, l', nd⟩
  . exact False.elim l_eq_nil
  . rw [List.Nodupkeys, List.Nodup] at ih
    rcases nd with ⟨nd1, nd2, nd3⟩
    rw [List.map_cons] at nd3
    simp only [List.cons.injEq] at nd3
    rcases nd3 with ⟨hd_fst_eq_a, nd3⟩
    rw [← nd3] at nd2
    specialize ih nd2
    rw [List.mem_cons] at h h'
    rcases h with s_eq_hd | s_in_tl
    . rcases h' with s'_eq_hd | s'_in_tl
      . rw [s_eq_hd, s'_eq_hd]
      . rw [← nd3, ← hd_fst_eq_a, ← s_eq_hd] at nd1
        specialize nd1 s'.1
        simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
          forall_exists_index] at nd1
        specialize nd1 s'.2 s'_in_tl
        exfalso
        exact nd1 keys_eq
    . rcases h' with s'_eq_hd | s'_in_tl
      . rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
        specialize nd1 s.1
        simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
          forall_exists_index] at nd1
        specialize nd1 s.2 s_in_tl
        exfalso
        exact nd1 keys_eq.symm
      . exact ih s_in_tl s'_in_tl
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.nil
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
nd : [].Nodupkeys
h : s ∈ []
h' : s' ∈ []
⊢ s.snd = s'.snd
Tactic:
exact False.elim $ List.not_mem_nil s h
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
nd : (hd :: tl).Nodupkeys
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
⊢ s.snd = s'.snd
Tactic:
rw [List.Nodupkeys, List.Nodup, List.Pairwise_iff] at nd
Proof state after:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
nd :
  map (fun x => x.fst) (hd :: tl) = [] ∨
    Exists fun {a} =>
      Exists fun {l'} =>
        (∀ (a' : α), a' ∈ l' → a ≠ a') ∧ Pairwise (fun x x_1 => x ≠ x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
nd :
  map (fun x => x.fst) (hd :: tl) = [] ∨
    Exists fun {a} =>
      Exists fun {l'} =>
        (∀ (a' : α), a' ∈ l' → a ≠ a') ∧ Pairwise (fun x x_1 => x ≠ x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
⊢ s.snd = s'.snd
Tactic:
simp only [List.map_eq_nil, ne_eq] at nd
Proof state after:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
nd :
  False ∨
    Exists fun {a} =>
      Exists fun {l'} =>
        (∀ (a' : α), a' ∈ l' → ¬a = a') ∧
          Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
nd :
  False ∨
    Exists fun {a} =>
      Exists fun {l'} =>
        (∀ (a' : α), a' ∈ l' → ¬a = a') ∧
          Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Tactic:
rcases nd with l_eq_nil | ⟨a, l', nd⟩
Proof state after:
case right.cons.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
l_eq_nil : False
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
l_eq_nil : False
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd
Tactic:
. exact False.elim l_eq_nil
Proof state after:
case right.cons.inr.intro.intro
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
ih : tl.Nodupkeys → s ∈ tl → s' ∈ tl → s.snd = s'.snd
h : s ∈ hd :: tl
h' : s' ∈ hd :: tl
a : α
l' : List α
nd : (∀ (a' : α), a' ∈ l' → ¬a = a') ∧ Pairwise (fun x x_1 => ¬x = x_1) l' ∧ map (fun x => x.fst) (hd :: tl) = a :: l'
⊢ s.snd = s'.snd