Theorem: Lean4Lean.VEnv.IsDefEqU.defeqDF (Lean4Lean/Theory/Typing/UniqueTyping.lean)

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

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

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