Theorem: Metamath.Statement.vars.mono' (Metamath/Translate.lean)

State before:
s₁ s₂ : Statement
H : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ s₂.ctx.hyps
H₂ : s₁.fmla = s₂.fmla
v : VR
⊢ v ∈ vars s₁ → v ∈ vars s₂
Tactic:
simp only [vars, List.mem_bind, List.mem_cons, H₂]
State after:
s₁ s₂ : Statement
H : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ s₂.ctx.hyps
H₂ : s₁.fmla = s₂.fmla
v : VR
⊢ (∃ a, (a = s₂.fmla ∨ a ∈ s₁.ctx.hyps) ∧ v ∈ Expr.vars a.snd) →
    ∃ a, (a = s₂.fmla ∨ a ∈ s₂.ctx.hyps) ∧ v ∈ Expr.vars a.snd

State before:
s₁ s₂ : Statement
H : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ s₂.ctx.hyps
H₂ : s₁.fmla = s₂.fmla
v : VR
⊢ (∃ a, (a = s₂.fmla ∨ a ∈ s₁.ctx.hyps) ∧ v ∈ Expr.vars a.snd) →
    ∃ a, (a = s₂.fmla ∨ a ∈ s₂.ctx.hyps) ∧ v ∈ Expr.vars a.snd
Tactic:
exact fun ⟨a, b, c⟩ => ⟨a, b.imp_right (H _), c⟩
State after:
no goals