mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {comm : (↑∅).Pairwise (Commute on f)}, (∀ a ∈ ∅, x ∉ (f a).support) → x ∉ (∅.noncommProd f comm).support

pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support

Tactic:
· simp

Goal state after:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(insert a s)).Pairwise (Commute on f)},
          (∀ a_3 ∈ insert a s, x ∉ (f a_3).support) → x ∉ ((insert a s).noncommProd f comm).support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ take n l ++ drop n l = l

pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = (drop n l).length

Tactic:
· simp

Goal state after:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = (drop n l).length
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝ : (z :: l).formPerm x = y
⊢ z ∈ y :: z :: l

pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : (z :: l).formPerm x = z
⊢ y ∈ y :: z :: l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : ¬(z :: l).formPerm x = z
⊢ (z :: l).formPerm x ∈ y :: z :: l

Tactic:
· simp

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : (z :: l).formPerm x = z
⊢ y ∈ y :: z :: l

case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : ¬(z :: l).formPerm x = z
⊢ (z :: l).formPerm x ∈ y :: z :: l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : (z :: l).formPerm x = z
⊢ y ∈ y :: z :: l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : ¬(z :: l).formPerm x = z
⊢ (z :: l).formPerm x ∈ y :: z :: l

Tactic:
· simp

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : ¬(z :: l).formPerm x = z
⊢ (z :: l).formPerm x ∈ y :: z :: l
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

Tactic:
· rw [formPerm_cons_cons, mul_apply, swap_apply_def]
      split_ifs
      · simp
      · simp
      · simp [*]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
⊢ f x ≠ x

Tactic:
← mem_support

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
⊢ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
w : (x :: xs).Nodup
h : xs.length < (x :: xs).length
this : xs.length ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = (x :: xs)[(xs.length + 1) % (x :: xs).length]

pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
· simp

Goal state after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| (x :: y :: l)[(k + 1 + n) % (x :: y :: l).length]

Tactic:
arg 2

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| (k + 1 + n) % (x :: y :: l).length
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| (x' :: y' :: l')[k + 1]

Tactic:
arg 2

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| k + 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
⊢ [].formPerm = 1 ↔ [].length ≤ 1

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1

Tactic:
· simp

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil.inl
α : Type u_1
inst✝ : DecidableEq α
hl hl' : [].Nodup
⊢ [].length ≤ 1

pp: case nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1

Tactic:
· simp

Goal state after:
case nil.inr
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
h : l'.length ≤ 1
⊢ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
x : Perm α
h : _root_.Disjoint x.support x.support
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
⊢ x ∈ ⊥

Tactic:
disjoint_self,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
x : Perm α
h : x.support = ⊥
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
⊢ x ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mem
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support

pp: case one
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ↑(support 1) ⊆ ⋃ b ∈ S, ↑b.support

pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

pp: case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
· exact fun x hx ↦ Set.subset_iUnion₂_of_subset x hx subset_rfl

Goal state after:
case one
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ↑(support 1) ⊆ ⋃ b ∈ S, ↑b.support

case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case one
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ↑(support 1) ⊆ ⋃ b ∈ S, ↑b.support

pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

pp: case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
· simp

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
⊢ f y = (swap x (f x)) y

Tactic:
rw [swap_apply_of_ne_of_ne hyx hfyx]
        refine by_contradiction fun hy => ?_
        obtain ⟨j, hj⟩ := hz.2 hy
        rw [← sub_add_cancel j i, zpow_add, mul_apply, hi] at hj
        rcases zpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji | hji
        · rw [← hj, hji] at hyx
          tauto
        · rw [← hj, hji] at hfyx
          tauto

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
⊢ f x ≠ x

Tactic:
← mem_support

Goal state after:
α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
⊢ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

Tactic:
rw [← mem_support, ← h, mem_support] at hx

Goal state after:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : (f ^ n) x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

pp: case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : ¬(f ^ n).support = f.support
⊢ f ^ n = 1

Tactic:
· rw [← mem_support, ← h, mem_support] at hx
        contradiction

Goal state after:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : ¬(f ^ n).support = f.support
⊢ f ^ n = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f.cycleOf x ^ Int.negSucc z) x = (f ^ Int.negSucc z) x

Tactic:
rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g (c x) = c (g x)

Tactic:
notMem_support.mp hx,

Goal state after:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g x = c (g x)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType.lcm = orderOf σ

Tactic:
by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => simp [hσ.cycleType, hσ.orderOf]
  | induction_disjoint σ τ hd _ hσ hτ => simp [hd.cycleType_mul, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ Option.map (⇑(removeNone σ)) none = (swap none (σ none)) (σ none)

pp: case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (σ (some x))

Tactic:
· simp

Goal state after:
case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (σ (some x))
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case zero
i : Fin (Nat.succ 0)
⊢ ↑((finRotate (Nat.succ 0)) i) = ↑((decomposeFin.symm (1, finRotate 0)) i)

pp: case succ
n✝ : ℕ
i : Fin (n✝ + 1).succ
⊢ ↑((finRotate (n✝ + 1).succ) i) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i)

Tactic:
· simp

Goal state after:
case succ
n✝ : ℕ
i : Fin (n✝ + 1).succ
⊢ ↑((finRotate (n✝ + 1).succ) i) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.refine_1
n✝ : ℕ
i : Fin (n✝ + 1).succ
⊢ ↑((finRotate (n✝ + 1).succ) 0) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) 0)

pp: case succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ ↑((finRotate (n✝ + 1).succ) i.succ) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i.succ)

Tactic:
· simp

Goal state after:
case succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ ↑((finRotate (n✝ + 1).succ) i.succ) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i.succ)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ
n : ℕ
⊢ sign (finRotate (n + 1)) = (-1) ^ (n + 1 - 1)

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero n
⊢ ↑((cycleRange 0) 0) = ↑(1 0)

pp: case inr
n : ℕ
inst✝ : NeZero n
j : Fin n
hj : 0 < j
⊢ ↑((cycleRange 0) j) = ↑(1 j)

Tactic:
· simp

Goal state after:
case inr
n : ℕ
inst✝ : NeZero n
j : Fin n
hj : 0 < j
⊢ ↑((cycleRange 0) j) = ↑(1 j)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : σ a ≠ a
⊢ σ ∈ l

Tactic:
← mem_support

Goal state after:
case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
⊢ σ ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (-1) ^ σ.cycleType.card = (-1) ^ (σ.cycleType.sum / n)

Tactic:
show σ.cycleType.sum = σ.cycleType.card * n by rw [hσ]; simp,

Goal state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (-1) ^ σ.cycleType.card = (-1) ^ (σ.cycleType.card * n / n)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
⊢ l'.prod = l.prod

Tactic:
hp,

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
⊢ l'.prod = σ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
x : α
hx : x ∈ p.support
⊢ p x ≠ x

Tactic:
← mem_support

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
x : α
hx : x ∈ p.support
⊢ x ∈ p.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
⊢ ∃ x, orderOf x = p

Tactic:
by
  have := Fintype.ofFinite G
  rw [Nat.card_eq_fintype_card] at hdvd
  exact exists_prime_orderOf_dvd_card p hdvd

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ {f : Perm α}, f ∈ cycleFactorsFinset 1 → (1 * f⁻¹).cycleFactorsFinset = cycleFactorsFinset 1 \ {f}

pp: case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ : Perm α),
    σ.IsCycle → ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}

pp: case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ τ : Perm α),
    σ.Disjoint τ →
      σ.IsCycle →
        (∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}) →
          (∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}) →
            ∀ {f : Perm α},
              f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}

Tactic:
· simp

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ : Perm α),
    σ.IsCycle → ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}

case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ τ : Perm α),
    σ.Disjoint τ →
      σ.IsCycle →
        (∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}) →
          (∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}) →
            ∀ {f : Perm α},
              f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr.h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ 3 ≤ #{g (g a)} + 1 + 1

pp: case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ g a ∉ {g (g a)}

Tactic:
· simp

Goal state after:
case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ g a ∉ {g (g a)}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : g.support = {a, g a, g (g a)}
this : #g.support = 3
⊢ [a, g a, g (g a)].Nodup

Tactic:
by grind

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg3 : g.IsThreeCycle
x : α
ha : x ∈ g.support
ha' : g.support = {x, g x, g (g x)}
ha'' : [x, g x, g (g x)].Nodup
⊢ x ≠ g x

Tactic:
by grind

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg3 : g.IsThreeCycle
x : α
ha : x ∈ g.support
ha' : g.support = {x, g x, g (g x)}
ha'' : [x, g x, g (g x)].Nodup
⊢ x ≠ g (g x)

Tactic:
by grind

Goal state after: