Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
this :
  IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (inst (lift e✝) e₀ (k + 1)) (inst (lift e✝) e₀ (k + 1))
    (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ (k + 1))
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (liftN 1 (inst B✝ e₀ (k + 1)) 1))
Tactic:
simp only [inst, ← lift_instN_lo] at this
Proof state after:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst A✝ e₀ k) (inst A✝ e₀ k) (inst (sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst B✝ e₀ k) (inst B✝ e₀ k) (inst (sort v✝) e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (lift A✝ :: A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (liftN 1 B✝ 1) e₀ k) (inst (liftN 1 B✝ 1) e₀ k) (inst (sort v✝) e₀ k)
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (lift e✝) e₀ k) (inst (lift e✝) e₀ k) (inst (forallE (lift A✝) (liftN 1 B✝ 1)) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hΓ' : CtxStrong env U (inst A✝ e₀ k :: Γ)
this :
  IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (inst (liftN 1 B✝ 1) e₀ (k + 1 + 1)))
⊢ IsDefEqStrong env U (inst A✝ e₀ k :: Γ) (lift (inst e✝ e₀ k)) (lift (inst e✝ e₀ k))
    (forallE (lift (inst A✝ e₀ k)) (liftN 1 (inst B✝ e₀ (k + 1)) 1))