Commit 2024-10-19 08:15 66f63643

View on Github →

chore: move trans tactic to Batteries (batteries#1001) (#17931)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Notation.lean

Modified Mathlib/Order/Defs.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/MoveAdd.lean

Deleted Mathlib/Tactic/Relation/Trans.lean

deleted inductive Mathlib.Tactic.TransRelation

deleted def Mathlib.Tactic.getExplicitFuncArg?

deleted def Mathlib.Tactic.getExplicitRelArg?

deleted def Mathlib.Tactic.getExplicitRelArgCore

deleted def Mathlib.Tactic.getRel

deleted def Mathlib.Tactic.transExt.config

deleted def Trans.het

deleted def Trans.simple

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

Modified Mathlib/Tactic/Widget/CongrM.lean

Modified lake-manifest.json

Modified scripts/noshake.json

Deleted test/trans.lean

deleted theorem MyLE.trans

deleted def MyLE

deleted def eq_trans

deleted def nleq

deleted def nleq_trans