mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ (a✝¹.cons a✝).reverse.reverse = a✝¹.cons a✝

Tactic:
Path.reverse,

Goal state after:
case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ ((Quiver.reverse a✝).toPath.comp a✝¹.reverse).reverse = a✝¹.cons a✝
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ F_obj = G_obj

Tactic:
ext X
      apply h_obj

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
⊢ 𝟙 X ≫ f ≫ (refl X).hom = f

Tactic:
Iso.refl_hom,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
⊢ 𝟙 X ≫ f ≫ 𝟙 X = f
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
P Q : IsLimit t
⊢ P = Q

Tactic:
cases P

Goal state after:
case mk
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
Q : IsLimit t
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ { lift := lift✝, fac := fac✝, uniq := uniq✝ } = Q
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ (𝟙 a) (𝟙 a) f).hom ▷ g ≫ (𝟙 a ◁ (λ_ f).hom) ▷ g ≫ (α_ (𝟙 a) f g).hom =
    (α_ (𝟙 a ≫ 𝟙 a) f g).hom ≫ (ρ_ (𝟙 a)).hom ▷ (f ≫ g)

Tactic:
←
      comp_whiskerRight_assoc,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ ((α_ (𝟙 a) (𝟙 a) f).hom ≫ 𝟙 a ◁ (λ_ f).hom) ▷ g ≫ (α_ (𝟙 a) f g).hom =
    (α_ (𝟙 a ≫ 𝟙 a) f g).hom ≫ (ρ_ (𝟙 a)).hom ▷ (f ≫ g)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X : C
R : F.RepresentableBy X
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.obj X).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom =
      (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f

Tactic:
by
    intro X Y f
    ext x
    exact R.homEquiv_comp f.unop _

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X Y : C
f : X ⟶ Y
this : Arrow.mk (F.map f) = Arrow.mk (G.map f)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
rw [Arrow.mk_eq_mk_iff] at this

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X Y : C
f : X ⟶ Y
this : ∃ (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y), F.map f = eqToHom hX ≫ G.map f ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : sq.LiftStruct
⊢ (adj.homEquiv B X) l.l ≫ F.map p = (adj.homEquiv B Y) v

Tactic:
by rw [← Adjunction.homEquiv_naturality_right, l.fac_right]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk c.inr c.inl))

Tactic:
exact
    ⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
      ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ lift (fst f g) (snd f g) ⋯ = 𝟙 (pullback f g)

Tactic:
apply hom_ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ desc (inl f g) (inr f g) ⋯ = 𝟙 (pushout f g)

Tactic:
apply hom_ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Over X
f : (post F).obj A ⟶ (post F).obj B
⊢ ∃ a, (post F).map a = f

Tactic:
by
    obtain ⟨a, ha⟩ := F.map_surjective f.left
    exact ⟨Over.homMk a (F.map_injective (by simp [ha, dsimp% f.w])), by cat_disch⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
⊢ ∃ a, (post F).map a = f

Tactic:
obtain ⟨a, ha⟩ := F.map_surjective f.right
    exact ⟨Under.homMk a (F.map_injective (by simp [ha, dsimp% f.w])), by ext; simpa⟩

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
⊢ (proj (Functor.diag T) X).map m ≫ Z✝.hom.1 = Y✝.hom.1

Tactic:
have := congrArg (·.1) m.w

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
this : ((Functor.diag T).map m.left ≫ Z✝.hom).1 = (Y✝.hom ≫ (Functor.fromPUnit X).map m.right).1
⊢ (proj (Functor.diag T) X).map m ≫ Z✝.hom.1 = Y✝.hom.1
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero

Tactic:
exact ι

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
⊢ i.inv ≫ s.ι = t.ι

Tactic:
← w,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
⊢ i.inv ≫ i.hom ≫ t.ι = t.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝ : Category.{v, u} C
f✝ g✝ : X✝ ⟶ Y✝
X Y : C
f g : X ⟶ Y
X' Y' : C
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
⊢ (parallelPair f g).map left ≫ e₁.hom = e₀.hom ≫ (parallelPair f' g').map left

Tactic:
by simp [comm₁]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ 0 = 0

Tactic:
change f ≫ (hO.from_ Y ≫ hO.to_ Z) = hO.from_ X ≫ hO.to_ Z
    rw [← Category.assoc]
    congr
    apply hO.eq_of_tgt

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
⊢ IsColimit (F.mapCocone c)

Tactic:
have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ IsColimit (F.mapCocone c)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitEpi f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
⊢ (coconeOfIsSplitEpi f).π ≫ section_ f ≫ s.π = s.π

Tactic:
by
      dsimp
      rw [← Category.assoc, ← s.condition, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.FinCategory.Basic

Goal state before:
pp: α : Type u_1
X Y : Discrete α
⊢ Fintype (X ⟶ Y)

Tactic:
classical
  apply ULift.fintype

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
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
⊢ s.ι ≫ f = s.ι ≫ 0

Tactic:
by rw [← cancel_mono g]; simp [← hh, s.condition]

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
⊢ ι f j ≫ (isoCoproduct f).hom = ι f j ≫ desc (Sigma.ι f)

Tactic:
by simp [← Iso.eq_comp_inv]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts C
F : C ⥤ D
h : leftExactFunctor C D F
⊢ additiveFunctor C D F

Tactic:
by
    simp only [leftExactFunctor_iff] at h
    exact Functor.additive_of_preservesBinaryBiproducts F

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 Q : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
A : BinaryBicone P Q
⊢ F.map A.inl ≫ F.map A.snd = 0

Tactic:
rw [← F.map_comp, A.inl_snd, F.map_zero]

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
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j ↦ if p j then 𝟙 (f j) else 0) ≫ π f i

Tactic:
by_cases h : p i

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

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
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
h : (f ^ n) x = f x
⊢ (f ^ (n + 1)) x = x

Tactic:
by rw [pow_succ', mul_apply, h, hffx]

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

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

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:
· exact c.invEmbedding_comp _ _

Goal state after:
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
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
⊢ f.extendSubtype * σ * f.extendSubtype⁻¹ = τ

Tactic:
rw [mul_inv_eq_iff_eq_mul]

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
⊢ f.extendSubtype * σ = τ * f.extendSubtype
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ c.boundary ⟨i, hi⟩ = j

Tactic:
rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
n : ℕ
hn : n + 1 < xs.length
⊢ xs.formPerm xs[n] = xs[n + 1]

Tactic:
induction n generalizing xs with
  | zero => simpa using formPerm_apply_getElem_zero _ h _
  | succ n IH =>
    rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
    · simp at hn
    · rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]
    · specialize IH (y :: l) h.of_cons _
      · simpa [Nat.succ_lt_succ_iff] using hn
      simp only [swap_apply_eq_iff, coe_mul, formPerm_cons_cons, Function.comp]
      simp only [getElem_cons_succ] at *
      rw [← IH, swap_apply_of_ne_of_ne] <;>
      · intro hx
        rw [← hx, IH] at h
        simp [getElem_mem] at h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : f a = a
ha' : ¬a = x ∧ ¬a = y
⊢ f a = (swap x y) a

Tactic:
rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ ((x :: l).formPerm ^ n) x = (x :: l)[n % (x :: l).length]

Tactic:
by
  convert! formPerm_pow_apply_getElem _ h n 0 (Nat.succ_pos _)
  simp

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
lt : i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
induction j using Fin.induction with
  | zero => cases lt
  | succ j ih =>
    have mem : swap j.castSucc j.succ ∈ Submonoid.closure
      (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) := Submonoid.subset_closure ⟨_, rfl⟩
    obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
    · exact mem
    rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]
    exact mul_mem (mul_mem mem <| ih lts.ne lts) mem

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Tactic:
rw [hn] at hk
    rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'
    · simp [← hk', eq_comm]
    · simpa [Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.succ_lt_succ_iff] using
        (k.zero_le.trans_lt hk').ne.symm

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

Goal state before:
pp: α : 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
⊢ signAux ((e.symm.trans f).trans e) = signAux2 (x :: l) f

Tactic:
rw [signAux2]

Goal state after:
α : 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
⊢ signAux ((e.symm.trans f).trans e) = if x = f x then signAux2 l f else -signAux2 l (swap x (f x) * f)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(a * b).support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
hd

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑(a * b).support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y : ℤ
x' y' d : ℕ
hx : x.natAbs = x'
hy : y.natAbs = y'
h : x'.lcm y' = d
⊢ x.lcm y = d

Tactic:
subst_vars; rw [Int.lcm_def]

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

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
m n : ℤ
⊢ (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD ↑(#s)]

Tactic:
rw [Int.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
  simp [sub_eq_neg_add, zpow_add, eq_symm_apply, eq_comm]

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

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

Tactic:
| ofNat z =>

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

Goal state before:
pp: case refine_2
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
⊢ (∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b) → a ∈ s ∧ b ∈ s

Tactic:
rintro ⟨n, -, a, ha, rfl, rfl⟩

Goal state after:
case refine_2
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
n : ℕ
a : α
ha : a ∈ s
⊢ a ∈ s ∧ (⇑f)^[n] a ∈ s
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
z : ℤ
⊢ ((f * g).cycleOf x) (((f * g) ^ z) x) = (f.cycleOf x) (((f * g) ^ z) x)

Tactic:
cycleOf_apply_apply_zpow_self

Goal state after:
case pos
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
z : ℤ
⊢ ((f * g) ^ (z + 1)) x = (f.cycleOf x) (((f * g) ^ z) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
⊢ (f * g).cycleOf x = f.cycleOf x

Tactic:
ext y
  by_cases hxy : (f * g).SameCycle x y
  · obtain ⟨z, rfl⟩ := hxy
    rw [cycleOf_apply_apply_zpow_self]
    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
  · rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
    contrapose hxy
    obtain ⟨z, rfl⟩ := hxy
    refine ⟨z, ?_⟩
    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
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)
⊢ f ∈ ⊥

Tactic:
have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) := by
    rw [← hgf, ← Fintype.card_pi]
    exact (orderOf_map_dvd _ _).trans orderOf_dvd_card

Goal state after:
case intro
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)
⊢ f ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∈ c.support
⊢ (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Tactic:
ofSubtype_subtypePerm_of_mem hc' ha

Goal state after:
case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∈ c.support
⊢ (c ^ k) a = g a ↔ (c ^ k) a = g a
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 α
⊢ (∀ (a : α), σ a ≠ a → σ a = l.prod a) → σ ∈ l

Tactic:
intro h
      have hσl : σ.support ⊆ l.prod.support := by
        intro x hx
        rw [mem_support] at hx
        rwa [mem_support, ← h _ hx]
      obtain ⟨a, ha, -⟩ := id h3
      rw [← mem_support] at ha
      obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
      have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
      have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x := by
        intro x hx
        rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
      convert! hτ
      refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
      exact key a (mem_inter_of_mem ha hτa)

Goal state after: