Alternative form of Tauto for simplifying but not completing

Stream: new members

[Colin Jones ⚛️]

Is there an alternative form of tauto to simplify a goal instead of completely solving it? For example:

import Mathlib
open Nat Set Finset
lemma divisors_eq_proper_union_self (hn : 0 < n) :
  Nat.divisors n = Nat.properDivisors n ∪ {n} := by
    dsimp [divisors, properDivisors]
    ext a
    simp [*]
    constructor
    <;> rintro ⟨⟨h1, h2⟩, h3⟩
    tauto

[Colin Jones ⚛️]

The tauto below generates an error because it cannot completely solve the goal; however, it greatly simplifies it which I would like to keep as the proof easily follows.

[Kyle Miller]

This isn't an answer to your question, but here's a way to finish your proof:

lemma divisors_eq_proper_union_self {n : Nat} (hn : 0 < n) :
  Nat.divisors n = Nat.properDivisors n ∪ {n} := by
    dsimp [divisors, properDivisors]
    ext a
    simp [*]
    constructor
    <;> rintro ⟨⟨h1, h2⟩, h3⟩
    · omega
    · omega
    · simp only [*, lt_add_iff_pos_right, zero_lt_one, and_true, dvd_refl]
      omega

[Kyle Miller]

The simp only came from simp? [*]

[Kyle Miller]

One trick to handle simplifying a goal with a closing tactic is to use suffices

[Colin Jones ⚛️]

Wow omega is powerful. Thanks for sharing.

[Kyle Miller]

It's not very easy to use, but here's what I mean about suffices:

    · suffices : ¬ a < n → a = n
      · tauto
      sorry