Commit 2022-12-21 06:35 047ae09b

View on Github →

fix: improved transitivity, handles HEq.trans (#1125) Transitivity handles heterogeneous cases and premutations of parameters. Fixes #1119

Estimated changes

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

Modified Mathlib/Tactic/Relation/Trans.lean

added def Mathlib.Tactic.getExplicitFuncArg?

added def Mathlib.Tactic.getExplicitRelArg?

added def Mathlib.Tactic.getExplicitRelArgCore

added def Trans.het

Modified test/trans.lean