Commit 2024-07-16 20:24 3fc989ab

View on Github →

chore(Tactic): reduce autoImplicit, part 4 (#14805) After this, the only remaining uses are Ring/Basic (which is requires more work, hence shall get its own PR), Sat/FromLRAT and four single declarations in ToExpr.

Estimated changes

Modified Mathlib/Tactic/Linarith/Frontend.lean

modified def Linarith.ExprMultiMap.find

modified def Linarith.ExprMultiMap.insert

Modified Mathlib/Tactic/Linarith/Lemmas.lean

modified theorem le_zero_of_zero_ge

modified theorem lt_zero_of_zero_gt

Modified Mathlib/Tactic/Linarith/Parsing.lean

modified def List.findDefeq

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

modified theorem Linarith.without_one_mul

Modified Mathlib/Tactic/Positivity/Basic.lean

Modified Mathlib/Tactic/Positivity/Core.lean

modified def Mathlib.Meta.Positivity.Strictness.toString

modified def Mathlib.Meta.Positivity.catchNone

modified theorem Mathlib.Meta.Positivity.lt_of_le_of_ne'

modified theorem Mathlib.Meta.Positivity.nonneg_of_isNat

modified theorem Mathlib.Meta.Positivity.nonneg_of_isRat

modified theorem Mathlib.Meta.Positivity.nz_of_isNegNat

modified theorem Mathlib.Meta.Positivity.nz_of_isRat

modified def Mathlib.Meta.Positivity.orElse

modified theorem Mathlib.Meta.Positivity.pos_of_isNat

modified theorem Mathlib.Meta.Positivity.pos_of_isRat

modified def Mathlib.Meta.Positivity.throwNone

modified theorem ne_of_ne_of_eq'

Modified Mathlib/Tactic/Relation/Trans.lean

Modified Mathlib/Tactic/Ring/RingNF.lean

Modified Mathlib/Tactic/ToExpr.lean