# Zulip Chat Archive

## Stream: new members

### Topic: how to congr inside a condition?

#### Alex Kontorovich (Feb 03 2022 at 03:09):

Another stupid question: how to prove this?

```
example (s : ℕ → finset ℕ) (t : ℕ → finset ℕ) (x : ℕ) (hst : ∀ n, n ≤ x → (s n).card = (t n).card) :
∑ n in finset.Icc 1 x, (s n).card = ∑ n in finset.Icc 1 x, (t n).card :=
begin
sorry,
end
```

I can't use `congr'`

, because then I lose the condition `n ≤ x`

, needed to apply `hst`

...?

#### Kyle Miller (Feb 03 2022 at 04:06):

You need to "attach" the membership condition:

```
import algebra.big_operators.basic
import data.nat.interval
open_locale big_operators
example (s t: ℕ → ℕ) (x : ℕ) (hst : ∀ n, n ≤ x → s n = t n) :
∑ n in finset.Icc 1 x, s n = ∑ n in finset.Icc 1 x, t n :=
begin
conv
{ congr,
rw ← finset.sum_attach,
skip,
rw ← finset.sum_attach, },
congr,
ext ⟨y, hy⟩,
rw finset.mem_Icc at hy,
simp [hst _ hy.2],
end
```

#### Johan Commelin (Feb 03 2022 at 04:11):

Shouldn't

```
apply finset.sum_congr rfl
intros i hi,
apply hst,
library_search
```

prove this? (Didn't test)

#### Kyle Miller (Feb 03 2022 at 04:14):

Oh, right, docs#finset.sum_congr.

You can simplify that down to

```
example (s t: ℕ → ℕ) (x : ℕ) (hst : ∀ n, n ≤ x → s n = t n) :
∑ n in finset.Icc 1 x, s n = ∑ n in finset.Icc 1 x, t n :=
begin
apply finset.sum_congr rfl,
simp [hst] { contextual := tt },
end
```

#### Yakov Pechersky (Feb 03 2022 at 04:15):

```
import number_theory.divisors
open_locale big_operators
example (s t: ℕ → ℕ) (x : ℕ) (hst : ∀ n, n ≤ x → s n = t n) :
∑ n in finset.Icc 1 x, s n = ∑ n in finset.Icc 1 x, t n :=
begin
refine finset.sum_congr rfl _,
simp only [finset.mem_Icc, and_imp],
intros y hy,
exact hst _
end
```

#### Kevin Buzzard (Feb 03 2022 at 08:58):

I can never remember that "get simp to do intros" trick. That's the `contextual := tt`

thing, right? Is this in some FAQ somewhere?

#### Kyle Miller (Feb 03 2022 at 18:10):

@Kevin Buzzard Yes, that's the `contextual := tt`

thing. The paragraph right before the last code block at the simp page mentions it.

#### Kyle Miller (Feb 03 2022 at 18:12):

I wish it were easier to invoke. An idea that came to mind this morning (similar to a proposal I had before but perhaps more sane) is to have flags for tactics. For example, this could be an additional way you can add `contextual := tt`

:

```
simp/c [hst]
```

#### Kyle Miller (Feb 03 2022 at 18:13):

Or,

```
simp+c [hst]
```

#### Kyle Miller (Feb 03 2022 at 18:16):

That way we could have negative flags, for example

```
simp-bezpi+c
-- short for
simp-b-e-z-p-i+c
```

could turn off beta reduction, eta equivalence, zeta reductions, projection reduction, recursor reduction, while turning on `contextual`

Last updated: Dec 20 2023 at 11:08 UTC