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

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₃ B
Tactic:
have ⟨_, h⟩ := h₁.uniq henv hΓ h₂
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₃ B

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