`simp_all` deleting hypotheses

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The simp_all tactic does not behave as expected when it is both unfolding a definition and simplifying an implication. This can cause important hypotheses to disappear from the context, potentially making the theorem unprovable.

Context

I personally use simp_all a lot, usually via aesop. This bug happens pretty frequently after, say, an induction step. The induction hypothesis will then have the form of an implication and can get deleted by this bug.

As a workaround, one can use simp_all only [def]; simp_all.

See discussion #lean4 > simp_all behavior.

Steps to Reproduce

1. Define a predicate which unfolds to another predicate, e.g.

opaque p (n : Nat) : Prop 
def P (n : Nat) : Prop := p n

2. Run simp_all on a goal which contains an implication of type P n → P m and P n.

example (h : P 0 → P 1) (h0 : P 0) : Target := by simp_all [P] 

See mwe.

Expected behavior: After simp_all [P], goal is h : p 1, h0 : p 0 ⊢ Target

Actual behavior: After simp_all [P], goal is h0 : p 0 ⊢ Target

Versions

4.25.0
4.27.0-nightly-2025-11-20

Begin with the minimal self-contained reproduction in the issue and inspect the simp_all tactic behavior when unfolding P and simplifying an implication. Compare the resulting context with the expected h : p 1 and h0 : p 0, using the simp_all only [P]; simp_all workaround as a reference for completion.