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

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X✝ Y✝ : D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hfg : F.map a₁✝ = F.map a₂✝
⊢ F.map ((L.objObjPreimageIso X✝).hom ≫ a₁✝ ≫ (L.objObjPreimageIso Y✝).inv) =
    F.map ((L.objObjPreimageIso X✝).hom ≫ a₂✝ ≫ (L.objObjPreimageIso Y✝).inv)

Tactic:
by simp [hfg]

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
hF : F.FullyFaithful
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C ⥤ D
f : ((Functor.whiskeringRight C D E).obj F).obj X✝ ⟶ ((Functor.whiskeringRight C D E).obj F).obj Y✝
x✝¹ x✝ : C
g : x✝¹ ⟶ x✝
⊢ X✝.map g ≫ hF.preimage (f.app x✝) = hF.preimage (f.app x✝¹) ≫ Y✝.map g

Tactic:
apply hF.map_injective
        simp only [map_comp, map_preimage]
        apply f.naturality

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y X' Y' : T
f : X ⟶ Y
f' : X' ⟶ Y'
⊢ mk f = mk f' ↔ ∃ hX hY, f = eqToHom hX ≫ f' ≫ eqToHom ⋯

Tactic:
constructor
  · intro h
    refine ⟨congr_arg Arrow.left h, congr_arg Arrow.right h, ?_⟩
    simpa [eqToHom_left, eqToHom_right] using! iso_w (eqToIso h.symm)
  · rintro ⟨rfl, rfl, h⟩
    simp only [eqToHom_refl, Category.comp_id, Category.id_comp] at h
    rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift ↔ ⋯.HasLift

Tactic:
rw [iff, iff]
  exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun

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

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P.isoClosure ≤ Q → P ≤ Q

Tactic:
exact P.le_isoClosure.trans

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

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
⊢ Function.Surjective f

Tactic:
refine Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => ?_

Goal state after:
case mp
X Y : Type u
f : X → Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), ↾f ≫ g = ↾f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ g₁ = g₂
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X✝ Y✝ : Type u
f : X✝ ⟶ Y✝
hf : Epi f
⊢ ↾Function.surjInv ⋯ ≫ f = 𝟙 Y✝

Tactic:
by
          ext x
          exact (Function.rightInverse_surjInv <| (epi_iff_surjective f).1 hf) x

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget CommSemiRingCat).map f)
    let ff : X →+* Y := f.hom
    let e : X ≃+* Y := { ff, i.toEquiv with }
    exact e.toCommSemiRingCatIso.isIso_hom

Goal state after:
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
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : f ≫ g = h ≫ G.map k
⊢ (adj.homEquiv X' Y').symm (f ≫ g) = (adj.homEquiv X' Y).symm h ≫ k

Tactic:
← homEquiv_naturality_right_symm,

Goal state after:
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
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : f ≫ g = h ≫ G.map k
⊢ (adj.homEquiv X' Y').symm (f ≫ g) = (adj.homEquiv X' Y').symm (h ≫ G.map k)
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
⊢ (limitCone h).extend (homOfCone h s) = s

Tactic:
← coneOfHom_homOfCone h s

Goal state after:
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
⊢ (limitCone h).extend (homOfCone h (coneOfHom h (homOfCone h s))) = coneOfHom h (homOfCone h s)
Module: Mathlib.CategoryTheory.Balanced

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Balanced C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
fmono : Mono f
fepi : Epi f
⊢ IsIso f

Tactic:
rw [← Quiver.Hom.op_unop f]
      exact isIso_of_op _

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

Goal state before:
pp: J : Type w
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
by
    cases f
    · exact g
    cases g
    apply Hom.init _

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
x y : StructuredArrow S T
hr : x.right = y.right
hh : x.hom ≫ T.map (eqToHom hr) = y.hom
⊢ x = y

Tactic:
cases x
  cases y
  cases hr
  cat_disch

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ (t.snd ≫
        Q.lift
          (mk (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } })
            (𝟙 { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }.pt))) ≫
      t.π.app { as := WalkingPair.left } =
    𝟙 t.pt ≫ t.π.app { as := WalkingPair.left }

Tactic:
apply P.hom_ext
      rintro ⟨⟨⟩⟩

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ (t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }))) ≫
      t.π.app { as := WalkingPair.right } =
    𝟙 t.pt ≫ t.π.app { as := WalkingPair.right }

Tactic:
apply P.hom_ext
      rintro ⟨⟨⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
inst✝¹ : S.Full
inst✝ : S.Faithful
c : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))
m : c.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt
⊢ m.left = (homMk (S.preimage c.pt.hom) ⋯).left

Tactic:
apply S.map_injective

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
inst✝¹ : S.Full
inst✝ : S.Faithful
c : Cone (Functor.empty (CostructuredArrow S (S.obj Y)))
m : c.pt ⟶ (asEmptyCone (mk (𝟙 (S.obj Y)))).pt
⊢ S.map m.left = S.map (homMk (S.preimage c.pt.hom) ⋯).left
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
⊢ t.fst ≫ f = t.snd ≫ g

Tactic:
by rw [← hxh, ← hyh, this]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }).hom ≫
      { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }.cone.π.app
        WalkingCospan.left =
    limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left
⊢ IsIso (pullback.fst (f ≫ i) i)

Tactic:
convert! (congrArg IsIso (show _ ≫ pullback.fst f (𝟙 Z) = _ from this)).mp inferInstance

Goal state after:
case e'_3.e'_7
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }).hom ≫
      { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }.cone.π.app
        WalkingCospan.left =
    limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left
⊢ i = 𝟙 Z ≫ i

case e'_5.e'_7
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }).hom ≫
      { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }.cone.π.app
        WalkingCospan.left =
    limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left
e_3✝ : pullback (f ≫ i) i = limit (cospan (f ≫ i) (𝟙 Z ≫ i))
⊢ i = 𝟙 Z ≫ i
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_to.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a = default

Tactic:
intro f
    ext
    apply (hF _).eq_of_src _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ I = J

Tactic:
cases I

Goal state after:
case mk
C : Type u
inst✝ : Category.{v, u} C
J : HasZeroMorphisms C
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ { zero := zero✝, comp_zero := comp_zero✝, zero_comp := zero_comp✝ } = J
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app one = s.π.app one

Tactic:
simp only [Fork.app_one_eq_ι_comp_left, ← Category.assoc]

Goal state after:
case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ (k ≫ t.ι) ≫ f = s.ι ≫ f
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g

Tactic:
rw [← sub_eq_zero, ← comp_sub, c.condition]

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
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
p : X ≅ X'
q : Y ≅ Y'
w : f ≫ q.hom = p.hom ≫ f'
⊢ f' ≫ q.inv = p.inv ≫ f

Tactic:
refine (cancel_mono q.hom).1 ?_
          simp [w]

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
B : Bicone F
j j' : J
h : j ≠ j'
⊢ B.ι j ≫ B.π j' = 0

Tactic:
by
  simpa [h] using B.ι_π j j'

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = ht.lift (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0) ≫ t.toCone.π.app j'

Tactic:
by
    rw [ht.fac]
    simp [t.ι_π]

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j =
    t.toCocone.ι.app j' ≫ ht.desc (Cofan.mk (f j) fun j' ↦ if h : j' = j then eqToHom ⋯ else 0)

Tactic:
by
    rw [ht.fac]
    simp [t.ι_π]

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

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
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBiproductsOfShape J C
X✝ Y✝ : Discrete J ⥤ C
η : X✝ ⟶ Y✝
x✝¹ : Discrete J
i : J
x✝ : Discrete J
j : J
⊢ (colimit.ι X✝ { as := i } ≫
        colim.map η ≫
          ((Sigma.isoColimit Y✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ Y✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ Y✝.obj { as := j }) ≪≫ Pi.isoLimit Y✝).hom) ≫
      limit.π Y✝ { as := j } =
    (colimit.ι X✝ { as := i } ≫
        ((Sigma.isoColimit X✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ X✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ X✝.obj { as := j }) ≪≫ Pi.isoLimit X✝).hom ≫
          lim.map η) ≫
      limit.π Y✝ { as := j }

Tactic:
by_cases h : i = j <;>
       simp_all [Sigma.isoColimit, Pi.isoLimit, biproduct.ι_π, biproduct.ι_π_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun t ↦ if t = i then a else 0) a_1 = f) →
    f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s

Tactic:
rintro ⟨a, _, hn, g, ⟨rfl, hg⟩, rfl⟩

Goal state after:
case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : ι → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
⊢ (addRightEmbedding fun t ↦ if t = i then a else 0) g i +
        ∑ x ∈ s, (addRightEmbedding fun t ↦ if t = i then a else 0) g x =
      n ∧
    ∀ (i_1 : ι), ¬(addRightEmbedding fun t ↦ if t = i then a else 0) g i_1 = 0 → i_1 = i ∨ i_1 ∈ s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
h : c.blocks = []
⊢ n = 0

Tactic:
simpa using congr(List.sum $h)

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
this : HasProduct fun b ↦ F.obj (f b)
j : J
⊢ ((F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom) ≫
      Pi.π (fun b ↦ F.obj (f b)) j =
    F.map (Pi.π f j)

Tactic:
simp [← Function.comp_def, ← Functor.map_comp]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ l.toFinset

Tactic:
have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
hx' : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l.toFinset
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : y ∈ (swap x (f x) * f).support
⊢ y ∈ f.support ∧ y ≠ x

Tactic:
simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f y = x then f x else if y = x then x else f y) ≠ y
⊢ f y ≠ y ∧ y ≠ x
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList (a :: l)

Tactic:
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]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f
Module: Mathlib.GroupTheory.Perm.Sign

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

Tactic:
wlog lt : i < j generalizing i j

Goal state after:
case inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this : ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

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

Goal state before:
pp: case zero
hn : 2 ≤ 0
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
norm_num at hn

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

Goal state before:
pp: case succ.zero
hn : 2 ≤ 0 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
norm_num at hn

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ x ∈ l

Tactic:
replace H := set_support_zpow_subset l.formPerm l.length H

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : x = (σ ^ n) x
⊢ swap x ((σ ^ (n + 1)) x) ∈ H

Tactic:
rw [pow_succ', mul_apply, ← h5]
        exact h4

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
⊢ Pairwise fun x y ↦ signAux2 l (swap x y) = -1

Tactic:
· intro x y hxy
    rw [← e.injective.ne_iff] at hxy
    rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hxy]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
⊢ Finset.univ.noncommProd (fun i ↦ (ϕ i) (1 i)) ⋯ = 1

Tactic:
by
    apply (Finset.noncommProd_eq_pow_card _ _ _ _ _).trans (one_pow _)
    simp

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
⊢ mrange (noncommPiCoprod ϕ hcomm) = ⨆ i, mrange (ϕ i)

Tactic:
let := Classical.decEq ι
  apply le_antisymm
  · rintro x ⟨f, rfl⟩
    refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
    apply Submonoid.mem_sSup_of_mem
    · use i
    simp
  · refine iSup_le ?_
    rintro i x ⟨y, rfl⟩
    exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ (noncommPiCoprod ϕ hcomm).ker
⊢ f ∈ ⊥

Tactic:
have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
    Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _)
      _ hind (by simp) heq1

Goal state after:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ (noncommPiCoprod ϕ hcomm).ker
this : ∀ i ∈ Finset.univ, (ϕ i) (f i) = 1
⊢ f ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ x ∈ (f.cycleOf x).support

Tactic:
by rw [mem_support_cycleOf_iff'_aux hx]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case hind
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ iSupIndep fun i ↦ (H i).subtype.range

Tactic:
simpa using hind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ f.cycleType ≤ g.cycleType

Tactic:
by
  have hf' := mem_cycleFactorsFinset_iff.1 hf
  rw [cycleType_def, cycleType_def, hf'.left.cycleFactorsFinset_eq_singleton]
  refine map_le_map ?_
  simpa only [Finset.singleton_val, singleton_le, Finset.mem_val] using hf

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

Goal state before:
pp: case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]
    · apply Fin.succ_ne_zero
    · apply (Fin.succ_injective _).ne hgt.ne.symm
    · simpa [Fin.le_iff_val_le_val] using hgt

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

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

Tactic:
· rw [Fin.succAbove_of_le_castSucc _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]

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
  · rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
  · rw [Fin.succAbove_of_le_castSucc _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]

Goal state after: