Theorem: getTypeReorder (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
⊢ x ≠ y → ∀ {z : V}, getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
intro h z
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
by_cases h' : z = x
State after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)

State before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
simp [h, h']
State after:
no goals

State before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
by_cases h'' : z = y
State after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : ¬z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)

State before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
simp [h', h'']
State after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ some σ' = if y = x then some σ else some σ'

State before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
⊢ some σ' = if y = x then some σ else some σ'
Tactic:
split_ifs with h
State after:
case pos.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ some σ' = some σ

case pos.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : ¬y = x
⊢ some σ' = some σ'

State before:
case pos.inl
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ some σ' = some σ
Tactic:
exfalso
State after:
case pos.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ False

State before:
case pos.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : y = x
⊢ False
Tactic:
rw [h''] at h'
State after:
case pos.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬y = x
h'' : z = y
h : y = x
⊢ False

State before:
case pos.inl.h
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬y = x
h'' : z = y
h : y = x
⊢ False
Tactic:
exact h' h
State after:
no goals

State before:
case pos.inr
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h✝ : x ≠ y
z : V
h' : ¬z = x
h'' : z = y
h : ¬y = x
⊢ some σ' = some σ'
Tactic:
rfl
State after:
no goals

State before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x y : V
σ σ' : 𝕋 𝕍
h : x ≠ y
z : V
h' : ¬z = x
h'' : ¬z = y
⊢ getType z ((Γ;; x : σ);; y : σ') = getType z ((Γ;; y : σ');; x : σ)
Tactic:
simp [h', h'']
State after:
no goals