[Merged by Bors] - feat(logic/function/iterate): Cancelling iterates

[YaelDillies]

We can cancel iterates of an injective function.

---

Match leanprover-community/mathlib4#1046

[eric-wieser]

What are your thoughts on a spelling without sub in the goal?

lemma iterate_cancel_of_iterate_add (hf : injective f) (ha : f^[m + n] a = (f^[n] a)) :
  f^[m] a = a :=
sorry

[YaelDillies]

The entire point of this lemma is the sub spelling, because rewriting m = n + (m - n) is very hard in other contexts (there will be several occurrences of m).

[eric-wieser]

I'm afraid I don't follow; can you give an example of hoow you intend to use thie lemma?

[YaelDillies]

Here is my use case

mathlib/src/combinatorics/additive/mathlib.lean

Lines 410 to 426 in 431a78f

	-- TODO: Golfable if we had an API for the order of an element under a permutation
	@[to_additive] lemma mem_stabilizer_finset' {s : finset β} :
	a ∈ stabilizer α s ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ s :=
	begin
	rw mem_stabilizer_finset,
	refine ⟨λ h b, (h _).2, λ h b, ⟨λ hab, _, λ hb, h hb⟩⟩,
	have : s.card < (finset.range (s.card + 1)).card := by simp,
	obtain ⟨m, n, hmn, hb⟩ : ∃ m n, m < n ∧ (((•) a)^[m]) b = (((•) a)^[n]) b,
	{ obtain ⟨m, -, n, -, hmn, hb⟩ :=
	finset.exists_ne_map_eq_of_card_lt_of_maps_to this (λ n hn, maps_to.iterate h n hab),
	obtain hmn | hnm := (nat.succ_ne_succ.2 hmn).lt_or_lt,
	{ exact ⟨_, _, hmn, hb⟩ },
	{ exact ⟨_, _, hnm, hb.symm⟩ } },
	rw [iterate_cancel_of_le (mul_action.injective _) hmn.le hb,
	←tsub_add_cancel_of_le (nat.succ_le_iff.2 $ tsub_pos_of_lt hmn)],
	exact maps_to.iterate h (n - m - 1) hab,
	end

[b-mehta]

I think the sub spelling is useful, but the add version could be useful too - can we just have both?

[YaelDillies]

Here's one. I will update the mathlib4 PR once you're happy with it.

[eric-wieser]

Mind merging this new lemma into your branch linked above, so I can see if it leads to a shorter proof?

[YaelDillies]

Done

[YaelDillies]

I am not using this lemma in branch kneser anymore. However, Sébastien's suggestion now justifies the sub spelling.

[eric-wieser]

bors d+

I'm not super happy with the name "cancel" because the cancellation only disappears from one side; but have no other suggestions.

Are either of these true as iffs (keeping injectivity as a hypothesis)?

Thanks! Don't forget to adjust the forward port.

[bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

mathlib4 PR approved

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests