Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le (LambdaCalculi/LambdaCalculus.lean)

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
u : LambdaTerm p U C
n : ℕ
h : freeVarRange u ≤ n
⊢ replace' liftFun n u = u
Tactic:
induction u generalizing n <;> rw [freeVarRange] at h
State after:
case const
p : LambdaParams
U : Type u_1
C : Type u_2
a✝ : C
n : ℕ
h : 0 ≤ n
⊢ replace' liftFun n (const a✝) = const a✝

case var
p : LambdaParams
U : Type u_1
C : Type u_2
a✝ n : ℕ
h : a✝ + 1 ≤ n
⊢ replace' liftFun n (var a✝) = var a✝

case lambda
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ - 1 ≤ n
⊢ replace' liftFun n (lambda a✝² a✝¹ a✝) = lambda a✝² a✝¹ a✝

case app
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.lambda = true
a✝¹ a✝ : LambdaTerm p U C
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (freeVarRange a✝¹) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (app a✝² a✝¹ a✝) = app a✝² a✝¹ a✝

case pair
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.prod = true
a✝¹ a✝ : LambdaTerm p U C
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (freeVarRange a✝¹) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (pair a✝² a✝¹ a✝) = pair a✝² a✝¹ a✝

case fst
p : LambdaParams
U : Type u_1
C : Type u_2
a✝¹ : p.prod = true
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (fst a✝¹ a✝) = fst a✝¹ a✝

case snd
p : LambdaParams
U : Type u_1
C : Type u_2
a✝¹ : p.prod = true
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (snd a✝¹ a✝) = snd a✝¹ a✝

case inl
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.coprod = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (inl a✝² a✝¹ a✝) = inl a✝² a✝¹ a✝

case inr
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.coprod = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (inr a✝² a✝¹ a✝) = inr a✝² a✝¹ a✝

case case
p : LambdaParams
U : Type u_1
C : Type u_2
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C
a_ih✝² : ∀ (n : ℕ), freeVarRange a✝² ≤ n → replace' liftFun n a✝² = a✝²
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (max (freeVarRange a✝²) (freeVarRange a✝¹) - 1) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (case a✝³ a✝² a✝¹ a✝) = case a✝³ a✝² a✝¹ a✝

case star
p : LambdaParams
U : Type u_1
C : Type u_2
a✝ : p.unit = true
n : ℕ
h : 0 ≤ n
⊢ replace' liftFun n (star a✝) = star a✝

case elim
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.empty = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (elim a✝² a✝¹ a✝) = elim a✝² a✝¹ a✝

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m + 1 ≤ n
⊢ replace' liftFun n (var m) = var m
Tactic:
case var m =>
  rw [Nat.add_one_le_iff] at h
  rw [replace'_var, liftFun]
  simp only
  rw [if_neg]
  rw [not_le]
  exact h
State after:
no goals

State before:
case const
p : LambdaParams
U : Type u_1
C : Type u_2
a✝ : C
n : ℕ
h : 0 ≤ n
⊢ replace' liftFun n (const a✝) = const a✝

case lambda
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ - 1 ≤ n
⊢ replace' liftFun n (lambda a✝² a✝¹ a✝) = lambda a✝² a✝¹ a✝

case app
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.lambda = true
a✝¹ a✝ : LambdaTerm p U C
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (freeVarRange a✝¹) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (app a✝² a✝¹ a✝) = app a✝² a✝¹ a✝

case pair
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.prod = true
a✝¹ a✝ : LambdaTerm p U C
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (freeVarRange a✝¹) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (pair a✝² a✝¹ a✝) = pair a✝² a✝¹ a✝

case fst
p : LambdaParams
U : Type u_1
C : Type u_2
a✝¹ : p.prod = true
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (fst a✝¹ a✝) = fst a✝¹ a✝

case snd
p : LambdaParams
U : Type u_1
C : Type u_2
a✝¹ : p.prod = true
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (snd a✝¹ a✝) = snd a✝¹ a✝

case inl
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.coprod = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (inl a✝² a✝¹ a✝) = inl a✝² a✝¹ a✝

case inr
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.coprod = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (inr a✝² a✝¹ a✝) = inr a✝² a✝¹ a✝

case case
p : LambdaParams
U : Type u_1
C : Type u_2
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C
a_ih✝² : ∀ (n : ℕ), freeVarRange a✝² ≤ n → replace' liftFun n a✝² = a✝²
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (max (freeVarRange a✝²) (freeVarRange a✝¹) - 1) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (case a✝³ a✝² a✝¹ a✝) = case a✝³ a✝² a✝¹ a✝

case star
p : LambdaParams
U : Type u_1
C : Type u_2
a✝ : p.unit = true
n : ℕ
h : 0 ≤ n
⊢ replace' liftFun n (star a✝) = star a✝

case elim
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.empty = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (elim a✝² a✝¹ a✝) = elim a✝² a✝¹ a✝
Tactic:
all_goals aesop
State after:
no goals

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m + 1 ≤ n
⊢ replace' liftFun n (var m) = var m
Tactic:
rw [Nat.add_one_le_iff] at h
State after:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ replace' liftFun n (var m) = var m

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ replace' liftFun n (var m) = var m
Tactic:
rw [replace'_var, liftFun]
State after:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ (match
      match var m with
      | var m => if n ≤ m then some (var (m + 1)) else none
      | x => none with
    | some u => u
    | none => var m) =
    var m

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ (match
      match var m with
      | var m => if n ≤ m then some (var (m + 1)) else none
      | x => none with
    | some u => u
    | none => var m) =
    var m
Tactic:
simp only
State after:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ (match if n ≤ m then some (var (m + 1)) else none with
    | some u => u
    | none => var m) =
    var m

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ (match if n ≤ m then some (var (m + 1)) else none with
    | some u => u
    | none => var m) =
    var m
Tactic:
rw [if_neg]
State after:
case hnc
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ ¬n ≤ m

State before:
case hnc
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ ¬n ≤ m
Tactic:
rw [not_le]
State after:
case hnc
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ m < n

State before:
case hnc
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ m < n
Tactic:
exact h
State after:
no goals

State before:
case elim
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.empty = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (elim a✝² a✝¹ a✝) = elim a✝² a✝¹ a✝
Tactic:
aesop
State after:
no goals