Theorem: LambdaCalculi.hasType_var (LambdaCalculi/HasType.lean)

State before:
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.var n ∶ σ) ↔ ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }
Tactic:
constructor
State after:
case mp
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.var n ∶ σ) → ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }

case mpr
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }) → (Γ ⊢[T] LambdaTerm.var n ∶ σ)

State before:
case mp
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.var n ∶ σ) → ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }
Tactic:
intro h
State after:
case mp
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.var n ∶ σ
⊢ ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }

State before:
case mp
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.var n ∶ σ
⊢ ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }
Tactic:
cases h
State after:
case mp.var
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
h✝ : n < List.length Γ
⊢ ∃ (h : n < List.length Γ), List.get Γ { val := n, isLt := h✝ } = List.get Γ { val := n, isLt := h }

State before:
case mp.var
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
h✝ : n < List.length Γ
⊢ ∃ (h : n < List.length Γ), List.get Γ { val := n, isLt := h✝ } = List.get Γ { val := n, isLt := h }
Tactic:
exact ⟨_, rfl⟩
State after:
no goals

State before:
case mpr
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }) → (Γ ⊢[T] LambdaTerm.var n ∶ σ)
Tactic:
rintro ⟨h, rfl⟩
State after:
case mpr.intro
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
h : n < List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var n ∶ List.get Γ { val := n, isLt := h }

State before:
case mpr.intro
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
h : n < List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var n ∶ List.get Γ { val := n, isLt := h }
Tactic:
exact .var h
State after:
no goals