Theorem: Lean4Lean.VExpr.of_liftN_eq_instL (Lean4Lean/Theory/VExpr.lean)

State before:
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e2 : VExpr
h : liftN n e1 k = instL ls e2
⊢ ∃ e', e1 = instL ls e' ∧ e2 = liftN n e' k
Tactic:
have : (instL ls e2).Skips n k := h ▸ .liftN
State after:
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e2 : VExpr
h : liftN n e1 k = instL ls e2
this : Skips (instL ls e2) n k
⊢ ∃ e', e1 = instL ls e' ∧ e2 = liftN n e' k

State before:
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e2 : VExpr
h : liftN n e1 k = instL ls e2
this : Skips (instL ls e2) n k
⊢ ∃ e', e1 = instL ls e' ∧ e2 = liftN n e' k
Tactic:
obtain ⟨e', rfl⟩ := skips_iff_exists.1 this.of_instL
State after:
case intro
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e' : VExpr
h : liftN n e1 k = instL ls (liftN n e' k)
this : Skips (instL ls (liftN n e' k)) n k
⊢ ∃ e'_1, e1 = instL ls e'_1 ∧ liftN n e' k = liftN n e'_1 k

State before:
case intro
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e' : VExpr
h : liftN n e1 k = instL ls (liftN n e' k)
this : Skips (instL ls (liftN n e' k)) n k
⊢ ∃ e'_1, e1 = instL ls e'_1 ∧ liftN n e' k = liftN n e'_1 k
Tactic:
refine ⟨e', ?_, rfl⟩
State after:
case intro
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e' : VExpr
h : liftN n e1 k = instL ls (liftN n e' k)
this : Skips (instL ls (liftN n e' k)) n k
⊢ e1 = instL ls e'

State before:
case intro
n : Nat
e1 : VExpr
k : Nat
ls : List VLevel
e' : VExpr
h : liftN n e1 k = instL ls (liftN n e' k)
this : Skips (instL ls (liftN n e' k)) n k
⊢ e1 = instL ls e'
Tactic:
rw [← liftN_inj, h, instL_liftN]
State after:
no goals