mathlib documentation

Apply a congruence lemma inside conv mode.

When called without an argument apply_congr will try applying all lemmas marked with @[congr]. Otherwise apply_congr e will apply the lemma e.

Recall that a goal that appears as ∣ X in conv mode represents a goal of ⊢ X = ?m, i.e. an equation with a metavariable for the right hand side.

To successfully use apply_congr e, e will need to be an equation (possibly after function arguments), which can be unified with a goal of the form X = ?m. The right hand side of e will then determine the metavariable, and conv will subsequently replace X with that right hand side.

As usual, apply_congr can create new goals; any of these which are _not_ equations with a metavariable on the right hand side will be hard to deal with in conv mode. Thus apply_congr automatically calls intros on any new goals, and fails if they are not then equations.

In particular it is useful for rewriting inside the operand of a finset.sum, as it provides an extra hypothesis asserting we are inside the domain.

For example:

example (f g : ℤ → ℤ) (S : finset ℤ) (h : ∀ m ∈ S, f m = g m) :
  finset.sum S f = finset.sum S g :=
begin
  conv_lhs {
    -- If we just call `congr` here, in the second goal we're helpless,
    -- because we are only given the opportunity to rewrite `f`.
    -- However `apply_congr` uses the appropriate `@[congr]` lemma,
    -- so we get to rewrite `f x`, in the presence of the crucial `H : x ∈ S` hypothesis.
    apply_congr,
    skip,
    simp [h, H],
  }
end

In the above example, when the apply_congr tactic is called it gives the hypothesis H : x ∈ S which is then used to rewrite the f x to g x.