Multiple apply

Stream: Is there code for X?

[Matias Heikkilä]

Is there tactic for writing

some_tactic [thm1, thm2, thm3]

instead of

apply thm1
apply thm2
apply thm3

[Matias Heikkilä]

Or some other smart way

[Ruben Van de Velde]

refine thm1 <| thm2 <| thm3 ?_ could work, depending on how much apply is hiding

[Alex J. Best]

You can use apply_rules for this (assuming that the greedy algorithm of apply these whenever you can is what you want) https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/SolveByElim.html#Mathlib.Tactic.SolveByElim.applyRulesSyntax

[Matias Heikkilä]

Thanks for the help, the latter worked in my case. I think I still have some work to do before I actually understand what apply really does

[Matias Heikkilä]

Or refine...