Theorem: Metamath.Provable.trans' (Metamath/Translate.lean)

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 _ }
State after:
no goals

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)
State after:
no goals

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⟩)
State after:
no goals

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]
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)

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
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)

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
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)

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 _ }
State after:
no goals

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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)

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]
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))

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 _
State after:
no goals