Commit 2024-07-15 16:11 cb401f88

View on Github →

chore(Tactic/NormNum): remove autoImplicit (#14725) This is exhaustive

Estimated changes

Modified Mathlib/Tactic/NormNum/Basic.lean

modified theorem Mathlib.Meta.NormNum.eq_of_false

modified def Mathlib.Meta.NormNum.inferDivisionRing

modified theorem Mathlib.Meta.NormNum.isNat_ofNat

modified theorem Mathlib.Meta.NormNum.isRat_div

modified theorem Mathlib.Meta.NormNum.ne_of_false_of_true

modified theorem Mathlib.Meta.NormNum.ne_of_true_of_false

Modified Mathlib/Tactic/NormNum/BigOperators.lean

Modified Mathlib/Tactic/NormNum/Core.lean

modified def Mathlib.Meta.NormNum.NormNums.erase

Modified Mathlib/Tactic/NormNum/DivMod.lean

modified theorem Mathlib.Meta.NormNum.isInt_ediv_neg

Modified Mathlib/Tactic/NormNum/Eq.lean

Modified Mathlib/Tactic/NormNum/Ineq.lean

Modified Mathlib/Tactic/NormNum/Inv.lean

modified theorem Mathlib.Meta.NormNum.isInt_ratCast

modified theorem Mathlib.Meta.NormNum.isNat_ratCast

modified theorem Mathlib.Meta.NormNum.isRat_ratCast

Modified Mathlib/Tactic/NormNum/OfScientific.lean

Modified Mathlib/Tactic/NormNum/Pow.lean

modified theorem Mathlib.Meta.NormNum.IsNatPowT.trans

modified theorem Mathlib.Meta.NormNum.intPow_negOfNat_bit0

modified theorem Mathlib.Meta.NormNum.intPow_negOfNat_bit1

Modified Mathlib/Tactic/NormNum/Result.lean

modified theorem Mathlib.Meta.NormNum.IsInt.to_raw_eq

modified theorem Mathlib.Meta.NormNum.IsNat.to_eq

modified theorem Mathlib.Meta.NormNum.IsNat.to_raw_eq

modified structure Mathlib.Meta.NormNum.IsNat

modified theorem Mathlib.Meta.NormNum.IsRat.to_raw_eq

modified def Mathlib.Meta.NormNum.Result.toRat

modified def Mathlib.Meta.NormNum.Result.toRatNZ

modified def Mathlib.Meta.NormNum.instAddMonoidWithOne

modified def Nat.rawCast

Modified Mathlib/Util/Qq.lean

modified theorem Qq.QuotedDefEq.rfl