internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
W : VLCtx.LiftN Δ ((some { name := NameGenerator.curr ngen }, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Tactic:
refine ⟨fun P hP => h1 _ hP.2, ?_⟩
Proof state after:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
W : VLCtx.LiftN Δ ((some { name := NameGenerator.curr ngen }, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ ∃ e' A',
    TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e e' ∧
      TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) A A' ∧
        HasType env (List.length Us) (VLCtx.toCtx ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e' A'
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
W : VLCtx.LiftN Δ ((some { name := NameGenerator.curr ngen }, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ ∃ e' A',
    TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e e' ∧
      TrExpr env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) A A' ∧
        HasType env (List.length Us) (VLCtx.toCtx ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e' A'
Tactic:
exact ⟨_, _, h2.weakN henv W hΔ, h3.weakN henv W hΔ, h4.weakN henv W.toCtx⟩
Proof state after:
no goals
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∀ (fv : FVarId),
    fv ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ) →
      NameGenerator.Reserves ngen fv → fv ∈ VLCtx.fvars Δ
Tactic:
intro _ h1 h2
Proof state after:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h1 : fv✝ ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)
h2 : NameGenerator.Reserves ngen fv✝
⊢ fv✝ ∈ VLCtx.fvars Δ
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h1 : fv✝ ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)
h2 : NameGenerator.Reserves ngen fv✝
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
simp at h1
Proof state after:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ = { name := NameGenerator.curr ngen } ∨ fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ = { name := NameGenerator.curr ngen } ∨ fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
rcases h1 with rfl | h1
Proof state after:
case refine_1.inl
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h2 : NameGenerator.Reserves ngen { name := NameGenerator.curr ngen }
⊢ { name := NameGenerator.curr ngen } ∈ VLCtx.fvars Δ

case refine_1.inr
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
case refine_1.inl
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h2 : NameGenerator.Reserves ngen { name := NameGenerator.curr ngen }
⊢ { name := NameGenerator.curr ngen } ∈ VLCtx.fvars Δ
Tactic:
cases Nat.lt_irrefl _ (h2 _ rfl)
Proof state after:
no goals
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
case refine_1.inr
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
fv✝ : FVarId
h2 : NameGenerator.Reserves ngen fv✝
h1 : fv✝ ∈ VLCtx.fvars Δ
⊢ fv✝ ∈ VLCtx.fvars Δ
Tactic:
exact h1
Proof state after:
no goals
Theorem: Lean.PersistentArray.size_push
Proof state before:
α : Type u_1
arr : PersistentArray α
x : α
⊢ (push arr x).size = arr.size + 1
Tactic:
simp [push]
Proof state after:
α : Type u_1
arr : PersistentArray α
x : α
⊢ (if Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size then
        { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
          tailOff := arr.tailOff }
      else
        mkNewTail
          { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
            tailOff := arr.tailOff }).size =
    arr.size + 1
Theorem: Lean.PersistentArray.size_push
Proof state before:
α : Type u_1
arr : PersistentArray α
x : α
⊢ (if Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size then
        { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
          tailOff := arr.tailOff }
      else
        mkNewTail
          { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
            tailOff := arr.tailOff }).size =
    arr.size + 1
Tactic:
split <;> [rfl; (simp [mkNewTail]; split <;> rfl)]
Proof state after:
no goals
Theorem: Lean.PersistentArray.size_push
Proof state before:
case inr
α : Type u_1
arr : PersistentArray α
x : α
h✝ : ¬(Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size)
⊢ (mkNewTail
        { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
          tailOff := arr.tailOff }).size =
    arr.size + 1
Tactic:
simp [mkNewTail]
Proof state after:
case inr
α : Type u_1
arr : PersistentArray α
x : α
h✝ : ¬(Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size)
⊢ (if arr.size + 1 ≤ USize.toNat (mul2Shift 1 (arr.shift + initShift)) then
        { root := insertNewLeaf arr.root (USize.ofNat arr.size) arr.shift (Array.push arr.tail x), tail := mkEmptyArray,
          size := arr.size + 1, shift := arr.shift, tailOff := arr.size + 1 }
      else
        {
          root :=
            PersistentArrayNode.node
              (Array.push (Array.push mkEmptyArray arr.root) (mkNewPath arr.shift (Array.push arr.tail x))),
          tail := #[], size := arr.size + 1, shift := arr.shift + initShift, tailOff := arr.size + 1 }).size =
    arr.size + 1
Theorem: Lean.PersistentArray.size_push
Proof state before:
case inr
α : Type u_1
arr : PersistentArray α
x : α
h✝ : ¬(Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size)
⊢ (if arr.size + 1 ≤ USize.toNat (mul2Shift 1 (arr.shift + initShift)) then
        { root := insertNewLeaf arr.root (USize.ofNat arr.size) arr.shift (Array.push arr.tail x), tail := mkEmptyArray,
          size := arr.size + 1, shift := arr.shift, tailOff := arr.size + 1 }
      else
        {
          root :=
            PersistentArrayNode.node
              (Array.push (Array.push mkEmptyArray arr.root) (mkNewPath arr.shift (Array.push arr.tail x))),
          tail := #[], size := arr.size + 1, shift := arr.shift + initShift, tailOff := arr.size + 1 }).size =
    arr.size + 1
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: Lean.PersistentArray.WF.toList'_length
Proof state before:
α✝ : Type u_1
arr : PersistentArray α✝
h : WF arr
⊢ List.length (toList' arr) = arr.size
Tactic:
induction h <;> simp [*]
Proof state after:
no goals
Theorem: Lean.PersistentHashMap.toList'_empty
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ toList' empty = []
Tactic:
have this n : @Node.toList' α β (.entries ⟨.replicate n .null⟩) = [] := by
  simp [Node.toList']
  induction n <;> simp [*]
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
this : ∀ (n : Nat), Node.toList' (Node.entries { data := List.replicate n Entry.null }) = []
⊢ toList' empty = []
Theorem: Lean.PersistentHashMap.toList'_empty
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
this : ∀ (n : Nat), Node.toList' (Node.entries { data := List.replicate n Entry.null }) = []
⊢ toList' empty = []
Tactic:
apply this
Proof state after:
no goals
Theorem: Lean.PersistentHashMap.toList'_empty
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
⊢ Node.toList' (Node.entries { data := List.replicate n Entry.null }) = []
Tactic:
simp [Node.toList']
Proof state after:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
⊢ Node.rec_2 (fun x => id) (fun ks xs x => List.zip ks.data xs.data) (fun x => id) [] (fun x x l1 l2 => l1 ++ l2)
      (fun a b => [(a, b)]) (fun x => id) [] (List.replicate n Entry.null) =
    []
Theorem: Lean.PersistentHashMap.toList'_empty
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
⊢ Node.rec_2 (fun x => id) (fun ks xs x => List.zip ks.data xs.data) (fun x => id) [] (fun x x l1 l2 => l1 ++ l2)
      (fun a b => [(a, b)]) (fun x => id) [] (List.replicate n Entry.null) =
    []
Tactic:
induction n <;> simp [*]
Proof state after:
no goals
Theorem: Lean.PersistentHashMap.WF.nodupKeys
Proof state before:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m : PersistentHashMap α β
h : WF m
⊢ List.NodupKeys (toList' m)
Tactic:
induction h with
| empty => simp; exact .nil
| insert h1 h2 ih =>
  rw [h2.find?_eq] at h1
  refine (h2.toList'_insert _ _ h1).nodupKeys_iff.2 (List.nodupKeys_cons.2 ⟨?_, ih⟩)
  rintro ⟨a, b⟩ h3 rfl
  cases h1.symm.trans (ih.lookup_eq_some.2 h3)
Proof state after:
no goals
Theorem: Lean.PersistentHashMap.WF.nodupKeys
Proof state before:
case empty
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m : PersistentHashMap α β
⊢ List.NodupKeys (toList' PersistentHashMap.empty)
Tactic:
simp
Proof state after:
case empty
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m : PersistentHashMap α β
⊢ List.NodupKeys []
Theorem: Lean.PersistentHashMap.WF.nodupKeys
Proof state before:
case empty
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m : PersistentHashMap α β
⊢ List.NodupKeys []
Tactic:
exact .nil
Proof state after:
no goals
Theorem: Lean.PersistentHashMap.WF.nodupKeys
Proof state before:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : find? m✝ a✝ = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ List.NodupKeys (toList' (PersistentHashMap.insert m✝ a✝ b✝))
Tactic:
rw [h2.find?_eq] at h1
Proof state after:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ List.NodupKeys (toList' (PersistentHashMap.insert m✝ a✝ b✝))
Theorem: Lean.PersistentHashMap.WF.nodupKeys
Proof state before:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ List.NodupKeys (toList' (PersistentHashMap.insert m✝ a✝ b✝))
Tactic:
refine (h2.toList'_insert _ _ h1).nodupKeys_iff.2 (List.nodupKeys_cons.2 ⟨?_, ih⟩)
Proof state after:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ ∀ (a' : α × β), a' ∈ toList' m✝ → (a✝, b✝).fst ≠ a'.fst
Theorem: Lean.PersistentHashMap.WF.nodupKeys
Proof state before:
case insert
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
⊢ ∀ (a' : α × β), a' ∈ toList' m✝ → (a✝, b✝).fst ≠ a'.fst
Tactic:
rintro ⟨a, b⟩ h3 rfl
Proof state after:
case insert.mk
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
b : β
h3 : ((a✝, b✝).fst, b) ∈ toList' m✝
⊢ False
Theorem: Lean.PersistentHashMap.WF.nodupKeys
Proof state before:
case insert.mk
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
inst✝ : Std.HashMap.LawfulHashable α
m m✝ : PersistentHashMap α β
a✝ : α
b✝ : β
h1 : List.lookup a✝ (toList' m✝) = none
h2 : WF m✝
ih : List.NodupKeys (toList' m✝)
b : β
h3 : ((a✝, b✝).fst, b) ∈ toList' m✝
⊢ False
Tactic:
cases h1.symm.trans (ih.lookup_eq_some.2 h3)
Proof state after:
no goals
Theorem: Array.ext_iff
Proof state before:
α : Type u_1
as bs : Array α
⊢ as = bs ↔ as.data = bs.data
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
as bs : Array α
⊢ as = bs → as.data = bs.data

case mpr
α : Type u_1
as bs : Array α
⊢ as.data = bs.data → as = bs
Theorem: Array.ext_iff
Proof state before:
case mp
α : Type u_1
as bs : Array α
⊢ as = bs → as.data = bs.data

case mpr
α : Type u_1
as bs : Array α
⊢ as.data = bs.data → as = bs
Tactic:
. intro eq
  simp only [eq]
Proof state after:
case mpr
α : Type u_1
as bs : Array α
⊢ as.data = bs.data → as = bs
Theorem: Array.ext_iff
Proof state before:
case mpr
α : Type u_1
as bs : Array α
⊢ as.data = bs.data → as = bs
Tactic:
. intro eq
  exact Array.ext' eq
Proof state after:
no goals
Theorem: List.modifyLast_singleton
Proof state before:
α : Type u_1
f : α → α
a : α
⊢ modifyLast f [a] = [f a]
Tactic:
rw [← nil_append [a], modifyLast_append_one, nil_append]
Proof state after:
no goals
Theorem: String.toNatAux_accumulates
Proof state before:
s : List Char
accum : ℕ
⊢ toNatAux s accum = toNatAux s 0 + accum * 10 ^ List.length s
Tactic:
induction s generalizing accum with
| nil => unfold toNatAux; simp
| cons head tail ih =>
  unfold toNatAux
  rw [ih]
  conv => right; rw [ih]
  simp [Nat.succ_eq_add_one]
  ring
Proof state after:
no goals
Theorem: String.toNatAux_accumulates
Proof state before:
case nil
accum : ℕ
⊢ toNatAux [] accum = toNatAux [] 0 + accum * 10 ^ List.length []
Tactic:
unfold toNatAux
Proof state after:
case nil
accum : ℕ
⊢ accum = 0 + accum * 10 ^ List.length []
Theorem: String.toNatAux_accumulates
Proof state before:
case nil
accum : ℕ
⊢ accum = 0 + accum * 10 ^ List.length []
Tactic:
simp
Proof state after:
no goals
Theorem: String.toNatAux_accumulates
Proof state before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux (head :: tail) accum = toNatAux (head :: tail) 0 + accum * 10 ^ List.length (head :: tail)
Tactic:
unfold toNatAux
Proof state after:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) =
    toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) + accum * 10 ^ List.length (head :: tail)
Theorem: String.toNatAux_accumulates
Proof state before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) =
    toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) + accum * 10 ^ List.length (head :: tail)
Tactic:
rw [ih]
Proof state after:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) + accum * 10 ^ List.length (head :: tail)
Theorem: String.toNatAux_accumulates
Proof state before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) + accum * 10 ^ List.length (head :: tail)
Tactic:
conv => right; rw [ih]
Proof state after:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail 0 + (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail +
      accum * 10 ^ List.length (head :: tail)
Theorem: String.toNatAux_accumulates
Proof state before:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail 0 + (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail +
      accum * 10 ^ List.length (head :: tail)
Tactic:
simp [Nat.succ_eq_add_one]
Proof state after:
case cons
head : Char
tail : List Char
ih : ∀ (accum : ℕ), toNatAux tail accum = toNatAux tail 0 + accum * 10 ^ List.length tail
accum : ℕ
⊢ toNatAux tail 0 + (accum * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    toNatAux tail 0 + (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail +
      accum * 10 ^ (List.length tail + 1)