mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun x ↦ count (e x) (map ⇑e ↑s)) (↑s).dedup = map (fun a ↦ count a ↑s) (↑s).dedup

Tactic:
congr

Goal state after:
case e_f
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ (fun x ↦ count (e x) (map ⇑e ↑s)) = fun a ↦ count a ↑s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ ⟨c.index ((c.embedding i) y), c.invEmbedding ((c.embedding i) y)⟩ = ⟨i, y⟩

Tactic:
congr

Goal state after:
case e_3
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.index ((c.embedding i) y) = i

case e_4
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.invEmbedding ((c.embedding i) y) ≍ y
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case refl.refl
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₁.blocksFun i₂

Tactic:
congr

Goal state after:
case refl.refl
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : ↑i₁ = ↑i₂
⊢ i₁ = i₂
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case refl
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ ⟨n, c⟩ = ⟨n, c'⟩

Tactic:
congr

Goal state after:
case refl
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ c = c'
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
⊢ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ⊆ s.finsuppAntidiag (e n)

Tactic:
by
  intro f
  simp only [mem_map, mem_finsuppAntidiag']
  rintro ⟨g, ⟨hsum, hsupp⟩, rfl⟩
  simp only [AddEquiv.toEquiv_eq_coe, mapRange.addEquiv_toEquiv, Equiv.coe_toEmbedding,
    mapRange.equiv_apply, EquivLike.coe_coe]
  constructor
  · rw [sum_mapRange_index (fun _ ↦ rfl), ← hsum, _root_.map_finsuppSum]
  · exact subset_trans (support_mapRange) hsupp

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ ↑(f.toEquivRange (e (f.toEquivRange.symm ⟨b, h⟩))) = f (e (⋯.invOfMemRange ⟨b, h⟩))

Tactic:
congr

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ (take i (map length (l.splitWrtComposition c))).sum = c.sizeUpTo i

Tactic:
congr

Goal state after:
case e_xs
α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ map length (l.splitWrtComposition c) = c.blocks
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ l
⊢ f ∈ permsOfList l

Tactic:
by
  induction l generalizing f with
  | nil =>
    simp only [not_mem_nil] at h
    exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.byContradiction <| 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
    simp
    grind
  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_flatMap]
  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 (Equiv.swap a (f a)) (Equiv.swap a (f a)), Equiv.swap_swap,
      ← Perm.one_def, one_mul]

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

Goal state before:
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)[i + 1] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
congr

Goal state after:
case cons.inr.e_i
α : 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
⊢ i + 1 = (i + 1) % (x :: xs).length
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #(f.support ∪ g.support)

Tactic:
congr

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).support = f.support ∪ g.support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case h.h.zero
α : 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
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
⊢ (x :: y :: l)[(0 + n) % (x :: y :: l).length] = (x :: y :: l).get ⟨n, hn⟩

Tactic:
congr

Goal state after:
case h.h.zero.e_i
α : 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
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
⊢ (0 + n) % (x :: y :: l).length = n
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : 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] = (x' :: y' :: l')[k + 1]

Tactic:
congr

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
| (x :: y :: l)[(k + 1 + n) % (x :: y :: l).length]

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]
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
⊢ signAux ((e.symm.trans f).trans e) = if x = f x then signAux2 l f else -signAux2 l (swap x (f x) * f)

Tactic:
rw [if_pos hfx]
      exact
        signAux_eq_signAux2 l f _ fun y (hy : f y ≠ y) =>
          List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h y hy)

Goal state after:
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
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
h✝ : f⁻¹ ((Equiv.symm f) b) = x
⊢ (Equiv.symm f) x ≠ (Equiv.symm f) b

Tactic:
simp [symm_apply_eq, eq_symm_apply] at *

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
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
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
h✝¹ : ¬f⁻¹ ((Equiv.symm f) b) = x
h✝ : f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x
⊢ x ≠ (Equiv.symm f) b

Tactic:
simp [symm_apply_eq, eq_symm_apply] at *

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)
h✝ : b = f x
⊢ ¬f x = b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
simp [symm_apply_eq, eq_symm_apply] at *

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

Goal state before:
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
this : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e
hefx : e x ≠ e (f x)
⊢ signAux ((e.symm.trans f).trans e) = if x = f x then signAux2 l f else -signAux2 l (swap x (f x) * f)

Tactic:
rw [if_neg hfx, ← signAux_eq_signAux2 _ _ e hy, this, signAux_mul, signAux_swap hefx]

Goal state after:
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
this : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e
hefx : e x ≠ e (f x)
⊢ signAux ((e.symm.trans f).trans e) = -(-1 * signAux ((e.symm.trans f).trans e))
Module: Mathlib.GroupTheory.Perm.Finite

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

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

Tactic:
· rw [hx]

Goal state after:
case neg
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
hg : ↑g.support ⊆ Set.ofPred p
x : α
hx : ¬g x = x
⊢ p (g x) ↔ p x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ (fun x ↦ signAux2 l₁ f) ≍ fun x ↦ signAux2 l₂ f

Tactic:
by
    rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
    refine Function.hfunext (forall_congr fun _ ↦ propext h.mem_iff) fun h₁ h₂ _ ↦ ?_
    rw [← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _, ← signAux_eq_signAux2 _ _ e fun _ _ => h₂ _]

Goal state after:
Module: Mathlib.Data.Nat.GCD.BigOperators

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

Tactic:
simp [Nat.coprime_mul_iff_left, *]

Goal state after:
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
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:
simp [Nat.coprime_mul_iff_left, *]

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

Goal state before:
pp: case h.right
α : 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
x : α
⊢ ∀ ⦃j : α⦄, x ≠ j → (fun x y ↦ signAux2 l (swap x y) = -1) x j

Tactic:
y

Goal state after:
case h.right
α : 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
x y : α
⊢ x ≠ y → (fun x y ↦ signAux2 l (swap x y) = -1) x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ ∀ (x : α), x ∈ (f ^ n).support ↔ x ∈ f.support

Tactic:
← Finset.ext_iff

Goal state after:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ (f ^ n).support = f.support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
| sign (f.subtypePerm h₁) = sign f

Tactic:
congr

Goal state after:
case a
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
| sign (f.subtypePerm h₁)

case a
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
| sign f
Module: Mathlib.GroupTheory.NoncommPiCoprod

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

Tactic:
by
  classical
    revert heq1
    induction s using Finset.induction_on with
    | empty => simp
    | insert i s hnotMem ih =>
      have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
      simp only [Finset.forall_mem_insert] at hmem
      have hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ (s : Set ι), K i := by
        refine Subgroup.noncommProd_mem _ _ ?_
        intro x hx
        have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
        exact this (hmem.2 x hx)
      intro heq1
      rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hnotMem] at heq1
      have hnotMem' : i ∉ (s : Set ι) := by simpa
      obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
        Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnotMem') hmem.1 hmem_bsupr heq1
      intro i h
      simp only [Finset.mem_insert] at h
      rcases h with (rfl | h)
      · exact heq1i
      · refine ih hcomm hmem.2 heq1S _ h

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 : β ≃ α
p : Perm α
g : α ≃ β
⊢ sign (f.trans (Equiv.trans p g)) = sign (g.permCongr p * f.trans g)

Tactic:
congr

Goal state after:
case e_6
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : β ≃ α
p : Perm α
g : α ≃ β
⊢ f.trans (Equiv.trans p g) = g.permCongr p * f.trans g
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)
inst✝ : DecidableEq ι
i : ι
y : N i
⊢ (noncommPiCoprod ϕ hcomm) (Pi.mulSingle i y) = (ϕ i) y

Tactic:
change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _)
    = ϕ i y

Goal state after:
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
⊢ Finset.univ.noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case right.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : sign (sumCongr 1 σb') = sign σb'
⊢ sign (sumCongr 1 (swap b₁ b₂ * σb')) = sign (swap b₁ b₂ * σb')

Tactic:
← one_mul (1 : Perm α),

Goal state after:
case right.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : sign (sumCongr 1 σb') = sign σb'
⊢ sign ((1 * 1).sumCongr (swap b₁ b₂ * σb')) = sign (swap b₁ b₂ * σb')
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : ℤˣ
σ : Perm α
⊢ σ ∈ ofSign s ↔ sign σ = s

Tactic:
ofSign,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : ℤˣ
σ : Perm α
⊢ σ ∈ {x | sign x = s} ↔ sign σ = s
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val

Tactic:
congr

Goal state after:
case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ σ.cycleFactorsFinset = s
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #(Finset.filter (Membership.mem (Function.fixedPoints ⇑σ)) Finset.univ) = #σ.supportᶜ

Tactic:
congr

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Finset.filter (Membership.mem (Function.fixedPoints ⇑σ)) Finset.univ = σ.supportᶜ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
n : ℕ
hn : n ∈ σ.cycleType
⊢ 2 ∣ n

Tactic:
by
      rw [_root_.le_antisymm
          (Nat.le_of_dvd zero_lt_two <|
            (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
          (two_le_of_mem_cycleType hn)]

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

Goal state before:
pp: case pos
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

pp: case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Tactic:
· simp [h, Equiv.Perm.decomposeFin]

Goal state after:
case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : 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 : α
hy : ((g.cycleOf x)⁻¹ * g) y ≠ y
h : y = x
⊢ False

Tactic:
rw [h, mul_apply, Ne, inv_eq_iff_eq, cycleOf_apply_self] at hy

Goal state after:
ι : 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 : α
hy : ¬g x = g x
h : y = x
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : 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
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : m = 0
⊢ g ^ m = 1 ↔ m = 0

Tactic:
simp only [hm0, pow_zero]

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

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

Tactic:
rcases lt_or_ge (castSucc j) i with h | h

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.cycleRange (i.succAbove j) = j.succ

case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.cycleRange (i.succAbove j) = j.succ
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
⊢ σ ∈ l

Tactic:
have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]

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
⊢ σ ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ ((↑v).head :: (↑v).tail.toList).prod = 1

Tactic:
← Vector.toList_cons,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ ((↑v).head ::ᵥ (↑v).tail).toList.prod = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
cycleOf_apply_of_not_sameCycle H

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : y ≠ y
H : ¬f.SameCycle x y
⊢ y = f y