Commit 2024-06-17 10:24 4c302e76
View on Github →feat(Tactic/Relation/Trans): trans tactic for implications (#13719)
Implications behave like transitive relations albeit not being such in mathlib for technical reasons. This extends the trans tactic to handle them alike. This means trans B turn a goal A → C into two goals A → B and B → C.