internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.liftVar_succ
Proof state before:
n i k : Nat
⊢ (if i < k then i + 1 else n + (i + 1)) = (if i < k then i else n + i) + 1
Tactic:
split <;> simp [Nat.add_assoc]
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_lt_add
Proof state before:
i k n j : Nat
self : i < k
⊢ liftVar n i j < k + n
Tactic:
simp [liftVar]
Proof state after:
i k n j : Nat
self : i < k
⊢ (if i < j then i else n + i) < k + n
Theorem: Lean4Lean.liftVar_lt_add
Proof state before:
i k n j : Nat
self : i < k
⊢ (if i < j then i else n + i) < k + n
Tactic:
split <;> rename_i h
Proof state after:
case inl
i k n j : Nat
self : i < k
h : i < j
⊢ i < k + n

case inr
i k n j : Nat
self : i < k
h : ¬i < j
⊢ n + i < k + n
Theorem: Lean4Lean.liftVar_lt_add
Proof state before:
case inl
i k n j : Nat
self : i < k
h : i < j
⊢ i < k + n
Tactic:
exact Nat.lt_of_lt_of_le self (Nat.le_add_right ..)
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_lt_add
Proof state before:
case inr
i k n j : Nat
self : i < k
h : ¬i < j
⊢ n + i < k + n
Tactic:
rw [Nat.add_comm]
Proof state after:
case inr
i k n j : Nat
self : i < k
h : ¬i < j
⊢ i + n < k + n
Theorem: Lean4Lean.liftVar_lt_add
Proof state before:
case inr
i k n j : Nat
self : i < k
h : ¬i < j
⊢ i + n < k + n
Tactic:
exact Nat.add_lt_add_right self _
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_zero
Proof state before:
e : VExpr
k : Nat
⊢ liftN 0 e k = e
Tactic:
induction e generalizing k <;> simp [liftN, liftVar, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN'_liftN'
Proof state before:
case bvar
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
⊢ (if (if i < k1 then i else n1 + i) < k2 then if i < k1 then i else n1 + i else n2 + if i < k1 then i else n1 + i) =
    if i < k1 then i else n1 + (n2 + i)
Tactic:
split <;> rename_i h
Proof state after:
case bvar.inl
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h : i < k1
⊢ (if i < k2 then i else n2 + i) = i

case bvar.inr
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h : ¬i < k1
⊢ (if n1 + i < k2 then n1 + i else n2 + (n1 + i)) = n1 + (n2 + i)
Theorem: Lean4Lean.VExpr.liftN'_liftN'
Proof state before:
case bvar.inl
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h : i < k1
⊢ (if i < k2 then i else n2 + i) = i
Tactic:
rw [if_pos (Nat.lt_of_lt_of_le h h1)]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN'_liftN'
Proof state before:
case bvar.inr
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h : ¬i < k1
⊢ (if n1 + i < k2 then n1 + i else n2 + (n1 + i)) = n1 + (n2 + i)
Tactic:
rw [if_neg (mt (fun h => ?_) h), Nat.add_left_comm]
Proof state after:
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h✝ : ¬i < k1
h : n1 + i < k2
⊢ i < k1
Theorem: Lean4Lean.VExpr.liftN'_liftN'
Proof state before:
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h✝ : ¬i < k1
h : n1 + i < k2
⊢ i < k1
Tactic:
exact (Nat.add_lt_add_iff_left ..).1 (Nat.lt_of_lt_of_le h h2)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN'_liftN'
Proof state before:
case forallE
n1 n2 : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ {k1 k2 : Nat}, k1 ≤ k2 → k2 ≤ n1 + k1 → liftN n2 (liftN n1 binderType✝ k1) k2 = liftN (n1 + n2) binderType✝ k1
IH2 : ∀ {k1 k2 : Nat}, k1 ≤ k2 → k2 ≤ n1 + k1 → liftN n2 (liftN n1 body✝ k1) k2 = liftN (n1 + n2) body✝ k1
k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
⊢ liftN n2 (liftN n1 body✝ (k1 + 1)) (k2 + 1) = liftN (n1 + n2) body✝ (k1 + 1)
Tactic:
rw [IH2 (Nat.succ_le_succ h1) (Nat.succ_le_succ h2)]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN'_liftN_lo
Proof state before:
e : VExpr
n k : Nat
⊢ liftN n (liftN k e) k = liftN (n + k) e
Tactic:
simpa [Nat.add_comm] using liftN'_liftN' (n1 := k) (n2 := n) (Nat.zero_le _) (Nat.le_refl _)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_liftN
Proof state before:
e : VExpr
n1 n2 : Nat
⊢ liftN n2 (liftN n1 e) = liftN (n1 + n2) e
Tactic:
simpa using liftN'_liftN' (Nat.zero_le _) (Nat.zero_le _)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN'_comm
Proof state before:
case bvar
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
⊢ (if (if i < k1 then i else n1 + i) < k2 then if i < k1 then i else n1 + i else n2 + if i < k1 then i else n1 + i) =
    if (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i
Tactic:
split <;> rename_i h'
Proof state after:
case bvar.inl
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
⊢ (if i < k2 then i else n2 + i) =
    if (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i

case bvar.inr
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : ¬i < k1
⊢ (if n1 + i < k2 then n1 + i else n2 + (n1 + i)) =
    if (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i
Theorem: Lean4Lean.VExpr.liftN'_comm
Proof state before:
case bvar.inl
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
⊢ (if i < k2 then i else n2 + i) =
    if (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i
Tactic:
rw [if_pos (c := _ < n2 + k1)]
Proof state after:
case bvar.inl.hc
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
⊢ (if i < k2 then i else n2 + i) < n2 + k1
Theorem: Lean4Lean.VExpr.liftN'_comm
Proof state before:
case bvar.inl.hc
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
⊢ (if i < k2 then i else n2 + i) < n2 + k1
Tactic:
split
Proof state after:
case bvar.inl.hc.inl
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
h✝ : i < k2
⊢ i < n2 + k1

case bvar.inl.hc.inr
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
h✝ : ¬i < k2
⊢ n2 + i < n2 + k1
Theorem: Lean4Lean.VExpr.liftN'_comm
Proof state before:
case bvar.inl.hc.inl
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
h✝ : i < k2
⊢ i < n2 + k1
Tactic:
exact Nat.lt_add_left _ h'
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN'_comm
Proof state before:
case bvar.inl.hc.inr
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
h✝ : ¬i < k2
⊢ n2 + i < n2 + k1
Tactic:
exact Nat.add_lt_add_left h' _
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN'_comm
Proof state before:
case bvar.inr
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : ¬i < k1
this : ¬i < k2
⊢ (if n1 + i < k2 then n1 + i else n2 + (n1 + i)) =
    if (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i
Tactic:
rw [if_neg (mt (Nat.lt_of_le_of_lt (Nat.le_add_left _ n1)) this),
  if_neg this, if_neg (mt (Nat.add_lt_add_iff_left ..).1 h'), Nat.add_left_comm]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.sizeOf_liftN
Proof state before:
n : Nat
e : VExpr
k : Nat
⊢ sizeOf e ≤ sizeOf (liftN n e k)
Tactic:
induction e generalizing k with simp [liftN, Nat.add_assoc, Nat.add_le_add_iff_left]
| bvar => simp [liftVar]; split <;> simp [Nat.le_add_left]
| _ => rename_i ih1 ih2; exact Nat.add_le_add (ih1 _) (ih2 _)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.sizeOf_liftN
Proof state before:
case bvar
n deBruijnIndex✝ k : Nat
⊢ deBruijnIndex✝ ≤ liftVar n deBruijnIndex✝ k
Tactic:
simp [liftVar]
Proof state after:
case bvar
n deBruijnIndex✝ k : Nat
⊢ deBruijnIndex✝ ≤ if deBruijnIndex✝ < k then deBruijnIndex✝ else n + deBruijnIndex✝
Theorem: Lean4Lean.VExpr.sizeOf_liftN
Proof state before:
case bvar
n deBruijnIndex✝ k : Nat
⊢ deBruijnIndex✝ ≤ if deBruijnIndex✝ < k then deBruijnIndex✝ else n + deBruijnIndex✝
Tactic:
split <;> simp [Nat.le_add_left]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.sizeOf_liftN
Proof state before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ : ∀ (k : Nat), sizeOf binderType✝ ≤ sizeOf (liftN n binderType✝ k)
body_ih✝ : ∀ (k : Nat), sizeOf body✝ ≤ sizeOf (liftN n body✝ k)
k : Nat
⊢ sizeOf binderType✝ + sizeOf body✝ ≤ sizeOf (liftN n binderType✝ k) + sizeOf (liftN n body✝ (k + 1))
Tactic:
rename_i ih1 ih2
Proof state after:
case forallE
n : Nat
binderType✝ body✝ : VExpr
ih1 : ∀ (k : Nat), sizeOf binderType✝ ≤ sizeOf (liftN n binderType✝ k)
ih2 : ∀ (k : Nat), sizeOf body✝ ≤ sizeOf (liftN n body✝ k)
k : Nat
⊢ sizeOf binderType✝ + sizeOf body✝ ≤ sizeOf (liftN n binderType✝ k) + sizeOf (liftN n body✝ (k + 1))
Theorem: Lean4Lean.VExpr.sizeOf_liftN
Proof state before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
ih1 : ∀ (k : Nat), sizeOf binderType✝ ≤ sizeOf (liftN n binderType✝ k)
ih2 : ∀ (k : Nat), sizeOf body✝ ≤ sizeOf (liftN n body✝ k)
k : Nat
⊢ sizeOf binderType✝ + sizeOf body✝ ≤ sizeOf (liftN n binderType✝ k) + sizeOf (liftN n body✝ (k + 1))
Tactic:
exact Nat.add_le_add (ih1 _) (ih2 _)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.mono
Proof state before:
k k' : Nat
e : VExpr
h : k ≤ k'
self : ClosedN e k
⊢ ClosedN e k'
Tactic:
induction e generalizing k k' with (simp [ClosedN] at self ⊢; try simp [self, *])
| bvar i => exact Nat.lt_of_lt_of_le self h
| app _ _ ih1 ih2 => exact ⟨ih1 h self.1, ih2 h self.2⟩
| lam _ _ ih1 ih2 | forallE _ _ ih1 ih2 =>
  exact ⟨ih1 h self.1, ih2 (Nat.succ_le_succ h) self.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.mono
Proof state before:
case const
declName✝ : Name
us✝ : List VLevel
k k' : Nat
h : k ≤ k'
self : ClosedN (const declName✝ us✝) k
⊢ ClosedN (const declName✝ us✝) k'
Tactic:
simp [ClosedN] at self ⊢
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.mono
Proof state before:
case bvar
i k k' : Nat
h : k ≤ k'
self : i < k
⊢ i < k'
Tactic:
exact Nat.lt_of_lt_of_le self h
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.mono
Proof state before:
case app
fn✝ arg✝ : VExpr
ih1 : ∀ {k k' : Nat}, k ≤ k' → ClosedN fn✝ k → ClosedN fn✝ k'
ih2 : ∀ {k k' : Nat}, k ≤ k' → ClosedN arg✝ k → ClosedN arg✝ k'
k k' : Nat
h : k ≤ k'
self : ClosedN fn✝ k ∧ ClosedN arg✝ k
⊢ ClosedN fn✝ k' ∧ ClosedN arg✝ k'
Tactic:
exact ⟨ih1 h self.1, ih2 h self.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.mono
Proof state before:
case forallE
binderType✝ body✝ : VExpr
ih1 : ∀ {k k' : Nat}, k ≤ k' → ClosedN binderType✝ k → ClosedN binderType✝ k'
ih2 : ∀ {k k' : Nat}, k ≤ k' → ClosedN body✝ k → ClosedN body✝ k'
k k' : Nat
h : k ≤ k'
self : ClosedN binderType✝ k ∧ ClosedN body✝ (k + 1)
⊢ ClosedN binderType✝ k' ∧ ClosedN body✝ (k' + 1)
Tactic:
exact ⟨ih1 h self.1, ih2 (Nat.succ_le_succ h) self.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq
Proof state before:
e : VExpr
k j n : Nat
self : ClosedN e k
h : k ≤ j
⊢ liftN n e j = e
Tactic:
induction e generalizing k j with
  (simp [ClosedN] at self; simp [self, liftN, *])
| bvar i => exact liftVar_lt (Nat.lt_of_lt_of_le self h)
| app _ _ ih1 ih2 => exact ⟨ih1 self.1 h, ih2 self.2 h⟩
| lam _ _ ih1 ih2 | forallE _ _ ih1 ih2 =>
  exact ⟨ih1 self.1 h, ih2 self.2 (Nat.succ_le_succ h)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq
Proof state before:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
k j : Nat
self : ClosedN (const declName✝ us✝) k
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝
Tactic:
simp [ClosedN] at self
Proof state after:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
k j : Nat
self : True
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq
Proof state before:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
k j : Nat
self : True
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝
Tactic:
simp [self, liftN, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq
Proof state before:
case bvar
n i k j : Nat
self : i < k
h : k ≤ j
⊢ liftVar n i j = i
Tactic:
exact liftVar_lt (Nat.lt_of_lt_of_le self h)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq
Proof state before:
case app
n : Nat
fn✝ arg✝ : VExpr
ih1 : ∀ {k j : Nat}, ClosedN fn✝ k → k ≤ j → liftN n fn✝ j = fn✝
ih2 : ∀ {k j : Nat}, ClosedN arg✝ k → k ≤ j → liftN n arg✝ j = arg✝
k j : Nat
self : ClosedN fn✝ k ∧ ClosedN arg✝ k
h : k ≤ j
⊢ liftN n fn✝ j = fn✝ ∧ liftN n arg✝ j = arg✝
Tactic:
exact ⟨ih1 self.1 h, ih2 self.2 h⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq
Proof state before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
ih1 : ∀ {k j : Nat}, ClosedN binderType✝ k → k ≤ j → liftN n binderType✝ j = binderType✝
ih2 : ∀ {k j : Nat}, ClosedN body✝ k → k ≤ j → liftN n body✝ j = body✝
k j : Nat
self : ClosedN binderType✝ k ∧ ClosedN body✝ (k + 1)
h : k ≤ j
⊢ liftN n binderType✝ j = binderType✝ ∧ liftN n body✝ (j + 1) = body✝
Tactic:
exact ⟨ih1 self.1 h, ih2 self.2 (Nat.succ_le_succ h)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN
Proof state before:
e : VExpr
k n j : Nat
self : ClosedN e k
⊢ ClosedN (liftN n e j) (k + n)
Tactic:
induction e generalizing k j with
  (simp [ClosedN] at self; simp [self, VExpr.liftN, ClosedN, *])
| bvar i => exact liftVar_lt_add self
| lam _ _ _ ih2 | forallE _ _ _ ih2 => exact Nat.add_right_comm .. ▸ ih2 self.2
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN
Proof state before:
case app
n : Nat
fn✝ arg✝ : VExpr
fn_ih✝ : ∀ {k j : Nat}, ClosedN fn✝ k → ClosedN (liftN n fn✝ j) (k + n)
arg_ih✝ : ∀ {k j : Nat}, ClosedN arg✝ k → ClosedN (liftN n arg✝ j) (k + n)
k j : Nat
self : ClosedN (app fn✝ arg✝) k
⊢ ClosedN (liftN n (app fn✝ arg✝) j) (k + n)
Tactic:
simp [ClosedN] at self
Proof state after:
case app
n : Nat
fn✝ arg✝ : VExpr
fn_ih✝ : ∀ {k j : Nat}, ClosedN fn✝ k → ClosedN (liftN n fn✝ j) (k + n)
arg_ih✝ : ∀ {k j : Nat}, ClosedN arg✝ k → ClosedN (liftN n arg✝ j) (k + n)
k j : Nat
self : ClosedN fn✝ k ∧ ClosedN arg✝ k
⊢ ClosedN (liftN n (app fn✝ arg✝) j) (k + n)
Theorem: Lean4Lean.VExpr.ClosedN.liftN
Proof state before:
case app
n : Nat
fn✝ arg✝ : VExpr
fn_ih✝ : ∀ {k j : Nat}, ClosedN fn✝ k → ClosedN (liftN n fn✝ j) (k + n)
arg_ih✝ : ∀ {k j : Nat}, ClosedN arg✝ k → ClosedN (liftN n arg✝ j) (k + n)
k j : Nat
self : ClosedN fn✝ k ∧ ClosedN arg✝ k
⊢ ClosedN (liftN n (app fn✝ arg✝) j) (k + n)
Tactic:
simp [self, VExpr.liftN, ClosedN, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN
Proof state before:
case bvar
n i k j : Nat
self : i < k
⊢ liftVar n i j < k + n
Tactic:
exact liftVar_lt_add self
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN
Proof state before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ : ∀ {k j : Nat}, ClosedN binderType✝ k → ClosedN (liftN n binderType✝ j) (k + n)
ih2 : ∀ {k j : Nat}, ClosedN body✝ k → ClosedN (liftN n body✝ j) (k + n)
k j : Nat
self : ClosedN binderType✝ k ∧ ClosedN body✝ (k + 1)
⊢ ClosedN (liftN n body✝ (j + 1)) (k + n + 1)
Tactic:
exact Nat.add_right_comm .. ▸ ih2 self.2
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq_rev
Proof state before:
n : Nat
e : VExpr
j k : Nat
self : ClosedN (liftN n e j) k
h : k ≤ j
⊢ liftN n e j = e
Tactic:
induction e generalizing k j with
  (simp [ClosedN] at self; simp [self, liftN, *])
| bvar i =>
  refine liftVar_lt (Nat.lt_of_lt_of_le ?_ h)
  unfold liftVar at self; split at self <;>
    [exact self; exact Nat.lt_of_le_of_lt (Nat.le_add_left ..) self]
| app _ _ ih1 ih2 => exact ⟨ih1 self.1 h, ih2 self.2 h⟩
| lam _ _ ih1 ih2 | forallE _ _ ih1 ih2 =>
  exact ⟨ih1 self.1 h, ih2 self.2 (Nat.succ_le_succ h)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq_rev
Proof state before:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
j k : Nat
self : ClosedN (liftN n (const declName✝ us✝) j) k
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝
Tactic:
simp [ClosedN] at self
Proof state after:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
j k : Nat
self : True
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq_rev
Proof state before:
case const
n : Nat
declName✝ : Name
us✝ : List VLevel
j k : Nat
self : True
h : k ≤ j
⊢ liftN n (const declName✝ us✝) j = const declName✝ us✝
Tactic:
simp [self, liftN, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq_rev
Proof state before:
case bvar
n i j k : Nat
self : liftVar n i j < k
h : k ≤ j
⊢ liftVar n i j = i
Tactic:
refine liftVar_lt (Nat.lt_of_lt_of_le ?_ h)
Proof state after:
case bvar
n i j k : Nat
self : liftVar n i j < k
h : k ≤ j
⊢ i < k
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq_rev
Proof state before:
case bvar
n i j k : Nat
self : liftVar n i j < k
h : k ≤ j
⊢ i < k
Tactic:
unfold liftVar at self
Proof state after:
case bvar
n i j k : Nat
self : (if i < j then i else n + i) < k
h : k ≤ j
⊢ i < k
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq_rev
Proof state before:
case bvar
n i j k : Nat
self : (if i < j then i else n + i) < k
h : k ≤ j
⊢ i < k
Tactic:
split at self <;>
[exact self; exact Nat.lt_of_le_of_lt (Nat.le_add_left ..) self]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq_rev
Proof state before:
case app
n : Nat
fn✝ arg✝ : VExpr
ih1 : ∀ {j k : Nat}, ClosedN (liftN n fn✝ j) k → k ≤ j → liftN n fn✝ j = fn✝
ih2 : ∀ {j k : Nat}, ClosedN (liftN n arg✝ j) k → k ≤ j → liftN n arg✝ j = arg✝
j k : Nat
self : ClosedN (liftN n fn✝ j) k ∧ ClosedN (liftN n arg✝ j) k
h : k ≤ j
⊢ liftN n fn✝ j = fn✝ ∧ liftN n arg✝ j = arg✝
Tactic:
exact ⟨ih1 self.1 h, ih2 self.2 h⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.liftN_eq_rev
Proof state before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
ih1 : ∀ {j k : Nat}, ClosedN (liftN n binderType✝ j) k → k ≤ j → liftN n binderType✝ j = binderType✝
ih2 : ∀ {j k : Nat}, ClosedN (liftN n body✝ j) k → k ≤ j → liftN n body✝ j = body✝
j k : Nat
self : ClosedN (liftN n binderType✝ j) k ∧ ClosedN (liftN n body✝ (j + 1)) (k + 1)
h : k ≤ j
⊢ liftN n binderType✝ j = binderType✝ ∧ liftN n body✝ (j + 1) = body✝
Tactic:
exact ⟨ih1 self.1 h, ih2 self.2 (Nat.succ_le_succ h)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instL_liftN
Proof state before:
n : Nat
e : VExpr
k : Nat
ls : List VLevel
⊢ instL ls (liftN n e k) = liftN n (instL ls e) k
Tactic:
cases e <;> simp [liftN, instL, instL_liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instL_instL
Proof state before:
ls ls' : List VLevel
e : VExpr
⊢ instL ls' (instL ls e) = instL (List.map (VLevel.inst ls') ls) e
Tactic:
cases e <;> simp [instL, instL_instL, Function.comp_def, VLevel.inst_inst]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.LevelWF.instL_id
Proof state before:
U : Nat
e : VExpr
h : LevelWF U e
⊢ instL (List.map VLevel.param (List.range U)) e = e
Tactic:
induction e <;> simp_all [instL, LevelWF, VLevel.inst_id]
Proof state after:
case const
U : Nat
declName✝ : Name
us✝ : List VLevel
h : ∀ (l : VLevel), l ∈ us✝ → VLevel.WF U l
⊢ List.map (VLevel.inst (List.map VLevel.param (List.range U))) us✝ = us✝
Theorem: Lean4Lean.VExpr.LevelWF.instL_id
Proof state before:
U : Nat
declName✝ : Name
us✝ : List VLevel
h : ∀ (l : VLevel), l ∈ us✝ → VLevel.WF U l
⊢ List.map (VLevel.inst (List.map VLevel.param (List.range U))) us✝ = us✝
Tactic:
case const => exact List.map_id'' _ fun _ h1 => VLevel.inst_id (h _ h1)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.LevelWF.instL_id
Proof state before:
U : Nat
declName✝ : Name
us✝ : List VLevel
h : ∀ (l : VLevel), l ∈ us✝ → VLevel.WF U l
⊢ List.map (VLevel.inst (List.map VLevel.param (List.range U))) us✝ = us✝
Tactic:
exact List.map_id'' _ fun _ h1 => VLevel.inst_id (h _ h1)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.levelWF_liftN
Proof state before:
n : Nat
e : VExpr
k U : Nat
⊢ LevelWF U (liftN n e k) ↔ LevelWF U e
Tactic:
induction e generalizing k <;> simp [liftN, LevelWF, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.LevelWF.instL
Proof state before:
ls : List VLevel
e : VExpr
U : Nat
h : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
⊢ LevelWF U (VExpr.instL ls e)
Tactic:
induction e <;> simp [instL, VLevel.WF.inst h, LevelWF, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instVar_lower
Proof state before:
e : VExpr
k : Nat
⊢ instVar 0 e (k + 1) = bvar 0
Tactic:
simp [instVar]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instVar_succ
Proof state before:
i : Nat
e : VExpr
k : Nat
⊢ instVar (i + 1) e (k + 1) = lift (instVar i e k)
Tactic:
simp [instVar, Nat.succ_lt_succ_iff]
Proof state after:
i : Nat
e : VExpr
k : Nat
⊢ (if i < k then bvar (i + 1) else if i = k then liftN (k + 1) e else bvar i) =
    lift (if i < k then bvar i else if i = k then liftN k e else bvar (i - 1))
Theorem: Lean4Lean.VExpr.instVar_succ
Proof state before:
i : Nat
e : VExpr
k : Nat
⊢ (if i < k then bvar (i + 1) else if i = k then liftN (k + 1) e else bvar i) =
    lift (if i < k then bvar i else if i = k then liftN k e else bvar (i - 1))
Tactic:
split <;> simp [lift, liftN]
Proof state after:
case inr
i : Nat
e : VExpr
k : Nat
h✝ : ¬i < k
⊢ (if i = k then liftN (k + 1) e else bvar i) = liftN 1 (if i = k then liftN k e else bvar (i - 1))
Theorem: Lean4Lean.VExpr.instVar_succ
Proof state before:
case inr
i : Nat
e : VExpr
k : Nat
h✝ : ¬i < k
⊢ (if i = k then liftN (k + 1) e else bvar i) = liftN 1 (if i = k then liftN k e else bvar (i - 1))
Tactic:
split <;> simp [liftN_liftN, liftN]
Proof state after:
case inr.inr
i : Nat
e : VExpr
k : Nat
h✝¹ : ¬i < k
h✝ : ¬i = k
⊢ i = i - 1 + 1
Theorem: Lean4Lean.VExpr.instVar_succ
Proof state before:
case inr.inr
i : Nat
e : VExpr
k : Nat
h✝¹ : ¬i < k
h✝ : ¬i = k
⊢ i = i - 1 + 1
Tactic:
have := Nat.lt_of_le_of_ne (Nat.not_lt.1 ‹_›) (Ne.symm ‹_›)
Proof state after:
case inr.inr
i : Nat
e : VExpr
k : Nat
h✝¹ : ¬i < k
h✝ : ¬i = k
this : k < i
⊢ i = i - 1 + 1
Theorem: Lean4Lean.VExpr.instVar_succ
Proof state before:
case inr.inr
i : Nat
e : VExpr
k : Nat
h✝¹ : ¬i < k
h✝ : ¬i = k
this : k < i
⊢ i = i - 1 + 1
Tactic:
let i+1 := i
Proof state after:
case inr.inr
i✝ : Nat
e : VExpr
k i : Nat
h✝¹ : ¬i + 1 < k
h✝ : ¬i + 1 = k
this : k < i + 1
⊢ i + 1 = i + 1 - 1 + 1
Theorem: Lean4Lean.VExpr.instVar_succ
Proof state before:
case inr.inr
i✝ : Nat
e : VExpr
k i : Nat
h✝¹ : ¬i + 1 < k
h✝ : ¬i + 1 = k
this : k < i + 1
⊢ i + 1 = i + 1 - 1 + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
⊢ liftN n (instVar i e j) k = instVar (liftVar n i k) e (n + j)
Tactic:
simp [instVar]
Proof state after:
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
⊢ liftN n (if i < j then bvar i else if i = j then liftN j e else bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
⊢ liftN n (if i < j then bvar i else if i = j then liftN j e else bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
split <;> rename_i h
Proof state after:
case inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : i < j
⊢ liftN n (bvar i) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)

case inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬i < j
⊢ liftN n (if i = j then liftN j e else bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Theorem: Lean4Lean.VExpr.liftN_instVar_lo
Proof state before:
case inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬i < j
⊢ liftN n (if i = j then liftN j e else bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)
Tactic:
split <;> rename_i h'
Proof state after:
case inr.inl
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬i < j
h' : i = j
⊢ liftN n (liftN j e) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)

case inr.inr
i n : Nat
e : VExpr
j k : Nat
hj : k ≤ j
h : ¬i < j
h' : ¬i = j
⊢ liftN n (bvar (i - 1)) k =
    if liftVar n i k < n + j then bvar (liftVar n i k)
    else if liftVar n i k = n + j then liftN (n + j) e else bvar (liftVar n i k - 1)