Theorem: Lean4Lean.VEnv.IsDefEq.skips (Lean4Lean/Theory/Typing/UniqueTyping.lean)

State before:
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
e₁ e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
H : IsDefEq env U Γ' e₁ e₂ A
h1 : VExpr.Skips e₁ n k
h2 : VExpr.Skips e₂ n k
⊢ ∃ B, IsDefEq env U Γ' e₁ e₂ B ∧ VExpr.Skips B n k
Tactic:
obtain ⟨e₁, rfl⟩ := VExpr.skips_iff_exists.1 h1
State after:
case intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
h2 : VExpr.Skips e₂ n k
e₁ : VExpr
H : IsDefEq env U Γ' (VExpr.liftN n e₁ k) e₂ A
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) e₂ B ∧ VExpr.Skips B n k

State before:
case intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
e₂ A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
h2 : VExpr.Skips e₂ n k
e₁ : VExpr
H : IsDefEq env U Γ' (VExpr.liftN n e₁ k) e₂ A
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) e₂ B ∧ VExpr.Skips B n k
Tactic:
obtain ⟨e₂, rfl⟩ := VExpr.skips_iff_exists.1 h2
State after:
case intro.intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
e₁ : VExpr
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
e₂ : VExpr
h2 : VExpr.Skips (VExpr.liftN n e₂ k) n k
H : IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) A
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) B ∧ VExpr.Skips B n k

State before:
case intro.intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
e₁ : VExpr
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
e₂ : VExpr
h2 : VExpr.Skips (VExpr.liftN n e₂ k) n k
H : IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) A
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) B ∧ VExpr.Skips B n k
Tactic:
have ⟨_, H⟩ := (IsDefEqU.weakN_iff henv hΓ W).1 ⟨_, H⟩
State after:
case intro.intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
e₁ : VExpr
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
e₂ : VExpr
h2 : VExpr.Skips (VExpr.liftN n e₂ k) n k
H✝ : IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) A
w✝ : VExpr
H : IsDefEq env U Γ e₁ e₂ w✝
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) B ∧ VExpr.Skips B n k

State before:
case intro.intro
env : VEnv
Γ' : List VExpr
U n k : Nat
Γ : List VExpr
A : VExpr
henv : Ordered env
hΓ : OnCtx Γ' (IsType env U)
W : Ctx.LiftN n k Γ Γ'
e₁ : VExpr
h1 : VExpr.Skips (VExpr.liftN n e₁ k) n k
e₂ : VExpr
h2 : VExpr.Skips (VExpr.liftN n e₂ k) n k
H✝ : IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) A
w✝ : VExpr
H : IsDefEq env U Γ e₁ e₂ w✝
⊢ ∃ B, IsDefEq env U Γ' (VExpr.liftN n e₁ k) (VExpr.liftN n e₂ k) B ∧ VExpr.Skips B n k
Tactic:
exact ⟨_, H.weakN henv W, .liftN⟩
State after:
no goals