Mono tactic explosion

Stream: mathlib4

[Eric Wieser]

How many goals do you think mono creates here?

import Mathlib

theorem mono_explodes (a : ℕ → ℕ) (i zi : ℕ) (h : ∀ (b : ℕ), i ≤ b → a zi ≤ a b) :
    a zi ≤ a zi := by
  mono
  run_tac Lean.logInfo m!"{(← Lean.Elab.Tactic.getGoals).length}"
  repeat sorry

[Eric Wieser]

attribute [-mono] hasProd_mono hasSum_mono seems to fix it (docs#hasProd_mono)

[Damiano Testa]

Here is another fix:

import Mathlib

theorem mono_explodes (a : ℕ → ℕ) (i zi : ℕ) (h : ∀ (b : ℕ), i ≤ b → a zi ≤ a b) :
    ((((((((((((((((((((((((((((((((((((((((((((((((((((a zi)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1 ≤ ((((((((((((((((((((((((((((((((((((((((((((((((((((a zi)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1)^1 := by
  mono
  run_tac Lean.logInfo m!"{(← Lean.Elab.Tactic.getGoals).length}"
  sorry

[Thomas Murrills]

Btw, this could also be attributed to the fact that mono is a thin wrapper around solve_by_elim, and uses backtracking := false. Changing this to backtracking := true fixes the issue. (Unfortunately passing a config option is not enough since these fields are overwritten; this would have to be done in source)