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

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
t u : LambdaTerm p U C
n : ℕ
h : freeVarRange u ≤ n
⊢ replace' (instantiateFun t) 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
t : LambdaTerm p U C
a✝ : C
n : ℕ
h : 0 ≤ n
⊢ replace' (instantiateFun t) n (const a✝) = const a✝

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

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

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

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

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

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

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

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

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

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

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

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
m n : ℕ
h : m + 1 ≤ n
⊢ replace' (instantiateFun t) n (var m) = var m
Tactic:
case var m =>
  rw [Nat.add_one_le_iff] at h
  rw [replace'_var, instantiateFun]
  aesop
State after:
no goals

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

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

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

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

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

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

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

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

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

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

case elim
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
a✝² : p.empty = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' (instantiateFun t) n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' (instantiateFun t) 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
t : LambdaTerm p U C
m n : ℕ
h : m + 1 ≤ n
⊢ replace' (instantiateFun t) 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
t : LambdaTerm p U C
m n : ℕ
h : m < n
⊢ replace' (instantiateFun t) n (var m) = var m

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

State before:
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
m n : ℕ
h : m < n
⊢ (match
      match var m with
      | var m => some (if m = n then t else if m < n then var m else var (m - 1))
      | x => none with
    | some u => u
    | none => var m) =
    var m
Tactic:
aesop
State after:
no goals

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