Tactic mode to term mode

Stream: general

[Ashvni Narayanan]

I am trying to convert a tactic mode proof into a term mode proof. It is quite confusing. I tried using show_term, but that did not work out too well. Is there any online guide/reference regarding this? Thank you!

[Mario Carneiro]

that's pretty broad. What tactics are you using?

[Mario Carneiro]

Here's a small listing of simple tactics and their term mode equivalents: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Basic.20building.20block.20tactics/near/189275113

[Ashvni Narayanan]

Mario Carneiro said:

that's pretty broad. What tactics are you using?

rintros, apply, split, cases, use, and simp. I tried to do away with as many simps as possible.

[Mario Carneiro]

you can often use calc in place of simp, to make the rewrites explicit

[Mario Carneiro]

but it's generally best to leave rewrites as by rw thm even in term mode proofs because the elaboration is more controlled than what you get with eq.rec_on thm

[Mario Carneiro]

everything else is easy term mode stuff

[Mario Carneiro]

especially if you cheat and use let <x, y, z> := or match in place of cases and rintros

[Ashvni Narayanan]

Thank you very much, I will give it another go.