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

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ Statement.provable' axs ax
Tactic:
have := Provable.ax (Γ := ax.ctx) VR.expr H ?disj ?hyp
State after:
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx (Formula.subst VR.expr ax.fmla)
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx (Formula.subst VR.expr ax.fmla)
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Tactic:
rw [Formula.subst_id] at this
State after:
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx ax.fmla
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
this : Provable axs ax.ctx ax.fmla
⊢ Statement.provable' axs ax

case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Tactic:
exact this
State after:
case disj
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj

case hyp
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj
Tactic:
case disj =>
  intro a b h a' b' h₁ h₂
  match a', b', h₁, h₂ with | _, _, .head _, .head _ => ?_
  exact h
State after:
no goals

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Tactic:
case hyp =>
  intro fmla h
  match fmla, h with
  | fmla, Or.inl h => rw [Formula.subst_id]; exact Provable.hyp _ h
  | _, Or.inr ⟨v, rfl⟩ => exact Provable.var v
State after:
no goals

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ DJ.subst VR.expr ax.ctx.dj ax.ctx.dj
Tactic:
intro a b h a' b' h₁ h₂
State after:
axs : Statement → Prop
ax : Statement
H : axs ax
a b : VR
h : DJ.disj ax.ctx.dj a b
a' b' : VR
h₁ : a' ∈' VR.expr a
h₂ : b' ∈' VR.expr b
⊢ DJ.disj ax.ctx.dj a' b'

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
a b : VR
h : DJ.disj ax.ctx.dj a b
a' b' : VR
h₁ : a' ∈' VR.expr a
h₂ : b' ∈' VR.expr b
⊢ DJ.disj ax.ctx.dj a' b'
Tactic:
match a', b', h₁, h₂ with | _, _, .head _, .head _ => ?_
State after:
axs : Statement → Prop
ax : Statement
H : axs ax
a b : VR
h : DJ.disj ax.ctx.dj a b
a' b' : VR
h₁ : a' ∈' VR.expr a
h₂ : b' ∈' VR.expr b
⊢ DJ.disj ax.ctx.dj a b

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
a b : VR
h : DJ.disj ax.ctx.dj a b
a' b' : VR
h₁ : a' ∈' VR.expr a
h₂ : b' ∈' VR.expr b
⊢ DJ.disj ax.ctx.dj a b
Tactic:
exact h
State after:
no goals

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
⊢ ∀ (h : Formula), (h ∈ ax.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs ax.ctx (Formula.subst VR.expr h)
Tactic:
intro fmla h
State after:
axs : Statement → Prop
ax : Statement
H : axs ax
fmla : Formula
h : fmla ∈ ax.ctx.hyps ∨ ∃ v, fmla = VR.vhyp v
⊢ Provable axs ax.ctx (Formula.subst VR.expr fmla)

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
fmla : Formula
h : fmla ∈ ax.ctx.hyps ∨ ∃ v, fmla = VR.vhyp v
⊢ Provable axs ax.ctx (Formula.subst VR.expr fmla)
Tactic:
match fmla, h with
| fmla, Or.inl h => rw [Formula.subst_id]; exact Provable.hyp _ h
| _, Or.inr ⟨v, rfl⟩ => exact Provable.var v
State after:
no goals

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
fmla✝ : Formula
h✝ : fmla✝ ∈ ax.ctx.hyps ∨ ∃ v, fmla✝ = VR.vhyp v
fmla : Formula
h : fmla ∈ ax.ctx.hyps
⊢ Provable axs ax.ctx (Formula.subst VR.expr fmla)
Tactic:
rw [Formula.subst_id]
State after:
axs : Statement → Prop
ax : Statement
H : axs ax
fmla✝ : Formula
h✝ : fmla✝ ∈ ax.ctx.hyps ∨ ∃ v, fmla✝ = VR.vhyp v
fmla : Formula
h : fmla ∈ ax.ctx.hyps
⊢ Provable axs ax.ctx fmla

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
fmla✝ : Formula
h✝ : fmla✝ ∈ ax.ctx.hyps ∨ ∃ v, fmla✝ = VR.vhyp v
fmla : Formula
h : fmla ∈ ax.ctx.hyps
⊢ Provable axs ax.ctx fmla
Tactic:
exact Provable.hyp _ h
State after:
no goals

State before:
axs : Statement → Prop
ax : Statement
H : axs ax
fmla : Formula
h : fmla ∈ ax.ctx.hyps ∨ ∃ v, fmla = VR.vhyp v
v : VR
⊢ Provable axs ax.ctx (Formula.subst VR.expr (VR.vhyp v))
Tactic:
exact Provable.var v
State after:
no goals