Theorem: typeOfDefinedOfInTCtxt (Nederpelt/STLC.lean)

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
⊢ ∀ (Γ : TCtxt V 𝕍) (x : V), x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
Tactic:
intros Γ x
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x : V
⊢ x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
Γ : TCtxt V 𝕍
x : V
⊢ x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
Tactic:
induction' Γ
State after:
case Empty
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
⊢ x ∈ DomTCtxt TCtxt.Empty → ∃ σ, getType x TCtxt.Empty = some σ

case VarCtxt
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x a✝² : V
a✝¹ : 𝕋 𝕍
a✝ : TCtxt V 𝕍
a_ih✝ : x ∈ DomTCtxt a✝ → ∃ σ, getType x a✝ = some σ
⊢ x ∈ DomTCtxt (a✝;; a✝² : a✝¹) → ∃ σ, getType x (a✝;; a✝² : a✝¹) = some σ

State before:
case Empty
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x : V
⊢ x ∈ DomTCtxt TCtxt.Empty → ∃ σ, getType x TCtxt.Empty = some σ
Tactic:
simp
State after:
no goals

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
⊢ x ∈ DomTCtxt (Γ;; x' : σ) → ∃ σ_1, getType x (Γ;; x' : σ) = some σ_1
Tactic:
simp only [DomTCtxt, Finset.mem_union, Finset.mem_singleton, getType]
State after:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1

State before:
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Tactic:
by_cases h' : x = x'
State after:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1

State before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1

case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Tactic:
. simp [h']
State after:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1

State before:
case pos
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Tactic:
simp [h']
State after:
no goals

State before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ ∨ x = x' → ∃ σ_1, (if x = x' then some σ else getType x Γ) = some σ_1
Tactic:
simp only [h', or_false, ite_false]
State after:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ

State before:
case neg
V 𝕍 : Type
inst✝¹ : DecidableEq V
inst✝ : DecidableEq 𝕍
x x' : V
σ : 𝕋 𝕍
Γ : TCtxt V 𝕍
h_ind : x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
h' : ¬x = x'
⊢ x ∈ DomTCtxt Γ → ∃ σ, getType x Γ = some σ
Tactic:
assumption
State after:
no goals