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

State before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
⊢ IsDefEq env U Γ e₁ e₂ A ↔ HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
Tactic:
refine ⟨fun h => ⟨h.hasType.1, h.hasType.2, _, h⟩, fun ⟨_, h2, _, h3⟩ => ?_⟩
State after:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
x✝ : HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
left✝ : HasType env U Γ e₁ A
h2 : HasType env U Γ e₂ A
w✝ : VExpr
h3 : IsDefEq env U Γ e₁ e₂ w✝
⊢ IsDefEq env U Γ e₁ e₂ A

State before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
x✝ : HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
left✝ : HasType env U Γ e₁ A
h2 : HasType env U Γ e₂ A
w✝ : VExpr
h3 : IsDefEq env U Γ e₁ e₂ w✝
⊢ IsDefEq env U Γ e₁ e₂ A
Tactic:
have ⟨_, h⟩ := h3.uniq henv hΓ h2
State after:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
x✝ : HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
left✝ : HasType env U Γ e₁ A
h2 : HasType env U Γ e₂ A
w✝¹ : VExpr
h3 : IsDefEq env U Γ e₁ e₂ w✝¹
w✝ : VLevel
h : IsDefEq env U Γ w✝¹ A (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₂ A

State before:
env : VEnv
Γ : List VExpr
U : Nat
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
x✝ : HasType env U Γ e₁ A ∧ HasType env U Γ e₂ A ∧ IsDefEqU env U Γ e₁ e₂
left✝ : HasType env U Γ e₁ A
h2 : HasType env U Γ e₂ A
w✝¹ : VExpr
h3 : IsDefEq env U Γ e₁ e₂ w✝¹
w✝ : VLevel
h : IsDefEq env U Γ w✝¹ A (VExpr.sort w✝)
⊢ IsDefEq env U Γ e₁ e₂ A
Tactic:
exact h.defeqDF h3
State after:
no goals