Theorem: free_subst_eq (LambdaCalculi/TypeSystem.lean)

State before:
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Tactic:
by_cases h : v ∈ free t
State after:
case pos
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∈ free t
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}

case neg
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free t
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}

State before:
case pos
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∈ free t
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Tactic:
simp [free_subst_of_free, h]
State after:
no goals

State before:
case neg
α : Type u_2
β : Type u_3
Λ : Type u_4
V : Type u_1
T : Type u_5
inst✝¹ : DeductionSystem α β
inst✝ : TypeSystem α β Λ V T
v : V
s t : Λ
h : v ∉ free t
⊢ free (t[v := s]) = free t \ {v} ∪ {w | w ∈ free s ∧ v ∈ free t}
Tactic:
simp [subst_eq_of_not_free, h]
State after:
no goals