Theorem: Metamath.Statement.untrim.mono (Metamath/Translate.lean)

State before:
s₁ s₂ : Statement
H : s₁.ctx.hyps = s₂.ctx.hyps
h : s₁ ≤ s₂
⊢ ∀ (a : Formula), a ∈ s₂.ctx.hyps → a ∈ s₁.ctx.hyps
Tactic:
rw [H]
State after:
s₁ s₂ : Statement
H : s₁.ctx.hyps = s₂.ctx.hyps
h : s₁ ≤ s₂
⊢ ∀ (a : Formula), a ∈ s₂.ctx.hyps → a ∈ s₂.ctx.hyps

State before:
s₁ s₂ : Statement
H : s₁.ctx.hyps = s₂.ctx.hyps
h : s₁ ≤ s₂
⊢ ∀ (a : Formula), a ∈ s₂.ctx.hyps → a ∈ s₂.ctx.hyps
Tactic:
exact fun _ => id
State after:
no goals