Theorem: Lean4Lean.VExpr.ClosedN.mono (Lean4Lean/Theory/VExpr.lean)

State before:
k k' : Nat
e : VExpr
h : k ≤ k'
self : ClosedN e k
⊢ ClosedN e k'
Tactic:
induction e generalizing k k' with (simp [ClosedN] at self ⊢; try simp [self, *])
| bvar i => exact Nat.lt_of_lt_of_le self h
| app _ _ ih1 ih2 => exact ⟨ih1 h self.1, ih2 h self.2⟩
| lam _ _ ih1 ih2 | forallE _ _ ih1 ih2 =>
  exact ⟨ih1 h self.1, ih2 (Nat.succ_le_succ h) self.2⟩
State after:
no goals

State before:
case const
declName✝ : Name
us✝ : List VLevel
k k' : Nat
h : k ≤ k'
self : ClosedN (const declName✝ us✝) k
⊢ ClosedN (const declName✝ us✝) k'
Tactic:
simp [ClosedN] at self ⊢
State after:
no goals

State before:
case bvar
i k k' : Nat
h : k ≤ k'
self : i < k
⊢ i < k'
Tactic:
exact Nat.lt_of_lt_of_le self h
State after:
no goals

State before:
case app
fn✝ arg✝ : VExpr
ih1 : ∀ {k k' : Nat}, k ≤ k' → ClosedN fn✝ k → ClosedN fn✝ k'
ih2 : ∀ {k k' : Nat}, k ≤ k' → ClosedN arg✝ k → ClosedN arg✝ k'
k k' : Nat
h : k ≤ k'
self : ClosedN fn✝ k ∧ ClosedN arg✝ k
⊢ ClosedN fn✝ k' ∧ ClosedN arg✝ k'
Tactic:
exact ⟨ih1 h self.1, ih2 h self.2⟩
State after:
no goals

State before:
case forallE
binderType✝ body✝ : VExpr
ih1 : ∀ {k k' : Nat}, k ≤ k' → ClosedN binderType✝ k → ClosedN binderType✝ k'
ih2 : ∀ {k k' : Nat}, k ≤ k' → ClosedN body✝ k → ClosedN body✝ k'
k k' : Nat
h : k ≤ k'
self : ClosedN binderType✝ k ∧ ClosedN body✝ (k + 1)
⊢ ClosedN binderType✝ k' ∧ ClosedN body✝ (k' + 1)
Tactic:
exact ⟨ih1 h self.1, ih2 (Nat.succ_le_succ h) self.2⟩
State after:
no goals