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

Goal state before:
pp: n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ (swap 0 1) 0 = 1

Tactic:
simp

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

Goal state before:
pp: case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : (swap 0 1) 0 = 1
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1

Tactic:
swap_apply_of_ne_of_ne (ne_of_gt H) ha₂,

Goal state after:
case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : (swap 0 1) 0 = 1
⊢ (if a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ (swap x y).signAux = -1

Tactic:
have h2n : 2 ≤ n + 2 := by exact le_add_self

Goal state after:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ (swap x y).signAux = -1
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

Tactic:
simp

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

Goal state before:
pp: case e'_2
α : 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
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) b
⊢ ((swap x (f⁻¹ x) * f⁻¹) ^ i * swap x (f⁻¹ x)) x = ((swap x (f⁻¹ x) * f⁻¹) ^ i * f⁻¹) x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n : ℕ
⊢ (iterate f a n).length = n

Tactic:
induction n generalizing a <;> simp [*]

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n : ℕ
x✝ : 0 < n + 1
⊢ (iterate f a (n + 1))[0]? = some (f^[0] a)

Tactic:
simp

Goal state after:
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

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
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:
simp

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case zero
α : Type u_1
f : α → α
n : ℕ
a : α
⊢ iterate f a (0 + n) = iterate f a 0 ++ iterate f (f^[0] a) n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Pairwise.List

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Prop
l : List α
inst✝ : Std.Symm r
hl : [].Nodup
⊢ {a | a ∈ []}.Pairwise r ↔ Pairwise r []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n✝ n : ℕ
ih : ∀ (a : α), iterate f a (n + n✝) = iterate f a n ++ iterate f (f^[n] a) n✝
a : α
⊢ a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n✝) = a :: iterate f (f a) n ++ iterate f (f^[n + 1] a) n✝

Tactic:
Nat.iterate,

Goal state after:
case succ
α : Type u_1
f : α → α
n✝ n : ℕ
ih : ∀ (a : α), iterate f a (n + n✝) = iterate f a n ++ iterate f (f^[n] a) n✝
a : α
⊢ a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n✝) = a :: iterate f (f a) n ++ iterate f (f^[n] (f a)) n✝
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g

Tactic:
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ (List.map (⇑sign) l).length = l.length

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f))

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → f x ≠ x → β
h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y
⊢ ∀ (x : α), f (f x) ≠ f x ↔ f x ≠ x

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → f x ≠ x → β
h : ∀ (x : α) (hx : f x ≠ x) (hx' : f (f x) ≠ f x), i (f x) hx' = g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ ≠ x₁) (hx₂ : f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), g y ≠ y → ∃ x, ∃ (hx : f x ≠ x), i x hx = y
⊢ ∀ (x : β), g (g x) ≠ g x ↔ g x ≠ x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case empty
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
comm : (↑∅).Pairwise (Function.onFun Commute f)
hmem : ∀ x ∈ ∅, f x ∈ K x
⊢ ∅.noncommProd f comm = 1 → ∀ i ∈ ∅, f i = 1

Tactic:
simp

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

Goal state before:
pp: n : ℤ
x✝ : (Equiv.addLeft 1) n ≠ n
⊢ (Equiv.addLeft 1 ^ n) 0 = n

Tactic:
simp

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

Goal state before:
pp: n : ℤ
x✝ : (Equiv.addRight 1) n ≠ n
⊢ (Equiv.addRight 1 ^ n) 0 = n

Tactic:
simp

Goal state after:
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)

Tactic:
simp

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

Goal state before:
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:
simp

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
⊢ a ∈ {a, b}

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝ : DecidableEq α
hab : a ≠ b
⊢ b ∈ {a, b}

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
y : β
hy : σ y ≠ y
⊢ (a, y).2 = y

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: 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)
⊢ ∀ x ∈ Finset.univ, (ϕ x) (1 x) = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
e : α ≃ β
p : Perm α
⊢ ∀ (x : β), e.symm ((e.permCongr p) x) = p (e.symm x)

Tactic:
simp

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

Goal state before:
pp: case e_6
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : β ≃ α
p : Perm α
g : α ≃ β
x✝ : β
⊢ (f.trans (Equiv.trans p g)) x✝ = (g.permCongr p * f.trans g) x✝

Tactic:
simp

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

Goal state before:
pp: case left.one
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σb : Perm β
⊢ sign (sumCongr 1 1) = sign 1

Tactic:
simp

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

Goal state before:
pp: case right.one
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
⊢ sign (sumCongr 1 1) = sign 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
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)
inst✝ : DecidableEq ι
i : ι
y : N i
⊢ ∀ x ∈ Finset.univ.erase i, (ϕ x) (Pi.mulSingle i y x) = 1

Tactic:
intro j

Goal state after:
case h
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)
inst✝ : DecidableEq ι
i : ι
y : N i
j : ι
⊢ j ∈ Finset.univ.erase i → (ϕ j) (Pi.mulSingle i y j) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
s : Set α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
h : g.IsCycleOn s
⊢ ∀ ⦃x : β⦄, x ∈ Subtype.val ∘ ⇑f '' s → ∀ ⦃y : β⦄, y ∈ Subtype.val ∘ ⇑f '' s → (g.extendDomain f).SameCycle x y

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
    exact (h.2 ha hb).extendDomain

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a.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 ι := ⋯
f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ (ϕ i) (f i) ∈ (fun i ↦ mrange (ϕ i)) i

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ↑s = {a | a ∈ s.toList}

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ s = {a | a ∈ hs'.toFinset.toList}

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
this✝ : Countable ↑s
this : Infinite ↑s
f : ℤ ≃ ↑s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ Subtype.val '' ⇑f.symm ⁻¹' {x | (Equiv.addRight 1) x ≠ x}

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a.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 ι := ⋯
f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ (ϕ i) (f i) ∈ (fun i ↦ (ϕ i).range) i

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: 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)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ (noncommPiCoprod ϕ hcomm).ker
⊢ ∀ x ∈ Finset.univ, (ϕ x) (f x) ∈ (ϕ x).range

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : f x = x
⊢ f.cycleOf x = if f x = x then 1 else f

Tactic:
if_pos hx,

Goal state after:
case pos
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : f x = x
⊢ f.cycleOf x = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ ¬f x = x

Tactic:
← cycleOf_eq_one_iff f

Goal state after:
α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : (f.cycleOf x).IsCycle
⊢ ¬f.cycleOf x = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
⊢ (τ * 1 * τ⁻¹).cycleType = cycleType 1

Tactic:
simp

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

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (cycleType 1).sum = #(support 1)

Tactic:
simp

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

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ sign 1 = (Multiset.map (fun n ↦ -(-1) ^ n) (cycleType 1)).prod

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (f.cycleOf x).support = ∅ ↔ x ∉ f.support

Tactic:
simp

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

Goal state before:
pp: case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (cycleType 1).lcm = orderOf 1

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Tactic:
rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ ∀ (a : ι) (b : a ≠ i), (Fintype.card (H ↑⟨a, b⟩)).Coprime (Fintype.card (H i))

Tactic:
intro j

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
j : ι
⊢ ∀ (b : j ≠ i), (Fintype.card (H ↑⟨j, b⟩)).Coprime (Fintype.card (H i))
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k + 1 < #(f.cycleOf x).support
hk' : (f ^ (k + 1)) x = y
⊢ 0 < k + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∉ f.support
⊢ 1 ≤ #(f.cycleOf x).support + 1

Tactic:
simp

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)

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
by
  by_cases hx : x ∈ f.support
  · obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
    rcases k with - | k
    · refine ⟨#(f.cycleOf x).support, hk, self_le_add_right _ _, ?_⟩
      simp only [pow_zero, coe_one, id_eq] at hk'
      subst hk'
      rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]
    · exact ⟨k + 1, by simp, Nat.le_succ_of_le hk.le, hk'⟩
  · refine ⟨1, zero_lt_one, by simp, ?_⟩
    obtain ⟨k, rfl⟩ := h
    rw [notMem_support] at hx
    rw [pow_apply_eq_self_of_apply_eq_self hx, zpow_apply_eq_self_of_apply_eq_self hx]

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

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
hs : (↑∅).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑∅).Pairwise fun i j ↦ Commute (k i) (k j)
⊢ (∅.noncommProd k hs').cycleType = ∑ i ∈ ∅, (k i).cycleType

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : σ (some x) = some val✝
hn : σ (some x) ≠ none
⊢ some x ≠ none

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ (fun i ↦ swap none i.1 * optionCongr i.2) ((fun σ ↦ (σ none, removeNone σ)) σ) = σ

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := ⋯
r : ℤ := ⋯
⊢ 0 < 2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
e : Perm α
i : Option α
⊢ (decomposeOption.symm (none, e)) i = Option.map (⇑e) i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ sign (decomposeOption.symm (none, e)) = sign e

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
div_euc : r + ↑(orderOf g) * q = n ∧ 0 ≤ r ∧ r < ↑(orderOf g)
m : ℕ
hm : r = ↑m
⊢ (g ^ n) x = x ↔ r = 0

Tactic:
simp only [hm, Nat.cast_nonneg, Nat.cast_lt, true_and] at div_euc

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ n) x = x ↔ r = 0
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)

Tactic:
simp

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

Goal state before:
pp: case insert
α : 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)
⊢ ∀ i_1 ∈ s, (k i).Disjoint (k i_1)

Tactic:
intro j

Goal state after:
case insert
α : 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 : ι
⊢ j ∈ s → (k i).Disjoint (k j)
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)

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ sign (finRotate 0) = (-1) ^ (0 - 1)

Tactic:
simp

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

Goal state before:
pp: case succ.zero
⊢ sign (finRotate (0 + 1)) = (-1) ^ (0 + 1 - 1)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
a✝ : Fin (n + 2)
⊢ a✝ ∈ (finRotate (n + 2)).support ↔ a✝ ∈ Finset.univ

Tactic:
simp

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

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : (σ * π).cycleType = τ.cycleType
⊢ IsConj (σ * π) τ

Tactic:
hd.cycleType_mul

Goal state after:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
⊢ IsConj (σ * π) τ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
⊢ (finRotate (n + 2)) 0 ≠ 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
⊢ i ∈ Set.range ⇑(castLEEmb ⋯)

Tactic:
simp

Goal state after:
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
⊢ i ≤ j
Module: Mathlib.Data.FunLike.Module

Goal state before:
pp: M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst✝⁷ : SMul M β
inst✝⁶ : SMul M' β
inst✝⁵ : SMul M F
inst✝⁴ : SMul M' F
inst✝³ : IsSMulApply M F α β
inst✝² : IsSMulApply M' F α β
inst✝¹ : SMul M M'
inst✝ : IsScalarTower M M' β
x✝² : M
x✝¹ : M'
x✝ : F
⊢ ∀ (x : α), ((x✝² • x✝¹) • x✝) x = (x✝² • x✝¹ • x✝) x

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : ¬i = j
hj1 : ↑(i + 1) = ↑i + 1
⊢ ↑(i.castLT ⋯) + 1 < ↑j + 1

Tactic:
simp

Goal state after:
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : ¬i = j
hj1 : ↑(i + 1) = ↑i + 1
⊢ i < j
Module: Mathlib.GroupTheory.Perm.Fin

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

Tactic:
simp

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i.cycleRange ((Equiv.symm i.cycleRange) 0) = i.cycleRange i

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.cycleRange ((Equiv.symm i.cycleRange) j.succ) = i.cycleRange (i.succAbove j)

Tactic:
simp

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

Tactic:
simp

Goal state after: