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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝ : b = f (f x)
⊢ ¬x = b

pp: case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝¹ : ¬b = f (f x)
h✝ : b = f x
⊢ ¬f x = b

pp: case neg
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝¹ : ¬b = f (f x)
h✝ : ¬b = f x
⊢ ¬b = f b

Tactic:
<;>

Goal state after:
case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝ : b = f (f x)
⊢ ¬x = b

case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝¹ : ¬b = f (f x)
h✝ : b = f x
⊢ ¬f x = b

case neg
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : ¬(swap x (f x)) (f b) = b
hfxb : ¬f x = b
hfb : ¬f b = b
hbx : ¬b = x
h : f x = (f ^ (n + 1)) b
h✝¹ : ¬b = f (f x)
h✝ : ¬b = f x
⊢ ¬b = f b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ (Equiv.symm f ^ n) ((Equiv.symm f) x) = (Equiv.symm f) b

Tactic:
rw [← mul_apply, ← pow_succ]; simpa [pow_succ', eq_symm_apply] using! h

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

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝ : f (e.symm x✝) = x
⊢ ↑(e (f x)) = ↑(e (f x))

pp: case pos
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝¹ : ¬f (e.symm x✝) = x
h✝ : e.symm x✝ = x
⊢ ↑(e x) = ↑(e x)

pp: case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝¹ : ¬f (e.symm x✝) = x
h✝ : ¬e.symm x✝ = x
⊢ ↑(e (f (e.symm x✝))) = ↑(e (f (e.symm x✝)))

Tactic:
<;>

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝ : f (e.symm x✝) = x
⊢ ↑(e (f x)) = ↑(e (f x))

case pos
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝¹ : ¬f (e.symm x✝) = x
h✝ : e.symm x✝ = x
⊢ ↑(e x) = ↑(e x)

case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝¹ : ¬f (e.symm x✝) = x
h✝ : ¬e.symm x✝ = x
⊢ ↑(e (f (e.symm x✝))) = ↑(e (f (e.symm x✝)))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case neg.refine_1
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
hg : ↑g.support ⊆ Set.ofPred p
x : α
hx : ¬g x = x
⊢ g x ∈ ↑g.support

pp: case neg.refine_2
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
hg : ↑g.support ⊆ Set.ofPred p
x : α
hx : ¬g x = x
⊢ x ∈ ↑g.support

Tactic:
<;>

Goal state after:
case neg.refine_1
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
hg : ↑g.support ⊆ Set.ofPred p
x : α
hx : ¬g x = x
⊢ g x ∈ ↑g.support

case neg.refine_2
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
hg : ↑g.support ⊆ Set.ofPred p
x : α
hx : ¬g x = x
⊢ x ∈ ↑g.support
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case zero
α : Type u_1
f : α → α
a : α
⊢ (iterate f a 0).length = 0

pp: case succ
α : Type u_1
f : α → α
n✝ : ℕ
a✝ : ∀ (a : α), (iterate f a n✝).length = n✝
a : α
⊢ (iterate f a (n✝ + 1)).length = n✝ + 1

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
f : α → α
a : α
⊢ (iterate f a 0).length = 0

case succ
α : Type u_1
f : α → α
n✝ : ℕ
a✝ : ∀ (a : α), (iterate f a n✝).length = n✝
a : α
⊢ (iterate f a (n✝ + 1)).length = n✝ + 1
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case hl
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ (map (fun x ↦ f^[x] a) (range n)).length = (iterate f a n).length

pp: case h
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ ∀ (i : ℕ) (h₁ : i < (map (fun x ↦ f^[x] a) (range n)).length) (h₂ : i < (iterate f a n).length),
    (map (fun x ↦ f^[x] a) (range n))[i] = (iterate f a n)[i]

Tactic:
<;>

Goal state after:
case hl
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ (map (fun x ↦ f^[x] a) (range n)).length = (iterate f a n).length

case h
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ ∀ (i : ℕ) (h₁ : i < (map (fun x ↦ f^[x] a) (range n)).length) (h₂ : i < (iterate f a n).length),
    (map (fun x ↦ f^[x] a) (range n))[i] = (iterate f a n)[i]
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: case nil
k : ℕ
⊢ [].prod.Coprime k ↔ ∀ n ∈ [], n.Coprime k

pp: case cons
k head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : tail✝.prod.Coprime k ↔ ∀ n ∈ tail✝, n.Coprime k
⊢ (head✝ :: tail✝).prod.Coprime k ↔ ∀ n ∈ head✝ :: tail✝, n.Coprime k

Tactic:
<;>

Goal state after:
case nil
k : ℕ
⊢ [].prod.Coprime k ↔ ∀ n ∈ [], n.Coprime k

case cons
k head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : tail✝.prod.Coprime k ↔ ∀ n ∈ tail✝, n.Coprime k
⊢ (head✝ :: tail✝).prod.Coprime k ↔ ∀ n ∈ head✝ :: tail✝, n.Coprime k
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
⊢ False

Tactic:
by
        have : ∀ f, IsSwap f → s f = 1 := fun f ⟨a, b, hab, hab'⟩ => by
          rw [← isConj_iff_eq, ← Or.resolve_right (Int.units_eq_one_or _) h, hab']
          exact s.map_isConj (isConj_swap hab hxy)
        let ⟨g, hg⟩ := hs (-1)
        let ⟨l, hl⟩ := (truncSwapFactors g).out
        have : ∀ a ∈ l.map s, a = (1 : ℤˣ) := fun a ha =>
          let ⟨g, hg⟩ := List.mem_map.1 ha
          hg.2 ▸ this _ (hl.2 _ hg.1)
        have : s l.prod = 1 := by
          rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
        rw [hl.1, hg] at this
        exact absurd this (by simp_all)

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

Goal state before:
pp: case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)

pp: case cons.inr
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)

Tactic:
<;>

Goal state after:
case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)

case cons.inr
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
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 : ¬¬orderOf f ∣ n
⊢ f ^ n = 1

Tactic:
Classical.not_not

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 : orderOf f ∣ n
⊢ f ^ n = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case e'_3
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑(Equiv.symm g) ⁻¹' s
y : α
hy : y ∈ ⇑(Equiv.symm g) ⁻¹' s
⊢ x = g ((Equiv.symm g) x)

pp: case e'_4
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑(Equiv.symm g) ⁻¹' s
y : α
hy : y ∈ ⇑(Equiv.symm g) ⁻¹' s
⊢ y = g ((Equiv.symm g) y)

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑(Equiv.symm g) ⁻¹' s
y : α
hy : y ∈ ⇑(Equiv.symm g) ⁻¹' s
⊢ x = g ((Equiv.symm g) x)

case e'_4
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑(Equiv.symm g) ⁻¹' s
y : α
hy : y ∈ ⇑(Equiv.symm g) ⁻¹' s
⊢ y = g ((Equiv.symm g) y)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl
α : Type u_2
b : α
inst✝ : DecidableEq α
x y : α
hab : x ≠ b
hy : y = x ∨ y = b
⊢ (swap x b).SameCycle x y

pp: case inr
α : Type u_2
a : α
inst✝ : DecidableEq α
x y : α
hab : a ≠ x
hy : y = a ∨ y = x
⊢ (swap a x).SameCycle x y

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
b : α
inst✝ : DecidableEq α
x y : α
hab : x ≠ b
hy : y = x ∨ y = b
⊢ (swap x b).SameCycle x y

case inr
α : Type u_2
a : α
inst✝ : DecidableEq α
x y : α
hab : a ≠ x
hy : y = a ∨ y = x
⊢ (swap a x).SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ {x | (f.subtypePerm ⋯) x ≠ x} = _root_.Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ ∀ (x : { x // x ∈ s }), x ∈ {x | (f.subtypePerm ⋯) x ≠ x}
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ x.gcd y ∣ d

Tactic:
rw [← Int.natCast_dvd_natCast, ← h₃]

Goal state after:
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(x.gcd y) ∣ x * a + y * b
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
⊢ mrange (noncommPiCoprod ϕ hcomm) ≤ ⨆ i, mrange (ϕ i)

Tactic:
rintro x ⟨f, rfl⟩

Goal state after:
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → N i
⊢ (noncommPiCoprod ϕ hcomm) f ∈ ⨆ i, mrange (ϕ i)
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
⊢ (noncommPiCoprod ϕ hcomm).range ≤ ⨆ i, (ϕ i).range

Tactic:
rintro x ⟨f, rfl⟩

Goal state after:
case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := Classical.decEq ι
f : (i : ι) → H i
⊢ (noncommPiCoprod ϕ hcomm) f ∈ ⨆ i, (ϕ i).range
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : f⁻¹.SameCycle x y
h✝ : f.SameCycle x (f⁻¹ y)
⊢ y = f (f⁻¹ y)

pp: case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : f⁻¹.SameCycle x y
h✝ : ¬f.SameCycle x (f⁻¹ y)
⊢ y = f⁻¹ y

pp: case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : ¬f⁻¹.SameCycle x y
h✝ : f.SameCycle x y
⊢ y = f y

pp: case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : ¬f⁻¹.SameCycle x y
h✝ : ¬f.SameCycle x y
⊢ y = y

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : f⁻¹.SameCycle x y
h✝ : f.SameCycle x (f⁻¹ y)
⊢ y = f (f⁻¹ y)

case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : f⁻¹.SameCycle x y
h✝ : ¬f.SameCycle x (f⁻¹ y)
⊢ y = f⁻¹ y

case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : ¬f⁻¹.SameCycle x y
h✝ : f.SameCycle x y
⊢ y = f y

case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : ¬f⁻¹.SameCycle x y
h✝ : ¬f.SameCycle x y
⊢ y = y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case succ
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ (f.cycleOf x ^ (n + 1)) x = (f ^ (n + 1)) x

Tactic:
rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]
    exact ⟨n, rfl⟩

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

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
⊢ y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support

Tactic:
rw [mem_support, cycleOf_apply]
    split_ifs with hy
    · simp only [hx, hy, Ne, not_false_iff, and_self_iff, mem_support]
      rcases hy with ⟨k, rfl⟩
      rw [← notMem_support]
      simpa using hx
    · simpa [hx] using hy

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
hy : i = y
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
hy : ¬i = y
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
hy : i = y
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝

case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
hy : ¬i = y
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case refine_1
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ sign (decomposeFin.symm (0, e)) = (if 0 = 0 then 1 else -1) * sign e

pp: case refine_2
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ∀ (i : Fin n), sign (decomposeFin.symm (i.succ, e)) = (if i.succ = 0 then 1 else -1) * sign e

Tactic:
<;>

Goal state after:
case refine_1
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ sign (decomposeFin.symm (0, e)) = (if 0 = 0 then 1 else -1) * sign e

case refine_2
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ∀ (i : Fin n), sign (decomposeFin.symm (i.succ, e)) = (if i.succ = 0 then 1 else -1) * sign e
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ i ∈ ↑(insert i s)

pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ j ∈ ↑(insert i s)

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ i ∈ ↑(insert i s)

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ j ∈ ↑(insert i s)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝¹ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
h : g y = y
h✝ : g.SameCycle x y
hy : ¬y = g y
⊢ False

pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝¹ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
h : g y = y
h✝ : ¬g.SameCycle x y
hy : ¬y = y
⊢ False

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝¹ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
h : g y = y
h✝ : g.SameCycle x y
hy : ¬y = g y
⊢ False

case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝¹ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
h : g y = y
h✝ : ¬g.SameCycle x y
hy : ¬y = y
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : IsConj σ τ
⊢ σ.cycleType = τ.cycleType

Tactic:
by
    obtain ⟨π, rfl⟩ := isConj_iff.1 h
    rw [cycleType_conj]

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

Goal state before:
pp: case zero
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
⊢ p.insertNth a x ((Equiv.symm p.cycleRange) 0) = cons a x 0

pp: case succ
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
i✝ : Fin n
⊢ p.insertNth a x ((Equiv.symm p.cycleRange) i✝.succ) = cons a x i✝.succ

Tactic:
<;>

Goal state after:
case zero
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
⊢ p.insertNth a x ((Equiv.symm p.cycleRange) 0) = cons a x 0

case succ
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
i✝ : Fin n
⊢ p.insertNth a x ((Equiv.symm p.cycleRange) i✝.succ) = cons a x i✝.succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case x
n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p : Fin (n + 1)
⊢ cons (x p) (p.removeNth x) 0 = (x ∘ ⇑(Equiv.symm p.cycleRange)) 0

pp: case p
n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p : Fin (n + 1)
i✝ : Fin n
⊢ cons (x p) (p.removeNth x) i✝.succ = (x ∘ ⇑(Equiv.symm p.cycleRange)) i✝.succ

Tactic:
<;>

Goal state after:
case x
n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p : Fin (n + 1)
⊢ cons (x p) (p.removeNth x) 0 = (x ∘ ⇑(Equiv.symm p.cycleRange)) 0

case p
n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p : Fin (n + 1)
i✝ : Fin n
⊢ cons (x p) (p.removeNth x) i✝.succ = (x ∘ ⇑(Equiv.symm p.cycleRange)) i✝.succ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ ↑((j - i).castLT ⋯) < ↑(subNat (↑i) (Fin.cast ⋯ k) ⋯)

Tactic:
simp [sub_val_of_le hij]

Goal state after:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ ↑j - ↑i < ↑k - ↑i
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) ^ ((Fintype.card α - (Fintype.card α - σ.cycleType.sum)) / n)

Tactic:
Nat.sub_sub_self σ.sum_cycleType_le,

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.sum / n)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : k = j
⊢ ↑(subNat (↑i) (Fin.cast ⋯ j) ⋯) = ↑((j - i).castLT ⋯)

Tactic:
simp [sub_val_of_le hij]

Goal state after: