mathlib3

91730057 - chore(tactic/finish): Remove broken ifinish (#5897)

chore(tactic/finish): Remove broken ifinish (#5897) See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/intuitionistic.20logic/near/224013270 Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>