internlm/Lean-Github huggingface dataset:
Theorem: Metamath.Provable.ax_self
Proof 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 _ => ?_
Proof 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
Theorem: Metamath.Provable.ax_self
Proof 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
Proof state after:
no goals
Theorem: Metamath.Provable.ax_self
Proof 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
Proof 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)
Theorem: Metamath.Provable.ax_self
Proof 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
Proof state after:
no goals
Theorem: Metamath.Provable.ax_self
Proof 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]
Proof 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
Theorem: Metamath.Provable.ax_self
Proof 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
Proof state after:
no goals
Theorem: Metamath.Provable.ax_self
Proof 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
Proof state after:
no goals
Theorem: Metamath.Provable.trans'
Proof state before:
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
pr : Provable axs Γ' fmla
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
⊢ Provable axs Γ (Formula.subst σ fmla)
Tactic:
induction pr with
| hyp f h => exact hh _ (Or.inl h)
| var v => exact hh _ (Or.inr ⟨v, rfl⟩)
| @ax σ' a ha dj' hh' IH =>
  rw [← Formula.subst_tr]
  apply ax (subst.trans σ' σ) ha
  focus
    intros a b ab c d hc hd
    let ⟨e, ea, ce⟩ := Expr.mem_subst hc
    let ⟨f, fb, df⟩ := Expr.mem_subst hd
    refine dj _ _ ?_ _ _ ce df
    exact dj' _ _ ab _ _ ea fb
  focus { intros f; rw [Formula.subst_tr]; refine IH _ }
Proof state after:
no goals
Theorem: Metamath.Provable.trans'
Proof state before:
case hyp
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
f : Formula
h : f ∈ Γ'.hyps
⊢ Provable axs Γ (Formula.subst σ f)
Tactic:
exact hh _ (Or.inl h)
Proof state after:
no goals
Theorem: Metamath.Provable.trans'
Proof state before:
case var
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
v : VR
⊢ Provable axs Γ (Formula.subst σ (VR.vhyp v))
Tactic:
exact hh _ (Or.inr ⟨v, rfl⟩)
Proof state after:
no goals
Theorem: Metamath.Provable.trans'
Proof state before:
case ax
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ Provable axs Γ (Formula.subst σ (Formula.subst σ' a.fmla))
Tactic:
rw [← Formula.subst_tr]
Proof state after:
case ax
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ Provable axs Γ (Formula.subst (subst.trans σ' σ) a.fmla)
Theorem: Metamath.Provable.trans'
Proof state before:
case ax
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ Provable axs Γ (Formula.subst (subst.trans σ' σ) a.fmla)
Tactic:
apply ax (subst.trans σ' σ) ha
Proof state after:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ DJ.subst (subst.trans σ' σ) a.ctx.dj Γ.dj

case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) h)
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ DJ.subst (subst.trans σ' σ) a.ctx.dj Γ.dj

case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) h)
Tactic:
focus
  intros a b ab c d hc hd
  let ⟨e, ea, ce⟩ := Expr.mem_subst hc
  let ⟨f, fb, df⟩ := Expr.mem_subst hd
  refine dj _ _ ?_ _ _ ce df
  exact dj' _ _ ab _ _ ea fb
Proof state after:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) h)
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) h)
Tactic:
focus { intros f; rw [Formula.subst_tr]; refine IH _ }
Proof state after:
no goals
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ DJ.subst (subst.trans σ' σ) a.ctx.dj Γ.dj
Tactic:
intros a b ab c d hc hd
Proof state after:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a✝ : Statement
ha : axs a✝
dj' : DJ.subst σ' a✝.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
⊢ DJ.disj Γ.dj c d
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a✝ : Statement
ha : axs a✝
dj' : DJ.subst σ' a✝.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
⊢ DJ.disj Γ.dj c d
Tactic:
let ⟨e, ea, ce⟩ := Expr.mem_subst hc
Proof state after:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a✝ : Statement
ha : axs a✝
dj' : DJ.subst σ' a✝.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
e : VR
ea : e ∈' σ' a
ce : c ∈' σ e
⊢ DJ.disj Γ.dj c d
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a✝ : Statement
ha : axs a✝
dj' : DJ.subst σ' a✝.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
e : VR
ea : e ∈' σ' a
ce : c ∈' σ e
⊢ DJ.disj Γ.dj c d
Tactic:
let ⟨f, fb, df⟩ := Expr.mem_subst hd
Proof state after:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a✝ : Statement
ha : axs a✝
dj' : DJ.subst σ' a✝.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
e : VR
ea : e ∈' σ' a
ce : c ∈' σ e
f : VR
fb : f ∈' σ' b
df : d ∈' σ f
⊢ DJ.disj Γ.dj c d
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a✝ : Statement
ha : axs a✝
dj' : DJ.subst σ' a✝.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
e : VR
ea : e ∈' σ' a
ce : c ∈' σ e
f : VR
fb : f ∈' σ' b
df : d ∈' σ f
⊢ DJ.disj Γ.dj c d
Tactic:
refine dj _ _ ?_ _ _ ce df
Proof state after:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a✝ : Statement
ha : axs a✝
dj' : DJ.subst σ' a✝.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
e : VR
ea : e ∈' σ' a
ce : c ∈' σ e
f : VR
fb : f ∈' σ' b
df : d ∈' σ f
⊢ DJ.disj Γ'.dj e f
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a✝ : Statement
ha : axs a✝
dj' : DJ.subst σ' a✝.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
a b : VR
ab : DJ.disj a✝.ctx.dj a b
c d : VR
hc : c ∈' subst.trans σ' σ a
hd : d ∈' subst.trans σ' σ b
e : VR
ea : e ∈' σ' a
ce : c ∈' σ e
f : VR
fb : f ∈' σ' b
df : d ∈' σ f
⊢ DJ.disj Γ'.dj e f
Tactic:
exact dj' _ _ ab _ _ ea fb
Proof state after:
no goals
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
⊢ ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) h)
Tactic:
intros f
Proof state after:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
f : Formula
⊢ (f ∈ a.ctx.hyps ∨ ∃ v, f = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) f)
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
f : Formula
⊢ (f ∈ a.ctx.hyps ∨ ∃ v, f = VR.vhyp v) → Provable axs Γ (Formula.subst (subst.trans σ' σ) f)
Tactic:
rw [Formula.subst_tr]
Proof state after:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
f : Formula
⊢ (f ∈ a.ctx.hyps ∨ ∃ v, f = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' f))
Theorem: Metamath.Provable.trans'
Proof state before:
case ax.a
axs : Statement → Prop
Γ : Context
σ : VR → Expr
Γ' : Context
fmla : Formula
dj : DJ.subst σ Γ'.dj Γ.dj
hh : ∀ (h : Formula), (h ∈ Γ'.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ h)
σ' : VR → Expr
a : Statement
ha : axs a
dj' : DJ.subst σ' a.ctx.dj Γ'.dj
hh' : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ' (Formula.subst σ' h)
IH : ∀ (h : Formula), (h ∈ a.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' h))
f : Formula
⊢ (f ∈ a.ctx.hyps ∨ ∃ v, f = VR.vhyp v) → Provable axs Γ (Formula.subst σ (Formula.subst σ' f))
Tactic:
refine IH _
Proof state after:
no goals
Theorem: Metamath.subst.ok.cons
Proof 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
Proof 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)
Theorem: Metamath.subst.ok.cons
Proof 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]
Proof 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)
Theorem: Metamath.subst.ok.cons
Proof 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
Proof state after:
no goals
Theorem: Metamath.subst.ok.cons
Proof 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
Proof 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)
Theorem: Metamath.subst.ok.cons
Proof 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₁
Proof state after:
no goals
Theorem: Metamath.subst.ok.cons
Proof 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
Proof state after:
no goals
Theorem: Metamath.Provable.thm
Proof 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]
Proof 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)
Theorem: Metamath.Provable.thm
Proof 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
Proof state after:
no goals
Theorem: Metamath.Provable.thm
Proof 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]
Proof 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)