Commit 2024-07-15 21:28 643e0fa3

View on Github →

chore(Tactic): reduce use of autoImplicit, part 3 (#14770)

Estimated changes

Modified Mathlib/Tactic/Basic.lean

modified def Mathlib.Tactic.pushFVarAliasInfo

Modified Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

modified def Mathlib.Tactic.BicategoryCoherence.exception

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean

modified def Mathlib.Tactic.Coherence.exception

Modified Mathlib/Tactic/CategoryTheory/Elementwise.lean

modified theorem Tactic.Elementwise.hom_elementwise

Modified Mathlib/Tactic/FieldSimp.lean

Modified Mathlib/Tactic/IntervalCases.lean

modified theorem Mathlib.Tactic.IntervalCases.le_of_not_le_of_le

Modified Mathlib/Tactic/LinearCombination.lean

Modified Mathlib/Tactic/ModCases.lean

Modified Mathlib/Tactic/Polyrith.lean

modified def Mathlib.Tactic.Polyrith.Poly.sumM

Modified Mathlib/Tactic/ReduceModChar.lean

modified theorem Tactic.ReduceModChar.CharP.isInt_of_mod

Modified Mathlib/Tactic/Relation/Trans.lean

modified def Trans.het

Modified Mathlib/Tactic/RewriteSearch.lean

Modified Mathlib/Tactic/Ring/Basic.lean

modified def Mathlib.Tactic.Ring.ExBase.toProd

modified inductive Mathlib.Tactic.Ring.ExBase