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

State before:
env : VEnv
henv : Ordered env
l : Lift
Γ Γ' : List VExpr
U : Nat
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
H : IsDefEq env U Γ e1 e2 A
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
Tactic:
generalize e : l.depth = n
State after:
env : VEnv
henv : Ordered env
l : Lift
Γ Γ' : List VExpr
U : Nat
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
H : IsDefEq env U Γ e1 e2 A
n : Nat
e : Lift.depth l = n
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)

State before:
env : VEnv
henv : Ordered env
l : Lift
Γ Γ' : List VExpr
U : Nat
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
H : IsDefEq env U Γ e1 e2 A
n : Nat
e : Lift.depth l = n
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
Tactic:
induction n generalizing l Γ' with
| zero => simpa [lift'_depth_zero e, W.depth_zero e] using H
| 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, lift'_comp, lift'_consN_skipN]
  exact (ih W1 Lift.depth_consN).weakN henv W2
State after:
no goals

State before:
case zero
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
l : Lift
Γ' : List VExpr
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.zero
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
Tactic:
simpa [lift'_depth_zero e, W.depth_zero e] using H
State after:
no goals

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

State before:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEq env U Γ' (lift' e1 (Lift.consN (Lift.skip l) k)) (lift' e2 (Lift.consN (Lift.skip l) k))
    (lift' A (Lift.consN (Lift.skip l) k))
Tactic:
have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
State after:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
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 Γ₁ Γ'
⊢ IsDefEq env U Γ' (lift' e1 (Lift.consN (Lift.skip l) k)) (lift' e2 (Lift.consN (Lift.skip l) k))
    (lift' A (Lift.consN (Lift.skip l) k))

State before:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
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 Γ₁ Γ'
⊢ IsDefEq env U Γ' (lift' e1 (Lift.consN (Lift.skip l) k)) (lift' e2 (Lift.consN (Lift.skip l) k))
    (lift' A (Lift.consN (Lift.skip l) k))
Tactic:
simp only [Lift.consN_skip_eq, lift'_comp, lift'_consN_skipN]
State after:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
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 Γ₁ Γ'
⊢ IsDefEq env U Γ' (liftN 1 (lift' e1 (Lift.consN l k)) k) (liftN 1 (lift' e2 (Lift.consN l k)) k)
    (liftN 1 (lift' A (Lift.consN l k)) k)

State before:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
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 Γ₁ Γ'
⊢ IsDefEq env U Γ' (liftN 1 (lift' e1 (Lift.consN l k)) k) (liftN 1 (lift' e2 (Lift.consN l k)) k)
    (liftN 1 (lift' A (Lift.consN l k)) k)
Tactic:
exact (ih W1 Lift.depth_consN).weakN henv W2
State after:
no goals