Theorem: Metamath.Statement.untrim_trim (Metamath/Translate.lean)

State before:
s : Statement
⊢ untrim (trim s) = untrim s
Tactic:
simp only [untrim, untrim', trim_vars]
State after:
s : Statement
⊢ { ctx := { hyps := (trim s).ctx.hyps, dj := DJ.untrim (trim s).ctx.dj fun v => v ∈ vars s }, fmla := (trim s).fmla } =
    { ctx := { hyps := s.ctx.hyps, dj := DJ.untrim s.ctx.dj fun v => v ∈ vars s }, fmla := s.fmla }

State before:
s : Statement
⊢ { ctx := { hyps := (trim s).ctx.hyps, dj := DJ.untrim (trim s).ctx.dj fun v => v ∈ vars s }, fmla := (trim s).fmla } =
    { ctx := { hyps := s.ctx.hyps, dj := DJ.untrim s.ctx.dj fun v => v ∈ vars s }, fmla := s.fmla }
Tactic:
simp only [trim, DJ.untrim_trim]
State after:
no goals