a way to limit the tactics

Stream: new members

[V S]

Hello! This is somewhat of a continuation of topics #new members > ✔ weird example of apply and #new members > ✔ completing the proof somewhat automatically.
I'm working with examples like

example: (ho: A) (h1 : B) (h2 : C): E := by
have a: (h1 : A) (h2 : B) : D := by ...
have b: (h: C) (h1: A) : F := by ...
have c: (h : F) (h : A) : G := by...
have c: (h1: D) (h2: G) (h3: F) : E := by ...

which can be checked (if true or not) by using a number of 'apply'-s or 'exact'-s. However, there are some examples where the 'apply' does more than it should, see below.
I'm interested in ways that could potentially limit the kernel, so that an example

import Mathlib

example: Int.gcd 12 480 = 12 := by
  have f: 2 + 10 = 12 := by norm_num
  apply f

would not work (thus, no approaches that do 'apply's or 'exact's automatically would work), since it makes no sense logically for a human, similar to how solve_by_elim does not check that if a + b + c = 5 was proven earlier for real numbers, than a + (b + c) = 5 is the same thing basically. Or is this not possible/requires writing my own tactic?

[Mario Carneiro]

You could try with_reducible to decrease the amount of automated reduction

[V S]

Mario Carneiro said:

You could try with_reducible to decrease the amount of automated reduction

Thank you! This works with that example (with_reducible apply f), however, if I were to use it with solve_by_elim, it still works. Is there a workaround for this particular example?

import Mathlib
example: Int.gcd 12 480 = 12 := by
  have f: 2 + 10 = 12 := by norm_num
  with_reducible solve_by_elim