Commit 2022-11-22 21:55 5230db6d

View on Github →

chore: remove upstreamed tactics 11-21 (#684)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/FunLike/Basic.lean

modified theorem FunLike.coe_eq_coe_fn

Modified Mathlib/Init/Logic.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Mathport/Syntax.lean

Deleted Mathlib/Tactic/Congr.lean

Deleted Mathlib/Tactic/DocCommands.lean

Deleted Mathlib/Tactic/SeqFocus.lean

Deleted Mathlib/Tactic/SimpTrace.lean

deleted def Mathlib.Tactic.dsimpLocation'

Modified Mathlib/Tactic/SolveByElim.lean

Modified scripts/style-exceptions.txt

Deleted test/DocCommands.lean

deleted def hi

deleted def one

deleted def three

deleted def two

Deleted test/SeqFocus.lean

Deleted test/congr.lean

Deleted test/simp_trace.lean

deleted def bar

deleted def baz

deleted def foo