Theorem: Metamath.subst.ok.cons (Metamath/Translate.lean)

State before:
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
⊢ ok axs Γ (subst_of ((x, e) :: σ))
Tactic:
intro v
State after:
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
⊢ Provable axs Γ (v.type, subst_of ((x, e) :: σ) v)

State before:
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
⊢ Provable axs Γ (v.type, subst_of ((x, e) :: σ) v)
Tactic:
simp only [subst_of]
State after:
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
⊢ Provable axs Γ (v.type, if x = v then e else subst_of σ v)

State before:
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
⊢ Provable axs Γ (v.type, if x = v then e else subst_of σ v)
Tactic:
cases Decidable.em (x = v) with simp [h]
| inl h => cases h; exact h₁
| inr h => exact h₂ v
State after:
no goals

State before:
case inl
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
h : x = v
⊢ Provable axs Γ (v.type, e)
Tactic:
cases h
State after:
case inl.refl
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
⊢ Provable axs Γ (x.type, e)

State before:
case inl.refl
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
⊢ Provable axs Γ (x.type, e)
Tactic:
exact h₁
State after:
no goals

State before:
case inr
axs : Statement → Prop
Γ : Context
e : Expr
σ : List (VR × Expr)
x : VR
h₁ : Provable axs Γ (x.type, e)
h₂ : ok axs Γ (subst_of σ)
v : VR
h : ¬x = v
⊢ Provable axs Γ (v.type, subst_of σ v)
Tactic:
exact h₂ v
State after:
no goals