Finiteness of a `Set (ℕ × ℕ × ℕ)` with bounded components

Stream: mathlib4

[Jeremy Tan]

What's the shortest way to prove that a Set of tuples of natural numbers is finite, given that all components of tuples in the set are bounded?

import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fintype.CardEmbedding
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic.Linarith

section Defs

variable (k : ℕ) [hk : Fact (4 * k + 1).Prime]

def zagierSet := {t : ℕ × ℕ × ℕ | t.1 * t.1 + 4 * t.2.1 * t.2.2 = 4 * k + 1}

theorem zagierSet_lower_bound (h : (x, y, z) ∈ zagierSet k) : 0 < x ∧ 0 < y ∧ 0 < z := by
  simp_rw [zagierSet, Set.mem_setOf_eq] at h
  refine' ⟨_, _, _⟩ <;> (by_contra q; push_neg at q; rw [le_zero_iff] at q; subst q; simp at h)
  · apply_fun (· % 4) at h
    simp [mul_assoc, Nat.add_mod] at h
  all_goals cases' (Nat.dvd_prime hk.out).1 (dvd_of_mul_left_eq _ h) with e e <;>
    (subst e; simp at h; subst h; simp at hk; exact hk.out)

theorem zagierSet_upper_bound (h : (x, y, z) ∈ zagierSet k) : x ≤ k + 1 ∧ y ≤ k ∧ z ≤ k := by
  obtain ⟨hx, hy, hz⟩ := zagierSet_lower_bound k h
  simp_rw [zagierSet, Set.mem_setOf_eq] at h
  refine' ⟨_, _, _⟩ <;> nlinarith

instance fintypeZagierSet : Fintype (zagierSet k) := by
  sorry

end Defs

[Adam Topaz]

You can embed it into a type that’s known to be finite and use Fintype.ofInjcetive.

[Adam Topaz]

docs#Fintype.ofInjective

[Anatole Dedecker]

It's probably easier to stay with docs#Set.Finite for the proof (e.g you have docs#Set.Finite.subset) and then use docs#Set.Finite.fintype

[Adam Topaz]

With the proven bounds, it should be easy to embed it in Fin (k+2) x Fin (k+1) x Fin (k+ 1)

[Jeremy Tan]

(The context is Zagier's "one-sentence proof" of the sum of two squares theorem, from Wikipedia, using cardinalities of involutions)

[Jeremy Tan]

Anatole Dedecker said:

It's probably easier to stay with docs#Set.Finite for the proof (e.g you have docs#Set.Finite.subset) and then use docs#Set.Finite.fintype

like this?

instance finiteZagierSet : (zagierSet k).Finite := by
  sorry

[Alex J. Best]

Jeremy Tan said:

(The context is Zagier's "one-sentence proof" of the sum of two squares theorem, from Wikipedia, using cardinalities of involutions)

I also tried this long ago in lean 3, hopefully it is much easier now with the development of mathlib. At the time I remember finiteness statements like this being a nightmare

[Alex J. Best]

Jeremy Tan said:

Anatole Dedecker said:

It's probably easier to stay with docs#Set.Finite for the proof (e.g you have docs#Set.Finite.subset) and then use docs#Set.Finite.fintype

like this?

instance fintypeZagierSet : Set.Finite (zagierSet k) := by
  sorry

Set.Finite isn't a typeclass, so this should just be a lemma

[Jeremy Tan]

oeps

[Jeremy Tan]

Adam Topaz said:

With the proven bounds, it should be easy to embed it in Fin (k+2) x Fin (k+1) x Fin (k+ 1)

Fin (k + 2) × Fin (k + 1) × Fin (k + 1) isn't a set…

[Adam Topaz]

Yes, your original message asked for a fintype instance…

[Jeremy Tan]

This doesn't work

theorem finiteZagierSet : (zagierSet k).Finite := by
  refine' @Set.Finite.subset (Fin (k + 2) × Fin (k + 1) × Fin (k + 1)) Set.univ inferInstance _ _

[Adam Topaz]

What I was suggesting is to define an injective map from the type associated to your set into this product of Fins, then use the lemma I mentioned to prove that the type associated to your set is a fintype. If you want a proof using Set.Finite then this approach might not be the best.

[Adam Topaz]

Unfortunately I’m away from my computer for the rest of the day, so I can’t help much with actual lean code

[Jeremy Tan]

I think I got the right statement

instance zagierSetEmbedding : {t // t ∈ zagierSet k} ↪ Fin (k + 2) × Fin (k + 1) × Fin (k + 1) := by
  sorry

[Adam Topaz]

That shouldn’t be an instance

[Adam Topaz]

And you don’t necessarily need subtype notation

[Eric Wieser]

I think you might have an easier time showing that it's equal to (Finset.Ioc 0 (k + 1)).product <| (Finset.Ioc 0 k)).product <| Finset.Ioc 0 k) filtered by the obvious relation

[Adam Topaz]

Maybe contained in, as opposed to equal to?

[Adam Topaz]

That way you don’t need any relation, and should still suffice for Set.Finite

[Adam Topaz]

Also, probably docs#Finset.Icc ?

[Jeremy Tan]

Eric Wieser said:

I think you might have an easier time showing that it's equal to (Finset.Ioc 0 (k + 1)).product <| (Finset.Ioc 0 k)).product <| Finset.Ioc 0 k) filtered by the obvious relation

failed to synthesize instance
  LocallyFiniteOrder ℕ

[Johan Commelin]

I hope that only means you are missing an import

[Jeremy Tan]

yeah, the required instance is in Data.Nat.Interval

[Jeremy Tan]

Seems a bit better now

import Mathlib.Data.Nat.Interval
import Mathlib.Data.Nat.Prime
import Mathlib.Tactic.Linarith

section Defs

open Finset

variable (k : ℕ) [hk : Fact (4 * k + 1).Prime]

def zagierSet := {t : ℕ × ℕ × ℕ | t.1 * t.1 + 4 * t.2.1 * t.2.2 = 4 * k + 1}

lemma zagierSet_lower_bound (h : (x, y, z) ∈ zagierSet k) : 0 < x ∧ 0 < y ∧ 0 < z := by
  simp_rw [zagierSet, Set.mem_setOf_eq] at h
  refine' ⟨_, _, _⟩ <;> (by_contra q; push_neg at q; rw [le_zero_iff] at q; subst q; simp at h)
  · apply_fun (· % 4) at h
    simp [mul_assoc, Nat.add_mod] at h
  all_goals cases' (Nat.dvd_prime hk.out).1 (dvd_of_mul_left_eq _ h) with e e <;>
    (subst e; simp at h; subst h; simp at hk; exact hk.out)

lemma zagierSet_upper_bound (h : (x, y, z) ∈ zagierSet k) : x ≤ k + 1 ∧ y ≤ k ∧ z ≤ k := by
  obtain ⟨hx, hy, hz⟩ := zagierSet_lower_bound k h
  simp_rw [zagierSet, Set.mem_setOf_eq] at h
  refine' ⟨_, _, _⟩ <;> nlinarith

def zagierFinset :=
  ((Ioc 0 (k + 1)).product ((Ioc 0 k).product (Ioc 0 k))).filter
    (fun ⟨x, y, z⟩ => x * x + 4 * y * z = 4 * k + 1)

def zagierSetEquiv : zagierSet k ≃ zagierFinset k where
  toFun := fun ⟨⟨x, y, z⟩, h⟩ => by
    obtain ⟨hx, hy, hz⟩ := zagierSet_upper_bound k h
    exact ⟨(x, y, z), by simp⟩
    sorry

end Defs

[Eric Wieser]

You should be showing zagierSet k = zagierFinset k!

[Jeremy Tan]

It's 1:30am here...

[Jeremy Tan]

I should be sleeping but the thrill is preventing me from doing that

[Jeremy Tan]

(deleted)

[Jeremy Tan]

What's the correct theorem to show that two sets are equal by showing that every element of one set is contained in the other?

[Jeremy Tan]

A documentation search doesn't turn up anything

[Jeremy Tan]

oh, wait, ext might do it

[Jeremy Tan]

whee

theorem zagierSet_eq : zagierSet k = zagierFinset k := by
  ext ⟨x, y, z⟩
  refine' ⟨fun h => _, fun h => _⟩
  · unfold zagierSet at h
    unfold zagierFinset; simp_all
    have lb := zagierSet_lower_bound k h
    have ub := zagierSet_upper_bound k h
    apply mem_product.2; simp
    constructor; · exact ⟨lb.1, ub.1⟩
    apply mem_product.2; simp
    exact ⟨⟨lb.2.1, ub.2.1⟩, ⟨lb.2.2, ub.2.2⟩⟩
  · unfold zagierFinset at h
    unfold zagierSet; simp_all

[Eric Wieser]

(zagierSet k).Finite should follow trivially from there, though you probably don't need it at all now you have the finset

[Yaël Dillies]

Eric Wieser said:

I think you might have an easier time showing that it's equal to (Finset.Ioc 0 (k + 1)).product <| (Finset.Ioc 0 k)).product <| Finset.Ioc 0 k) filtered by the obvious relation

/me screams in unused notation

[Eric Wieser]

I never set up a global input method and didn't have lean open. Indeed, using notation for docs#Finset.product would be better

[Jeremy Tan]

This is the key theorem used in Zagier's proof – not sure how to go from here

import Mathlib.Dynamics.PeriodicPts
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Nat.ModEq

variable [Fintype α] [DecidableEq α] {p : ℕ} [Fact p.Prime]

open Function

theorem card_fixedPoints_modEq_card (f : α → α) (hf : f^[p] = id) :
    Fintype.card (fixedPoints f) ≡ Fintype.card α [MOD p] := by
  sorry

[Jeremy Tan]

There needs to be some statement that "α decomposes into its orbits under f" but no idea where that is

[Jeremy Tan]

The orbit-stabiliser theorem may help, but how do I put a group structure on the function application?

[Eric Wieser]

docs#Function.End

[Alex J. Best]

Probably the quickest way in mathlib is to use the fact that the submonoid generated by your fixed morphism is finite, hence actually a group

[Alex J. Best]

Searching the docs I found https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/PGroup.html#IsPGroup.card_modEq_card_fixedPoints

[Jeremy Tan]

OK, I'm really confused now

import Mathlib.Dynamics.PeriodicPts
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Nat.ModEq
import Mathlib.GroupTheory.GroupAction.Quotient
import Mathlib.GroupTheory.PGroup
import Mathlib.GroupTheory.Submonoid.Membership

variable {α : Type*} [Fintype α] [DecidableEq α] {p : ℕ} [Fact p.Prime]
  (f : α → α) (hf : f^[p] = id)

open Function Submonoid

def iterClosure : Submonoid (Function.End α) := powers f

def groupIterClosure : Group (iterClosure f) where
  inv g := ⟨f^[p - 1], by
    unfold iterClosure
    rw [mem_powers_iff]
    use p - 1
    sorry⟩
  mul_left_inv k := sorry

I don't know how to get from HPow to Nat.iterate in the first sorry

α: Type u_1
inst✝²: Fintype α
inst✝¹: DecidableEq α
p: ℕ
inst✝: Fact (Nat.Prime p)
f: α → α
hf: f^[p] = id
g: { x // x ∈ iterClosure f }
⊢ f ^ (p - 1) = f^[p - 1]

[Jeremy Tan]

MonoidHom.coe_pow doesn't work because it expects Monoid.End rather than the type of f, which is Function.End

[Damiano Testa]

I do not really know the End-part of mathlib, but maybe there is a missing lemma:

theorem missing? (f : Function.End α) (k : ℕ) : f ^ k = f^[k] := by
  induction k with
    | zero => rfl
    | succ n ih =>
      simp only [iterate_succ', ← ih, pow_succ]
      rfl

def groupIterClosure : Group (iterClosure f) where
  inv g := ⟨f^[p - 1], by
    unfold iterClosure
    rw [mem_powers_iff]
    use p - 1
    apply missing?⟩
  mul_left_inv k := sorry

[Yaël Dillies]

Note that I have a PR making missing? true definitionally.

[Damiano Testa]

It seems that missing API in Lean is a synonym for "Yaël has a PR for it".

[Yaël Dillies]

... or Eric!

[Jeremy Tan]

Yaël Dillies said:

Note that I have a PR making missing? true definitionally.

Yes. Where is it?

[Jeremy Tan]

Is it #862?!

[Eric Wieser]

I'd argue we're missing some API for type-casting with Function.End and Monoid.End, which is why missing? is missing

[Jeremy Tan]

I don't know how to deal with the build failures in #862

[Jeremy Tan]

The failures in Algebra.Group.Units mention rfl but rfl is nowhere to be found

[Eric Wieser]

the rfl is in the default value for a field you didn't provide

[Jeremy Tan]

Now Lean simply refuses to rewrite the * in the goal state before the sorry (g^[p - 1] * g = 1) to function composition

import Mathlib.Dynamics.PeriodicPts
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Nat.ModEq
import Mathlib.GroupTheory.GroupAction.Quotient
import Mathlib.GroupTheory.PGroup
import Mathlib.GroupTheory.Submonoid.Membership

variable {α : Type*} [Fintype α] [DecidableEq α] {p : ℕ} [Fact p.Prime]
  (f : Function.End α) (hf : f^[p] = id)

open Function Submonoid

theorem pow_eq_iterate (k : ℕ) : f ^ k = f^[k] := by
  induction k with
    | zero => rfl
    | succ n ih =>
      simp only [iterate_succ', ← ih, pow_succ]
      rfl

def iterClosure : Submonoid (Function.End α) := powers f

def groupIterClosure : Group (iterClosure f) where
  inv := fun ⟨g, hg⟩ => ⟨g^[p - 1], by
    unfold iterClosure at hg ⊢
    rw [mem_powers_iff] at hg ⊢
    obtain ⟨k, hk⟩ := hg
    use k * (p - 1)
    rw [← pow_eq_iterate, ← hk, pow_mul]⟩
  mul_left_inv := fun ⟨g, hg⟩ => by
    simp only [ge_iff_le, mk_mul_mk]
    congr
    sorry

[Jeremy Tan]

wait…

[Jeremy Tan]

yeah this works

import Mathlib.Dynamics.PeriodicPts
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Nat.ModEq
import Mathlib.GroupTheory.GroupAction.Quotient
import Mathlib.GroupTheory.PGroup
import Mathlib.GroupTheory.Submonoid.Membership

variable {α : Type*} [Fintype α] [DecidableEq α] {p : ℕ} [hp : Fact p.Prime]
  (f : Function.End α) (hf : f^[p] = id)

open Function Submonoid

theorem pow_eq_iterate (k : ℕ) : f ^ k = f^[k] := by
  induction k with
    | zero => rfl
    | succ n ih =>
      simp only [iterate_succ', ← ih, pow_succ]
      rfl

def groupIterClosure : Group (powers f) where
  inv := fun ⟨g, hg⟩ => ⟨g^[p - 1], by
    rw [mem_powers_iff] at hg ⊢
    obtain ⟨k, hk⟩ := hg
    use k * (p - 1)
    rw [← pow_eq_iterate, ← hk, pow_mul]⟩
  mul_left_inv := fun ⟨g, hg⟩ => by
    simp only [ge_iff_le, mk_mul_mk]
    congr
    rw [← pow_eq_iterate, ← pow_succ',
      Nat.sub_add_cancel (one_le_two.trans (Nat.Prime.two_le hp.out))]
    rw [mem_powers_iff] at hg
    obtain ⟨k, hk⟩ := hg
    rw [← hk, ← pow_mul, mul_comm, pow_mul, pow_eq_iterate f, hf, pow_eq_iterate, iterate_id]
    rfl

[Jeremy Tan]

(hp being the Fact that p is prime)

[Jeremy Tan]

This is much better, but how can I prove the last instance below (with the sorry)?

import Mathlib.GroupTheory.PGroup

section Key

variable {α : Type*} [Fintype α] [DecidableEq α] {p : ℕ} [hp : Fact p.Prime]
  (f : Function.End α) (hf : f^[p] = id)

open Function Submonoid

/-- A shim theorem. -/
theorem pow_eq_iterate (k : ℕ) : f ^ k = f^[k] := by
  induction k with
    | zero => rfl
    | succ n ih =>
      simp only [iterate_succ', ← ih, pow_succ]
      rfl

def groupPowers : Group (powers f) where
  inv := fun ⟨g, hg⟩ => ⟨g^[p - 1], by
    rw [mem_powers_iff] at hg ⊢
    obtain ⟨k, hk⟩ := hg
    use k * (p - 1)
    rw [← pow_eq_iterate, ← hk, pow_mul]⟩
  mul_left_inv := fun ⟨g, hg⟩ => by
    simp only [ge_iff_le, mk_mul_mk]
    congr
    rw [← pow_eq_iterate, ← pow_succ',
      Nat.sub_add_cancel (one_le_two.trans (Nat.Prime.two_le hp.out))]
    rw [mem_powers_iff] at hg
    obtain ⟨k, hk⟩ := hg
    rw [← hk, ← pow_mul, mul_comm, pow_mul, pow_eq_iterate f, hf, pow_eq_iterate, iterate_id]
    rfl

instance mulActionPowers : MulAction (powers f) α where
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

theorem isPGroup_of_powers : @IsPGroup p (powers f) (groupPowers f hf) := by
  unfold IsPGroup
  intro ⟨g, hg⟩
  use 1
  simp; congr
  rw [mem_powers_iff] at hg
  obtain ⟨k, hk⟩ := hg
  rw [← hk, ← pow_mul, mul_comm, pow_mul, pow_eq_iterate f, hf, pow_eq_iterate, iterate_id]
  rfl

instance : Fintype (MulAction.fixedPoints (powers f) α) := by
  convert Set.fintypeSubset (@Set.univ α) _
  · sorry
  · simp

def key := @IsPGroup.card_modEq_card_fixedPoints _ _ (_) (isPGroup_of_powers f hf) _ α _ _ _

end Key

[Jeremy Tan]

Since MulAction.fixedPoints (powers f) α is of type Set α and α is already a Fintype, there should be an obvious lemma I am missing

[Alex J. Best]

exact? finds the answer for me

[Jeremy Tan]

My code's gotten big enough that I've pushed all of it to the zagier branch on mathlib4:
https://github.com/leanprover-community/mathlib4/tree/zagier

I now have a problem at the sorry on L145 of Mathlib/NumberTheory/Zagier.lean.

theorem sq_add_sq_of_nonempty_fixedPoints
    (hn : (MulAction.fixedPoints (powers (obvInvo k)) (zagierSubtype k)).Nonempty) :
    ∃ a b : ℕ, a * a + b * b = 4 * k + 1 := by
  obtain ⟨⟨⟨x, y, z⟩, he⟩, hf⟩ := hn
  rw [MulAction.mem_fixedPoints, Subtype.forall] at hf
  have := hf (obvInvo k) (mem_powers _)
  sorry

k: ℕ
hk: Fact (Nat.Prime (4 * k + 1))
xyz: ℕ
he: (x, y, z) ∈ zagierSet k
hf: ∀ (a : Function.End (zagierSubtype k)) (b : a ∈ powers (obvInvo k)),
  { val := a, property := b } • { val := (x, y, z), property := he } = { val := (x, y, z), property := he }
this: { val := obvInvo k, property := (_ : obvInvo k ∈ powers (obvInvo k)) } • { val := (x, y, z), property := he } =
  { val := (x, y, z), property := he }
⊢ ∃ a b, a * a + b * b = 4 * k + 1

I want to simplify this to the condition that y = z but I can't get through the • of subtypes

[Jeremy Tan]

Here obvInvo is the obvious involution in Zagier's proof (x, y, z) -> (x, z, y). Its fixed points correspond to representations of a 4k+1 prime as a sum of two squares

[Jeremy Tan]

Then there is a more complicated involution (not yet defined in the branch), defined piecewise, which Zagier shows to have exactly one fixed point (1, 1, k). His argument then goes

• since there is exactly 1 fixed point of the complicated involution, Odd (Fintype.card (zagierSubtype k))
• therefore (MulAction.fixedPoints (powers (obvInvo k)) (zagierSubtype k)).Nonempty by modular considerations
• the fixed point of obvInvo gives a representation of 4 * k + 1 as a sum of two squares.

[Kevin Buzzard]

I thought that we already had a proof that primes which are 1 mod 4 are the sum of two squares

[Johan Commelin]

But not a proof that fits in the title of a PR.

[Jeremy Tan]

Right, now how do I get from this to y = z?

[Eric Wieser]

I would guess congr_arg subtype.val this followed by dsimp

[Jeremy Tan]

Eric Wieser said:

I would guess congr_arg subtype.val this followed by dsimp

Doesn't work. I have

theorem sq_add_sq_of_nonempty_fixedPoints
    (hn : (MulAction.fixedPoints (powers (obvInvo k)) (zagierSubtype k)).Nonempty) :
    ∃ a b : ℕ, a * a + b * b = 4 * k + 1 := by
  obtain ⟨⟨⟨x, y, z⟩, he⟩, hf⟩ := hn
  rw [MulAction.mem_fixedPoints, Subtype.forall] at hf
  have := hf (obvInvo k) (mem_powers _)
  apply_fun Subtype.val at this
  dsimp at this

but in the goal state this still has outside SMul:

this: ↑({ val := obvInvo k, property := (_ : obvInvo k ∈ powers (obvInvo k)) } • { val := (x, y, z), property := he }) =
  (x, y, z)

[Eric Wieser]

It looks like a dsimp lemma is missing. Does change _ • _ = _ at this help?

[Eric Wieser]

Which instance is that •?

[Jeremy Tan]

That change doesn't work either. The SMul instance is

@HSMul.hSMul { x // x ∈ powers (obvInvo k) } (zagierSubtype k) (zagierSubtype k) instHSMul
  { val := obvInvo k, property := (_ : obvInvo k ∈ powers (obvInvo k)) } { val := (x, y, z), property := he } : zagierSubtype k

[Jeremy Tan]

(bear in mind you can now pull the zagier branch)

[Eric Wieser]

What's the instHSMul there?

[Jeremy Tan]

@instHSMul { x // x ∈ powers (obvInvo k) } (zagierSubtype k) MulAction.toSMul : HSMul { x // x ∈ powers (obvInvo k) } (zagierSubtype k) (zagierSubtype k)

[Eric Wieser]

And the MulAction.toSMul? you want to trace it back until you're past all the Foo.toBar instances

[Jeremy Tan]

@MulAction.toSMul { x // x ∈ powers (obvInvo k) } (zagierSubtype k) (toMonoid (powers (obvInvo k)))
  (mulActionPowers (obvInvo k)) : SMul { x // x ∈ powers (obvInvo k) } (zagierSubtype k)

[Eric Wieser]

Is mulActionPowers your own instance?

[Jeremy Tan]

Yes (it's defined in L92 of Zagier.lean in the branch)

[Jeremy Tan]

instance mulActionPowers : MulAction (powers f) α where
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

[Eric Wieser]

Does rw [Submonoid.smul_def] at this (then dsimp) make progress?

[Jeremy Tan]

Now _that_ works:

theorem sq_add_sq_of_nonempty_fixedPoints
    (hn : (MulAction.fixedPoints (powers (obvInvo k)) (zagierSubtype k)).Nonempty) :
    ∃ a b : ℕ, a * a + b * b = 4 * k + 1 := by
  obtain ⟨⟨⟨x, y, z⟩, he⟩, hf⟩ := hn
  rw [MulAction.mem_fixedPoints, Subtype.forall] at hf
  have := hf (obvInvo k) (mem_powers _)
  apply_fun Subtype.val at this
  rw [Submonoid.smul_def, End.smul_def] at this
  dsimp at this

[Jeremy Tan]

After the dsimp I have this: ↑(obvInvo k { val := (x, y, z), property := he }) = (x, y, z)

[Eric Wieser]

Sounds like you forgot to teach lean that obvInvo was obvious

[Jeremy Tan]

Full proof:

theorem sq_add_sq_of_nonempty_fixedPoints
    (hn : (MulAction.fixedPoints (powers (obvInvo k)) (zagierSubtype k)).Nonempty) :
    ∃ a b : ℕ, a * a + b * b = 4 * k + 1 := by
  obtain ⟨⟨⟨x, y, z⟩, he⟩, hf⟩ := hn
  rw [MulAction.mem_fixedPoints, Subtype.forall] at hf
  have := hf (obvInvo k) (mem_powers _)
  apply_fun Subtype.val at this
  rw [Submonoid.smul_def, End.smul_def] at this
  unfold obvInvo at this; simp at this
  unfold zagierSet at he; simp at he
  use x, (2 * y)
  rw [this.1, show 4 * y * y = 2 * y * (2 * y) by linarith] at he
  assumption

[Jeremy Tan]

THE PROOF IS FINISHED
#6629

[Damiano Testa]

This is a really long line!

[Jeremy Tan]

@Eric Wieser @Alex J. Best I have responded to your reviews

[Jeremy Tan]

@Thomas Browning how to prove the sorry below? The function is in GroupTheory.Perm.Cycle.Type after card_compl_support_modEq

/-- The number of fixed points of a `p ^ n`-th root of the identity function over a finite set
and the set's cardinality have the same residue modulo `p`, where `p` is a prime. -/
theorem card_modEq_card_fixedPoints_of_pow_prime [DecidableEq α] {f : Function.End α} {p n : ℕ}
    [hp : Fact p.Prime] (hf : f ^ p ^ n = 1) :
    Fintype.card α ≡ Fintype.card f.fixedPoints [MOD p] := by
  let σ : α ≃ α := ⟨f, f ^ (p ^ n - 1),
  by
    simp_rw [Function.LeftInverse, ← Function.comp_apply (g := f),
      show (f ^ (p ^ n - 1)) ∘ f = f ^ (p ^ n - 1) * f by rfl, ← pow_succ',
      Nat.sub_add_cancel (pow_pos hp.out.pos n)]
    exact congrFun hf,
  by
    simp_rw [Function.RightInverse, Function.LeftInverse, ← Function.comp_apply (f := f),
      show f ∘ (f ^ (p ^ n - 1)) = f * f ^ (p ^ n - 1) by rfl, ← pow_succ,
      Nat.sub_add_cancel (pow_pos hp.out.pos n)]
    exact congrFun hf⟩
  have hσ : σ ^ p ^ n = 1 := by
    sorry
  suffices : Fintype.card f.fixedPoints = (support σ)ᶜ.card
  · exact this ▸ (card_compl_support_modEq hσ).symm
  suffices : f.fixedPoints = (support σ)ᶜ
  · simp only [this]; apply Fintype.card_coe
  simp [Set.ext_iff, Function.IsFixedPt]

[Thomas Browning]

Yes, it's more painful than it ought to be. I answered on github.

[Jeremy Tan]

It does not seem to help if I define npow on instMonoidEnd as follows:

instance : Monoid (Function.End α) where
  one := id
  mul := (· ∘ ·)
  mul_assoc f g h := rfl
  mul_one f := rfl
  one_mul f := rfl
  npow n f := f^[n]
  npow_zero _ := rfl
  npow_succ _ _ := by simp only [Function.iterate_succ']; rfl

[Jeremy Tan]

However, a less hacky way might be to override npow in instMonoidEnd

Yeah, I've overridden it, now what?

[Eric Wieser]

I don't think you should be refactoring that in that PR

[Jeremy Tan]

@Eric Wieser I have not committed the npow override to my PR