Theorem: Lean4Lean.VEnv.IsDefEq.weakN_iff' (Lean4Lean/Theory/Typing/UniqueTyping.lean)

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

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

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

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