convert to term mode

Stream: new members

[Ashwin Iyengar]

Hi, I don't really understand term mode. Right now this works:

noncomputable def add (f g : mv_restricted_power_series σ R) : mv_restricted_power_series σ R := ⟨f.1 + g.1, begin
  have x := tendsto.add f.2 g.2,
  simp at x,
  exact x,
end⟩

But this doesn't work:

noncomputable def add (f g : mv_restricted_power_series σ R) : mv_restricted_power_series σ R := ⟨f.1 + g.1, tendsto.add f.2 g.2⟩

So how do I convert the first block into term mode and incorporate the simp?

[Yakov Pechersky]

Does this work for you?

noncomputable def add (f g : mv_restricted_power_series σ R) : mv_restricted_power_series σ R := ⟨f.1 + g.1, by simpa using tendsto.add f.2 g.2⟩

[Ashwin Iyengar]

Yes, thanks! And I just found the documentation for by, so that's helpful.