internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip
Proof state before:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
Γ✝ Γ'✝ : List VExpr
A : VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ✝ Γ'✝
w✝ : List VExpr
h1 : Lift' (Lift.consN l k) Γ✝ w✝
h2 : LiftN 1 k w✝ Γ'✝
⊢ ∃ Γ₂,
    Lift' (Lift.consN l (Nat.succ k)) (A :: Γ✝) Γ₂ ∧
      LiftN 1 (Nat.succ k) Γ₂ (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Tactic:
refine ⟨_, .cons h1, ?_⟩
Proof state after:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
Γ✝ Γ'✝ : List VExpr
A : VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ✝ Γ'✝
w✝ : List VExpr
h1 : Lift' (Lift.consN l k) Γ✝ w✝
h2 : LiftN 1 k w✝ Γ'✝
⊢ LiftN 1 (Nat.succ k) (lift' A (Lift.consN l k) :: w✝) (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip
Proof state before:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
Γ✝ Γ'✝ : List VExpr
A : VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ✝ Γ'✝
w✝ : List VExpr
h1 : Lift' (Lift.consN l k) Γ✝ w✝
h2 : LiftN 1 k w✝ Γ'✝
⊢ LiftN 1 (Nat.succ k) (lift' A (Lift.consN l k) :: w✝) (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Tactic:
simp only [Ctx.liftN_iff_lift'] at h2 ⊢
Proof state after:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
Γ✝ Γ'✝ : List VExpr
A : VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ✝ Γ'✝
w✝ : List VExpr
h1 : Lift' (Lift.consN l k) Γ✝ w✝
h2 : Lift' (Lift.consN (Lift.skipN 1) k) w✝ Γ'✝
⊢ Lift' (Lift.consN (Lift.skipN 1) (Nat.succ k)) (lift' A (Lift.consN l k) :: w✝)
    (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip
Proof state before:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
Γ✝ Γ'✝ : List VExpr
A : VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ✝ Γ'✝
w✝ : List VExpr
h1 : Lift' (Lift.consN l k) Γ✝ w✝
h2 : Lift' (Lift.consN (Lift.skipN 1) k) w✝ Γ'✝
⊢ Lift' (Lift.consN (Lift.skipN 1) (Nat.succ k)) (lift' A (Lift.consN l k) :: w✝)
    (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Tactic:
simpa [← VExpr.lift'_comp, ← Lift.consN_comp] using h2.cons (A := lift' A (.consN l k))
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.depth_zero
Proof state before:
l✝ : Lift
Γ Γ' : List VExpr
l : Lift
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
H : Lift' l Γ✝ Γ'✝
h : Lift.depth (Lift.cons l) = 0
⊢ A✝ :: Γ✝ = lift' A✝ l :: Γ'✝
Tactic:
rw [VExpr.lift'_depth_zero (l := l) h, H.depth_zero (l := l) h]
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.lt
Proof state before:
Γ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ i A
⊢ i < List.length Γ
Tactic:
induction H with
| zero => apply Nat.succ_pos
| succ _ ih => apply Nat.succ_lt_succ ih
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.lt
Proof state before:
case zero
Γ : List VExpr
i : Nat
A ty✝ : VExpr
Γ✝ : List VExpr
⊢ 0 < List.length (ty✝ :: Γ✝)
Tactic:
apply Nat.succ_pos
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.lt
Proof state before:
case succ
Γ : List VExpr
i : Nat
A : VExpr
Γ✝ : List VExpr
n✝ : Nat
ty✝ A✝ : VExpr
a✝ : Lookup Γ✝ n✝ ty✝
ih : n✝ < List.length Γ✝
⊢ n✝ + 1 < List.length (A✝ :: Γ✝)
Tactic:
apply Nat.succ_lt_succ ih
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
n k : Nat
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.LiftN n k Γ Γ'
H : Lookup Γ i A
⊢ Lookup Γ' (liftVar n i k) (liftN n A k)
Tactic:
induction W generalizing i A with
| zero As =>
  rw [liftVar_base, Nat.add_comm]
  subst n
  induction As with simp [*]
  | cons _ _ ih => rw [liftN_succ]; exact .succ ih
| @succ k _ _ _ _ ih =>
  match H with
  | .zero => rw [liftVar_zero, ← lift_liftN']; exact .zero
  | .succ H => rw [liftVar_succ, ← lift_liftN']; exact (ih H).succ
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (liftVar n i) (liftN n A)
Tactic:
rw [liftVar_base, Nat.add_comm]
Proof state after:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (i + n) (liftN n A)
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (i + n) (liftN n A)
Tactic:
subst n
Proof state after:
case zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A)
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
case zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A)
Tactic:
induction As with simp [*]
| cons _ _ ih => rw [liftN_succ]; exact .succ ih
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
head✝ : VExpr
tail✝ : List VExpr
ih : Lookup (tail✝ ++ Γ✝) (i + List.length tail✝) (liftN (List.length tail✝) A)
⊢ Lookup (head✝ :: (tail✝ ++ Γ✝)) (i + Nat.succ (List.length tail✝)) (liftN (Nat.succ (List.length tail✝)) A)
Tactic:
rw [liftN_succ]
Proof state after:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
head✝ : VExpr
tail✝ : List VExpr
ih : Lookup (tail✝ ++ Γ✝) (i + List.length tail✝) (liftN (List.length tail✝) A)
⊢ Lookup (head✝ :: (tail✝ ++ Γ✝)) (i + Nat.succ (List.length tail✝)) (lift (liftN (List.length tail✝) A))
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
head✝ : VExpr
tail✝ : List VExpr
ih : Lookup (tail✝ ++ Γ✝) (i + List.length tail✝) (liftN (List.length tail✝) A)
⊢ Lookup (head✝ :: (tail✝ ++ Γ✝)) (i + Nat.succ (List.length tail✝)) (lift (liftN (List.length tail✝) A))
Tactic:
exact .succ ih
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
case succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H : Lookup (A✝ :: Γ✝) i A
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i (k + 1)) (liftN n A (k + 1))
Tactic:
match H with
| .zero => rw [liftVar_zero, ← lift_liftN']; exact .zero
| .succ H => rw [liftVar_succ, ← lift_liftN']; exact (ih H).succ
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H : Lookup (A✝ :: Γ✝) i A
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n 0 (k + 1)) (liftN n (lift A✝) (k + 1))
Tactic:
rw [liftVar_zero, ← lift_liftN']
Proof state after:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H : Lookup (A✝ :: Γ✝) i A
⊢ Lookup (liftN n A✝ k :: Γ'✝) 0 (lift (liftN n A✝ k))
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H : Lookup (A✝ :: Γ✝) i A
⊢ Lookup (liftN n A✝ k :: Γ'✝) 0 (lift (liftN n A✝ k))
Tactic:
exact .zero
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H✝ : Lookup (A✝ :: Γ✝) i A
n✝ : Nat
ty✝ : VExpr
H : Lookup Γ✝ n✝ ty✝
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n (n✝ + 1) (k + 1)) (liftN n (lift ty✝) (k + 1))
Tactic:
rw [liftVar_succ, ← lift_liftN']
Proof state after:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H✝ : Lookup (A✝ :: Γ✝) i A
n✝ : Nat
ty✝ : VExpr
H : Lookup Γ✝ n✝ ty✝
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n n✝ k + 1) (lift (liftN n ty✝ k))
Theorem: Lean4Lean.Lookup.weakN
Proof state before:
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ✝ i A → Lookup Γ'✝ (liftVar n i k) (liftN n A k)
i : Nat
A : VExpr
H✝ : Lookup (A✝ :: Γ✝) i A
n✝ : Nat
ty✝ : VExpr
H : Lookup Γ✝ n✝ ty✝
⊢ Lookup (liftN n A✝ k :: Γ'✝) (liftVar n n✝ k + 1) (lift (liftN n ty✝ k))
Tactic:
exact (ih H).succ
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
n k : Nat
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ Lookup Γ' (liftVar n i k) (liftN n A k) ↔ Lookup Γ i A
Tactic:
refine ⟨fun H => ?_, fun H => H.weakN W⟩
Proof state after:
n k : Nat
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.LiftN n k Γ Γ'
H : Lookup Γ' (liftVar n i k) (liftN n A k)
⊢ Lookup Γ i A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
n k : Nat
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.LiftN n k Γ Γ'
H : Lookup Γ' (liftVar n i k) (liftN n A k)
⊢ Lookup Γ i A
Tactic:
induction W generalizing i A with
| zero As =>
  rw [liftVar_base, Nat.add_comm] at H
  subst n
  induction As with simp at H
  | nil => exact H
  | cons A As ih =>
    rw [liftN_succ] at H
    generalize eq : lift (liftN ..) = A' at H
    obtain _|H := H; cases liftN_inj.1 eq
    exact ih H
| @succ k _ _ _ _ ih =>
  generalize eA : liftN n A (k+1) = A' at H
  cases i with
  | zero =>
    simp at H; let .zero := H
    rw [lift, liftN'_comm (h := Nat.zero_le _), Nat.add_comm 1, liftN_inj] at eA
    subst A; exact .zero
  | succ i =>
    simp at H; let .succ H := H
    obtain ⟨_, rfl, rfl⟩ := of_liftN_eq_liftN (k2 := 0) eA
    exact .succ (ih H)
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup (As ++ Γ✝) (liftVar n i) (liftN n A)
⊢ Lookup Γ✝ i A
Tactic:
rw [liftVar_base, Nat.add_comm] at H
Proof state after:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup (As ++ Γ✝) (i + n) (liftN n A)
⊢ Lookup Γ✝ i A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
i : Nat
A : VExpr
H : Lookup (As ++ Γ✝) (i + n) (liftN n A)
⊢ Lookup Γ✝ i A
Tactic:
subst n
Proof state after:
case zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
i : Nat
A : VExpr
H : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A)
⊢ Lookup Γ✝ i A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
i : Nat
A : VExpr
H : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A)
⊢ Lookup Γ✝ i A
Tactic:
induction As with simp at H
| nil => exact H
| cons A As ih =>
  rw [liftN_succ] at H
  generalize eq : lift (liftN ..) = A' at H
  obtain _|H := H; cases liftN_inj.1 eq
  exact ih H
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero.nil
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A : VExpr
H : Lookup Γ✝ i A
⊢ Lookup Γ✝ i A
Tactic:
exact H
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
H : Lookup (A :: (As ++ Γ✝)) (i + Nat.succ (List.length As)) (liftN (Nat.succ (List.length As)) A✝)
⊢ Lookup Γ✝ i A✝
Tactic:
rw [liftN_succ] at H
Proof state after:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
H : Lookup (A :: (As ++ Γ✝)) (i + Nat.succ (List.length As)) (lift (liftN (List.length As) A✝))
⊢ Lookup Γ✝ i A✝
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
H : Lookup (A :: (As ++ Γ✝)) (i + Nat.succ (List.length As)) (lift (liftN (List.length As) A✝))
⊢ Lookup Γ✝ i A✝
Tactic:
generalize eq : lift (liftN ..) = A' at H
Proof state after:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
A' : VExpr
eq : lift (liftN (List.length As) A✝) = A'
H : Lookup (A :: (As ++ Γ✝)) (i + Nat.succ (List.length As)) A'
⊢ Lookup Γ✝ i A✝
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
A' : VExpr
eq : lift (liftN (List.length As) A✝) = A'
H : Lookup (A :: (As ++ Γ✝)) (i + Nat.succ (List.length As)) A'
⊢ Lookup Γ✝ i A✝
Tactic:
obtain _|H := H
Proof state after:
case zero.cons.succ
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
ty✝ : VExpr
H : Lookup (As ++ Γ✝) (Nat.add i (List.length As)) ty✝
eq : lift (liftN (List.length As) A✝) = lift ty✝
⊢ Lookup Γ✝ i A✝
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero.cons.succ
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
ty✝ : VExpr
H : Lookup (As ++ Γ✝) (Nat.add i (List.length As)) ty✝
eq : lift (liftN (List.length As) A✝) = lift ty✝
⊢ Lookup Γ✝ i A✝
Tactic:
cases liftN_inj.1 eq
Proof state after:
case zero.cons.succ.refl
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
H : Lookup (As ++ Γ✝) (Nat.add i (List.length As)) (liftN (List.length As) A✝)
eq : lift (liftN (List.length As) A✝) = lift (liftN (List.length As) A✝)
⊢ Lookup Γ✝ i A✝
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case zero.cons.succ.refl
k : Nat
Γ Γ' Γ✝ : List VExpr
i : Nat
A✝ A : VExpr
As : List VExpr
ih : Lookup (As ++ Γ✝) (i + List.length As) (liftN (List.length As) A✝) → Lookup Γ✝ i A✝
H : Lookup (As ++ Γ✝) (Nat.add i (List.length As)) (liftN (List.length As) A✝)
eq : lift (liftN (List.length As) A✝) = lift (liftN (List.length As) A✝)
⊢ Lookup Γ✝ i A✝
Tactic:
exact ih H
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
i : Nat
A : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i (k + 1)) (liftN n A (k + 1))
⊢ Lookup (A✝ :: Γ✝) i A
Tactic:
generalize eA : liftN n A (k+1) = A' at H
Proof state after:
case succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
i : Nat
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i (k + 1)) A'
⊢ Lookup (A✝ :: Γ✝) i A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
i : Nat
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i (k + 1)) A'
⊢ Lookup (A✝ :: Γ✝) i A
Tactic:
cases i with
| zero =>
  simp at H; let .zero := H
  rw [lift, liftN'_comm (h := Nat.zero_le _), Nat.add_comm 1, liftN_inj] at eA
  subst A; exact .zero
| succ i =>
  simp at H; let .succ H := H
  obtain ⟨_, rfl, rfl⟩ := of_liftN_eq_liftN (k2 := 0) eA
  exact .succ (ih H)
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n Nat.zero (k + 1)) A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Tactic:
simp at H
Proof state after:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Tactic:
let .zero := H
Proof state after:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
eA : liftN n A (k + 1) = lift (liftN n A✝ k)
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
eA : liftN n A (k + 1) = lift (liftN n A✝ k)
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Tactic:
rw [lift, liftN'_comm (h := Nat.zero_le _), Nat.add_comm 1, liftN_inj] at eA
Proof state after:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
eA : A = liftN 1 A✝
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
eA : A = liftN 1 A✝
⊢ Lookup (A✝ :: Γ✝) Nat.zero A
Tactic:
subst A
Proof state after:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero (liftN 1 A✝)
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.zero
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A' : VExpr
H : Lookup (liftN n A✝ k :: Γ'✝) 0 A'
⊢ Lookup (A✝ :: Γ✝) Nat.zero (liftN 1 A✝)
Tactic:
exact .zero
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
i : Nat
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n (Nat.succ i) (k + 1)) A'
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) A
Tactic:
simp at H
Proof state after:
case succ.succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
i : Nat
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
eA : liftN n A (k + 1) = A'
i : Nat
H : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) A
Tactic:
let .succ H := H
Proof state after:
case succ.succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
i : Nat
H✝ : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
ty✝ : VExpr
H : Lookup Γ'✝ (liftVar n i k) ty✝
eA : liftN n A (k + 1) = lift ty✝
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) A
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.succ
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A A' : VExpr
i : Nat
H✝ : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
ty✝ : VExpr
H : Lookup Γ'✝ (liftVar n i k) ty✝
eA : liftN n A (k + 1) = lift ty✝
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) A
Tactic:
obtain ⟨_, rfl, rfl⟩ := of_liftN_eq_liftN (k2 := 0) eA
Proof state after:
case succ.succ.intro.intro
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A' : VExpr
i : Nat
H✝ : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
w✝ : VExpr
H : Lookup Γ'✝ (liftVar n i k) (liftN n w✝ (k + 0))
eA : liftN n (liftN 1 w✝) (k + 1) = lift (liftN n w✝ (k + 0))
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) (liftN 1 w✝)
Theorem: Lean4Lean.Lookup.weakN_iff
Proof state before:
case succ.succ.intro.intro
n k✝ : Nat
Γ Γ' : List VExpr
k : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.LiftN n k Γ✝ Γ'✝
ih : ∀ {i : Nat} {A : VExpr}, Lookup Γ'✝ (liftVar n i k) (liftN n A k) → Lookup Γ✝ i A
A' : VExpr
i : Nat
H✝ : Lookup (liftN n A✝ k :: Γ'✝) (liftVar n i k + 1) A'
w✝ : VExpr
H : Lookup Γ'✝ (liftVar n i k) (liftN n w✝ (k + 0))
eA : liftN n (liftN 1 w✝) (k + 1) = lift (liftN n w✝ (k + 0))
⊢ Lookup (A✝ :: Γ✝) (Nat.succ i) (liftN 1 w✝)
Tactic:
exact .succ (ih H)
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weak'_iff
Proof state before:
l : Lift
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.Lift' l Γ Γ'
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A
Tactic:
generalize e : l.depth = n
Proof state after:
l : Lift
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A