Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case eta
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 Γ
⊢ IsDefEqStrong env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)
Tactic:
have :=
  have hΓ' := ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩
  IsDefEqStrong.eta h1 h2 (ih1 W hΓ) (ih2 W.succ hΓ')
    (by
      have := ih3 W.succ.succ ⟨hΓ', _, by
        rw [← lift_instN_lo]; exact (ih1 W hΓ).hasType.1.weakN henv .one⟩
      rwa [lift_instN_lo, liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1])
    (ih4 W hΓ)
    (by
      have := ih5 W.succ hΓ'
      simp only [inst, ← lift_instN_lo] at this
      rwa [liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1])
Proof state after:
case eta
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 Γ
this :
  IsDefEqStrong env U Γ (lam (inst A✝ e₀ k) (app (lift (inst e✝ e₀ k)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEqStrong env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (forallE A✝ B✝) e₀ k)