mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
s : KernelFork f
hs : IsLimit s
s' : KernelFork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : e.hom ≫ Fork.ι s' = Fork.ι s ≫ eX.hom
α : parallelPair f 0 ≅ parallelPair f' 0 := parallelPairIsoMk eX eY ⋯ ⋯
⊢ ∀ (j : WalkingParallelPair), ((Cone.postcompose α.hom).obj s).π.app j = e.hom ≫ s'.π.app j

Tactic:
rintro (_ | _) <;> simp [α, ← H']

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0
inst✝ : HasCokernel f
⊢ colimit.ι (parallelPair f 0) zero ≫ cokernel.desc f g h = 0

Tactic:
rw [(colimit.w (parallelPair f 0) WalkingParallelPairHom.left).symm]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0
inst✝ : HasCokernel f
⊢ ((parallelPair f 0).map WalkingParallelPairHom.left ≫ colimit.ι (parallelPair f 0) one) ≫ cokernel.desc f g h = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasCokernel f✝
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
⊢ parallelPair f 0 ≅ parallelPair g 0

Tactic:
simp [h]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasCokernel f✝
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
⊢ parallelPair g 0 ≅ parallelPair g 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasCokernel f✝
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
⊢ parallelPair f 0 ≅ parallelPair g 0

Tactic:
simp [h]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasCokernel f✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
e : Y ⟶ Z
he : g ≫ e = 0
⊢ f ≫ e = 0

Tactic:
by simp [h, he]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
h : j ≠ j'
⊢ ι f j ≫ π f j' = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
s : CokernelCofork f
hs : IsColimit s
s' : CokernelCofork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : eY.hom ≫ Cofork.π s' = Cofork.π s ≫ e.hom
α : parallelPair f 0 ≅ parallelPair f' 0 := parallelPairIsoMk eX eY ⋯ ⋯
⊢ ∀ (j : WalkingParallelPair), ((Cocone.precompose α.symm.hom).obj s).ι.app j ≫ e.hom = s'.ι.app j

Tactic:
rintro (_ | _) <;> simp [α, ← H']

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
j j' : WalkingPair
⊢ WalkingPair.casesOn j b.inl b.inr ≫ WalkingPair.casesOn j' b.fst b.snd = if h : j = j' then eqToHom ⋯ else 0

Tactic:
rcases j with ⟨⟩ <;> rcases j' with ⟨⟩

Goal state after:
case left.left
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
⊢ WalkingPair.casesOn WalkingPair.left b.inl b.inr ≫ WalkingPair.casesOn WalkingPair.left b.fst b.snd =
    if h : WalkingPair.left = WalkingPair.left then eqToHom ⋯ else 0

case left.right
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
⊢ WalkingPair.casesOn WalkingPair.left b.inl b.inr ≫ WalkingPair.casesOn WalkingPair.right b.fst b.snd =
    if h : WalkingPair.left = WalkingPair.right then eqToHom ⋯ else 0

case right.left
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
⊢ WalkingPair.casesOn WalkingPair.right b.inl b.inr ≫ WalkingPair.casesOn WalkingPair.left b.fst b.snd =
    if h : WalkingPair.right = WalkingPair.left then eqToHom ⋯ else 0

case right.right
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P P' Q Q' X Y : C
b : BinaryBicone X Y
⊢ WalkingPair.casesOn WalkingPair.right b.inl b.inr ≫ WalkingPair.casesOn WalkingPair.right b.fst b.snd =
    if h : WalkingPair.right = WalkingPair.right then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
h : p i
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j ↦ if p j then 𝟙 (f j) else 0) ≫ π f i

Tactic:
simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
h : ¬p i
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j ↦ if p j then 𝟙 (f j) else 0) ≫ π f i

Tactic:
simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
b b' : β
h : ¬b' = b
⊢ ε b' ≠ ε b

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
⊢ StrictMono (cons 0 f) ↔ f = succ

Tactic:
refine ⟨fun h ↦ funext fun i ↦ ?_, fun h ↦ by simp [h, strictMono_id]⟩

Goal state after:
n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
⊢ f i = i.succ
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ ↑j - c.sizeUpTo ↑(c.index j) < c.blocksFun (c.index j)

Tactic:
tsub_lt_iff_right,

Goal state after:
n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < c.blocksFun (c.index j) + c.sizeUpTo ↑(c.index j)

n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Fintype τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
nz : 𝟙 (S s) ≠ 0
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)

Tactic:
apply truncSigmaOfExists
    have t := Biproduct.column_nonzero_of_iso'.{v} s f
    by_contra h
    simp only [not_exists_not] at h
    exact nz (t h)

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

Goal state before:
pp: case e_4.h
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ c.blocksFun (c.index ((c.embedding i) y)) = c.blocksFun i

Tactic:
rw [c.index_embedding]

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

Goal state before:
pp: n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
⊢ ∀ {i : ℕ}, i ∈ [n] → 0 < i

Tactic:
simp [h]

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

Goal state before:
pp: β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), σ ↑a = ↑((Finset.equivOfCardEq h) a)
⊢ t.card ≤ (Finset.map (Equiv.toEmbedding σ) s).card

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l ++ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l).Nodup

Tactic:
List.nodup_append',

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Nodup ∧
    (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l).Nodup ∧
      (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ #{x | σ x = x} < Fintype.card α - 1

Tactic:
rw [Nat.lt_sub_iff_add_lt, ← Nat.lt_sub_iff_add_lt', ← Finset.card_compl, Finset.compl_filter]
  exact one_lt_card_support_of_ne_one h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ (l.rotate 1)[(k + 1) % (l.rotate 1).length] = l.formPerm (l.rotate 1)[k]

Tactic:
getElem_rotate l,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ l[((k + 1) % (l.rotate 1).length + 1) % l.length] = l.formPerm (l.rotate 1)[k]
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ l[((k + 1) % (l.rotate 1).length + 1) % l.length] = l.formPerm (l.rotate 1)[k]

Tactic:
getElem_rotate l,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ l[((k + 1) % (l.rotate 1).length + 1) % l.length] = l.formPerm l[(k + 1) % l.length]
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
⊢ ↑((((setCongr hd1').trans (Set.union hd1'')).trans
          (((subtypeEquiv f ⋯).sumCongr (subtypeEquiv g ⋯)).trans ((setCongr hd2').trans (Set.union hd2'')).symm))
        ⟨(σ * τ) x, ⋯⟩) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((((setCongr hd1').trans (Set.union hd1'')).trans
            (((subtypeEquiv f ⋯).sumCongr (subtypeEquiv g ⋯)).trans ((setCongr hd2').trans (Set.union hd2'')).symm))
          ⟨x, hx⟩)

Tactic:
simp only [trans_apply, symm_trans_apply, Equiv.setCongr_apply, Equiv.setCongr_symm_apply,
    Equiv.sumCongr_apply]

Goal state after:
case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩ ∈ finPairsLT n
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

Tactic:
mem_finPairsLT

Goal state after:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
x y : α
⊢ SameCycle 1 x y ↔ x = y

Tactic:
simp [SameCycle]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ (∃ b, (f⁻¹ ^ (Equiv.symm (Equiv.neg ℤ)) b) x = y) ↔ f.SameCycle x y

Tactic:
simp [SameCycle]

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

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
mem_finPairsLT

Goal state after:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : tl = []
⊢ (hd :: tl).formPerm = 1

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
⊢ g ∈ ofSubtype.range ↔ ↑g.support ⊆ Set.ofPred p

Tactic:
constructor
  · rintro ⟨k, rfl⟩ x
    simp only [Finset.mem_coe, mem_support_ofSubtype, Set.mem_ofPred_eq]
    exact fun ⟨hx, _⟩ ↦ hx
  · intro hg
    refine ⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩
    by_cases hx : g x = x
    · rw [hx]
    · refine iff_of_true (hg ?_) (hg ?_) <;> simpa

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ sign (Equiv.trans f g) = sign g * sign f

Tactic:
by
  rw [← mul_def, sign_mul]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ |↑(sign f)| = 1

Tactic:
Int.abs_eq_natAbs,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ↑(↑(sign f)).natAbs = 1
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
h1 : f (f x) = x
⊢ Equiv.trans (swap x (f x)) (swap x (f x)) = Equiv.refl α

Tactic:
swap_swap

Goal state after:
α : 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
h1 : f (f x) = x
⊢ Equiv.refl α = Equiv.refl α
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = 1
⊢ sign 1 = a

Tactic:
simp [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 : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
⊢ ∀ (x : β), g x = ((e.symm.trans f).trans e) x

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
x : β
hx : f x ≠ x
⊢ (f ^ a) x = (f ^ b) x

Tactic:
simp [h]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

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

Tactic:
Finset.noncommProd_insert_of_notMem _ _ _ _ hnotMem

Goal state after:
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i * s.noncommProd f ⋯ = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1
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]

Goal state after:
case neg
α : Type u_2
f : Perm α
x y : α
inst✝² : DecidableRel f.SameCycle
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hx : ¬f x = x
⊢ (if f.SameCycle x y then f y else y) ≠ y ↔ f.SameCycle x y ∧ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : f.cycleOf x = 1
⊢ #(f.cycleOf x).support < 2

Tactic:
simp [h]

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✝
⊢ σ (some x) ≠ none

Tactic:
simp [h]

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)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ (g ^ ↑m * g ^ (↑(orderOf g) * q)) x = x ↔ r = 0

Tactic:
simp only [hm, Nat.cast_eq_zero, zpow_natCast, coe_mul, comp_apply, zpow_mul,
    pow_orderOf_eq_one, one_zpow, coe_one, id_eq]

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 ^ m) x = x ↔ m = 0
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case pos
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : i = Fin.last n✝
⊢ 0 = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Tactic:
simp [h]

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

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

Tactic:
cases j using Fin.cases <;> simp

Goal state after:
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
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ → l'.toFinset = l.toFinset

Tactic:
rintro ⟨hc, hd, hp⟩
    refine List.toFinset_eq_of_perm _ _ ?_
    refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd
    rw [hp, hp']

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
h : sign σ = σ.signAux
⊢ (∏ x ∈ finPairsLT n, if σ x.fst ≤ σ x.snd then -1 else 1) =
    ∏ x ∈ Finset.univ.sigma Finset.Iio, if σ x.snd < σ x.fst then 1 else -1

Tactic:
convert! rfl using 2 with x hx

Goal state after:
case e'_3.h
n : ℕ
σ : Perm (Fin n)
h : sign σ = σ.signAux
⊢ Finset.univ.sigma Finset.Iio = finPairsLT n

case e'_3.a
n : ℕ
σ : Perm (Fin n)
h : sign σ = σ.signAux
x : (_ : Fin n) × Fin n
hx : x ∈ finPairsLT n
⊢ (if σ x.snd < σ x.fst then 1 else -1) = if σ x.fst ≤ σ x.snd then -1 else 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ j, ∏ i < j, f (σ i) (σ j) = ↑↑(sign σ) * ∏ j, ∏ i < j, f i j

Tactic:
← σ.sign_inv,

Goal state after:
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ j, ∏ i < j, f (σ i) (σ j) = ↑↑(sign σ⁻¹) * ∏ j, ∏ i < j, f i j
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val✝ : Fintype β
this : ∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
x : { l // l.prod = σ ∧ (∀ g ∈ l, g.IsCycle) ∧ List.Pairwise Disjoint l } := σ.truncCycleFactors.out
⊢ P σ

Tactic:
exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)

Goal state after:
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 : a ∈ g.support
⊢ #g.support ≤ #{a, g a, g (g a)}

Tactic:
rw [hg3.card_support]

Goal state after:
case mpr.h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ 3 ≤ #{a, g a, g (g a)}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ ¬(a = g a ∨ a = g (g a))

Tactic:
contrapose ha

Goal state after:
case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a = g a ∨ a = g (g a)
⊢ g a = a