Theorem: Lean4Lean.VEnv.IsDefEq.defeqDFC' (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
env : VEnv
U : Nat
Γ₀ Γ₁ Γ₂ Δ : List VExpr
e₁ e₂ A : VExpr
henv : Ordered env
h1 : IsDefEqCtx env U Γ₀ Γ₁ Γ₂
h2 : IsDefEq env U (Δ ++ Γ₁) e₁ e₂ A
⊢ IsDefEq env U (Δ ++ Γ₂) e₁ e₂ A
Tactic:
induction h1 generalizing e₁ e₂ A Δ with
| zero => exact h2
| @succ _ _ _ A₂ _ _ AA ih =>
  simpa using ih (Δ := Δ ++ [A₂]) (by simpa using AA.defeqDF_l' henv h2)
State after:
no goals

State before:
case zero
env : VEnv
U : Nat
Γ₀ Γ₁ Γ₂ : List VExpr
henv : Ordered env
Δ : List VExpr
e₁ e₂ A : VExpr
h2 : IsDefEq env U (Δ ++ Γ₀) e₁ e₂ A
⊢ IsDefEq env U (Δ ++ Γ₀) e₁ e₂ A
Tactic:
exact h2
State after:
no goals

State before:
case succ
env : VEnv
U : Nat
Γ₀ Γ₁ Γ₂ : List VExpr
henv : Ordered env
Γ₁✝ Γ₂✝ : List VExpr
A₁✝ A₂ : VExpr
u✝ : VLevel
a✝ : IsDefEqCtx env U Γ₀ Γ₁✝ Γ₂✝
AA : IsDefEq env U Γ₁✝ A₁✝ A₂ (VExpr.sort u✝)
ih : ∀ {Δ : List VExpr} {e₁ e₂ A : VExpr}, IsDefEq env U (Δ ++ Γ₁✝) e₁ e₂ A → IsDefEq env U (Δ ++ Γ₂✝) e₁ e₂ A
Δ : List VExpr
e₁ e₂ A : VExpr
h2 : IsDefEq env U (Δ ++ A₁✝ :: Γ₁✝) e₁ e₂ A
⊢ IsDefEq env U (Δ ++ A₂ :: Γ₂✝) e₁ e₂ A
Tactic:
simpa using ih (Δ := Δ ++ [A₂]) (by simpa using AA.defeqDF_l' henv h2)
State after:
no goals

State before:
env : VEnv
U : Nat
Γ₀ Γ₁ Γ₂ : List VExpr
henv : Ordered env
Γ₁✝ Γ₂✝ : List VExpr
A₁✝ A₂ : VExpr
u✝ : VLevel
a✝ : IsDefEqCtx env U Γ₀ Γ₁✝ Γ₂✝
AA : IsDefEq env U Γ₁✝ A₁✝ A₂ (VExpr.sort u✝)
ih : ∀ {Δ : List VExpr} {e₁ e₂ A : VExpr}, IsDefEq env U (Δ ++ Γ₁✝) e₁ e₂ A → IsDefEq env U (Δ ++ Γ₂✝) e₁ e₂ A
Δ : List VExpr
e₁ e₂ A : VExpr
h2 : IsDefEq env U (Δ ++ A₁✝ :: Γ₁✝) e₁ e₂ A
⊢ IsDefEq env U (Δ ++ [A₂] ++ Γ₁✝) e₁ e₂ A
Tactic:
simpa using AA.defeqDF_l' henv h2
State after:
no goals