Commit 2026-01-08 16:40 001c934c

View on Github →

chore(Tactic): remove duplicate instances (#33666) This PR removes the two duplicate instances that were detected in Mathlib.Tactic.

Estimated changes

Modified Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean

deleted def Std.TreeSet.sdiff

Modified Mathlib/Tactic/NormNum/Basic.lean

Modified Mathlib/Tactic/NormNum/Core.lean

Modified Mathlib/Tactic/NormNum/GCD.lean

Modified Mathlib/Tactic/NormNum/NatFactorial.lean

Modified Mathlib/Tactic/NormNum/NatFib.lean

Modified Mathlib/Tactic/NormNum/NatLog.lean

Modified Mathlib/Tactic/NormNum/NatSqrt.lean

Modified Mathlib/Tactic/NormNum/Pow.lean

Modified Mathlib/Tactic/NormNum/Prime.lean

Modified Mathlib/Tactic/NormNum/Result.lean

deleted def Mathlib.Meta.NormNum.instAddMonoidWithOneNat

Modified Mathlib/Tactic/ReduceModChar.lean