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

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

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