Theorem: varSubPreservesTypeVar (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
⊢ (Γ ⊢ N : σ) → typeOf (Γ;; x : σ) (Λ.Var y) = typeOf Γ (subVarInTerm x N (Λ.Var y))
Tactic:
intro h
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ typeOf (Γ;; x : σ) (Λ.Var y) = typeOf Γ (subVarInTerm x N (Λ.Var y))

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ typeOf (Γ;; x : σ) (Λ.Var y) = typeOf Γ (subVarInTerm x N (Λ.Var y))
Tactic:
simp
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ (if y = x then some σ else getType y Γ) = typeOf Γ (if x = y then N else Λ.Var y)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
⊢ (if y = x then some σ else getType y Γ) = typeOf Γ (if x = y then N else Λ.Var y)
Tactic:
split_ifs with h' h'' h''
State after:
case inl.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : x = y
⊢ some σ = typeOf Γ N

case inl.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : ¬x = y
⊢ some σ = typeOf Γ (Λ.Var y)

case inr.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : x = y
⊢ getType y Γ = typeOf Γ N

case inr.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : ¬x = y
⊢ getType y Γ = typeOf Γ (Λ.Var y)

State before:
case inl.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : x = y
⊢ some σ = typeOf Γ N
Tactic:
rw [h]
State after:
no goals

State before:
case inl.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : ¬x = y
⊢ some σ = typeOf Γ (Λ.Var y)
Tactic:
exfalso
State after:
case inl.inr.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : ¬x = y
⊢ False

State before:
case inl.inr.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : y = x
h'' : ¬x = y
⊢ False
Tactic:
exact h'' (Eq.symm h')
State after:
no goals

State before:
case inr.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : x = y
⊢ getType y Γ = typeOf Γ N
Tactic:
exfalso
State after:
case inr.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : x = y
⊢ False

State before:
case inr.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : x = y
⊢ False
Tactic:
exact h' (Eq.symm h'')
State after:
no goals

State before:
case inr.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
N : Λ V 𝕍
x y : V
σ : 𝕋 𝕍
h : Γ ⊢ N : σ
h' : ¬y = x
h'' : ¬x = y
⊢ getType y Γ = typeOf Γ (Λ.Var y)
Tactic:
simp
State after:
no goals