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

State before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
h1 : IsDefEq env U Γ A A' (VExpr.sort u)
h2 : IsDefEq env U (Δ ++ A :: Γ) e1 e2 B
⊢ IsDefEq env U (Δ ++ A' :: Γ) e1 e2 B
Tactic:
have ⟨_, H1, H2⟩ : ∃ Γ', Ctx.LiftN 1 (Δ.length + 1) (Δ ++ A :: Γ) Γ' ∧
    Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) Δ.length Γ' (Δ ++ A' :: Γ) := by
  clear h1 h2
  induction Δ with
  | nil => exact ⟨_, .succ (.one (A := A')), .zero⟩
  | cons B Δ ih =>
    have ⟨Γ', h1, h2⟩ := ih
    exact ⟨_, .succ h1, by simpa [instN_bvar0] using h2.succ (A := liftN 1 B (Δ.length + 1))⟩
State after:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
h1 : IsDefEq env U Γ A A' (VExpr.sort u)
h2 : IsDefEq env U (Δ ++ A :: Γ) e1 e2 B
w✝ : List VExpr
H1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) w✝
H2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) w✝ (Δ ++ A' :: Γ)
⊢ IsDefEq env U (Δ ++ A' :: Γ) e1 e2 B

State before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
h1 : IsDefEq env U Γ A A' (VExpr.sort u)
h2 : IsDefEq env U (Δ ++ A :: Γ) e1 e2 B
w✝ : List VExpr
H1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) w✝
H2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) w✝ (Δ ++ A' :: Γ)
⊢ IsDefEq env U (Δ ++ A' :: Γ) e1 e2 B
Tactic:
simpa [instN_bvar0] using
  instN henv (h1.weakN henv (.one (A := A')) |>.symm.defeq (.bvar .zero)) H2 (.weakN henv H1 h2)
State after:
no goals

State before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
h1 : IsDefEq env U Γ A A' (VExpr.sort u)
h2 : IsDefEq env U (Δ ++ A :: Γ) e1 e2 B
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Tactic:
clear h1 h2
State after:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)

State before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Tactic:
induction Δ with
| nil => exact ⟨_, .succ (.one (A := A')), .zero⟩
| cons B Δ ih =>
  have ⟨Γ', h1, h2⟩ := ih
  exact ⟨_, .succ h1, by simpa [instN_bvar0] using h2.succ (A := liftN 1 B (Δ.length + 1))⟩
State after:
no goals

State before:
case nil
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B : VExpr
henv : Ordered env
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length [] + 1) ([] ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length []) Γ' ([] ++ A' :: Γ)
Tactic:
exact ⟨_, .succ (.one (A := A')), .zero⟩
State after:
no goals

State before:
case cons
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B✝ : VExpr
henv : Ordered env
B : VExpr
Δ : List VExpr
ih :
  ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length (B :: Δ) + 1) (B :: Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length (B :: Δ)) Γ' (B :: Δ ++ A' :: Γ)
Tactic:
have ⟨Γ', h1, h2⟩ := ih
State after:
case cons
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B✝ : VExpr
henv : Ordered env
B : VExpr
Δ : List VExpr
ih :
  ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Γ' : List VExpr
h1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ'
h2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length (B :: Δ) + 1) (B :: Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length (B :: Δ)) Γ' (B :: Δ ++ A' :: Γ)

State before:
case cons
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B✝ : VExpr
henv : Ordered env
B : VExpr
Δ : List VExpr
ih :
  ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Γ' : List VExpr
h1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ'
h2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length (B :: Δ) + 1) (B :: Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length (B :: Δ)) Γ' (B :: Δ ++ A' :: Γ)
Tactic:
exact ⟨_, .succ h1, by simpa [instN_bvar0] using h2.succ (A := liftN 1 B (Δ.length + 1))⟩
State after:
no goals

State before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B✝ : VExpr
henv : Ordered env
B : VExpr
Δ : List VExpr
ih :
  ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Γ' : List VExpr
h1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ'
h2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
⊢ Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length (B :: Δ)) (liftN 1 B (List.length (B :: Δ)) :: Γ')
    (B :: Δ ++ A' :: Γ)
Tactic:
simpa [instN_bvar0] using h2.succ (A := liftN 1 B (Δ.length + 1))
State after:
no goals