Theorem: Metamath.Statement.trimmed.trim_eq (Metamath/Translate.lean)

State before:
a : List Formula
b : DJ
c : Formula
h : trimmed { ctx := { hyps := a, dj := b }, fmla := c }
⊢ trim { ctx := { hyps := a, dj := b }, fmla := c } = { ctx := { hyps := a, dj := b }, fmla := c }
Tactic:
simp only [trim]
State after:
a : List Formula
b : DJ
c : Formula
h : trimmed { ctx := { hyps := a, dj := b }, fmla := c }
⊢ { ctx := { hyps := a, dj := DJ.trim b fun v => v ∈ vars { ctx := { hyps := a, dj := b }, fmla := c } }, fmla := c } =
    { ctx := { hyps := a, dj := b }, fmla := c }

State before:
a : List Formula
b : DJ
c : Formula
h : trimmed { ctx := { hyps := a, dj := b }, fmla := c }
⊢ { ctx := { hyps := a, dj := DJ.trim b fun v => v ∈ vars { ctx := { hyps := a, dj := b }, fmla := c } }, fmla := c } =
    { ctx := { hyps := a, dj := b }, fmla := c }
Tactic:
rw [DJ.trimmed.trim_eq h]
State after:
no goals