## 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