Theorem: LambdaCalculi.LambdaTerm.instantiate'_eq_of_freeVarRange_le
Proof 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
Proof 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✝