internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.trans_r
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
w✝ : VLevel
h : IsDefEq env U Γ A B (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₃ B
Tactic:
exact .trans (.defeqDF h h₁) h₂
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.trans_l
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
⊢ IsDefEq env U Γ e₁ e₃ A
Tactic:
have ⟨_, h⟩ := h₁.uniq henv hΓ h₂
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
w✝ : VLevel
h : IsDefEq env U Γ A B (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₃ A
Theorem: Lean4Lean.VEnv.IsDefEq.trans_l
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A e₃ B : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEq env U Γ e₁ e₂ A
h₂ : IsDefEq env U Γ e₂ e₃ B
w✝ : VLevel
h : IsDefEq env U Γ A B (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₃ A
Tactic:
exact h₁.trans (.defeqDF (.symm h) h₂)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqU.defeqDF
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
A B e₁ e₂ : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁ : IsDefEqU env U Γ A B
h₂ : IsDefEq env U Γ e₁ e₂ A
⊢ IsDefEq env U Γ e₁ e₂ B
Tactic:
have ⟨_, h₁⟩ := h₁
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
A B e₁ e₂ : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁✝ : IsDefEqU env U Γ A B
h₂ : IsDefEq env U Γ e₁ e₂ A
w✝ : VExpr
h₁ : IsDefEq env U Γ A B w✝
⊢ IsDefEq env U Γ e₁ e₂ B
Theorem: Lean4Lean.VEnv.IsDefEqU.defeqDF
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
A B e₁ e₂ : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁✝ : IsDefEqU env U Γ A B
h₂ : IsDefEq env U Γ e₁ e₂ A
w✝ : VExpr
h₁ : IsDefEq env U Γ A B w✝
⊢ IsDefEq env U Γ e₁ e₂ B
Tactic:
have ⟨_, hA⟩ := h₂.isType henv hΓ
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
A B e₁ e₂ : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁✝ : IsDefEqU env U Γ A B
h₂ : IsDefEq env U Γ e₁ e₂ A
w✝¹ : VExpr
h₁ : IsDefEq env U Γ A B w✝¹
w✝ : VLevel
hA : HasType env U Γ A (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₂ B
Theorem: Lean4Lean.VEnv.IsDefEqU.defeqDF
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
A B e₁ e₂ : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
h₁✝ : IsDefEqU env U Γ A B
h₂ : IsDefEq env U Γ e₁ e₂ A
w✝¹ : VExpr
h₁ : IsDefEq env U Γ A B w✝¹
w✝ : VLevel
hA : HasType env U Γ A (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₂ B
Tactic:
exact .defeqDF (hA.trans_l henv hΓ h₁) h₂
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqU.weakN_iff
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
n k : Nat
Γ : List VExpr
e1 e2 : VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqU env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) ↔ IsDefEqU env U Γ e1 e2
Tactic:
refine ⟨fun h => have := henv; have := hΓ; sorry, fun h => h.weakN henv W⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.skips
Proof state before:
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
H : IsDefEq env U Γ' e₁ e₂ A
h1 : VExpr.Skips e₁ n k
h2 : VExpr.Skips e₂ n k
⊢ ∃ B, IsDefEq env U Γ' e₁ e₂ B ∧ VExpr.Skips B n k
Tactic:
obtain ⟨e₁, rfl⟩ := VExpr.skips_iff_exists.1 h1
Proof state after:
case intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
h2 : VExpr.Skips e₂ n k
e₁ : VExpr
H : IsDefEq env U Γ' (VExpr.liftN n e₁ k) e₂ A
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) e₂ B ∧ VExpr.Skips B n k
Theorem: Lean4Lean.VEnv.IsDefEq.skips
Proof state before:
case intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
h2 : VExpr.Skips e₂ n k
e₁ : VExpr
H : IsDefEq env U Γ' (VExpr.liftN n e₁ k) e₂ A
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) e₂ B ∧ VExpr.Skips B n k
Tactic:
obtain ⟨e₂, rfl⟩ := VExpr.skips_iff_exists.1 h2
Proof state after:
case intro.intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
e₁ : VExpr
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
e₂ : VExpr
h2 : VExpr.Skips (VExpr.liftN n e₂ k) n k
H : IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) A
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) B ∧ VExpr.Skips B n k
Theorem: Lean4Lean.VEnv.IsDefEq.skips
Proof state before:
case intro.intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
e₁ : VExpr
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
e₂ : VExpr
h2 : VExpr.Skips (VExpr.liftN n e₂ k) n k
H : IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) A
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) B ∧ VExpr.Skips B n k
Tactic:
have ⟨_, H⟩ := (IsDefEqU.weakN_iff henv hΓ W).1 ⟨_, H⟩
Proof state after:
case intro.intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
e₁ : VExpr
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
e₂ : VExpr
h2 : VExpr.Skips (VExpr.liftN n e₂ k) n k
H✝ : IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) A
w✝ : VExpr
H : IsDefEq env U Γ e₁ e₂ w✝
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) B ∧ VExpr.Skips B n k
Theorem: Lean4Lean.VEnv.IsDefEq.skips
Proof state before:
case intro.intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
e₁ : VExpr
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
e₂ : VExpr
h2 : VExpr.Skips (VExpr.liftN n e₂ k) n k
H✝ : IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) A
w✝ : VExpr
H : IsDefEq env U Γ e₁ e₂ w✝
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) B ∧ VExpr.Skips B n k
Tactic:
exact ⟨_, H.weakN henv W, .liftN⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN_iff'
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
Γ : List VExpr
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
hΓ : OnCtx Γ (IsType env U)
n k : Nat
e1 e2 A : VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEq env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) (VExpr.liftN n A k) ↔ IsDefEq env U Γ e1 e2 A
Tactic:
refine ⟨fun h => ?_, fun h => h.weakN henv W⟩
Proof state after:
env : VEnv
Γ' : List VExpr
U : Nat
Γ : List VExpr
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
hΓ : OnCtx Γ (IsType env U)
n k : Nat
e1 e2 A : VExpr
W : Ctx.LiftN n k Γ Γ'
h : IsDefEq env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) (VExpr.liftN n A k)
⊢ IsDefEq env U Γ e1 e2 A
Theorem: Lean4Lean.VEnv.IsDefEq.weakN_iff'
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
Γ : List VExpr
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
hΓ : OnCtx Γ (IsType env U)
n k : Nat
e1 e2 A : VExpr
W : Ctx.LiftN n k Γ Γ'
h : IsDefEq env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) (VExpr.liftN n A k)
⊢ IsDefEq env U Γ e1 e2 A
Tactic:
have ⟨_, H⟩ := (IsDefEqU.weakN_iff henv hΓ' W).1 ⟨_, h⟩
Proof state after:
env : VEnv
Γ' : List VExpr
U : Nat
Γ : List VExpr
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
hΓ : OnCtx Γ (IsType env U)
n k : Nat
e1 e2 A : VExpr
W : Ctx.LiftN n k Γ Γ'
h : IsDefEq env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) (VExpr.liftN n A k)
w✝ : VExpr
H : IsDefEq env U Γ e1 e2 w✝
⊢ IsDefEq env U Γ e1 e2 A
Theorem: Lean4Lean.VEnv.IsDefEq.weakN_iff'
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
Γ : List VExpr
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
hΓ : OnCtx Γ (IsType env U)
n k : Nat
e1 e2 A : VExpr
W : Ctx.LiftN n k Γ Γ'
h : IsDefEq env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) (VExpr.liftN n A k)
w✝ : VExpr
H : IsDefEq env U Γ e1 e2 w✝
⊢ IsDefEq env U Γ e1 e2 A
Tactic:
refine IsDefEqU.defeqDF henv hΓ ?_ H
Proof state after:
env : VEnv
Γ' : List VExpr
U : Nat
Γ : List VExpr
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
hΓ : OnCtx Γ (IsType env U)
n k : Nat
e1 e2 A : VExpr
W : Ctx.LiftN n k Γ Γ'
h : IsDefEq env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) (VExpr.liftN n A k)
w✝ : VExpr
H : IsDefEq env U Γ e1 e2 w✝
⊢ IsDefEqU env U Γ w✝ A
Theorem: Lean4Lean.VEnv.IsDefEq.weakN_iff'
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
Γ : List VExpr
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
hΓ : OnCtx Γ (IsType env U)
n k : Nat
e1 e2 A : VExpr
W : Ctx.LiftN n k Γ Γ'
h : IsDefEq env U Γ' (VExpr.liftN n e1 k) (VExpr.liftN n e2 k) (VExpr.liftN n A k)
w✝ : VExpr
H : IsDefEq env U Γ e1 e2 w✝
⊢ IsDefEqU env U Γ w✝ A
Tactic:
exact (IsDefEqU.weakN_iff henv hΓ' W).1 <| (H.weakN henv W).uniqU henv hΓ' h.symm
Proof state after:
no goals
Theorem: Lean4Lean.OnCtx.weakN_inv
Proof state before:
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U : Nat
W : Ctx.LiftN n k Γ Γ'
H : OnCtx Γ' (IsType env U)
⊢ OnCtx Γ (IsType env U)
Tactic:
induction W with
| zero As h =>
  clear h
  induction As with
  | nil => exact H
  | cons A As ih => exact ih H.1
| succ W ih =>
  let ⟨H1, _, H2⟩ := H
  exact ⟨ih H1, _, (IsDefEq.weakN_iff' henv H1 (ih H1) W).1 H2⟩
Proof state after:
no goals
Theorem: Lean4Lean.OnCtx.weakN_inv
Proof state before:
case zero
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U : Nat
Γ✝ As : List VExpr
h : List.length As = n
H : OnCtx (As ++ Γ✝) (IsType env U)
⊢ OnCtx Γ✝ (IsType env U)
Tactic:
clear h
Proof state after:
case zero
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U : Nat
Γ✝ As : List VExpr
H : OnCtx (As ++ Γ✝) (IsType env U)
⊢ OnCtx Γ✝ (IsType env U)
Theorem: Lean4Lean.OnCtx.weakN_inv
Proof state before:
case zero
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U : Nat
Γ✝ As : List VExpr
H : OnCtx (As ++ Γ✝) (IsType env U)
⊢ OnCtx Γ✝ (IsType env U)
Tactic:
induction As with
| nil => exact H
| cons A As ih => exact ih H.1
Proof state after:
no goals
Theorem: Lean4Lean.OnCtx.weakN_inv
Proof state before:
case zero.nil
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U : Nat
Γ✝ : List VExpr
H : OnCtx ([] ++ Γ✝) (IsType env U)
⊢ OnCtx Γ✝ (IsType env U)
Tactic:
exact H
Proof state after:
no goals
Theorem: Lean4Lean.OnCtx.weakN_inv
Proof state before:
case zero.cons
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U : Nat
Γ✝ : List VExpr
A : VExpr
As : List VExpr
ih : OnCtx (As ++ Γ✝) (IsType env U) → OnCtx Γ✝ (IsType env U)
H : OnCtx (A :: As ++ Γ✝) (IsType env U)
⊢ OnCtx Γ✝ (IsType env U)
Tactic:
exact ih H.1
Proof state after:
no goals
Theorem: Lean4Lean.OnCtx.weakN_inv
Proof state before:
case succ
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
W : Ctx.LiftN n k✝ Γ✝ Γ'✝
ih : OnCtx Γ'✝ (IsType env U) → OnCtx Γ✝ (IsType env U)
H : OnCtx (VExpr.liftN n A✝ k✝ :: Γ'✝) (IsType env U)
⊢ OnCtx (A✝ :: Γ✝) (IsType env U)
Tactic:
let ⟨H1, _, H2⟩ := H
Proof state after:
case succ
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
W : Ctx.LiftN n k✝ Γ✝ Γ'✝
ih : OnCtx Γ'✝ (IsType env U) → OnCtx Γ✝ (IsType env U)
H : OnCtx (VExpr.liftN n A✝ k✝ :: Γ'✝) (IsType env U)
H1 : OnCtx Γ'✝ (IsType env U)
w✝ : VLevel
H2 : HasType env U Γ'✝ (VExpr.liftN n A✝ k✝) (VExpr.sort w✝)
⊢ OnCtx (A✝ :: Γ✝) (IsType env U)
Theorem: Lean4Lean.OnCtx.weakN_inv
Proof state before:
case succ
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
W : Ctx.LiftN n k✝ Γ✝ Γ'✝
ih : OnCtx Γ'✝ (IsType env U) → OnCtx Γ✝ (IsType env U)
H : OnCtx (VExpr.liftN n A✝ k✝ :: Γ'✝) (IsType env U)
H1 : OnCtx Γ'✝ (IsType env U)
w✝ : VLevel
H2 : HasType env U Γ'✝ (VExpr.liftN n A✝ k✝) (VExpr.sort w✝)
⊢ OnCtx (A✝ :: Γ✝) (IsType env U)
Tactic:
exact ⟨ih H1, _, (IsDefEq.weakN_iff' henv H1 (ih H1) W).1 H2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqU.weak'_iff
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 : VExpr
W : Ctx.Lift' l Γ Γ'
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Tactic:
generalize e : l.depth = n
Proof state after:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Theorem: Lean4Lean.VEnv.IsDefEqU.weak'_iff
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Tactic:
induction n generalizing l Γ' with
| zero => simp [VExpr.lift'_depth_zero e, W.depth_zero e]
| succ n ih =>
  obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
  have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
  simp only [Lift.consN_skip_eq, VExpr.lift'_comp, VExpr.lift'_consN_skipN,
    weakN_iff henv hΓ' W2, ih (hΓ'.weakN_inv henv W2) W1 Lift.depth_consN]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqU.weak'_iff
Proof state before:
case zero
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.zero
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Tactic:
simp [VExpr.lift'_depth_zero e, W.depth_zero e]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqU.weak'_iff
Proof state before:
case succ
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
n : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l : Lift},
        Ctx.Lift' l Γ Γ' →
          Lift.depth l = n → (IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2)
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.succ n
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Tactic:
obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
Proof state after:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEqU env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) ↔ IsDefEqU env U Γ e1 e2)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k)) ↔
    IsDefEqU env U Γ e1 e2
Theorem: Lean4Lean.VEnv.IsDefEqU.weak'_iff
Proof state before:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEqU env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) ↔ IsDefEqU env U Γ e1 e2)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k)) ↔
    IsDefEqU env U Γ e1 e2
Tactic:
have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
Proof state after:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEqU env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) ↔ IsDefEqU env U Γ e1 e2)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k)) ↔
    IsDefEqU env U Γ e1 e2
Theorem: Lean4Lean.VEnv.IsDefEqU.weak'_iff
Proof state before:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEqU env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) ↔ IsDefEqU env U Γ e1 e2)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k)) ↔
    IsDefEqU env U Γ e1 e2
Tactic:
simp only [Lift.consN_skip_eq, VExpr.lift'_comp, VExpr.lift'_consN_skipN,
  weakN_iff henv hΓ' W2, ih (hΓ'.weakN_inv henv W2) W1 Lift.depth_consN]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weak'_iff
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
⊢ IsDefEq env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) (VExpr.lift' A l) ↔ IsDefEq env U Γ e1 e2 A
Tactic:
generalize e : l.depth = n
Proof state after:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ IsDefEq env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) (VExpr.lift' A l) ↔ IsDefEq env U Γ e1 e2 A
Theorem: Lean4Lean.VEnv.IsDefEq.weak'_iff
Proof state before:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ IsDefEq env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) (VExpr.lift' A l) ↔ IsDefEq env U Γ e1 e2 A
Tactic:
induction n generalizing l Γ' with
| zero => simp [VExpr.lift'_depth_zero e, W.depth_zero e]
| succ n ih =>
  obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
  have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
  simp only [Lift.consN_skip_eq, VExpr.lift'_comp, VExpr.lift'_consN_skipN,
    weakN_iff henv hΓ' W2, ih (hΓ'.weakN_inv henv W2) W1 Lift.depth_consN]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weak'_iff
Proof state before:
case zero
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 A : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.zero
⊢ IsDefEq env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) (VExpr.lift' A l) ↔ IsDefEq env U Γ e1 e2 A
Tactic:
simp [VExpr.lift'_depth_zero e, W.depth_zero e]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weak'_iff
Proof state before:
case succ
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 A : VExpr
n : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l : Lift},
        Ctx.Lift' l Γ Γ' →
          Lift.depth l = n →
            (IsDefEq env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) (VExpr.lift' A l) ↔ IsDefEq env U Γ e1 e2 A)
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.succ n
⊢ IsDefEq env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) (VExpr.lift' A l) ↔ IsDefEq env U Γ e1 e2 A
Tactic:
obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
Proof state after:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 A : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEq env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) (VExpr.lift' A l_1) ↔ IsDefEq env U Γ e1 e2 A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEq env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k))
      (VExpr.lift' A (Lift.consN (Lift.skip l) k)) ↔
    IsDefEq env U Γ e1 e2 A
Theorem: Lean4Lean.VEnv.IsDefEq.weak'_iff
Proof state before:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 A : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEq env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) (VExpr.lift' A l_1) ↔ IsDefEq env U Γ e1 e2 A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEq env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k))
      (VExpr.lift' A (Lift.consN (Lift.skip l) k)) ↔
    IsDefEq env U Γ e1 e2 A
Tactic:
have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
Proof state after:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 A : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEq env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) (VExpr.lift' A l_1) ↔ IsDefEq env U Γ e1 e2 A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEq env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k))
      (VExpr.lift' A (Lift.consN (Lift.skip l) k)) ↔
    IsDefEq env U Γ e1 e2 A
Theorem: Lean4Lean.VEnv.IsDefEq.weak'_iff
Proof state before:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 A : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEq env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) (VExpr.lift' A l_1) ↔ IsDefEq env U Γ e1 e2 A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEq env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k))
      (VExpr.lift' A (Lift.consN (Lift.skip l) k)) ↔
    IsDefEq env U Γ e1 e2 A
Tactic:
simp only [Lift.consN_skip_eq, VExpr.lift'_comp, VExpr.lift'_consN_skipN,
  weakN_iff henv hΓ' W2, ih (hΓ'.weakN_inv henv W2) W1 Lift.depth_consN]
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.isSuffix
Proof state before:
n k : Nat
Γ Γ' : List VExpr
H : LiftN n k Γ Γ'
⊢ ∃ Γ₀ As Δ Δ', List.length As = n ∧ List.length Δ = k ∧ List.length Δ' = k ∧ Γ = Δ ++ Γ₀ ∧ Γ' = Δ' ++ As ++ Γ₀
Tactic:
induction H with
| @zero Γ As h => exact ⟨Γ, As, [], [], h, rfl, rfl, rfl, rfl⟩
| succ _ ih =>
  obtain ⟨_, _, Δ, Δ', hn, hΔ, hΔ', rfl, rfl⟩ := ih
  exact ⟨_, _, _ :: Δ, _ :: Δ', hn, by simp [hΔ], by simp [hΔ'], rfl, rfl⟩
Proof state after:
no goals