internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VExpr.liftN_instN_hi
Proof state before:
case forallE
e2 : VExpr
n k : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (j : Nat), liftN n (inst binderType✝ e2 j) (k + j) = inst (liftN n binderType✝ (k + j + 1)) (liftN n e2 k) j
IH : ∀ (j : Nat), liftN n (inst body✝ e2 j) (k + j) = inst (liftN n body✝ (k + j + 1)) (liftN n e2 k) j
j : Nat
⊢ liftN n (inst body✝ e2 (j + 1)) (k + j + 1) = inst (liftN n body✝ (k + j + 1 + 1)) (liftN n e2 k) (j + 1)
Tactic:
apply IH
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_liftN
Proof state before:
k : Nat
e1 e2 : VExpr
⊢ inst (liftN 1 e1 k) e2 k = e1
Tactic:
induction e1 generalizing k with simp [liftN, inst, *]
| bvar i =>
  simp only [liftVar, instVar, Nat.add_comm 1]; split <;> [rfl; rename_i h]
  rw [if_neg (mt (Nat.lt_of_le_of_lt (Nat.le_succ _)) h),
    if_neg (mt (by rintro rfl; apply Nat.lt_succ_self) h)]; rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_liftN
Proof state before:
case bvar
e2 : VExpr
i k : Nat
⊢ instVar (liftVar 1 i k) e2 k = bvar i
Tactic:
simp only [liftVar, instVar, Nat.add_comm 1]
Proof state after:
case bvar
e2 : VExpr
i k : Nat
⊢ (if (if i < k then i else i + 1) < k then bvar (if i < k then i else i + 1)
    else if (if i < k then i else i + 1) = k then liftN k e2 else bvar ((if i < k then i else i + 1) - 1)) =
    bvar i
Theorem: Lean4Lean.VExpr.inst_liftN
Proof state before:
case bvar
e2 : VExpr
i k : Nat
⊢ (if (if i < k then i else i + 1) < k then bvar (if i < k then i else i + 1)
    else if (if i < k then i else i + 1) = k then liftN k e2 else bvar ((if i < k then i else i + 1) - 1)) =
    bvar i
Tactic:
split <;> [rfl; rename_i h]
Proof state after:
case bvar.inr
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ (if i + 1 < k then bvar (i + 1) else if i + 1 = k then liftN k e2 else bvar (i + 1 - 1)) = bvar i
Theorem: Lean4Lean.VExpr.inst_liftN
Proof state before:
case bvar.inr
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ (if i + 1 < k then bvar (i + 1) else if i + 1 = k then liftN k e2 else bvar (i + 1 - 1)) = bvar i
Tactic:
rw [if_neg (mt (Nat.lt_of_le_of_lt (Nat.le_succ _)) h),
  if_neg (mt (by rintro rfl; apply Nat.lt_succ_self) h)]
Proof state after:
case bvar.inr
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ bvar (i + 1 - 1) = bvar i
Theorem: Lean4Lean.VExpr.inst_liftN
Proof state before:
case bvar.inr
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ bvar (i + 1 - 1) = bvar i
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_liftN
Proof state before:
e2 : VExpr
i k : Nat
h : ¬i < k
⊢ i + 1 = k → i < k
Tactic:
rintro rfl
Proof state after:
e2 : VExpr
i : Nat
h : ¬i < i + 1
⊢ i < i + 1
Theorem: Lean4Lean.VExpr.inst_liftN
Proof state before:
e2 : VExpr
i : Nat
h : ¬i < i + 1
⊢ i < i + 1
Tactic:
apply Nat.lt_succ_self
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_liftN'
Proof state before:
n k : Nat
e1 e2 : VExpr
⊢ inst (liftN (n + 1) e1 k) e2 k = liftN n e1 k
Tactic:
rw [← liftN'_liftN_hi, inst_liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.LevelWF.inst
Proof state before:
e1 e2 : VExpr
k U : Nat
h1 : LevelWF U e1
h2 : LevelWF U e2
⊢ LevelWF U (inst e1 e2 k)
Tactic:
induction e1 generalizing k <;> simp_all [inst, instVar, LevelWF]
Proof state after:
case bvar
e2 : VExpr
U : Nat
h2 : LevelWF U e2
deBruijnIndex✝ k : Nat
⊢ LevelWF U
    (if deBruijnIndex✝ < k then bvar deBruijnIndex✝
    else if deBruijnIndex✝ = k then VExpr.liftN k e2 else bvar (deBruijnIndex✝ - 1))
Theorem: Lean4Lean.VExpr.LevelWF.inst
Proof state before:
e2 : VExpr
U : Nat
h2 : LevelWF U e2
deBruijnIndex✝ k : Nat
⊢ LevelWF U
    (if deBruijnIndex✝ < k then bvar deBruijnIndex✝
    else if deBruijnIndex✝ = k then VExpr.liftN k e2 else bvar (deBruijnIndex✝ - 1))
Tactic:
case bvar => split <;> [trivial; split <;> [exact h2.liftN; trivial]]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.LevelWF.inst
Proof state before:
e2 : VExpr
U : Nat
h2 : LevelWF U e2
deBruijnIndex✝ k : Nat
⊢ LevelWF U
    (if deBruijnIndex✝ < k then bvar deBruijnIndex✝
    else if deBruijnIndex✝ = k then VExpr.liftN k e2 else bvar (deBruijnIndex✝ - 1))
Tactic:
split <;> [trivial; split <;> [exact h2.liftN; trivial]]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.unliftN_liftN
Proof state before:
n : Nat
e : VExpr
k : Nat
⊢ unliftN (liftN n e k) n k = e
Tactic:
induction n <;> simp [unliftN, inst_liftN', *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.unliftN_add
Proof state before:
e : VExpr
n1 n2 k : Nat
⊢ unliftN e (n1 + n2) k = unliftN (unliftN e n1 k) n2 k
Tactic:
induction n1 generalizing e <;> simp [unliftN, Nat.succ_add, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.unliftN_succ'
Proof state before:
e : VExpr
n k : Nat
⊢ unliftN e (n + 1) k = inst (unliftN e n k) default k
Tactic:
rw [unliftN_add]
Proof state after:
e : VExpr
n k : Nat
⊢ unliftN (unliftN e n k) 1 k = inst (unliftN e n k) default k
Theorem: Lean4Lean.VExpr.unliftN_succ'
Proof state before:
e : VExpr
n k : Nat
⊢ unliftN (unliftN e n k) 1 k = inst (unliftN e n k) default k
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_unliftN_hi
Proof state before:
k2 k1 n1 : Nat
e : VExpr
n2 : Nat
h : k2 ≤ k1
⊢ liftN n1 (unliftN e n2 k2) k1 = unliftN (liftN n1 e (k1 + n2)) n2 k2
Tactic:
obtain ⟨k1, rfl⟩ := Nat.le_iff_exists_add'.1 h
Proof state after:
case intro
k2 n1 : Nat
e : VExpr
n2 k1 : Nat
h : k2 ≤ k1 + k2
⊢ liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
Theorem: Lean4Lean.VExpr.liftN_unliftN_hi
Proof state before:
case intro
k2 n1 : Nat
e : VExpr
n2 k1 : Nat
h : k2 ≤ k1 + k2
⊢ liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
Tactic:
induction n2 generalizing e with simp [unliftN]
| succ n2 ih =>
  rw [ih, Nat.add_right_comm, liftN_instN_hi e default n1 (k1+n2) k2,
    Nat.add_right_comm k1]; rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_unliftN_hi
Proof state before:
case intro.succ
k2 n1 k1 : Nat
h : k2 ≤ k1 + k2
n2 : Nat
ih : ∀ {e : VExpr}, liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
e : VExpr
⊢ liftN n1 (unliftN (inst e default k2) n2 k2) (k1 + k2) =
    unliftN (inst (liftN n1 e (k1 + k2 + Nat.succ n2)) default k2) n2 k2
Tactic:
rw [ih, Nat.add_right_comm, liftN_instN_hi e default n1 (k1+n2) k2,
  Nat.add_right_comm k1]
Proof state after:
case intro.succ
k2 n1 k1 : Nat
h : k2 ≤ k1 + k2
n2 : Nat
ih : ∀ {e : VExpr}, liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
e : VExpr
⊢ unliftN (inst (liftN n1 e (k1 + k2 + n2 + 1)) (liftN n1 default (k1 + n2)) k2) n2 k2 =
    unliftN (inst (liftN n1 e (k1 + k2 + Nat.succ n2)) default k2) n2 k2
Theorem: Lean4Lean.VExpr.liftN_unliftN_hi
Proof state before:
case intro.succ
k2 n1 k1 : Nat
h : k2 ≤ k1 + k2
n2 : Nat
ih : ∀ {e : VExpr}, liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
e : VExpr
⊢ unliftN (inst (liftN n1 e (k1 + k2 + n2 + 1)) (liftN n1 default (k1 + n2)) k2) n2 k2 =
    unliftN (inst (liftN n1 e (k1 + k2 + Nat.succ n2)) default k2) n2 k2
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.Skips.liftN
Proof state before:
n : Nat
e : VExpr
k : Nat
⊢ Skips (liftN n e k) n k
Tactic:
simp [Skips]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.Skips.zero
Proof state before:
e : VExpr
k : Nat
⊢ Skips e 0 k
Tactic:
simp [Skips, unliftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftN_inj
Proof state before:
n : Nat
e1 : VExpr
k : Nat
e2 : VExpr
H : liftN n e1 k = liftN n e2 k
⊢ e1 = e2
Tactic:
rw [← unliftN_liftN (e := e1), H, unliftN_liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.liftVar_inj
Proof state before:
n i k i' : Nat
⊢ liftVar n i k = liftVar n i' k ↔ i = i'
Tactic:
simpa [liftN] using @liftN_inj n (.bvar i) k (.bvar i')
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.Skips.of_liftN_hi
Proof state before:
n1 : Nat
e : VExpr
k1 n2 k2 : Nat
self : Skips (liftN n1 e k1) n2 k2
h : n2 + k2 ≤ k1
⊢ Skips e n2 k2
Tactic:
obtain ⟨k1, rfl⟩ := Nat.le_iff_exists_add'.1 h
Proof state after:
case intro
n1 : Nat
e : VExpr
n2 k2 k1 : Nat
self : Skips (liftN n1 e (k1 + (n2 + k2))) n2 k2
h : n2 + k2 ≤ k1 + (n2 + k2)
⊢ Skips e n2 k2
Theorem: Lean4Lean.VExpr.Skips.of_liftN_hi
Proof state before:
case intro
n1 : Nat
e : VExpr
n2 k2 k1 : Nat
self : Skips (liftN n1 e (k1 + (n2 + k2))) n2 k2
h : n2 + k2 ≤ k1 + (n2 + k2)
⊢ Skips e n2 k2
Tactic:
rwa [Skips, Nat.add_comm n2, ← Nat.add_assoc, ← liftN_unliftN_hi (Nat.le_add_left ..),
  liftN'_comm (h := Nat.le_add_left ..), Nat.add_comm, liftN_inj] at self
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_add
Proof state before:
e : VExpr
n1 n2 k : Nat
⊢ Skips e (n1 + n2) k ↔ ∃ e', Skips e' n1 k ∧ e = liftN n2 e' k
Tactic:
simp [skips_iff_exists, ← liftN'_liftN_hi]
Proof state after:
e : VExpr
n1 n2 k : Nat
⊢ (∃ e', e = liftN n2 (liftN n1 e' k) k) ↔ ∃ e', (∃ e'_1, e' = liftN n1 e'_1 k) ∧ e = liftN n2 e' k
Theorem: Lean4Lean.VExpr.skips_add
Proof state before:
e : VExpr
n1 n2 k : Nat
⊢ (∃ e', e = liftN n2 (liftN n1 e' k) k) ↔ ∃ e', (∃ e'_1, e' = liftN n1 e'_1 k) ∧ e = liftN n2 e' k
Tactic:
exact ⟨fun ⟨_, h⟩ => ⟨_, ⟨_, rfl⟩, h⟩, fun ⟨_, ⟨_, rfl⟩, h⟩ => ⟨_, h⟩⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case zero
k : Nat
e : VExpr
⊢ Skips e Nat.zero k ↔ Skips' Nat.zero e k
Tactic:
simp [Skips, unliftN]
Proof state after:
case zero
k : Nat
e : VExpr
⊢ Skips' 0 e k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case zero
k : Nat
e : VExpr
⊢ Skips' 0 e k
Tactic:
induction e generalizing k <;> simp [Skips', *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ
k n : Nat
ih : ∀ {e : VExpr}, Skips e n k ↔ Skips' n e k
e : VExpr
⊢ Skips e (Nat.succ n) k ↔ Skips' (Nat.succ n) e k
Tactic:
simp [Nat.succ_eq_add_one, skips_add, ih]
Proof state after:
case succ
k n : Nat
ih : ∀ {e : VExpr}, Skips e n k ↔ Skips' n e k
e : VExpr
⊢ (∃ e', Skips' n e' k ∧ e = liftN 1 e' k) ↔ Skips' (n + 1) e k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ
k n : Nat
ih : ∀ {e : VExpr}, Skips e n k ↔ Skips' n e k
e : VExpr
⊢ (∃ e', Skips' n e' k ∧ e = liftN 1 e' k) ↔ Skips' (n + 1) e k
Tactic:
clear ih
Proof state after:
case succ
k n : Nat
e : VExpr
⊢ (∃ e', Skips' n e' k ∧ e = liftN 1 e' k) ↔ Skips' (n + 1) e k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.bvar
n i k : Nat
⊢ (∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k) ↔ Skips' (n + 1) (bvar i) k
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, fun h => ?_⟩
Proof state after:
case succ.bvar.refine_1
n i k : Nat
x✝ : ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : bvar i = liftN 1 e' k
⊢ Skips' (n + 1) (bvar i) k

case succ.bvar.refine_2
n i k : Nat
h : Skips' (n + 1) (bvar i) k
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.bvar.refine_1
n i k : Nat
x✝ : ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : bvar i = liftN 1 e' k
⊢ Skips' (n + 1) (bvar i) k
Tactic:
cases e' <;> cases h2
Proof state after:
case succ.bvar.refine_1.bvar.refl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
⊢ Skips' (n + 1) (bvar (liftVar 1 deBruijnIndex✝ k)) k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.bvar.refine_1.bvar.refl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
⊢ Skips' (n + 1) (bvar (liftVar 1 deBruijnIndex✝ k)) k
Tactic:
simp [Skips', liftVar]
Proof state after:
case succ.bvar.refine_1.bvar.refl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
⊢ (if deBruijnIndex✝ < k then deBruijnIndex✝ else 1 + deBruijnIndex✝) < k + (n + 1) →
    (if deBruijnIndex✝ < k then deBruijnIndex✝ else 1 + deBruijnIndex✝) < k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.bvar.refine_1.bvar.refl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
⊢ (if deBruijnIndex✝ < k then deBruijnIndex✝ else 1 + deBruijnIndex✝) < k + (n + 1) →
    (if deBruijnIndex✝ < k then deBruijnIndex✝ else 1 + deBruijnIndex✝) < k
Tactic:
split
Proof state after:
case succ.bvar.refine_1.bvar.refl.inl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : deBruijnIndex✝ < k
⊢ deBruijnIndex✝ < k + (n + 1) → deBruijnIndex✝ < k

case succ.bvar.refine_1.bvar.refl.inr
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : ¬deBruijnIndex✝ < k
⊢ 1 + deBruijnIndex✝ < k + (n + 1) → 1 + deBruijnIndex✝ < k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.bvar.refine_1.bvar.refl.inl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : deBruijnIndex✝ < k
⊢ deBruijnIndex✝ < k + (n + 1) → deBruijnIndex✝ < k
Tactic:
intro
Proof state after:
case succ.bvar.refine_1.bvar.refl.inl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : deBruijnIndex✝ < k
a✝ : deBruijnIndex✝ < k + (n + 1)
⊢ deBruijnIndex✝ < k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.bvar.refine_1.bvar.refl.inl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : deBruijnIndex✝ < k
a✝ : deBruijnIndex✝ < k + (n + 1)
⊢ deBruijnIndex✝ < k
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.bvar.refine_1.bvar.refl.inr
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : ¬deBruijnIndex✝ < k
⊢ 1 + deBruijnIndex✝ < k + (n + 1) → 1 + deBruijnIndex✝ < k
Tactic:
next h2 =>
rw [Nat.add_comm, ← Nat.add_assoc, Nat.succ_lt_succ_iff]
exact fun h => h2.elim (h1 h)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h2 : ¬deBruijnIndex✝ < k
⊢ 1 + deBruijnIndex✝ < k + (n + 1) → 1 + deBruijnIndex✝ < k
Tactic:
rw [Nat.add_comm, ← Nat.add_assoc, Nat.succ_lt_succ_iff]
Proof state after:
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h2 : ¬deBruijnIndex✝ < k
⊢ deBruijnIndex✝ < k + n → deBruijnIndex✝ + 1 < k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h2 : ¬deBruijnIndex✝ < k
⊢ deBruijnIndex✝ < k + n → deBruijnIndex✝ + 1 < k
Tactic:
exact fun h => h2.elim (h1 h)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.bvar.refine_2
n i k : Nat
h : Skips' (n + 1) (bvar i) k
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Tactic:
simp [Skips'] at h
Proof state after:
case succ.bvar.refine_2
n i k : Nat
h : i < k + (n + 1) → i < k
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : i < k + n + 1
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Tactic:
exact ⟨.bvar i, fun _ => h h', by simp [liftN, liftVar, h h']⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : i < k + n + 1
⊢ bvar i = liftN 1 (bvar i) k
Tactic:
simp [liftN, liftVar, h h']
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : ¬i < k + n + 1
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Tactic:
have := Nat.not_lt.1 h'
Proof state after:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : ¬i < k + n + 1
this : k + n + 1 ≤ i
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : ¬i < k + n + 1
this : k + n + 1 ≤ i
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Tactic:
let i+1 := i
Proof state after:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i + 1 < k + n + 1
this : k + n + 1 ≤ i + 1
⊢ ∃ e', Skips' n e' k ∧ bvar (i + 1) = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i + 1 < k + n + 1
this : k + n + 1 ≤ i + 1
⊢ ∃ e', Skips' n e' k ∧ bvar (i + 1) = liftN 1 e' k
Tactic:
rw [Nat.add_lt_add_iff_right] at h'
Proof state after:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this : k + n + 1 ≤ i + 1
⊢ ∃ e', Skips' n e' k ∧ bvar (i + 1) = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this✝ : k + n + 1 ≤ i + 1
this : ¬i < k
⊢ ∃ e', Skips' n e' k ∧ bvar (i + 1) = liftN 1 e' k
Tactic:
exact ⟨.bvar i, h'.elim, by simp [liftN, liftVar]; rw [if_neg this, Nat.add_comm]⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this✝ : k + n + 1 ≤ i + 1
this : ¬i < k
⊢ bvar (i + 1) = liftN 1 (bvar i) k
Tactic:
simp [liftN, liftVar]
Proof state after:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this✝ : k + n + 1 ≤ i + 1
this : ¬i < k
⊢ i + 1 = if i < k then i else 1 + i
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this✝ : k + n + 1 ≤ i + 1
this : ¬i < k
⊢ i + 1 = if i < k then i else 1 + i
Tactic:
rw [if_neg this, Nat.add_comm]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.sort
n : Nat
u : VLevel
k : Nat
⊢ (∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k) ↔ Skips' (n + 1) (sort u) k
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, fun _ => ⟨.sort u, by simp [Skips', liftN]⟩⟩
Proof state after:
case succ.sort
n : Nat
u : VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : sort u = liftN 1 e' k
⊢ Skips' (n + 1) (sort u) k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.sort
n : Nat
u : VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : sort u = liftN 1 e' k
⊢ Skips' (n + 1) (sort u) k
Tactic:
cases e' <;> cases h2
Proof state after:
case succ.sort.sort.refl
n : Nat
u : VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k
h1 : Skips' n (sort u) k
⊢ Skips' (n + 1) (sort u) k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.sort.sort.refl
n : Nat
u : VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k
h1 : Skips' n (sort u) k
⊢ Skips' (n + 1) (sort u) k
Tactic:
simp [Skips']
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n : Nat
u : VLevel
k : Nat
x✝ : Skips' (n + 1) (sort u) k
⊢ Skips' n (sort u) k ∧ sort u = liftN 1 (sort u) k
Tactic:
simp [Skips', liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.const
n : Nat
c : Name
ls : List VLevel
k : Nat
⊢ (∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k) ↔ Skips' (n + 1) (const c ls) k
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, fun _ => ⟨.const c ls, by simp [Skips', liftN]⟩⟩
Proof state after:
case succ.const
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : const c ls = liftN 1 e' k
⊢ Skips' (n + 1) (const c ls) k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.const
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : const c ls = liftN 1 e' k
⊢ Skips' (n + 1) (const c ls) k
Tactic:
cases e' <;> cases h2
Proof state after:
case succ.const.const.refl
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k
h1 : Skips' n (const c ls) k
⊢ Skips' (n + 1) (const c ls) k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.const.const.refl
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k
h1 : Skips' n (const c ls) k
⊢ Skips' (n + 1) (const c ls) k
Tactic:
simp [Skips']
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : Skips' (n + 1) (const c ls) k
⊢ Skips' n (const c ls) k ∧ const c ls = liftN 1 (const c ls) k
Tactic:
simp [Skips', liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.app
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k) ↔ Skips' (n + 1) (app f a) k
Tactic:
simp [Skips', ← fIH, ← aIH]
Proof state after:
case succ.app
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.app
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, ?_⟩
Proof state after:
case succ.app.refine_1
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : app f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k

case succ.app.refine_2
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ ((∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k) →
    ∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.app.refine_1
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : app f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k
Tactic:
cases e' <;> cases h2
Proof state after:
case succ.app.refine_1.app.refl
n k : Nat
fn✝ arg✝ : VExpr
h1 : Skips' n (app fn✝ arg✝) k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 fn✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 fn✝ k) k_1
aIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 arg✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 arg✝ k) k_1
x✝ : ∃ e', Skips' n e' k ∧ app (liftN 1 fn✝ k) (liftN 1 arg✝ k) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 fn✝ k = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ liftN 1 arg✝ k = liftN 1 e' k