how to congr inside a condition?

Stream: new members

[Alex Kontorovich]

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]

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]

Shouldn't

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

prove this? (Didn't test)

[Kyle Miller]

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]

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]

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]

@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]

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]

Or,

simp+c [hst]

[Kyle Miller]

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