internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
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
Tactic:
exact ⟨⟨_, h1.1, rfl⟩, ⟨_, h1.2, rfl⟩⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
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
Tactic:
rintro ⟨⟨e1, h1, rfl⟩, ⟨e2, h2, rfl⟩⟩
Proof state after:
case succ.app.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 k
aIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 k) k_1
⊢ ∃ e', Skips' n e' k ∧ app (liftN 1 e1 k) (liftN 1 e2 k) = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.app.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 k
aIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 k) k_1
⊢ ∃ e', Skips' n e' k ∧ app (liftN 1 e1 k) (liftN 1 e2 k) = liftN 1 e' k
Tactic:
exact ⟨.app .., ⟨h1, h2⟩, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.forallE
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 ∧ forallE f a = liftN 1 e' k) ↔ Skips' (n + 1) (forallE f a) k
Tactic:
simp [Skips', ← fIH, ← aIH]
Proof state after:
case succ.forallE
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 ∧ forallE f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.forallE
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 ∧ forallE f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, ?_⟩
Proof state after:
case succ.forallE.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 ∧ forallE f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : forallE f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)

case succ.forallE.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 + 1) ∧ a = liftN 1 e' (k + 1)) →
    ∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.forallE.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 ∧ forallE f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : forallE f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Tactic:
cases e' <;> cases h2
Proof state after:
case succ.forallE.refine_1.forallE.refl
n k : Nat
binderType✝ body✝ : VExpr
h1 : Skips' n (forallE binderType✝ body✝) k
fIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 binderType✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 binderType✝ k) k_1
aIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 body✝ (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 body✝ (k + 1)) k_1
x✝ : ∃ e', Skips' n e' k ∧ forallE (liftN 1 binderType✝ k) (liftN 1 body✝ (k + 1)) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 binderType✝ k = liftN 1 e' k) ∧
    ∃ e', Skips' n e' (k + 1) ∧ liftN 1 body✝ (k + 1) = liftN 1 e' (k + 1)
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.forallE.refine_1.forallE.refl
n k : Nat
binderType✝ body✝ : VExpr
h1 : Skips' n (forallE binderType✝ body✝) k
fIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 binderType✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 binderType✝ k) k_1
aIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 body✝ (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 body✝ (k + 1)) k_1
x✝ : ∃ e', Skips' n e' k ∧ forallE (liftN 1 binderType✝ k) (liftN 1 body✝ (k + 1)) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 binderType✝ k = liftN 1 e' k) ∧
    ∃ e', Skips' n e' (k + 1) ∧ liftN 1 body✝ (k + 1) = liftN 1 e' (k + 1)
Tactic:
exact ⟨⟨_, h1.1, rfl⟩, ⟨_, h1.2, rfl⟩⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.forallE.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 + 1) ∧ a = liftN 1 e' (k + 1)) →
    ∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k
Tactic:
rintro ⟨⟨e1, h1, rfl⟩, ⟨e2, h2, rfl⟩⟩
Proof state after:
case succ.forallE.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 (k + 1)
aIH :
  ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 (k + 1)) k_1
⊢ ∃ e', Skips' n e' k ∧ forallE (liftN 1 e1 k) (liftN 1 e2 (k + 1)) = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.forallE.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 (k + 1)
aIH :
  ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 (k + 1)) k_1
⊢ ∃ e', Skips' n e' k ∧ forallE (liftN 1 e1 k) (liftN 1 e2 (k + 1)) = liftN 1 e' k
Tactic:
exact ⟨.forallE .., ⟨h1, h2⟩, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.lam
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 ∧ lam f a = liftN 1 e' k) ↔ Skips' (n + 1) (lam f a) k
Tactic:
simp [Skips', ← fIH, ← aIH]
Proof state after:
case succ.lam
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 ∧ lam f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.lam
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 ∧ lam f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, ?_⟩
Proof state after:
case succ.lam.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 ∧ lam f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : lam f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)

case succ.lam.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 + 1) ∧ a = liftN 1 e' (k + 1)) →
    ∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.lam.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 ∧ lam f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : lam f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Tactic:
cases e' <;> cases h2
Proof state after:
case succ.lam.refine_1.lam.refl
n k : Nat
binderType✝ body✝ : VExpr
h1 : Skips' n (lam binderType✝ body✝) k
fIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 binderType✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 binderType✝ k) k_1
aIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 body✝ (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 body✝ (k + 1)) k_1
x✝ : ∃ e', Skips' n e' k ∧ lam (liftN 1 binderType✝ k) (liftN 1 body✝ (k + 1)) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 binderType✝ k = liftN 1 e' k) ∧
    ∃ e', Skips' n e' (k + 1) ∧ liftN 1 body✝ (k + 1) = liftN 1 e' (k + 1)
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.lam.refine_1.lam.refl
n k : Nat
binderType✝ body✝ : VExpr
h1 : Skips' n (lam binderType✝ body✝) k
fIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 binderType✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 binderType✝ k) k_1
aIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 body✝ (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 body✝ (k + 1)) k_1
x✝ : ∃ e', Skips' n e' k ∧ lam (liftN 1 binderType✝ k) (liftN 1 body✝ (k + 1)) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 binderType✝ k = liftN 1 e' k) ∧
    ∃ e', Skips' n e' (k + 1) ∧ liftN 1 body✝ (k + 1) = liftN 1 e' (k + 1)
Tactic:
exact ⟨⟨_, h1.1, rfl⟩, ⟨_, h1.2, rfl⟩⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.lam.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 + 1) ∧ a = liftN 1 e' (k + 1)) →
    ∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k
Tactic:
rintro ⟨⟨e1, h1, rfl⟩, ⟨e2, h2, rfl⟩⟩
Proof state after:
case succ.lam.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 (k + 1)
aIH :
  ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 (k + 1)) k_1
⊢ ∃ e', Skips' n e' k ∧ lam (liftN 1 e1 k) (liftN 1 e2 (k + 1)) = liftN 1 e' k
Theorem: Lean4Lean.VExpr.skips_iff
Proof state before:
case succ.lam.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 (k + 1)
aIH :
  ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 (k + 1)) k_1
⊢ ∃ e', Skips' n e' k ∧ lam (liftN 1 e1 k) (liftN 1 e2 (k + 1)) = liftN 1 e' k
Tactic:
exact ⟨.lam .., ⟨h1, h2⟩, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.of_liftN_eq_liftN
Proof state before:
n1 : Nat
e1 : VExpr
k1 n2 k2 : Nat
e2 : VExpr
h : liftN n1 e1 (k1 + n2 + k2) = liftN n2 e2 k2
⊢ ∃ e', e1 = liftN n2 e' k2 ∧ e2 = liftN n1 e' (k1 + k2)
Tactic:
have : (liftN n1 e1 (k1+n2+k2)).Skips n2 k2 := h ▸ .liftN
Proof state after:
n1 : Nat
e1 : VExpr
k1 n2 k2 : Nat
e2 : VExpr
h : liftN n1 e1 (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 e1 (k1 + n2 + k2)) n2 k2
⊢ ∃ e', e1 = liftN n2 e' k2 ∧ e2 = liftN n1 e' (k1 + k2)
Theorem: Lean4Lean.VExpr.of_liftN_eq_liftN
Proof state before:
n1 : Nat
e1 : VExpr
k1 n2 k2 : Nat
e2 : VExpr
h : liftN n1 e1 (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 e1 (k1 + n2 + k2)) n2 k2
⊢ ∃ e', e1 = liftN n2 e' k2 ∧ e2 = liftN n1 e' (k1 + k2)
Tactic:
obtain ⟨e', rfl⟩ := skips_iff_exists.1 <|
  this.of_liftN_hi (Nat.add_assoc .. ▸ Nat.le_add_left ..)
Proof state after:
case intro
n1 k1 n2 k2 : Nat
e2 e' : VExpr
h : liftN n1 (liftN n2 e' k2) (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 (liftN n2 e' k2) (k1 + n2 + k2)) n2 k2
⊢ ∃ e'_1, liftN n2 e' k2 = liftN n2 e'_1 k2 ∧ e2 = liftN n1 e'_1 (k1 + k2)
Theorem: Lean4Lean.VExpr.of_liftN_eq_liftN
Proof state before:
case intro
n1 k1 n2 k2 : Nat
e2 e' : VExpr
h : liftN n1 (liftN n2 e' k2) (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 (liftN n2 e' k2) (k1 + n2 + k2)) n2 k2
⊢ ∃ e'_1, liftN n2 e' k2 = liftN n2 e'_1 k2 ∧ e2 = liftN n1 e'_1 (k1 + k2)
Tactic:
refine ⟨e', rfl, ?_⟩
Proof state after:
case intro
n1 k1 n2 k2 : Nat
e2 e' : VExpr
h : liftN n1 (liftN n2 e' k2) (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 (liftN n2 e' k2) (k1 + n2 + k2)) n2 k2
⊢ e2 = liftN n1 e' (k1 + k2)
Theorem: Lean4Lean.VExpr.of_liftN_eq_liftN
Proof state before:
case intro
n1 k1 n2 k2 : Nat
e2 e' : VExpr
h : liftN n1 (liftN n2 e' k2) (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 (liftN n2 e' k2) (k1 + n2 + k2)) n2 k2
⊢ e2 = liftN n1 e' (k1 + k2)
Tactic:
rw [← liftN_inj, ← h, liftN'_comm (n1 := n1) (h := Nat.le_add_left ..),
  Nat.add_left_comm, Nat.add_assoc]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instL_instN
Proof state before:
k : Nat
ls : List VLevel
e1 e2 : VExpr
⊢ instL ls (inst e1 e2 k) = inst (instL ls e1) (instL ls e2) k
Tactic:
induction e1 generalizing k <;> simp [instL, inst, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instL_unliftN
Proof state before:
ls : List VLevel
e : VExpr
n k : Nat
⊢ instL ls (unliftN e n k) = unliftN (instL ls e) n k
Tactic:
induction n generalizing e with simp [unliftN]
| succ _ ih => rw [ih, instL_instN]; rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instL_unliftN
Proof state before:
case succ
ls : List VLevel
k n✝ : Nat
ih : ∀ {e : VExpr}, instL ls (unliftN e n✝ k) = unliftN (instL ls e) n✝ k
e : VExpr
⊢ instL ls (unliftN (inst e default k) n✝ k) = unliftN (inst (instL ls e) default k) n✝ k
Tactic:
rw [ih, instL_instN]
Proof state after:
case succ
ls : List VLevel
k n✝ : Nat
ih : ∀ {e : VExpr}, instL ls (unliftN e n✝ k) = unliftN (instL ls e) n✝ k
e : VExpr
⊢ unliftN (inst (instL ls e) (instL ls default) k) n✝ k = unliftN (inst (instL ls e) default k) n✝ k
Theorem: Lean4Lean.VExpr.instL_unliftN
Proof state before:
case succ
ls : List VLevel
k n✝ : Nat
ih : ∀ {e : VExpr}, instL ls (unliftN e n✝ k) = unliftN (instL ls e) n✝ k
e : VExpr
⊢ unliftN (inst (instL ls e) (instL ls default) k) n✝ k = unliftN (inst (instL ls e) default k) n✝ k
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.Skips.of_instL
Proof state before:
ls : List VLevel
e : VExpr
n k : Nat
self : Skips (instL ls e) n k
⊢ Skips e n k
Tactic:
rw [skips_iff] at self ⊢
Proof state after:
ls : List VLevel
e : VExpr
n k : Nat
self : Skips' n (instL ls e) k
⊢ Skips' n e k
Theorem: Lean4Lean.VExpr.Skips.of_instL
Proof state before:
ls : List VLevel
e : VExpr
n k : Nat
self : Skips' n (instL ls e) k
⊢ Skips' n e k
Tactic:
induction e generalizing k <;> simp_all [Skips']
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.of_liftN_eq_instL
Proof state before:
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e2 : VExpr
h : liftN n e1 k = instL ls e2
⊢ ∃ e', e1 = instL ls e' ∧ e2 = liftN n e' k
Tactic:
have : (instL ls e2).Skips n k := h ▸ .liftN
Proof state after:
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e2 : VExpr
h : liftN n e1 k = instL ls e2
this : Skips (instL ls e2) n k
⊢ ∃ e', e1 = instL ls e' ∧ e2 = liftN n e' k
Theorem: Lean4Lean.VExpr.of_liftN_eq_instL
Proof state before:
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e2 : VExpr
h : liftN n e1 k = instL ls e2
this : Skips (instL ls e2) n k
⊢ ∃ e', e1 = instL ls e' ∧ e2 = liftN n e' k
Tactic:
obtain ⟨e', rfl⟩ := skips_iff_exists.1 this.of_instL
Proof state after:
case intro
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e' : VExpr
h : liftN n e1 k = instL ls (liftN n e' k)
this : Skips (instL ls (liftN n e' k)) n k
⊢ ∃ e'_1, e1 = instL ls e'_1 ∧ liftN n e' k = liftN n e'_1 k
Theorem: Lean4Lean.VExpr.of_liftN_eq_instL
Proof state before:
case intro
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e' : VExpr
h : liftN n e1 k = instL ls (liftN n e' k)
this : Skips (instL ls (liftN n e' k)) n k
⊢ ∃ e'_1, e1 = instL ls e'_1 ∧ liftN n e' k = liftN n e'_1 k
Tactic:
refine ⟨e', ?_, rfl⟩
Proof state after:
case intro
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e' : VExpr
h : liftN n e1 k = instL ls (liftN n e' k)
this : Skips (instL ls (liftN n e' k)) n k
⊢ e1 = instL ls e'
Theorem: Lean4Lean.VExpr.of_liftN_eq_instL
Proof state before:
case intro
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e' : VExpr
h : liftN n e1 k = instL ls (liftN n e' k)
this : Skips (instL ls (liftN n e' k)) n k
⊢ e1 = instL ls e'
Tactic:
rw [← liftN_inj, h, instL_liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.instN_eq
Proof state before:
e1 : VExpr
k j : Nat
e2 : VExpr
self : ClosedN e1 k
h : k ≤ j
⊢ inst e1 e2 j = e1
Tactic:
conv => lhs; rw [← self.liftN_eq (n := 1) h]
Proof state after:
e1 : VExpr
k j : Nat
e2 : VExpr
self : ClosedN e1 k
h : k ≤ j
⊢ inst (liftN 1 e1 j) e2 j = e1
Theorem: Lean4Lean.VExpr.ClosedN.instN_eq
Proof state before:
e1 : VExpr
k j : Nat
e2 : VExpr
self : ClosedN e1 k
h : k ≤ j
⊢ inst (liftN 1 e1 j) e2 j = e1
Tactic:
rw [inst_liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.instN
Proof state before:
e : VExpr
k j : Nat
e2 : VExpr
h1 : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
⊢ ClosedN (inst (bvar i) e2 j) (k + j)
Tactic:
simp [inst, instVar]
Proof state after:
e : VExpr
k j : Nat
e2 : VExpr
h1 : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
⊢ ClosedN (if i < j then bvar i else if i = j then liftN j e2 else bvar (i - 1)) (k + j)
Theorem: Lean4Lean.VExpr.ClosedN.instN
Proof state before:
e : VExpr
k j : Nat
e2 : VExpr
h1 : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
⊢ ClosedN (if i < j then bvar i else if i = j then liftN j e2 else bvar (i - 1)) (k + j)
Tactic:
split <;> rename_i h1
Proof state after:
case inl
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : i < j
⊢ ClosedN (bvar i) (k + j)

case inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
⊢ ClosedN (if i = j then liftN j e2 else bvar (i - 1)) (k + j)
Theorem: Lean4Lean.VExpr.ClosedN.instN
Proof state before:
case inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
⊢ ClosedN (if i = j then liftN j e2 else bvar (i - 1)) (k + j)
Tactic:
split <;> rename_i h1'
Proof state after:
case inr.inl
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : i = j
⊢ ClosedN (liftN j e2) (k + j)

case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : ¬i = j
⊢ ClosedN (bvar (i - 1)) (k + j)
Theorem: Lean4Lean.VExpr.ClosedN.instN
Proof state before:
case inl
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : i < j
⊢ ClosedN (bvar i) (k + j)
Tactic:
exact Nat.lt_of_lt_of_le h1 (Nat.le_add_left ..)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.instN
Proof state before:
case inr.inl
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : i = j
⊢ ClosedN (liftN j e2) (k + j)
Tactic:
exact h2.liftN
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.ClosedN.instN
Proof state before:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : ¬i = j
⊢ ClosedN (bvar (i - 1)) (k + j)
Tactic:
have hk := Nat.lt_of_le_of_ne (Nat.not_lt.1 h1) (Ne.symm h1')
Proof state after:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : ¬i = j
hk : j < i
⊢ ClosedN (bvar (i - 1)) (k + j)
Theorem: Lean4Lean.VExpr.ClosedN.instN
Proof state before:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i : Nat
h : ClosedN (bvar i) (k + j + 1)
h1 : ¬i < j
h1' : ¬i = j
hk : j < i
⊢ ClosedN (bvar (i - 1)) (k + j)
Tactic:
let i+1 := i
Proof state after:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i✝ i : Nat
h : ClosedN (bvar (i + 1)) (k + j + 1)
h1 : ¬i + 1 < j
h1' : ¬i + 1 = j
hk : j < i + 1
⊢ ClosedN (bvar (i + 1 - 1)) (k + j)
Theorem: Lean4Lean.VExpr.ClosedN.instN
Proof state before:
case inr.inr
e : VExpr
k j : Nat
e2 : VExpr
h1✝ : ClosedN e (k + j + 1)
h2 : ClosedN e2 k
i✝ i : Nat
h : ClosedN (bvar (i + 1)) (k + j + 1)
h1 : ¬i + 1 < j
h1' : ¬i + 1 = j
hk : j < i + 1
⊢ ClosedN (bvar (i + 1 - 1)) (k + j)
Tactic:
exact Nat.lt_of_succ_lt_succ h
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof state before:
i : Nat
e2 e3 : VExpr
k j : Nat
⊢ inst (instVar i e2 k) e3 (j + k) = inst (instVar i e3 (j + k + 1)) (inst e2 e3 j) k
Tactic:
simp [instVar]
Proof state after:
i : Nat
e2 e3 : VExpr
k j : Nat
⊢ inst (if i < k then bvar i else if i = k then liftN k e2 else bvar (i - 1)) e3 (j + k) =
    inst (if i < j + k + 1 then bvar i else if i = j + k + 1 then liftN (j + k + 1) e3 else bvar (i - 1)) (inst e2 e3 j)
      k
Theorem: Lean4Lean.VExpr.inst_instVar_hi
Proof state before:
i : Nat
e2 e3 : VExpr
k j : Nat
⊢ inst (if i < k then bvar i else if i = k then liftN k e2 else bvar (i - 1)) e3 (j + k) =
    inst (if i < j + k + 1 then bvar i else if i = j + k + 1 then liftN (j + k + 1) e3 else bvar (i - 1)) (inst e2 e3 j)
      k
Tactic:
split <;> rename_i h
Proof state after:
case inl
i : Nat
e2 e3 : VExpr
k j : Nat
h : i < k
⊢ inst (bvar i) e3 (j + k) =
    inst (if i < j + k + 1 then bvar i else if i = j + k + 1 then liftN (j + k + 1) e3 else bvar (i - 1)) (inst e2 e3 j)
      k

case inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k
⊢ inst (if i = k then liftN k e2 else bvar (i - 1)) e3 (j + k) =
    inst (if i < j + k + 1 then bvar i else if i = j + k + 1 then liftN (j + k + 1) e3 else bvar (i - 1)) (inst e2 e3 j)
      k