## Stream: general

### Topic: weird simp behavior

#### Sebastien Gouezel (Apr 11 2020 at 15:41):

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 (Apr 11 2020 at 15:59):

Probably type of something depends on the old H.

#### Kevin Buzzard (Apr 11 2020 at 16:03):

Is the old H mentioned in eg the goal?

Last updated: May 14 2021 at 07:19 UTC