Theorem: Metamath.Provable.thm (Metamath/Translate.lean)

State before:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
dj✝ : List (VR × VR)
hyps : List Formula
c : CN
s : Expr
pr : Provable axs (Context.mk' dj✝ hyps) (c, s)
hv : subst.ok axs Γ σ
dj : DJ.subst σ (DJ.mk' dj✝) Γ.dj
hh : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
e : Expr
inst : Subst σ s e
⊢ Provable axs Γ (c, e)
Tactic:
rw [← inst.out]
State after:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
dj✝ : List (VR × VR)
hyps : List Formula
c : CN
s : Expr
pr : Provable axs (Context.mk' dj✝ hyps) (c, s)
hv : subst.ok axs Γ σ
dj : DJ.subst σ (DJ.mk' dj✝) Γ.dj
hh : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
e : Expr
inst : Subst σ s e
⊢ Provable axs Γ (c, Expr.subst σ s)

State before:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
dj✝ : List (VR × VR)
hyps : List Formula
c : CN
s : Expr
pr : Provable axs (Context.mk' dj✝ hyps) (c, s)
hv : subst.ok axs Γ σ
dj : DJ.subst σ (DJ.mk' dj✝) Γ.dj
hh : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
e : Expr
inst : Subst σ s e
⊢ Provable axs Γ (c, Expr.subst σ s)
Tactic:
exact Metamath.Provable.trans' σ pr dj fun
  | f, Or.inl h => hh _ h
  | _, Or.inr ⟨v, rfl⟩ =>
    show Provable axs Γ (v.type, σ v ++ show Expr from []) by
    rw [List.append_nil]; exact hv v
State after:
no goals

State before:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
dj✝ : List (VR × VR)
hyps : List Formula
c : CN
s : Expr
pr : Provable axs (Context.mk' dj✝ hyps) (c, s)
hv : subst.ok axs Γ σ
dj : DJ.subst σ (DJ.mk' dj✝) Γ.dj
hh : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
e : Expr
inst : Subst σ s e
v : VR
⊢ Provable axs Γ
    (v.type,
      σ v ++
        let_fun this := [];
        this)
Tactic:
rw [List.append_nil]
State after:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
dj✝ : List (VR × VR)
hyps : List Formula
c : CN
s : Expr
pr : Provable axs (Context.mk' dj✝ hyps) (c, s)
hv : subst.ok axs Γ σ
dj : DJ.subst σ (DJ.mk' dj✝) Γ.dj
hh : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
e : Expr
inst : Subst σ s e
v : VR
⊢ Provable axs Γ (v.type, σ v)

State before:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
dj✝ : List (VR × VR)
hyps : List Formula
c : CN
s : Expr
pr : Provable axs (Context.mk' dj✝ hyps) (c, s)
hv : subst.ok axs Γ σ
dj : DJ.subst σ (DJ.mk' dj✝) Γ.dj
hh : ∀ (h : Formula), h ∈ hyps → Provable axs Γ (Formula.subst σ h)
e : Expr
inst : Subst σ s e
v : VR
⊢ Provable axs Γ (v.type, σ v)
Tactic:
exact hv v
State after:
no goals