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

State before:
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e : Formula
pr : Provable axs₁ Γ₁ e
⊢ Provable axs₂ Γ₂ e
Tactic:
induction pr with
| hyp e h => exact hyp e (hΓ.1 _ h)
| var v => exact var v
| ax σ ha h₁ _ IH =>
  exact ax σ (haxs _ ha) (h₁.mono (DJ.refl _) hΓ.2) fun e h => IH _ h
State after:
no goals

State before:
case hyp
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e✝ e : Formula
h : e ∈ Γ₁.hyps
⊢ Provable axs₂ Γ₂ e
Tactic:
exact hyp e (hΓ.1 _ h)
State after:
no goals

State before:
case var
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e : Formula
v : VR
⊢ Provable axs₂ Γ₂ (VR.vhyp v)
Tactic:
exact var v
State after:
no goals

State before:
case ax
axs₁ axs₂ : Statement → Prop
haxs : ∀ (a : Statement), axs₁ a → axs₂ a
Γ₁ Γ₂ : Context
hΓ : Γ₁ ≤ Γ₂
e : Formula
σ : VR → Expr
ax✝ : Statement
ha : axs₁ ax✝
h₁ : DJ.subst σ ax✝.ctx.dj Γ₁.dj
a✝ : ∀ (h : Formula), (h ∈ ax✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs₁ Γ₁ (Formula.subst σ h)
IH : ∀ (h : Formula), (h ∈ ax✝.ctx.hyps ∨ ∃ v, h = VR.vhyp v) → Provable axs₂ Γ₂ (Formula.subst σ h)
⊢ Provable axs₂ Γ₂ (Formula.subst σ ax✝.fmla)
Tactic:
exact ax σ (haxs _ ha) (h₁.mono (DJ.refl _) hΓ.2) fun e h => IH _ h
State after:
no goals