Theorem: Lean4Lean.VEnv.IsDefEqStrong.weakN
Proof state before:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih3 :
  IsDefEqStrong env U (liftN n (lift a) (k + 1) :: liftN n a k :: Γ') (liftN n (liftN 1 B 1) (k + 1 + 1))
    (liftN n (liftN 1 B 1) (k + 1 + 1)) (liftN n (sort v) (k + 1 + 1))
this : liftN 1 (liftN n B (k + 1)) 1 = liftN n (liftN 1 B 1) (1 + (k + 1))
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)
Tactic:
rw [Nat.add_comm 1] at this
Proof state after:
case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
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.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
ih3 :
  IsDefEqStrong env U (liftN n (lift a) (k + 1) :: liftN n a k :: Γ') (liftN n (liftN 1 B 1) (k + 1 + 1))
    (liftN n (liftN 1 B 1) (k + 1 + 1)) (liftN n (sort v) (k + 1 + 1))
this : liftN 1 (liftN n B (k + 1)) 1 = liftN n (liftN 1 B 1) (k + 1 + 1)
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)