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

State before:
n : Nat
e : VExpr
k : Nat
⊢ sizeOf e ≤ sizeOf (liftN n e k)
Tactic:
induction e generalizing k with simp [liftN, Nat.add_assoc, Nat.add_le_add_iff_left]
| bvar => simp [liftVar]; split <;> simp [Nat.le_add_left]
| _ => rename_i ih1 ih2; exact Nat.add_le_add (ih1 _) (ih2 _)
State after:
no goals

State before:
case bvar
n deBruijnIndex✝ k : Nat
⊢ deBruijnIndex✝ ≤ liftVar n deBruijnIndex✝ k
Tactic:
simp [liftVar]
State after:
case bvar
n deBruijnIndex✝ k : Nat
⊢ deBruijnIndex✝ ≤ if deBruijnIndex✝ < k then deBruijnIndex✝ else n + deBruijnIndex✝

State before:
case bvar
n deBruijnIndex✝ k : Nat
⊢ deBruijnIndex✝ ≤ if deBruijnIndex✝ < k then deBruijnIndex✝ else n + deBruijnIndex✝
Tactic:
split <;> simp [Nat.le_add_left]
State after:
no goals

State before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ : ∀ (k : Nat), sizeOf binderType✝ ≤ sizeOf (liftN n binderType✝ k)
body_ih✝ : ∀ (k : Nat), sizeOf body✝ ≤ sizeOf (liftN n body✝ k)
k : Nat
⊢ sizeOf binderType✝ + sizeOf body✝ ≤ sizeOf (liftN n binderType✝ k) + sizeOf (liftN n body✝ (k + 1))
Tactic:
rename_i ih1 ih2
State after:
case forallE
n : Nat
binderType✝ body✝ : VExpr
ih1 : ∀ (k : Nat), sizeOf binderType✝ ≤ sizeOf (liftN n binderType✝ k)
ih2 : ∀ (k : Nat), sizeOf body✝ ≤ sizeOf (liftN n body✝ k)
k : Nat
⊢ sizeOf binderType✝ + sizeOf body✝ ≤ sizeOf (liftN n binderType✝ k) + sizeOf (liftN n body✝ (k + 1))

State before:
case forallE
n : Nat
binderType✝ body✝ : VExpr
ih1 : ∀ (k : Nat), sizeOf binderType✝ ≤ sizeOf (liftN n binderType✝ k)
ih2 : ∀ (k : Nat), sizeOf body✝ ≤ sizeOf (liftN n body✝ k)
k : Nat
⊢ sizeOf binderType✝ + sizeOf body✝ ≤ sizeOf (liftN n binderType✝ k) + sizeOf (liftN n body✝ (k + 1))
Tactic:
exact Nat.add_le_add (ih1 _) (ih2 _)
State after:
no goals