Commit 2024-07-15 14:00 9c748dc6

View on Github →

chore(Tactic): reduce use of Implicit, part 2 (#14726)

Estimated changes

Modified Mathlib/Tactic/Abel.lean

modified theorem Mathlib.Tactic.Abel.term_eq

modified theorem Mathlib.Tactic.Abel.termg_eq

Modified Mathlib/Tactic/CongrExclamation.lean

Modified Mathlib/Tactic/Core.lean

Modified Mathlib/Tactic/FunProp/ToBatteries.lean

Modified Mathlib/Tactic/Linarith/Verification.lean

modified def Linarith.addExprs'

modified def Linarith.mulExpr'

Modified Mathlib/Tactic/Nontriviality/Core.lean

modified def Mathlib.Tactic.Nontriviality.nontrivialityByElim

Modified Mathlib/Tactic/Propose.lean

Modified Mathlib/Tactic/PushNeg.lean

modified theorem Mathlib.Tactic.PushNeg.empty_ne_eq_nonempty

modified theorem Mathlib.Tactic.PushNeg.ne_empty_eq_nonempty

modified theorem Mathlib.Tactic.PushNeg.not_nonempty_eq

Modified Mathlib/Tactic/Relation/Symm.lean

Modified Mathlib/Tactic/Relation/Trans.lean

modified def Trans.simple

Modified Mathlib/Tactic/SuccessIfFailWithMsg.lean

modified def Mathlib.Tactic.successIfFailWithMessage

Modified Mathlib/Tactic/SudoSetOption.lean

Modified Mathlib/Tactic/TermCongr.lean

modified def Mathlib.Tactic.TermCongr.throwCongrEx

Modified Mathlib/Tactic/ToAdditive.lean

modified def ToAdditive.additivizeLemmas

modified def ToAdditive.warnAttr

modified def ToAdditive.warnExt

modified def ToAdditive.warnParametricAttr

Modified Mathlib/Tactic/ToLevel.lean

Modified Mathlib/Tactic/UnsetOption.lean