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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (b : D) (a : C), Function.Injective fun g ↦ L.map (q.adj₂.counit.app a) ≫ g) ↔
    ∀ (X : D) (Z : C), Function.Injective fun g ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
refine forall_congr' fun X ↦ forall_congr' fun Y ↦ ?_

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
⊢ (Function.Injective fun g ↦ L.map (q.adj₂.counit.app Y) ≫ g) ↔
    Function.Injective fun g ↦ g ≫ q.adj₃.unit.app (F.obj X)
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)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (adj₁.homEquiv (U.obj X) (R.obj Y')).symm
      ((adj₂.homEquiv (U.obj X) Y)
          ↑((Cofork.IsColimit.homIso
                (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y)
              h) ≫
        (R ⋙ U).map g) =
    ↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y))
          ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
            ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
                ((adj₂.homEquiv (U.obj X) Y)
                  ↑((Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                      h)),
              ⋯⟩)) ≫
      R.map g

Tactic:
Functor.comp_map

Goal state after:
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)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (adj₁.homEquiv (U.obj X) (R.obj Y')).symm
      ((adj₂.homEquiv (U.obj X) Y)
          ↑((Cofork.IsColimit.homIso
                (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y)
              h) ≫
        U.map (R.map g)) =
    ↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y))
          ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
            ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
                ((adj₂.homEquiv (U.obj X) Y)
                  ↑((Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                      h)),
              ⋯⟩)) ≫
      R.map g
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : Quot Rel), Quot.map₂ Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel (Hom₂.id X)) f = f

Tactic:
rintro f g ⟨η⟩
    exact Quot.sound (Rel.id_comp η)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : Quot Rel), Quot.map₂ Hom₂.vcomp ⋯ ⋯ f (Quot.mk Rel (Hom₂.id Y)) = f

Tactic:
by
    rintro f g ⟨η⟩
    exact Quot.sound (Rel.comp_id η)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
rw [naturality_comp η]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case some
X Y : Pointed
f : X ⟶ Y
a : X.X
ha : a ≠ X.point
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫ (Pointed.Iso.mk (Equiv.optionSubtypeNe Y.point) ⋯).hom).toFun
      (some ⟨a, ha⟩) =
    ((Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯).hom ≫ (𝟭 Pointed).map f).toFun (some ⟨a, ha⟩)

Tactic:
simp_all [Equiv.optionSubtypeNe, Equiv.optionSubtype,
          Option.casesOn'_eq_elim, Part.elim_toOption]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = (f.core s ∪ f.Domᶜ) ∩ Set.univ

Tactic:
Set.inter_univ,

Goal state after:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.core s = f.core s ∪ f.Domᶜ
Module: Mathlib.CategoryTheory.Widesubcategory

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty D
inst✝ : P.IsMultiplicative
X Y : InducedWideCategory D F P
f g : X ⟶ Y
eq : (wideInducedFunctor F P).map f = (wideInducedFunctor F P).map g
⊢ f = g

Tactic:
cases f
    cases g
    aesop

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
f₂ : X₂ ⟶ Y₂
⊢ (X₁ ◁ f₂) ▷ X₃ ≫ (α_ X₁ Y₂ X₃).hom = (α_ X₁ X₂ X₃).hom ≫ X₁ ◁ f₂ ▷ X₃

Tactic:
simp only [← tensorHom_id, ← id_tensorHom, associator_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    ((α_ Y₁ Y₂ Y₃).hom ≫ 𝟙 (Y₁ ⊗ Y₂ ⊗ Y₃) ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom)

Tactic:
comp_id

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom) =
    ((α_ Y₁ Y₂ Y₃).hom ⊗ₘ 𝟙 Y₄) ≫ (α_ Y₁ (Y₂ ⊗ Y₃) Y₄).hom ≫ (𝟙 Y₁ ⊗ₘ (α_ Y₂ Y₃ Y₄).hom)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom ≫ 𝟙 (Y₁ ⊗ Y₂ ⊗ Y₃ ⊗ Y₄) =
    (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom

Tactic:
comp_id

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : L'.obj X₁ ≅ Y₁
X₂ : C
e₂ : L'.obj X₂ ≅ Y₂
X₃ : C
e₃ : L'.obj X₃ ≅ Y₃
X₄ : C
e₄ : L'.obj X₄ ≅ Y₄
this : Pentagon (L'.obj X₁) (L'.obj X₂) (L'.obj X₃) (L'.obj X₄)
⊢ (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom = (α_ (Y₁ ⊗ Y₂) Y₃ Y₄).hom ≫ (α_ Y₁ Y₂ (Y₃ ⊗ Y₄)).hom
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ V₁.str ≫ F.map h.inv = h.inv ≫ V₀.str

Tactic:
rw [h.eq_inv_comp, ← Category.assoc, ← w, Category.assoc, ← F.map_comp]
        simp only [Iso.hom_inv_id, Functor.map_id, Category.comp_id]

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

Goal state before:
pp: V : Type u₁
inst✝³ : Category.{v₁, u₁} V
inst✝² : MonoidalCategory V
inst✝¹ : BraidedCategory V
C : Type u
inst✝ : EnrichedCategory V C
x✝³ x✝² x✝¹ x✝ : Cᵒᵖ
⊢ (α_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
          (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).inv ≫
      (β_ ((Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ⊗ Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
            (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
        (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) ◁
            (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)).hom ≫
          (α_ (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹) (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²)
                (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³)).inv ≫
            (comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ▷
                Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ≫
              comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³) =
    (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁
        (β_ (Opposite.unop x✝¹ ⟶[V] Opposite.unop x✝²) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝¹)).hom ≫
      (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) ◁ comp (Opposite.unop x✝) (Opposite.unop x✝¹) (Opposite.unop x✝²) ≫
        (β_ (Opposite.unop x✝² ⟶[V] Opposite.unop x✝³) (Opposite.unop x✝ ⟶[V] Opposite.unop x✝²)).hom ≫
          comp (Opposite.unop x✝) (Opposite.unop x✝²) (Opposite.unop x✝³)

Tactic:
simp only [braiding_tensor_left_hom, Category.assoc, Iso.inv_hom_id_assoc,
      braiding_naturality_right_assoc, braiding_tensor_right_hom]

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

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j ≫ 𝟙 (F₁.obj j ⟶[V] F₂.obj j) = end_.π (diagram V F₁ F₂) j

Tactic:
comp_id

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j = end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j ≫ 𝟙 (F₁.obj j ⟶[V] F₂.obj j) = end_.π (diagram V F₁ F₂) j

Tactic:
comp_id

Goal state after:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j = end_.π (diagram V F₁ F₂) j
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : ↑(F.obj { as := op S })
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
⊢ (fiberInclusion.map f).base = 𝟙 S

Tactic:
simpa using (IsHomLift.fac (forget F) (𝟙 S) (fiberInclusion.map f)).symm

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom
        ((Types.binaryProductIso ((pair X Y ⋙ F ⋙ FintypeCat.incl).obj { as := WalkingPair.left })
              ((pair X Y ⋙ F ⋙ FintypeCat.incl).obj { as := WalkingPair.right })).inv ≫
          prod.fst))
      (x, y) =
    x

Tactic:
Types.binaryProductIso_inv_comp_fst

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
x : (F.obj X).obj
y : (F.obj Y).obj
⊢ (ConcreteCategory.hom (↾_root_.Prod.fst)) (x, y) = x
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
f : End F
A : PointedGaloisObject F
⊢ (↑((Types.limitEquivSections (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}))
            ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).toEquiv
              (((yoneda.obj (F ⋙ FintypeCat.incl)).mapIso
                    (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).op).toEquiv
                (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f))))
        A).down =
    (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
Types.limitEquivSections_apply,

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ ((ConcreteCategory.hom (limit.π (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}) A))
        ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).toEquiv
          (((yoneda.obj (F ⋙ FintypeCat.incl)).mapIso
                (colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).op).toEquiv
            (((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f)))).down =
    (ConcreteCategory.hom (f.app A.obj)) A.pt
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).obj
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
h : Function.Surjective ⇑(toAut F G)
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
⊢ ∃ g, g • x = y

Tactic:
by
    obtain ⟨t, ht⟩ := MulAction.exists_smul_eq (Aut F) x y
    obtain ⟨g, rfl⟩ := h t
    exact ⟨g, ht⟩

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

Goal state before:
pp: G : Type u₁
inst✝ : Groupoid G
⊢ lift (𝟭 G) ⋙ of G = 𝟭 (FreeGroupoid G)

Tactic:
lift_unique (of G) (lift (𝟭 G) ⋙ of G) (by rw [← Functor.assoc, lift_spec, Functor.id_comp])

Goal state after:
G : Type u₁
inst✝ : Groupoid G
⊢ lift (of G) = 𝟭 (FreeGroupoid G)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
⊢ BijOn (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)

Tactic:
refine ⟨fun γ γS => Sn.conj p γS, fun γ₁ _ γ₂ _ h => ?_, fun δ δS =>
    ⟨p ≫ δ ≫ Groupoid.inv p, Sn.conj' p δS, ?_⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
γ₁ : c ⟶ c
x✝¹ : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
x✝ : γ₂ ∈ S.arrows c c
h : (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) γ₂
⊢ γ₁ = γ₂

case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
δ : d ⟶ d
δS : δ ∈ S.arrows d d
⊢ (fun γ ↦ Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U V W : FormalCoproduct C
f : U ⟶ V
g : V ⟶ W
α : Type t
inst✝ : HasProductsOfShape α C
i✝ : (U.power α).I
⊢ (powerMap (f ≫ g) α).φ i✝ ≫ eqToHom ⋯ = (powerMap f α ≫ powerMap g α).φ i✝

Tactic:
dsimp
    ext
    simp only [Category.comp_id, Category.assoc, Pi.map_π, Function.comp_apply,
      Pi.map_π_assoc]
    apply Pi.map_π

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
m : (c₁.mapBifunctor c₂ F).pt ⟶ s.pt
hm : Cofork.π (c₁.mapBifunctor c₂ F) ≫ m = s.π
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m =
    (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ ⋯.choose

Tactic:
(exists_desc hc₁ hc₂ F s).choose_spec,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : Cofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂)) 0
m : (c₁.mapBifunctor c₂ F).pt ⟶ s.pt
hm : Cofork.π (c₁.mapBifunctor c₂ F) ≫ m = s.π
⊢ (F.map (Cofork.π c₁)).app Y₂ ≫ (F.obj c₁.pt).map (Cofork.π c₂) ≫ m = s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ IsPushout 0 0 coprod.inl coprod.inr

Tactic:
convert! @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial

Goal state after:
case e'_7
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
e_4✝ : X = (pair X Y).obj { as := WalkingPair.left }
⊢ 0 = HasZeroObject.zeroIsInitial.to ((pair X Y).obj { as := WalkingPair.left })

case e'_8
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
e_5✝ : Y = (pair X Y).obj { as := WalkingPair.right }
⊢ 0 = HasZeroObject.zeroIsInitial.to ((pair X Y).obj { as := WalkingPair.right })
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout b.inr 0 b.fst 0

Tactic:
by
  refine of_top ?_ (by simp) (of_isBilimit h)
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫
        LaxMonoidal.μ L' (X ⊗ Y) Z ≫
          L'.map (α_ X Y Z).hom ≫ OplaxMonoidal.δ L' X (Y ⊗ Z) ≫ L'.obj X ◁ OplaxMonoidal.δ L' Y Z) ≫
      ((braidingNatIso L W ε).hom.app (L'.obj X)).app (L'.obj Y ⊗ L'.obj Z) ≫
        LaxMonoidal.μ L' Y Z ▷ L'.obj X ≫
          LaxMonoidal.μ L' (Y ⊗ Z) X ≫
            L'.map (α_ Y Z X).hom ≫ OplaxMonoidal.δ L' Y (Z ⊗ X) ≫ L'.obj Y ◁ OplaxMonoidal.δ L' Z X =
    ((((LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫ LaxMonoidal.μ L' (X ⊗ Y) Z ≫ L'.map ((β_ X Y).hom ▷ Z)) ≫
            L'.map (α_ Y X Z).hom) ≫
          OplaxMonoidal.δ L' Y (X ⊗ Z)) ≫
        L'.obj Y ◁ OplaxMonoidal.δ L' X Z) ≫
      L'.obj Y ◁ ((LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom) ≫ OplaxMonoidal.δ L' Z X)

Tactic:
slice_lhs 6 7 =>
    rw [braidingNatIso_hom_app_naturality_μ_left, braidingNatIso_hom_app]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫
      LaxMonoidal.μ L' (X ⊗ Y) Z ≫
        L'.map (α_ X Y Z).hom ≫
          OplaxMonoidal.δ L' X (Y ⊗ Z) ≫
            L'.obj X ◁ OplaxMonoidal.δ L' Y Z ≫
              ((((L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
                        LaxMonoidal.μ L' X (Y ⊗ Z) ≫ L'.map (β_ X (Y ⊗ Z)).hom ≫ OplaxMonoidal.δ L' (Y ⊗ Z) X) ≫
                      LaxMonoidal.μ L' (Y ⊗ Z) X) ≫
                    L'.map (α_ Y Z X).hom) ≫
                  OplaxMonoidal.δ L' Y (Z ⊗ X)) ≫
                L'.obj Y ◁ OplaxMonoidal.δ L' Z X =
    ((((LaxMonoidal.μ L' X Y ▷ L'.obj Z ≫ LaxMonoidal.μ L' (X ⊗ Y) Z ≫ L'.map ((β_ X Y).hom ▷ Z)) ≫
            L'.map (α_ Y X Z).hom) ≫
          OplaxMonoidal.δ L' Y (X ⊗ Z)) ≫
        L'.obj Y ◁ OplaxMonoidal.δ L' X Z) ≫
      L'.obj Y ◁ ((LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom) ≫ OplaxMonoidal.δ L' Z X)