Commit 2023-11-14 09:14 a977ca14

View on Github →

chore: bump Std (#8403)

Estimated changes

Modified Archive/Imo/Imo1969Q1.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/CharZero/Defs.lean

Modified Mathlib/Data/FunLike/Basic.lean

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/Init/Data/Ordering/Lemmas.lean

modified theorem cmpUsing_eq_lt

Modified Mathlib/Lean/Meta/Simp.lean

deleted def Lean.Meta.Simp.mkCast

deleted def Lean.Meta.Simp.mkEqSymm

deleted def Lean.Meta.Simp.mkSimpContext'

Modified Mathlib/Logic/Basic.lean

deleted theorem dite_eq_left_iff

deleted theorem dite_eq_right_iff

deleted theorem forall_prop_of_false

deleted theorem ite_eq_left_iff

deleted theorem ite_eq_right_iff

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/Find.lean

Modified Mathlib/Tactic/LibrarySearch.lean

Deleted Mathlib/Tactic/NormCast.lean

Deleted Mathlib/Tactic/NormCast/Tactic.lean

deleted def Tactic.NormCast.derive

deleted def Tactic.NormCast.evalConvNormCast

deleted def Tactic.NormCast.evalPushCast

deleted def Tactic.NormCast.isCoeOf?

deleted def Tactic.NormCast.isNumeral?

deleted def Tactic.NormCast.mkCoe

deleted def Tactic.NormCast.normCastHyp

deleted def Tactic.NormCast.normCastTarget

deleted def Tactic.NormCast.numeralToCoe

deleted def Tactic.NormCast.prove

deleted def Tactic.NormCast.proveEqUsing

deleted def Tactic.NormCast.proveEqUsingDown

deleted def Tactic.NormCast.splittingProcedure

Modified Mathlib/Tactic/Propose.lean

Modified Mathlib/Tactic/Qify.lean

Modified Mathlib/Tactic/ReduceModChar.lean

Modified Mathlib/Tactic/Rewrites.lean

Modified Mathlib/Tactic/Zify.lean

Modified lake-manifest.json

Modified test/norm_cast.lean

Modified test/toAdditive.lean