Theorem: Lean4Lean.OnCtx.weakN_inv (Lean4Lean/Theory/Typing/UniqueTyping.lean)

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⟩
State after:
no goals

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
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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)

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⟩
State after:
no goals