[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ length (permsOfList (a :: l)) = (length (a :: l))!
[PROOFSTEP]
rw [length_cons, Nat.factorial_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ length (permsOfList (a :: l)) = (length l + 1) * (length l)!
[PROOFSTEP]
simp only [permsOfList, length_append, length_permsOfList, length_bind, comp, length_map, map_const', sum_replicate,
  smul_eq_mul, succ_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
⊢ (length l)! + length l * (length l)! = length l * (length l)! + (length l)!
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ l
⊢ f ∈ permsOfList l
[PROOFSTEP]
induction l generalizing f with
| nil =>
  -- Porting note: applied `not_mem_nil` because it is no longer true definitionally.
  simp only [not_mem_nil] at h 
  exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.by_contradiction <| h x)
| cons a l IH =>
  by_cases hfa : f a = a
  · refine' mem_append_left _ (IH fun x hx => mem_of_ne_of_mem _ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l :=
    by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx 
    split_ifs at hx  with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
  suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
  refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ l
⊢ f ∈ permsOfList l
[PROOFSTEP]
induction l generalizing f with
| nil =>
  -- Porting note: applied `not_mem_nil` because it is no longer true definitionally.
  simp only [not_mem_nil] at h 
  exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.by_contradiction <| h x)
| cons a l IH =>
  by_cases hfa : f a = a
  · refine' mem_append_left _ (IH fun x hx => mem_of_ne_of_mem _ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l :=
    by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx 
    split_ifs at hx  with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
  suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
  refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
⊢ f ∈ permsOfList []
[PROOFSTEP]

| nil =>
  -- Porting note: applied `not_mem_nil` because it is no longer true definitionally.
  simp only [not_mem_nil] at h 
  exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.by_contradiction <| h x)
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
⊢ f ∈ permsOfList []
[PROOFSTEP]
simp only [not_mem_nil] at h 
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → False
⊢ f ∈ permsOfList []
[PROOFSTEP]
exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.by_contradiction <| h x)
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]

| cons a l IH =>
  by_cases hfa : f a = a
  · refine' mem_append_left _ (IH fun x hx => mem_of_ne_of_mem _ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l :=
    by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx 
    split_ifs at hx  with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
  suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
  refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
by_cases hfa : f a = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ↑f a = a
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
refine' mem_append_left _ (IH fun x hx => mem_of_ne_of_mem _ (h x hx))
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ↑f a = a
x : α
hx : ↑f x ≠ x
⊢ x ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
hx : ↑f x ≠ x
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ↑f x = x
⊢ False
[PROOFSTEP]
exact hx hfa
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l :=
  by
  intro x hx
  have hxa : x ≠ a := by
    rintro rfl
    apply hx
    simp only [mul_apply, swap_apply_right]
  refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
  simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx 
  split_ifs at hx  with h_1
  exacts [hxa (h.symm.trans h_1), hx h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
⊢ ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hx : ↑(Equiv.swap a (↑f a) * f) x ≠ x
⊢ x ∈ l
[PROOFSTEP]
have hxa : x ≠ a := by
  rintro rfl
  apply hx
  simp only [mul_apply, swap_apply_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hx : ↑(Equiv.swap a (↑f a) * f) x ≠ x
⊢ x ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ¬↑f x = x
hfa' : ↑f (↑f x) ≠ ↑f x
hx : ↑(Equiv.swap x (↑f x) * f) x ≠ x
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ¬↑f x = x
hfa' : ↑f (↑f x) ≠ ↑f x
hx : ↑(Equiv.swap x (↑f x) * f) x ≠ x
⊢ ↑(Equiv.swap x (↑f x) * f) x = x
[PROOFSTEP]
simp only [mul_apply, swap_apply_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hx : ↑(Equiv.swap a (↑f a) * f) x ≠ x
hxa : x ≠ a
⊢ x ∈ l
[PROOFSTEP]
refine' List.mem_of_ne_of_mem hxa (h x fun h => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hx : ↑(Equiv.swap a (↑f a) * f) x ≠ x
hxa : x ≠ a
h : ↑f x = x
⊢ False
[PROOFSTEP]
simp only [mul_apply, swap_apply_def, mul_apply, Ne.def, apply_eq_iff_eq] at hx 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hxa : x ≠ a
h : ↑f x = x
hx : ¬(if ↑f x = a then ↑f a else if x = a then a else ↑f x) = x
⊢ False
[PROOFSTEP]
split_ifs at hx  with h_1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hxa : x ≠ a
h : ↑f x = x
h_1 : ↑f x = a
hx : ¬↑f a = x
⊢ False
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
x : α
hxa : x ≠ a
h : ↑f x = x
h_1 : ¬↑f x = a
hx : ¬↑f x = x
⊢ False
[PROOFSTEP]
exacts [hxa (h.symm.trans h_1), hx h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
  simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this✝ : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
this : f ∈ permsOfList l ∨ ∃ b, b ∈ l ∧ ∃ g, g ∈ permsOfList l ∧ Equiv.swap a b * g = f
⊢ f ∈ permsOfList (a :: l)
[PROOFSTEP]
simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_bind]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList l ∨ ∃ b, b ∈ l ∧ ∃ g, g ∈ permsOfList l ∧ Equiv.swap a b * g = f
[PROOFSTEP]
refine' or_iff_not_imp_left.2 fun _hfl => ⟨f a, _, Equiv.swap a (f a) * f, IH this, _⟩
[GOAL]
case neg.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
_hfl : ¬f ∈ permsOfList l
⊢ ↑f a ∈ l
[PROOFSTEP]
exact mem_of_ne_of_mem hfa (h _ hfa')
[GOAL]
case neg.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), ↑f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), ↑f x ≠ x → x ∈ a :: l
hfa : ¬↑f a = a
hfa' : ↑f (↑f a) ≠ ↑f a
this : ∀ (x : α), ↑(Equiv.swap a (↑f a) * f) x ≠ x → x ∈ l
_hfl : ¬f ∈ permsOfList l
⊢ Equiv.swap a (↑f a) * (Equiv.swap a (↑f a) * f) = f
[PROOFSTEP]
rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ ↑f heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []
[PROOFSTEP]
have : f = 1 := by simpa [permsOfList] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f = 1
[PROOFSTEP]
simpa [permsOfList] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
this : f = 1
⊢ ↑f heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
this : f = 1
⊢ ↑1 heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : x = a
⊢ x ∈ a :: l
[PROOFSTEP]
simp [hxa]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : x = y
⊢ x ∈ l
[PROOFSTEP]
rwa [hxy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ ↑g x ≠ x
[PROOFSTEP]
rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ (if ↑f x = a then y else if ↑f x = y then a else ↑f x) ≠ x
[PROOFSTEP]
split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ (if ↑f x = a then y else if ↑f x = y then a else ↑f x) ≠ x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝¹ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h✝ : ↑f x = a
⊢ y ≠ x
[PROOFSTEP]
exact Ne.symm hxy
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝² : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h✝¹ : ¬↑f x = a
h✝ : ↑f x = y
⊢ a ≠ x
[PROOFSTEP]
exact Ne.symm hxa
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
f : Equiv.Perm α
h✝² : f ∈ permsOfList (a :: l)
x : α
h : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
hx : ↑f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f => Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h✝¹ : ¬↑f x = a
h✝ : ¬↑f x = y
⊢ ↑f x ≠ x
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝ : Nodup []
⊢ Nodup (permsOfList [])
[PROOFSTEP]
simp [permsOfList]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
⊢ Nodup (permsOfList (a :: l))
[PROOFSTEP]
have hl' : l.Nodup := hl.of_cons
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
⊢ Nodup (permsOfList (a :: l))
[PROOFSTEP]
have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
⊢ Nodup (permsOfList (a :: l))
[PROOFSTEP]
have hmeml : ∀ {f : Perm α}, f ∈ permsOfList l → f a = a := fun {f} hf =>
  not_not.1 (mt (mem_of_mem_permsOfList hf _) (nodup_cons.1 hl).1)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList (a :: l))
[PROOFSTEP]
rw [permsOfList, List.nodup_append, List.nodup_bind, pairwise_iff_get]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList l) ∧
    ((∀ (x : α), x ∈ l → Nodup (List.map (fun f => Equiv.swap a x * f) (permsOfList l))) ∧
        ∀ (i j : Fin (length l)),
          i < j →
            List.Disjoint (List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l))
              (List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l))) ∧
      List.Disjoint (permsOfList l) (List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
[PROOFSTEP]
refine ⟨?_, ⟨⟨?_, ?_⟩, ?_⟩⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList l)
[PROOFSTEP]
exact hln'
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ ∀ (x : α), x ∈ l → Nodup (List.map (fun f => Equiv.swap a x * f) (permsOfList l))
[PROOFSTEP]
exact fun _ _ => hln'.map fun _ _ => mul_left_cancel
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ ∀ (i j : Fin (length l)),
    i < j →
      List.Disjoint (List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l))
        (List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l))
[PROOFSTEP]
intros i j hij x hx₁ hx₂
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
⊢ False
[PROOFSTEP]
let ⟨f, hf⟩ := List.mem_map.1 hx₁
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
⊢ False
[PROOFSTEP]
let ⟨g, hg⟩ := List.mem_map.1 hx₂
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
⊢ False
[PROOFSTEP]
have hix : x a = List.get l i := by rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
⊢ ↑x a = List.get l i
[PROOFSTEP]
rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
⊢ False
[PROOFSTEP]
have hiy : x a = List.get l j := by rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
⊢ ↑x a = List.get l j
[PROOFSTEP]
rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
hiy : ↑x a = List.get l j
⊢ False
[PROOFSTEP]
have hieqj : i = j := nodup_iff_injective_get.1 hl' (hix.symm.trans hiy)
[GOAL]
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
hiy : ↑x a = List.get l j
hieqj : i = j
⊢ False
[PROOFSTEP]
exact absurd hieqj (_root_.ne_of_lt hij)
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ List.Disjoint (permsOfList l) (List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
[PROOFSTEP]
intros f hf₁ hf₂
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
⊢ False
[PROOFSTEP]
let ⟨x, hx, hx'⟩ := List.mem_bind.1 hf₂
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
⊢ False
[PROOFSTEP]
let ⟨g, hg⟩ := List.mem_map.1 hx'
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ False
[PROOFSTEP]
have hgxa : g⁻¹ x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ ↑f (↑g⁻¹ x) = ↑f a
[PROOFSTEP]
rw [hmeml hf₁, ← hg.2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ ↑(Equiv.swap a x * g) (↑g⁻¹ x) = a
[PROOFSTEP]
simp
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hgxa : ↑g⁻¹ x = a
⊢ False
[PROOFSTEP]
have hxa : x ≠ a := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
[GOAL]
case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hgxa : ↑g⁻¹ x = a
hxa : x ≠ a
⊢ False
[PROOFSTEP]
exact (List.nodup_cons.1 hl).1 <| hgxa ▸ mem_of_mem_permsOfList hg.1 _ (by rwa [apply_inv_self, hgxa])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hgxa : ↑g⁻¹ x = a
hxa : x ≠ a
⊢ ↑g (↑g⁻¹ x) ≠ ↑g⁻¹ x
[PROOFSTEP]
rwa [apply_inv_self, hgxa]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
a b : List α
hab : a ≈ b
ha : Multiset.Nodup (Quotient.mk (isSetoid α) a)
hb : Multiset.Nodup (Quotient.mk (isSetoid α) b)
x✝ : HEq ha hb
⊢ ∀ (a_1 : Equiv.Perm α),
    a_1 ∈ { val := ↑(permsOfList a), nodup := (_ : Nodup (permsOfList a)) } ↔
      a_1 ∈ { val := ↑(permsOfList b), nodup := (_ : Nodup (permsOfList b)) }
[PROOFSTEP]
simp [mem_permsOfList_iff, hab.mem_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ∀ {s : Finset α} {f : Equiv.Perm α}, f ∈ permsOfFinset s ↔ ∀ {x : α}, ↑f x ≠ x → x ∈ s
[PROOFSTEP]
rintro ⟨⟨l⟩, hs⟩ f
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk Setoid.r l)
f : Equiv.Perm α
⊢ f ∈ permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs } ↔
    ∀ {x : α}, ↑f x ≠ x → x ∈ { val := Quot.mk Setoid.r l, nodup := hs }
[PROOFSTEP]
exact mem_permsOfList_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ∀ (s : Finset α), card (permsOfFinset s) = (card s)!
[PROOFSTEP]
rintro ⟨⟨l⟩, hs⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk Setoid.r l)
⊢ card (permsOfFinset { val := Quot.mk Setoid.r l, nodup := hs }) = (card { val := Quot.mk Setoid.r l, nodup := hs })!
[PROOFSTEP]
exact length_permsOfList l
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Fintype α
⊢ ∀ (x : Equiv.Perm α), x ∈ permsOfFinset univ
[PROOFSTEP]
simp [mem_perms_of_finset_iff]
