weird simp behavior

Stream: general

[Sebastien Gouezel]

In my context, I have

H :
  ⟨k, blocks_fun⟩ ∈
    finset.sigma (finset.range N) (λ (n : ℕ), fintype.pi_finset (λ (i : fin n), finset.Ico 1 N))

Then I do simp at H and I get in the context

H :
  ⟨k, blocks_fun⟩ ∈
    finset.sigma (finset.range N) (λ (n : ℕ), fintype.pi_finset (λ (i : fin n), finset.Ico 1 N)),
H : k < N ∧ ∀ (a : fin k), 1 ≤ blocks_fun a ∧ blocks_fun a < N

So, the first H hasn't disappeared, but a new one with the simplified version has appeared. No MWE, sorry. Any idea why this could happen?

[Yury G. Kudryashov]

Probably type of something depends on the old H.

[Kevin Buzzard]

Is the old H mentioned in eg the goal?