import Mathlib.GroupTheory.Perm.Cycle.Concrete
import Mathlib.Data.List.Card
import Mathlib.Data.List.Indexes

open Equiv List MulAction Pointwise Set Subgroup

variable {α : Type*} [DecidableEq α]

lemma length_remove_le (l : List α) (a : α) :
    (l.remove a).length ≤ l.length := by
  induction' l with b l ih
  · simp [remove]
  · simp [remove]
    split_ifs
    · linarith
    · simp
      linarith

lemma length_remove_lt_of_mem {l : List α} {a : α} (h : a ∈ l) :
    (l.remove a).length < l.length := by
  induction' l with b l ih
  · contradiction
  · rw [mem_cons] at h
    rcases h with rfl | h
    · simp [remove]
      have := length_remove_le l a
      linarith
    · specialize ih h
      simp [remove]
      split_ifs
      · linarith
      · simp
        linarith

def swapFactorsAux (l0 : List α) (a : α) (f : Perm α) (hf : ∀ {x}, f x ≠ x → x ∈ l0) :
    { l : List α // (l.map (fun x ↦ swap x (f x))).prod = f ∧ f⁻¹ a ∉ l ∧ ∀ x ∈ l, x ∈ l0 } :=
  if ha0 : f a = a then
    if ha : a ∈ l0 then
      have : (l0.remove a).length < l0.length := by
        exact length_remove_lt_of_mem ha
      let p := swapFactorsAux (l0.remove a) a f (by
        intro x hx
        rw [mem_remove_iff]
        refine' ⟨hf hx, _⟩
        rintro rfl
        contradiction)
      ⟨p, p.2.1, p.2.2.1, by
        intro x hx
        exact mem_of_mem_remove (p.2.2.2 x hx)
        ⟩
    else
      match l0 with
      | [] => ⟨[], Equiv.ext fun x => by
          rw [map_nil, prod_nil]
          exact (Classical.not_not.1 (mt hf (List.not_mem_nil _))).symm,
        by simp⟩
      | x :: l =>
          if hx : f x = x then
            let p := swapFactorsAux l a f (by
              intro y hy
              specialize hf hy
              rw [mem_cons] at hf
              rcases hf with rfl | hf
              · contradiction
              · exact hf
            )
            ⟨p, p.2.1, p.2.2.1, by
              intro x hx
              rw [mem_cons]
              exact Or.inr (p.2.2.2 x hx)
            ⟩
          else
            have : (l.remove x).length < (x :: l).length := by
              have := length_remove_le l x
              simp
              linarith
            let p := swapFactorsAux (l.remove x) (f x) (swap x (f x) * f) (by
              intro y hy
              rw [Perm.mul_apply] at hy
              rcases eq_or_ne x y with rfl | h1
              · rw [swap_apply_right] at hy
                contradiction
              · rcases eq_or_ne x (f y) with rfl | h2
                · specialize hf h1
                  rw [mem_cons, eq_comm] at hf
                  rcases hf with _ | hf
                  · contradiction
                  · rw [mem_remove_iff]
                    exact ⟨hf, h1.symm⟩
                · rw [swap_apply_of_ne_of_ne h2.symm] at hy
                  · specialize hf hy
                    rw [mem_cons] at hf
                    rcases hf with _ | hf
                    · symm at h1
                      contradiction
                    · rw [mem_remove_iff]
                      exact ⟨hf, h1.symm⟩
                  · contrapose! h1
                    symm
                    simp only [EmbeddingLike.apply_eq_iff_eq] at h1
                    exact h1
            )
            ⟨x :: p.1, by
              rw [map_cons, prod_cons]
              have key := p.2.1
              rw [← eq_inv_mul_iff_mul_eq, swap_inv]
              refine' Eq.trans _ key
              apply congrArg
              apply List.map_congr
              intro y hy
              congr 1
              have key' := p.2.2.1
              simp_rw [mul_inv_rev, swap_inv, Perm.mul_apply, swap_apply_right] at key'
              have : y ≠ f⁻¹ x
              · intro h
                rw [h] at hy
                exfalso
                refine' key' hy
              have : f y ≠ x
              · contrapose! this
                exact Perm.eq_inv_iff_eq.mpr this
              rw [Perm.mul_apply]
              have key'' := p.2.2.2 y hy
              rw [swap_apply_of_ne_of_ne this]
              simp only [ne_eq, EmbeddingLike.apply_eq_iff_eq]
              rintro rfl
              rw [mem_remove_iff] at key''
              apply key''.2
              rfl
              ,
              by
                have key := p.2.2.1
                simp_rw [mul_inv_rev, swap_inv, Perm.mul_apply, swap_apply_right] at key
                rw [mem_cons, not_or]
                have : f⁻¹ a = a
                · rw [← ha0]
                  simp
                  simp [ha0]
                rw [this]
                rw [mem_cons, not_or] at ha
                refine' ⟨ha.1, _⟩
                intro h
                apply ha.2
                exact mem_of_mem_remove (p.2.2.2 a h)
              , by
                  intro y hy
                  rw [mem_cons] at hy ⊢
                  rcases hy with hy | hy
                  · exact Or.inl hy
                  · exact Or.inr (mem_of_mem_remove (p.2.2.2 y hy))⟩
  else
    have : (l0.remove a).length < l0.length := by
      exact length_remove_lt_of_mem (hf ha0)
    let p := swapFactorsAux (l0.remove a) (f a) (swap a (f a) * f) (by
      intro x hx
      rw [mem_remove_iff]
      rw [Perm.mul_apply] at hx
      rcases eq_or_ne x a with rfl | h
      · rw [swap_apply_right] at hx
        contradiction
      · refine' ⟨_, h⟩
        apply hf
        intro h'
        rw [h'] at hx
        rw [swap_apply_ne_self_iff] at hx
        replace hx := hx.2
        rcases hx with rfl | rfl
        · contradiction
        · simp only [EmbeddingLike.apply_eq_iff_eq] at h'
          contradiction
      )
    ⟨a :: p.1, by
      have key := p.2.1
      rw [map_cons, prod_cons]
      rw [← eq_inv_mul_iff_mul_eq, swap_inv]
      refine' Eq.trans _ key
      apply congrArg
      apply List.map_congr
      intro x hx
      congr 1
      have key' := p.2.2.1
      simp_rw [mul_inv_rev, swap_inv, Perm.mul_apply, swap_apply_right] at key'
      have : x ≠ f⁻¹ a
      · intro h
        rw [h] at hx
        exfalso
        refine' key' hx
      have : f x ≠ a
      · contrapose! this
        exact Perm.eq_inv_iff_eq.mpr this
      rw [Perm.mul_apply]
      have key'' := p.2.2.2 x hx
      rw [mem_remove_iff] at key''
      rw [swap_apply_of_ne_of_ne this]
      simp only [ne_eq, EmbeddingLike.apply_eq_iff_eq]
      exact key''.2,
        by
      have key := p.2.2.1
      simp_rw [mul_inv_rev, swap_inv, Perm.mul_apply, swap_apply_right] at key
      rw [mem_cons, not_or]
      refine' ⟨_, key⟩
      intro h
      apply ha0
      exact (eq_symm_apply f).mp (id h.symm), by
        intro x hx
        rw [mem_cons] at hx
        rcases hx with rfl | hx
        · exact hf ha0
        · exact mem_of_mem_remove (p.2.2.2 x hx)
      ⟩
termination_by swapFactorsAux l _ _ _ => l.length

def swapFactorsAux' (l0 : List α) (a : α) (f : Perm α) (hf : ∀ {x}, f x ≠ x → x ∈ l0) :
    { l : List α // (l.map (fun x ↦ swap x (f x))).prod = f } :=
  let h := swapFactorsAux l0 a f hf
  ⟨h.1, h.2.1⟩

def truncSwapFactors [Fintype α] (f : Perm α) (a : α) :
    Trunc { l : List α // (l.map (fun x ↦ swap x (f x))).prod = f } :=
  Quotient.recOnSubsingleton (@Finset.univ α _).1 (fun l h => Trunc.mk (swapFactorsAux' l a f (h _)))
    (show ∀ x, f x ≠ x → x ∈ (@Finset.univ α _).1 from fun _ _ => Finset.mem_univ _)

def exists_list_swap [Fintype α] (f : Perm α) :
    ∃ l : List α, (l.map (fun x ↦ swap x (f x))).prod = f := by
  rcases isEmpty_or_nonempty α with h | ⟨⟨a⟩⟩
  · exact ⟨[], Subsingleton.elim _ _⟩
  · have q := truncSwapFactors f a
    refine' ⟨q.out, q.out.2⟩

variable [Finite α]

theorem aux2
    {H : Subgroup (Perm α)} {T : Set α} (hT : T.Pairwise (swap · · ∈ H))
    {a b : α} (ha : a ∈ T) (hab : swap a b ∈ H) :
    ({b} ∪ T).Pairwise (swap · · ∈ H) := by
  rintro x (rfl | hx) y (rfl | hy) hxy
  · contradiction
  · rcases eq_or_ne y a with rfl | h
    · exact swap_comm x y ▸ hab
    rw [← swap_mul_swap_mul_swap h hxy.symm]
    exact H.mul_mem (H.mul_mem hab (hT hy ha h)) hab
  · rcases eq_or_ne x a with rfl | h
    · exact swap_comm x y ▸ hab
    rw [swap_comm, ← swap_mul_swap_mul_swap h hxy]
    exact H.mul_mem (H.mul_mem hab (hT hx ha h)) hab
  · exact hT hx hy hxy

lemma orbit_lemma {G : Type*} [Group G] {α : Type*} [MulAction G α] {a b c : α} (h1 : a ∈ orbit G c) :
    b ∈ orbit G c ↔ b ∈ orbit G a := by
  simp only [← orbit_eq_iff] at h1 ⊢
  rw [h1]

theorem swap_mem_closure_iff_mem_orbit_of_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap)
    {x y : α} : swap x y ∈ closure S ↔ x ∈ orbit (closure S) y := by
  refine ⟨fun h ↦ mem_orbit_iff.mpr ⟨⟨swap x y, h⟩, swap_apply_right x y⟩, fun hf ↦ ?_⟩
  let P : Set α → Prop := fun T ↦ T.Pairwise (swap · · ∈ closure S)
  suffices : P (orbit (closure S) y)
  · rcases eq_or_ne x y with rfl | hxy
    · rw [swap_self]
      apply one_mem
    · exact this hf (mem_orbit_self y) hxy
  refine' (toFinite _).induction_to ∅ (empty_subset _) (pairwise_empty _) (fun T hT ih ↦ _)
  rcases T.eq_empty_or_nonempty with rfl | hT'
  · exact ⟨y, by simp⟩
  have key0 : ¬ closure S ≤ stabilizer (Perm α) T
  · obtain ⟨a, haT⟩ := hT'
    obtain ⟨b, hb, hbT⟩ := exists_of_ssubset hT
    have ha : a ∈ orbit (closure S) y := hT.1 haT
    obtain ⟨⟨σ, hσ⟩, rfl⟩ := (orbit_lemma ha).mp hb
    exact fun h ↦ hbT (h hσ ▸ smul_mem_smul_set haT)
  have key : ∃ a b, swap a b ∈ S ∧ a ∈ T ∧ b ∉ T
  · rw [closure_le, not_subset] at key0
    obtain ⟨τ, hτ, hτ'⟩ := key0
    obtain ⟨x, y, -, rfl⟩ := hS τ hτ
    rw [SetLike.mem_coe, swap_mem_stabilizer, not_iff] at hτ'
    by_cases hx : x ∈ T
    · exact ⟨x, y, hτ, hx, fun hy ↦ hτ'.mpr hy hx⟩
    · exact ⟨y, x, swap_comm x y ▸ hτ, hτ'.mp hx, hx⟩
  obtain ⟨a, b, hab, ha, hb⟩ := key
  refine' ⟨b, ⟨_, hb⟩, aux2 ih ha (subset_closure hab)⟩
  exact (orbit_lemma (hT.1 ha)).mpr ⟨⟨swap a b, subset_closure hab⟩, swap_apply_left a b⟩

theorem mem_closure_iff_mem_orbit_of_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap)
    {f : Perm α} : f ∈ closure S ↔ ∀ x, f x ∈ orbit (closure S) x := by
  refine ⟨fun hf x ↦ mem_orbit_iff.mpr ⟨⟨f, hf⟩, rfl⟩, fun hf ↦ ?_⟩
  have := Fintype.ofFinite α
  obtain ⟨l, hl⟩ := exists_list_swap f
  refine hl ▸ list_prod_mem (fun x hx ↦ ?_)
  obtain ⟨y, -, rfl⟩ := List.mem_map.mp hx
  rw [swap_comm, swap_mem_closure_iff_mem_orbit_of_isSwap hS]
  exact hf y

import Mathlib.Data.Set.Finite
import Mathlib.GroupTheory.GroupAction.Basic
import Mathlib.GroupTheory.Perm.Support

open Equiv List MulAction Pointwise Set Subgroup

variable {G α : Type*} [Group G] [MulAction G α] [DecidableEq α]

lemma orbit_lemma {a b c : α} (h : a ∈ orbit G c) :
    b ∈ orbit G c ↔ b ∈ orbit G a := by
  simp only [← orbit_eq_iff] at h ⊢
  rw [h]

theorem aux1 (S : Set G) (T : Set α) {a : α} (hS : ∀ g ∈ S, g⁻¹ ∈ S)
    (subset : T ⊆ orbit (closure S) a) (not_mem : a ∉ T) (nonempty : T.Nonempty) :
    ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T := by
  have key0 : ¬ closure S ≤ stabilizer G T
  · have ⟨b, hb⟩ := nonempty
    obtain ⟨σ, rfl⟩ := subset hb
    refine fun h ↦ not_mem ?_
    rw [← h (inv_mem σ.2), mem_smul_set]
    exact ⟨_, hb, show σ⁻¹ • σ • a = _ by simp⟩
  contrapose! key0
  refine (closure_le _).mpr fun σ hσ ↦ by_contra fun h ↦ ?_
  simp_rw [SetLike.mem_coe, mem_stabilizer_iff, Set.ext_iff, not_forall, mem_smul_set] at h
  obtain ⟨a, h⟩ := h
  exact h ⟨fun ⟨b, hb, h⟩ ↦ h ▸ key0 _ hσ _ hb, fun h ↦ ⟨_, key0 _ (hS σ hσ) _ h, by simp⟩⟩

theorem SubmonoidClass.swap_mem_trans {a b c : α} {C} [SetLike C (Perm α)]
    [SubmonoidClass C (Perm α)] (M : C)
    (hab : swap a b ∈ M) (hbc : swap b c ∈ M) : swap a c ∈ M := by
  obtain rfl | hab' := eq_or_ne a b; · exact hbc
  obtain rfl | hac := eq_or_ne a c; · rw [swap_self]; exact one_mem M
  rw [swap_comm, ← swap_mul_swap_mul_swap hab' hac]
  exact mul_mem (mul_mem hbc hab) hbc

theorem swap_mem_closure_iff_mem_orbit_of_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap)
    {x y : α} : swap x y ∈ closure S ↔ x ∈ orbit (closure S) y := by
  refine ⟨fun h ↦ mem_orbit_iff.mpr ⟨⟨swap x y, h⟩, swap_apply_right x y⟩, fun hf ↦ ?_⟩
  by_contra h
  have := aux1 S {x | swap x y ∈ closure S} (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩
  · obtain ⟨σ, hσ, a, ha, hσa⟩ := this
    obtain ⟨z, w, hzw, rfl⟩ := hS σ hσ
    rw [Perm.smul_def] at hσa
    have := ne_of_mem_of_not_mem ha hσa
    rw [ne_comm, swap_apply_ne_self_iff, and_iff_right hzw] at this
    rw [mem_setOf] at ha hσa
    apply hσa; clear hσa
    obtain rfl | rfl := this
    on_goal 1 => rw [swap_apply_left]; rw [swap_comm] at hσ
    on_goal 2 => rw [swap_apply_right]
    all_goals exact SubmonoidClass.swap_mem_trans _ (subset_closure hσ) ha
  · obtain ⟨x, y, -, rfl⟩ := hS f hf; rwa [swap_inv]
  · exact (orbit_lemma hf).mp ⟨⟨_ ,hz⟩, swap_apply_right z y⟩
  · rw [mem_setOf, swap_self]; exact one_mem _

-- `Equiv.Perm.set_support_mul_subset` etc. could be generalized to MulAction

theorem finite_apply_ne_self_closure_iff {S : Set G} :
    (∀ g ∈ closure S, {x : α | g • x ≠ x}.Finite) ↔ ∀ g ∈ S, {x : α | g • x ≠ x}.Finite :=
  ⟨fun h g hg ↦ h g (subset_closure hg), fun h g hg ↦ by
    refine closure_induction hg h (by simp) (fun g g' hg hg' ↦ (hg.union hg').subset ?_) fun g hg ↦ ?_
    · simp_rw [Ne, mul_smul, ← compl_setOf, ← compl_inter, compl_subset_compl]
      intro a ⟨hg, hg'⟩; rw [mem_setOf] at hg hg' ⊢; rw [hg', hg]
    · convert hg using 1; simp_rw [Ne, inv_smul_eq_iff, eq_comm]⟩

theorem finite_swap_apply_ne_self {x y : α} : {a | swap x y a ≠ a}.Finite :=
  Set.Finite.subset (s := {x, y}) (by simp)
    (by simp_rw [swap_apply_ne_self_iff]; exact fun _ ↦ (·.2))

theorem Equiv.Perm.IsSwap.finite_apply_ne_self {σ : Perm α} (h : σ.IsSwap) :
    {a | σ a ≠ a}.Finite := by
  obtain ⟨x, y, -, rfl⟩ := h; exact finite_swap_apply_ne_self

theorem mem_closure_iff_mem_orbit_of_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap)
    {f : Perm α} : f ∈ closure S ↔ {x | f x ≠ x}.Finite ∧ ∀ x, f x ∈ orbit (closure S) x := by
  refine ⟨fun hf ↦ ⟨?_, fun x ↦ mem_orbit_iff.mpr ⟨⟨f, hf⟩, rfl⟩⟩, ?_⟩
  · exact finite_apply_ne_self_closure_iff.mpr (fun f hf ↦ (hS f hf).finite_apply_ne_self) _ hf
  rintro ⟨fin, hf⟩
  set supp := {x | f x ≠ x} with supp_eq
  suffices : {x | f x ≠ x} ⊆ supp → f ∈ closure S
  · exact this supp_eq.symm.subset
  clear_value supp; clear supp_eq; revert f
  apply fin.induction_on ..
  · rintro f - emp; convert (closure S).one_mem; ext; by_contra h; exact emp h
  rintro a s has - ih f hf supp_subset
  refine (mul_mem_cancel_left ((swap_mem_closure_iff_mem_orbit_of_isSwap hS).2 (hf a))).1
    (ih (fun b ↦ ?_) fun b hb ↦ (supp_subset ?_).resolve_left ?_)
  · rw [Perm.mul_apply, orbit_lemma (hf b)]
    by_cases h' : f b = a; · rw [h', swap_apply_right]; apply hf
    by_cases h : f b = f a; · rw [h, swap_apply_left, ← orbitRel_apply, Setoid.comm']; apply hf
    rw [swap_apply_of_ne_of_ne h h']; apply mem_orbit_self
  · rw [mem_setOf] at hb ⊢; contrapose! hb; rw [Perm.mul_apply, hb]
    obtain rfl | hba := eq_or_ne b a; · rwa [swap_apply_right]
    refine swap_apply_of_ne_of_ne ?_ hba
    contrapose! hba; exact f.injective (hb.trans hba)
  · rw [mem_setOf] at hb; contrapose! hb; rw [Perm.mul_apply, hb, swap_apply_left]