mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : g = adj.unit.app A ≫ G.map f
⊢ F.map g ≫ adj.counit.app B = f

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ { pt := s.pt, π := h.homEquiv (h.homEquiv.symm s.π) } = s

Tactic:
match s with
  | .mk s_pt s_π =>
    congr
    exact h.homEquiv.apply_symm_apply s_π

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
Y : Cᵒᵖ
G : Cᵒᵖ ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : yoneda.obj (unop X) ⟶ F
⊢ ((ConcreteCategory.hom ((yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun a).down =
    ((ConcreteCategory.hom ((yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f)).toFun a).down

Tactic:
dsimp [yonedaEvaluation, yonedaEquiv]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
Y : Cᵒᵖ
G : Cᵒᵖ ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : yoneda.obj (unop X) ⟶ F
⊢ (ConcreteCategory.hom (f.2.app Y)) ((ConcreteCategory.hom (a.app Y)) (𝟙 (unop Y) ≫ f.1.unop)) =
    (ConcreteCategory.hom (f.2.app Y))
      ((ConcreteCategory.hom (F.map f.1)) ((ConcreteCategory.hom (a.app X)) (𝟙 (unop X))))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).map f ≫ yonedaEquiv.toIso.hom =
    yonedaEquiv.toIso.hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj F).map f

Tactic:
ext a

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : Cᵒᵖ ⥤ Type u₁
X Y : Cᵒᵖ
f : X ⟶ Y
a : ((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).obj X
⊢ (ConcreteCategory.hom
          (((yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj F).map f ≫
            yonedaEquiv.toIso.hom)).toFun
      a =
    (ConcreteCategory.hom (yonedaEquiv.toIso.hom ≫ ((𝟭 (Cᵒᵖ ⥤ Type u₁)).obj F).map f)).toFun a
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : C ⥤ Type u₁
X Y : C
f : X ⟶ Y
⊢ ((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).map f ≫ coyonedaEquiv.toIso.hom =
    coyonedaEquiv.toIso.hom ≫ ((𝟭 (C ⥤ Type u₁)).obj F).map f

Tactic:
ext a

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : C ⥤ Type u₁
X Y : C
f : X ⟶ Y
a : ((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).obj X
⊢ (ConcreteCategory.hom
          (((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).map f ≫
            coyonedaEquiv.toIso.hom)).toFun
      a =
    (ConcreteCategory.hom (coyonedaEquiv.toIso.hom ≫ ((𝟭 (C ⥤ Type u₁)).obj F).map f)).toFun a
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ lift F c ≫ limMap α ≫ π G j✝ = lift G ((Cone.postcompose α).obj c) ≫ π G j✝

Tactic:
limMap_π,

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ lift F c ≫ π F j✝ ≫ α.app j✝ = lift G ((Cone.postcompose α).obj c) ≫ π G j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (post F G) ≫ H.map (π (F ⋙ G) j✝) = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝

Tactic:
← H.map_comp,

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (post F G ≫ π (F ⋙ G) j✝) = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ H.map (ι (F ⋙ G) j) ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Tactic:
← H.map_comp,

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ H.map (ι (F ⋙ G) j ≫ post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (ι F j✝) ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H

Tactic:
← H.map_comp,

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (ι F j✝ ≫ colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
i : ι
⊢ ((WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor ⋙
            WidePullbackShape.wideCospan X (fun i ↦ Y (e i)) fun i ↦ f (e i)).map
        (WidePullbackShape.Hom.term i) ≫
      (Iso.refl X).hom =
    (eqToIso ⋯).hom ≫ (WidePullbackShape.wideCospan X Y f).map (WidePullbackShape.Hom.term i)

Tactic:
simp [← eqToHom_naturality]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y : C
inst✝ : HasBinaryCoproduct X Y
x✝ : Discrete WalkingPair
u : WalkingPair
⊢ (colimit.cocone (pair X Y)).ι.app { as := u } ≫ (Iso.refl (colimit.cocone (pair X Y)).pt).hom =
    (BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := u }

Tactic:
by
    cases u
    · dsimp; simp only [Category.comp_id]
    · dsimp; simp only [Category.comp_id]

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✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
j : J
⊢ homMk (hc.lift ((forget X).mapCone t)) ⋯ ≫ (liftCone D s c p hp).π.app j = t.π.app j

Tactic:
ext
    simp [dsimp% hc.fac ((forget X).mapCone t) j]

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
P : C
ι ι' : P ⟶ X
w : ι ≫ f = ι ≫ g
w' : ι' ≫ f = ι' ≫ g
h : ι = ι'
⊢ (Iso.refl (Fork.ofι ι w).pt).hom ≫ (Fork.ofι ι' w').ι = (Fork.ofι ι w).ι

Tactic:
by simp [h]

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
P : C
π π' : Y ⟶ P
w : f ≫ π = g ≫ π
w' : f ≫ π' = g ≫ π'
h : π = π'
⊢ (Cofork.ofπ π w).π ≫ (Iso.refl (Cofork.ofπ π w).pt).hom = (Cofork.ofπ π' w').π

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasImage f
inst✝ : Epi (factorThruImage f)
h : f ≫ g = 0
⊢ factorThruImage f ≫ image.ι f ≫ g = 0

Tactic:
by simp [h]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : HasImage g
h : f ≫ g = 0
⊢ (f ≫ factorThruImage g) ≫ image.ι g = 0

Tactic:
by simp [h]

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
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm✝ : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m✝ : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m✝ ≫ (Fork.ofι c.ι ⋯).ι = s.ι
⊢ m✝ = ↑l

Tactic:
by
      apply Fork.IsLimit.hom_ext i; rw [Fork.ι_ofι] at hm; rw [hm]; exact l.2.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : IsZero G
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c✝ : Cone K
x✝ : IsLimit c✝
⊢ IsLimit (G.mapCone c✝)

Tactic:
rw [Functor.isZero_iff] at hG
    exact IsLimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)

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

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ some j')

Tactic:
rw [h]
        exact {Hom.id j}

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' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = s.ι
⊢ m✝ = ↑l

Tactic:
by
      apply Fork.IsLimit.hom_ext i; rw [Fork.ι_ofι] at hm; rw [hm]; exact l.2.symm

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
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W'✝ : C
s : W'✝ ⟶ X'
hs : s ≫ g' = 0
m : W'✝ ⟶ c.pt
hm : m ≫ Fork.ι c ≫ e.hom = s
⊢ m ≫ Fork.ι c = hc.lift (ofι (s ≫ e.inv) ⋯) ≫ Fork.ι c

Tactic:
simpa [← cancel_mono e.hom] using hm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ IsLimit (G.mapCone (Fan.mk P g)) ≃ IsLimit (Fan.mk (G.obj P) fun j ↦ G.map (g j))

Tactic:
by
  refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
  · exact Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
  exact Cone.ext (Iso.refl _) fun j ↦ by dsimp; cases j; simp

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:
by simp [h]

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
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)) ≫ biprod.desc (F.map f) (F.map g) = F.map f + F.map g

Tactic:
biprod.add_eq_lift_id_desc

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)) ≫ biprod.desc (F.map f) (F.map g) =
    biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)) ≫ biprod.desc (F.map f) (F.map g)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
val✝ : Fintype J
⊢ HasBiproduct f

Tactic:
exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

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

Goal state before:
pp: case hnc
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
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ ¬(p ↑k)ᶜ

Tactic:
exact not_not.mpr k.2

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:
by simp [h]

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

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
ha : a ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) a = g a

Tactic:
ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha,

Goal state after:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
ha : a ∈ s
⊢ ↑((g.subtypePerm hg) ⟨a, ha⟩) = g a
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) a = c a

Tactic:
h a ha,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) a = g a
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) a = g a

Tactic:
ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∈ s
⊢ ↑((g.subtypePerm hg) ⟨a, ha⟩) = g a
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:
by simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬↑(f (g (f.symm ⟨b, pb⟩))) = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
grind [asEmbedding_apply]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ∀ (a b : α), f a = a ∨ f b = b ∨ a = b
⊢ f = 1

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ∀ (a b : α), f a = a ∨ f b = b ∨ a = b
a : α
⊢ f a = 1 a
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp
α : 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
⊢ f = swap x y

Tactic:
ext a

Goal state after:
case mp
α : 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 : α
⊢ f a = (swap x y) a
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
a b : α
⊢ (x :: y :: l ++ [a, b]).formPerm = (x :: y :: l ++ [a]).formPerm * Equiv.swap a b

Tactic:
simpa [mul_assoc] using formPerm_append_pair (y::l) a b

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
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ f ((Equiv.symm g) x) = f a

Tactic:
rw [hmeml hf₁, ← hg.2]

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
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ (Equiv.swap a x * g) ((Equiv.symm g) x) = a
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inl
n : ℕ
a₂ : Fin (n + 2)
ha₂ : ⟨0, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < 0
⊢ (if (swap 0 1) 0 ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
exact absurd a₂.zero_le ha₁.not_ge

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableEq α
⊢ f.IsSwap → f.IsCycle

Tactic:
by
  rintro ⟨x, y, hxy, rfl⟩
  exact isCycle_swap hxy

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm ^ l.length) x = 1 x

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
· obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
    simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ ⟨0, ⋯⟩ ≠ ⟨1, ⋯⟩

Tactic:
by exact of_decide_eq_true rfl

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

Goal state before:
pp: case e'_3
α : 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⁻¹) b = (Equiv.symm f) b

Tactic:
· exact swap_apply_of_ne_of_ne (by simpa [eq_comm, eq_symm_apply, symm_apply_eq] using! hfxb)
        (by simpa [eq_comm, eq_symm_apply, symm_apply_eq])

Goal state after:
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:
by simp [h]

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

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

Tactic:
let ⟨l, hl⟩ := (truncSwapFactors g).out

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
⊢ False
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:
by 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:
by simp [h]

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

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

Tactic:
exact ⟨x, hx, by 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:
by simp [h]

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

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

Tactic:
exact ⟨x, hx, by simp [h]⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : ∃ a, (a.IsCycle ∧ ∀ a_1 ∈ a.support, a a_1 = σ a_1) ∧ #a.support = n
⊢ 2 ≤ n

Tactic:
obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ w✝ : Perm α
hc : w✝.IsCycle
⊢ 2 ≤ #w✝.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
by_cases hx : f x = x
  · rw [← cycleOf_eq_one_iff] at hx
    simp [hx]
  · refine dvd_of_mem_cycleType ?_
    rw [cycleType, Multiset.mem_map]
    refine ⟨f.cycleOf x, ?_, ?_⟩
    · rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
    · simp [(isCycle_cycleOf _ hx).orderOf]

Goal state after: