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

Goal state before:
pp: case refine_2
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
x : (fun X ↦ X) (∏ᶜ fun s ↦ colimit (F s))
k : (s : α) → I s
p : (s : α) → (F s).obj (k s)
hk : ∀ (s : α), (hom (colimit.ι (F s) (k s))) (p s) = (hom (Pi.π (fun s ↦ colimit (F s)) s)) x
x✝ : Discrete α
s : α
this :
  (hom (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (productIso fun j ↦ (F j).obj (k j)).inv) p) =
    (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) ((hom (productIso fun j ↦ (F j).obj (k j)).inv) p)
⊢ (hom (limit.π (Discrete.functor fun s ↦ colimit (F s)) { as := s }))
      ((hom (colimitPointwiseProductToProductColimit F))
        ((hom (colimit.ι (pointwiseProduct F) k)) ((hom (productIso ((Functor.pi F).obj k)).inv) p))) =
    (hom (limit.π (Discrete.functor fun s ↦ colimit (F s)) { as := s })) x

Tactic:
exact this.trans (by simpa [Functor.pi] using hk _)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n

Tactic:
erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ P.ι.f 0 ≫ g.f 0 = f ≫ Q.ι.f 0

Tactic:
← HomologicalComplex.comp_f,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ (P.ι ≫ g).f 0 = f ≫ Q.ι.f 0
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ CreatesColimit (parallelPair f 0) P.ι

Tactic:
fapply createsColimitFullSubcategoryInclusion'

Goal state after:
case c
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ Cocone (parallelPair f 0 ⋙ P.ι)

case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ IsColimit ?c

case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ P (Cocone.pt ?c)
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
a b : N ⋊[φ] G
this :
  ∀ (n : G) (g : N), (fn.comp (MulEquiv.toMonoidHom (φ n))) g = ((MulEquiv.toMonoidHom (MulAut.conj (fg n))).comp fn) g
⊢ fn (a * b).left * fg (a * b).right = fn a.left * fg a.right * (fn b.left * fg b.right)

Tactic:
simp only [MulAut.conj_apply, MonoidHom.comp_apply, MulEquiv.coe_toMonoidHom] at this

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
a b : N ⋊[φ] G
this : ∀ (n : G) (g : N), fn ((φ n) g) = fg n * fn g * (fg n)⁻¹
⊢ fn (a * b).left * fg (a * b).right = fn a.left * fg a.right * (fn b.left * fg b.right)
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁴ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝³ : ConcreteCategory V FV
inst✝² : HasForget₂ V TopCat
G : Type u_4
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
X : Action V G
g h : G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ (g * h) • x = g • h • x

Tactic:
change (CategoryTheory.forget₂ _ TopCat).map (X.ρ (g * h)) x =
      ((CategoryTheory.forget₂ _ TopCat).map (X.ρ h) ≫
        (CategoryTheory.forget₂ _ TopCat).map (X.ρ g)) x
    rw [← Functor.map_comp, map_mul]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
⊢ PreservesFiniteLimits L

Tactic:
by
  let := abelian L P
  rw [((Functor.preservesFiniteLimits_tfae L).out 3 2 :)]
  intro _ _ f
  exact preservesKernel L P f

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F
map_coeval : F.map coeval = η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y
⊢ F.map (Y ◁ coeval ≫ (α_ Y X Y).inv ≫ eval ▷ Y) = F.map ((ρ_ Y).hom ≫ (λ_ Y).inv)

Tactic:
simp [map_eval, map_coeval, Functor.Monoidal.map_whiskerLeft,
        Functor.Monoidal.map_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F
map_coeval : F.map coeval = η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y
⊢ F.map (coeval ▷ X ≫ (α_ X Y X).hom ≫ X ◁ eval) = F.map ((λ_ X).hom ≫ (ρ_ X).inv)

Tactic:
simp [map_eval, map_coeval, Functor.Monoidal.map_whiskerLeft,
        Functor.Monoidal.map_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝¹ : Abelian D := abelian L P
this✝ : PreservesFiniteLimits L
x✝² : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
x✝¹ x✝ : D
f : x✝¹ ⟶ x✝
f' : Arrow C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
have : PreservesLimit (parallelPair (L.map f'.hom) 0) G :=
    preservesLimit_of_preserves_limit_cone
      (KernelFork.isLimitMapConeEquiv _ _
        (isLimitOfPreserves L (kernelIsKernel f'.hom)))
          ((KernelFork.isLimitMapConeEquiv _ G).symm
            (KernelFork.isLimitMapConeEquiv _ (L ⋙ G)
              (isLimitOfPreserves (L ⋙ G) (kernelIsKernel f'.hom))))

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝² : Abelian D := abelian L P
this✝¹ : PreservesFiniteLimits L
x✝² : PreservesFiniteLimits (L ⋙ G)
this✝ : G.Additive
x✝¹ x✝ : D
f : x✝¹ ⟶ x✝
f' : Arrow C
iso : L.mapArrow.obj f' ≅ Arrow.mk f
this : PreservesLimit (parallelPair (L.map f'.hom) 0) G
⊢ PreservesLimit (parallelPair f 0) G
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ { f // F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f } ≃
    { g // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g }

Tactic:
apply (adj₂.homEquiv _ _).subtypeEquiv _
      intro f
      rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left,
        otherMap, assoc, adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality,
        adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit, adj₂.right_triangle_components,
        comp_id, Functor.comp_map, ← U.map_comp, assoc]
      dsimp
      rw [← adj₁.counit_naturality]
      simp [dsimp% adj₂.homEquiv_unit _ _ f ]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (X : C), Mono (t.leftToRight.app X)
X : D
⊢ Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)

Tactic:
by rw [← leftToRight_app_obj]; exact h _

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ 𝟙 (h ≫ 𝟙 a) ⊗≫ ((h ≫ 𝟙 a) ◁ adj.unit ≫ s.unit ▷ (f ≫ u)) ⊗≫ s.lift ◁ adj.counit ▷ u ⊗≫ 𝟙 (s.lift ≫ u) =
    s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u)

Tactic:
rw [whisker_exchange, rightZigzag]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
⊢ (↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map (f ≫ g)).toFunctor.map g_1 ≫ eqToHom ⋯) =
    (↾fun g ↦ eqToHom ⋯ ≫ (F.map f).toFunctor.map g ≫ eqToHom ⋯) ≫
      ↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map g).toFunctor.map g_1 ≫ eqToHom ⋯

Tactic:
ext h

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
h : (hom (limit.π (F ⋙ objects) x✝¹)) X ⟶ (hom (limit.π (F ⋙ objects) x✝¹)) Y
⊢ (hom (↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map (f ≫ g)).toFunctor.map g_1 ≫ eqToHom ⋯)).toFun h =
    (hom
          ((↾fun g ↦ eqToHom ⋯ ≫ (F.map f).toFunctor.map g ≫ eqToHom ⋯) ≫
            ↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map g).toFunctor.map g_1 ≫ eqToHom ⋯)).toFun
      h
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
W₁ W₂ : Cowedge F
e : W₁.pt ≅ W₂.pt
he : ∀ (j : J), Multicofork.π W₁ j ≫ e.hom = Multicofork.π W₂ j
j : WalkingMultispan (multispanShapeCoend J)
f : (multispanShapeCoend J).L
⊢ W₁.ι.app (WalkingMultispan.left f) ≫ e.hom = W₂.ι.app (WalkingMultispan.left f)

Tactic:
by simpa using! _ ≫= (he f.left)

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (eHomEquiv V) f ▷ 𝟙_ V ≫
        (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
          (eHomWhiskerRight V α.inv Y ▷ Y ⟶[V] Z) ≫
            (eHomWhiskerLeft V X₁ β.hom ▷ Y ⟶[V] Z) ≫
              (X₁ ⟶[V] Y₁) ◁ eHomWhiskerRight V β.inv Z ≫ (X₁ ⟶[V] Y₁) ◁ eHomWhiskerLeft V Y₁ γ.hom ≫ eComp V X₁ Y₁ Z₁

Tactic:
← eComp_eHomWhiskerLeft,

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (eHomEquiv V) f ▷ 𝟙_ V ≫
        (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
          (eHomWhiskerRight V α.inv Y ▷ Y ⟶[V] Z) ≫
            (eHomWhiskerLeft V X₁ β.hom ▷ Y ⟶[V] Z) ≫
              (X₁ ⟶[V] Y₁) ◁ eHomWhiskerRight V β.inv Z ≫ eComp V X₁ Y₁ Z ≫ eHomWhiskerLeft V X₁ γ.hom
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X✝ : C
inst✝ : IsConnected X✝
x✝ y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x✝
hx' : x' = (e X✝).symm x✝
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ (ConcreteCategory.hom
        (FintypeCat.equivEquivIso
            ((F.obj Y).uSwitchEquiv.symm.trans
              ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (F.obj Y).uSwitchEquiv))).hom)
      ((ConcreteCategory.hom (F.map f)) x) =
    (F.obj Y).uSwitchEquiv
      ((ConcreteCategory.hom ((F ⋙ FintypeCat.uSwitch).map f))
        ((FintypeCat.equivEquivIso.symm (Iso.app g' X)) ((F.obj X).uSwitchEquiv.symm x)))

Tactic:
erw [← NatTrans.naturality_apply, FintypeCat.uSwitchEquiv_symm_naturality (F.map f)]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X✝ : C
inst✝ : IsConnected X✝
x✝ y : (F.obj X✝).obj
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := comp_right FintypeCat.uSwitch
e : (Y : C) → (F'.obj Y).obj ≃ (F.obj Y).obj := fun Y ↦ (F.obj Y).uSwitchEquiv
x' : (F'.obj X✝).obj := (e X✝).symm x✝
hx' : x' = (e X✝).symm x✝
y' : (F'.obj X✝).obj := (e X✝).symm y
hy' : y' = (e X✝).symm y
g' : Aut F'
hg' : (ConcreteCategory.hom (g'.hom.app X✝)) x' = y'
gapp : (Y : C) → F.obj Y ≅ F.obj Y :=
  fun Y ↦ FintypeCat.equivEquivIso ((e Y).symm.trans ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (e Y)))
X Y : C
f : X ⟶ Y
x : (F.obj X).obj
⊢ (ConcreteCategory.hom
        (FintypeCat.equivEquivIso
            ((F.obj Y).uSwitchEquiv.symm.trans
              ((FintypeCat.equivEquivIso.symm (Iso.app g' Y)).trans (F.obj Y).uSwitchEquiv))).hom)
      ((ConcreteCategory.hom (F.map f)) x) =
    (F.obj Y).uSwitchEquiv
      ((ConcreteCategory.hom (g'.hom.app Y)) ((F.obj Y).uSwitchEquiv.symm ((ConcreteCategory.hom (F.map f)) x)))
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (HomRel.CompClosure redStep) (p ≫ Path.reverse p) = Quot.mk (HomRel.CompClosure redStep) (𝟙 X)

Tactic:
apply Quot.eqvGen_sound
  induction p with
  | nil => apply EqvGen.refl
  | cons q f ih =>
    simp only [Quiver.Path.reverse]
    fapply EqvGen.trans
    -- Porting note: dot notation for `Quiver.Path.*` and `Quiver.Hom.*` not working
    · exact q ≫ Quiver.Path.reverse q
    · apply EqvGen.symm
      apply EqvGen.rel
      have : HomRel.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
          (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫
            Quiver.Path.reverse q) := by
        apply HomRel.CompClosure.intro
        apply redStep.step
      simp only [Category.assoc, Category.id_comp] at this ⊢
      -- Porting note: `simp` cannot see how `Quiver.Path.comp_assoc` is relevant, so change to
      -- category notation
      change HomRel.CompClosure redStep (q ≫ Quiver.Path.reverse q)
        (Quiver.Path.cons q f ≫ (Quiver.Hom.toPath (Quiver.reverse f)) ≫ (Quiver.Path.reverse q))
      simp only [← Category.assoc] at this ⊢
      exact this
    · exact ih

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ Function.Injective S.hom.obj

Tactic:
by
  rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd
  simp only [Subtype.mk_eq_mk]; exact hcd

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : p✝ ∈ ⋂ S ∈ s, S.arrows c✝ d✝
⊢ Groupoid.inv p✝ ∈ ⋂ S ∈ s, S.arrows d✝ c✝

Tactic:
rw [mem_iInter₂] at hp ⊢

Goal state after:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
s : Set (Subgroupoid C)
c✝ d✝ : C
p✝ : c✝ ⟶ d✝
hp : ∀ i ∈ s, p✝ ∈ i.arrows c✝ d✝
⊢ ∀ i ∈ s, Groupoid.inv p✝ ∈ i.arrows d✝ c✝
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), 𝟙 c ∈ (sInf s).arrows c c

Tactic:
simp_rw [sInf, mem_iInter₂]; exact fun c S Ss => (sn S Ss).wide c

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
s : Set (Subgroupoid C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C), 𝟙 c ∈ (sInf s).arrows c c

Tactic:
by simp_rw [sInf, mem_iInter₂]; exact fun c S Ss => (sn S Ss).wide c

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

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
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
Fₗ Gₗ : C ⥤ E
α : Fₗ ≅ Gₗ
H : D ⥤ E'
⊢ (mapIsoWhiskerRight α H).inv = mapWhiskerRight α.inv H

Tactic:
ext x
  cases x <;> simp [mapIsoWhiskerRight]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
s : { p // p.1 ≫ f = p.2 ≫ g }
i : T.I
⊢ (↑s).1.φ i ≫
      f.φ (↑⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩) =
    (↑s).2.φ i ≫ g.φ (↑⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).2

Tactic:
by simpa using ((hom_ext_iff _ _).1 s.2).2 i

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inr ≫ (binaryCoproductIso F G).hom = coprod.inr

Tactic:
by
  simp [binaryCoproductIso]
  aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
l : Y ⟶ h.pullback
h₁ : l ≫ h.p₁ = g₁
h₂ : l ≫ h.p₂ = g₂
⊢ Nonempty (h.LiftStruct g₁ g₂ b)

Tactic:
exact ⟨{
    f := l
    f_p₁ := h₁
    f_p₂ := h₂
    f_p := by rw [← h.hp₁, ← hf₁, reassoc_of% h₁] }⟩

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

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
⊢ IsClosedUnderColimitsOfShape (fun f ↦ Coequifibered f.hom) J

Tactic:
by
  have : IsClosedUnderIsomorphisms fun f : Under F ↦ f.hom.Coequifibered :=
    ⟨fun {X Y} e ↦ by rw [← Under.w e.hom, Coequifibered.cancel_right_of_respectsIso]; simp⟩
  have (a b : Cᵒᵖ) : HasCoproductsOfShape (a ⟶ b) Dᵒᵖ :=
    hasColimitsOfShape_of_equivalence (Discrete.equivalence Quiver.Hom.opEquiv)
  let e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv _ (opUnopEquiv _ _)).symm.trans (opEquivOpUnder F)
  rw [isClosedUnderColimitsOfShape_iff_op, ← isClosedUnderLimitsOfShape_inverseImage_iff _ _ e]
  convert!
    (inferInstance : IsClosedUnderLimitsOfShape (fun f : Over F.op ↦ f.hom.Equifibered) Jᵒᵖ) with f
  simp [e, MorphismProperty.cancel_left_of_respectsIso, ← coequifibered_unop_iff]
  rfl

Goal state after: