Theorem: Lean4Lean.VEnv.IsDefEqU.weak'_iff (Lean4Lean/Theory/Typing/UniqueTyping.lean)

State before:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 : VExpr
W : Ctx.Lift' l Γ Γ'
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Tactic:
generalize e : l.depth = n
State after:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2

State before:
env : VEnv
Γ' : List VExpr
U : Nat
henv : Ordered env
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
Γ : List VExpr
e1 e2 : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Tactic:
induction n generalizing l Γ' with
| zero => simp [VExpr.lift'_depth_zero e, W.depth_zero e]
| succ n ih =>
  obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
  have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
  simp only [Lift.consN_skip_eq, VExpr.lift'_comp, VExpr.lift'_consN_skipN,
    weakN_iff henv hΓ' W2, ih (hΓ'.weakN_inv henv W2) W1 Lift.depth_consN]
State after:
no goals

State before:
case zero
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.zero
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Tactic:
simp [VExpr.lift'_depth_zero e, W.depth_zero e]
State after:
no goals

State before:
case succ
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
n : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l : Lift},
        Ctx.Lift' l Γ Γ' →
          Lift.depth l = n → (IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2)
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.succ n
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 l) (VExpr.lift' e2 l) ↔ IsDefEqU env U Γ e1 e2
Tactic:
obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
State after:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEqU env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) ↔ IsDefEqU env U Γ e1 e2)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k)) ↔
    IsDefEqU env U Γ e1 e2

State before:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEqU env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) ↔ IsDefEqU env U Γ e1 e2)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k)) ↔
    IsDefEqU env U Γ e1 e2
Tactic:
have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
State after:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEqU env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) ↔ IsDefEqU env U Γ e1 e2)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k)) ↔
    IsDefEqU env U Γ e1 e2

State before:
case succ.intro.intro.intro
env : VEnv
U : Nat
henv : Ordered env
Γ : List VExpr
e1 e2 : VExpr
Γ' : List VExpr
hΓ' : OnCtx Γ' (IsType env U)
l : Lift
k : Nat
ih :
  ∀ {Γ' : List VExpr},
    OnCtx Γ' (IsType env U) →
      ∀ {l_1 : Lift},
        Ctx.Lift' l_1 Γ Γ' →
          Lift.depth l_1 = Lift.depth l →
            (IsDefEqU env U Γ' (VExpr.lift' e1 l_1) (VExpr.lift' e2 l_1) ↔ IsDefEqU env U Γ e1 e2)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEqU env U Γ' (VExpr.lift' e1 (Lift.consN (Lift.skip l) k)) (VExpr.lift' e2 (Lift.consN (Lift.skip l) k)) ↔
    IsDefEqU env U Γ e1 e2
Tactic:
simp only [Lift.consN_skip_eq, VExpr.lift'_comp, VExpr.lift'_consN_skipN,
  weakN_iff henv hΓ' W2, ih (hΓ'.weakN_inv henv W2) W1 Lift.depth_consN]
State after:
no goals