Tactic for cleaning up proofs

Stream: mathlib4

[Michael Bucko]

@Mario Carneiro posted this in the ET project channel, and mentioned that commenting out isGood_left/isGood_right does not break the proof (below).

Does there exist a tactic in Lean (or a plugin) like suggest_tactics, but for rewriting / modifying the proof until a shorter version has been reached?

class RelaxedWeakCentralGroupoid (G : Type*) extends Magma G where
  Path : G → G → Prop
  IsGood : G → G → G → Prop
  op_isGood (x y : G) : IsGood x (x ◇ y) y
  isGood_path {x y z : G} : IsGood x y z → Path x y ∧ Path y z
  -- isGood_left {x y : G} : Path x y → ∃ z, IsGood z x y
  -- isGood_right {x y : G} : Path x y → ∃ z, IsGood x y z
  isGood_five {a b c d e : G} : IsGood a b c → IsGood c d e → Path e a → IsGood b c d