Commit 2023-10-19 08:30 d478563b

View on Github →

chore: bump dependencies (#7767)

Estimated changes

Modified Mathlib/Init/Align.lean

Modified Mathlib/Init/Core.lean

Modified Mathlib/Init/Logic.lean

Modified Mathlib/Lean/Meta.lean

deleted def Lean.Elab.Tactic.liftMetaFinishingTactic

deleted def Lean.MVarId.replace

Modified Mathlib/Logic/Function/Conjugate.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/GCongr/Core.lean

Modified Mathlib/Tactic/LibrarySearch.lean

Modified Mathlib/Tactic/Relation/Rfl.lean

deleted def Lean.MVarId.rfl

Modified Mathlib/Tactic/Relation/Symm.lean

deleted def Lean.Expr.symm

deleted def Lean.Expr.symmAux

deleted def Lean.MVarId.symm

deleted def Lean.MVarId.symmAt

deleted def Lean.MVarId.symmAux

Modified Mathlib/Tactic/Rewrites.lean

Modified Mathlib/Tactic/ToAdditive.lean

Modified lake-manifest.json

Deleted test/rfl.lean

deleted def Foo.le

deleted theorem Foo.le_refl

deleted structure Foo

deleted def iseqv_refl