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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    Quot.map (Hom₂.whisker_right (g ≫ h)) ⋯ η =
      { hom := Quot.mk Rel (Hom₂.associator f g h), inv := Quot.mk Rel (Hom₂.associator_inv f g h), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.inv ≫
        Quot.map (Hom₂.whisker_right h) ⋯ (Quot.map (Hom₂.whisker_right g) ⋯ η) ≫
          { hom := Quot.mk Rel (Hom₂.associator f' g h), inv := Quot.mk Rel (Hom₂.associator_inv f' g h),
              hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom

Tactic:
rintro a b c d f f' ⟨η⟩ g h

Goal state after:
case mk
B : Type u
inst✝ : Quiver B
a b c d : FreeBicategory B
f f' : a ⟶ b
η✝ : f ⟶ f'
η : Hom₂ f f'
g : b ⟶ c
h : c ⟶ d
⊢ Quot.map (Hom₂.whisker_right (g ≫ h)) ⋯ (Quot.mk Rel η) =
    { hom := Quot.mk Rel (Hom₂.associator f g h), inv := Quot.mk Rel (Hom₂.associator_inv f g h), hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.inv ≫
      Quot.map (Hom₂.whisker_right h) ⋯ (Quot.map (Hom₂.whisker_right g) ⋯ (Quot.mk Rel η)) ≫
        { hom := Quot.mk Rel (Hom₂.associator f' g h), inv := Quot.mk Rel (Hom₂.associator_inv f' g h), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : { of := m X✝.of }.of
⊢ (ConcreteCategory.hom { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso }.iso.hom).toFun x✝ =
    (ConcreteCategory.hom
          ({ iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso } ≫
                { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso }).iso.hom).toFun
      x✝

Tactic:
simp [Equiv.toIso, EquivFunctor.map_trans']

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u

Tactic:
← rightZigzag,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ t.lift ◁ rightZigzag t.unit ε ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
⊢ ∀ {X Y Z : (i : I) × C i} (f : X ⟶ Y) (g : Y ⟶ Z), descMap F X Z (f ≫ g) = descMap F X Y f ≫ descMap F Y Z g

Tactic:
by
    rintro ⟨i, X⟩ ⟨_, Y⟩ ⟨_, Z⟩ ⟨f⟩ ⟨g⟩
    apply (F i).map_comp

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ SigmaHom.mk ((F ⟨i, X⟩.fst).map f ≫ (α ⟨i, Y✝⟩.fst).app ⟨i, Y✝⟩.snd) =
    SigmaHom.mk ((α ⟨i, X⟩.fst).app ⟨i, X⟩.snd ≫ (G ⟨i, X⟩.fst).map f)

Tactic:
(α i).naturality

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ SigmaHom.mk ((α i).app ⟨i, X⟩.snd ≫ (G i).map f) = SigmaHom.mk ((α ⟨i, X⟩.fst).app ⟨i, X⟩.snd ≫ (G ⟨i, X⟩.fst).map f)
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X✝ : Type u
C✝ : Cat
C : Cat
X : Type u
⊢ (connectedComponents.obj C ⟶ X) ≃ (C ⟶ typeToCat.obj X)

Tactic:
refine TypeCat.homEquiv.trans ?_
      exact (ConnectedComponents.typeToCatHomEquiv _ _).trans
        (Functor.equivCatHom _ _)

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

Goal state before:
pp: X✝ Y✝ : Type u_1
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : typeToPartialFun.map a₁✝ = typeToPartialFun.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext x
    exact congrFun (PFun.lift_injective h) x

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
⊢ (f.comp g).Dom = g.preimage f.Dom

Tactic:
ext
  simp
  grind

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 y z : (ForgetEnrichment V C)ᵒᵖ
f : x ⟶ y
g : y ⟶ z
⊢ (f ≫ g).unop = f.unop ≫ g.unop

Tactic:
by
    have : g.unop ≫ f.unop = homTo V (g.unop ≫ f.unop) := rfl
    dsimp
    rw [this, ForgetEnrichment.homTo_comp, Category.assoc, unitors_inv_equal,
      ← leftUnitor_inv_braiding_assoc]
    have : (β_ _ _).hom ≫ (homTo V g.unop ⊗ₘ homTo V f.unop) ≫
      eComp V («to» V z.unop) («to» V y.unop) («to» V x.unop) =
      ((homTo V f.unop) ⊗ₘ (homTo V g.unop)) ≫ eComp V x y z := (tensorHom_eComp_op_eq V _ _).symm
    rw [this, ← Category.assoc]
    congr 1

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
hab : a = b
R : 𝒮
hR : p.obj a = R
⊢ p.IsHomLift (𝟙 R) (eqToHom hab)

Tactic:
subst hR hab; simp

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
⊢ IsCartesian.map p f φ (ψ ≫ φ'.inv) ≫ φ ≫ φ'.hom = ψ

Tactic:
by simp only [fac_assoc, assoc, Iso.inv_hom_id, comp_id]

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₂
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂ =
    𝟙 (enrichedHom V F₁ F₂)

Tactic:
ext j
  rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def, assoc,
    ← comp_whiskerRight_assoc, enrichedId_π, ← whisker_exchange_assoc,
    id_whiskerLeft, assoc, assoc, Iso.inv_hom_id_assoc]
  dsimp
  rw [e_id_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Fiber

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p✝ : 𝒳 ⥤ 𝒮
S✝ : 𝒮
p : 𝒳 ⥤ 𝒮
S : 𝒮
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ 𝒳
hF : F ⋙ p = (const C).obj S
X✝ Y✝ : C
φ : X✝ ⟶ Y✝
⊢ p.map (F.map φ) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ 𝟙 S

Tactic:
by simpa using (eqToIso hF).hom.naturality φ

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsLeftDerivedFunctor α W ↔ LF.IsRightKanExtension α

Tactic:
constructor
  · exact fun _ => IsLeftDerivedFunctor.isRightKanExtension LF α W
  · exact fun h => ⟨h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ L₁.map (adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app X₂

Tactic:
adj.right_triangle_components,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ L₁.map (𝟙 (F.obj X₂)) ≫ β.app X₂ = β.app X₂
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
⊢ ∃ g, g • x = y

Tactic:
let T : Set X.V := MulAction.orbit G x
    have : Fintype T := Fintype.ofFinite T
    let : MulAction G (FintypeCat.of T) := inferInstanceAs <| MulAction G
      ↑(MulAction.orbit G x)
    let T' : Action FintypeCat G := Action.FintypeCat.ofMulAction G (FintypeCat.of T)
    let i : T' ⟶ X := ⟨FintypeCat.homMk Subtype.val, fun _ ↦ rfl⟩
    have : Mono i := ConcreteCategory.mono_of_injective _ (Subtype.val_injective)
    have : IsIso i := by
      apply IsConnected.noTrivialComponent T' i
      apply (not_initial_iff_fiber_nonempty (Action.forget _ _) T').mpr
      exact Set.Nonempty.coe_sort (MulAction.nonempty_orbit x)
    have hb : Function.Bijective i.hom := by
      apply (ConcreteCategory.isIso_iff_bijective i.hom).mp
      exact map_isIso (forget₂ _ FintypeCat) i
    obtain ⟨⟨y', ⟨g, (hg : g • x = y')⟩⟩, (hy' : y' = y)⟩ := hb.surjective y
    use g
    exact hg.trans hy'

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
A X : C
inst✝ : IsConnected A
a : (F.obj A).obj
f g : A ⟶ X
⊢ (fun f ↦ (ConcreteCategory.hom (F.map f)) a) f = (fun f ↦ (ConcreteCategory.hom (F.map f)) a) g → f = g

Tactic:
(h : F.map f a = F.map g a)

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).obj
f g : A ⟶ X
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) a
⊢ f = g
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ Aut B

pp: case refine_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ (fun τ ↦ f ≫ τ.hom = σ.hom ≫ f) ?refine_1

pp: case refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∀ (y : Aut B), (fun τ ↦ f ≫ τ.hom = σ.hom ≫ f) y → y = ?refine_1

Tactic:
· exact (evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)

Goal state after:
case refine_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ (fun τ ↦ f ≫ τ.hom = σ.hom ≫ f)
    ((evaluationEquivOfIsGalois F B ((ConcreteCategory.hom (F.map f)) a)).symm
      ((ConcreteCategory.hom (F.map (σ.hom ≫ f))) a))

case refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).obj
⊢ ∀ (y : Aut B),
    (fun τ ↦ f ≫ τ.hom = σ.hom ≫ f) y →
      y =
        (evaluationEquivOfIsGalois F B ((ConcreteCategory.hom (F.map f)) a)).symm
          ((ConcreteCategory.hom (F.map (σ.hom ≫ f))) a)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan f₁
c₂ : Cofan f₂
bc : BinaryCofan c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
w : ι₁ ⊕ ι₂
⊢ ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj w ≫
      IsColimit.desc h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (WalkingPair.casesOn i c₁.pt c₂.pt ⟶ s.pt)) i
          (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) ⋯) =
    s.inj w

Tactic:
cases w <;>
      · simp only [cofan_mk_inj, combPairHoms, Category.assoc]
        erw [h.fac]
        simp only [Cofan.mk_ι_app, Cofan.IsColimit.fac]

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) ((ConcreteCategory.hom (F.map u)) b) =
    (ConcreteCategory.hom (F.map (selfProdProj u t))) b

Tactic:
simp only [selfProdProj, map_comp, FintypeCat.comp_apply]; rfl

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F✝ : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F✝
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : ContAction FintypeCat (Aut F)
⊢ (functorToContAction F).essImage X

Tactic:
have : ContinuousSMul (Aut F) X.obj.V := X.2

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F✝ : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F✝
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : ContAction FintypeCat (Aut F)
this : ContinuousSMul (Aut F) X.obj.V.obj
⊢ (functorToContAction F).essImage X
Module: Mathlib.CategoryTheory.Generator.Type

Goal state before:
pp: X Y : Type u
f g : X ⟶ Y
h : ∀ (G : Type u), ObjectProperty.singleton PUnit.{u + 1} G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
x : X
⊢ (ConcreteCategory.hom f).toFun x = (ConcreteCategory.hom g).toFun x

Tactic:
exact ConcreteCategory.congr_hom (h PUnit (by simp) (↾fun _ ↦ x))
    .unit

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
⊢ { f := biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p, comm := ⋯ } ≫
      { f := (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j', comm := ⋯ } =
    if h : j = j' then eqToHom ⋯ else 0

Tactic:
split_ifs with h
    · subst h
      simp only [biproduct.ι_map, biproduct.bicone_π, biproduct.map_π, eqToHom_refl,
        id_f, hom_ext_iff, comp_f, assoc, bicone_ι_π_self_assoc, idem]
    · dsimp
      simp only [biproduct.ι_map, biproduct.map_π, hom_ext_iff, comp_f,
        assoc, biproduct.ι_π_ne_assoc _ h, zero_comp, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ P.decompId_i ≫ P.complement.decompId_p = 0

Tactic:
simp only [zero_def, hom_ext_iff, complement_X, comp_f,
          decompId_i_f, decompId_p_f, complement_p, comp_sub, comp_id, idem, sub_self]

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

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
this : d' ∈ (im φ hφ).objs
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'

Tactic:
mem_im_objs_iff

Goal state after:
case refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
this : ∃ c, φ.obj c = d'
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝² : Cocone (pair F G)
x✝¹ : (binaryCoproductCocone F G).pt ⟶ x✝².pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x✝¹ = x✝².ι.app j
x✝ : C
x : (binaryCoproductCocone F G).pt.obj x✝
⊢ (hom (x✝¹.app x✝)).toFun x = (hom ((coprod.desc (BinaryCofan.inl x✝²) (BinaryCofan.inr x✝²)).app x✝)).toFun x

Tactic:
cases x with | _ => simp [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]

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

Goal state before:
pp: case refine_4
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), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst
hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
k : J
⊢ (m ≫ ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }).π.app k) ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k).hom.app i =
    { pt := s.1,
              π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }.π.app
        k ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k).hom.app i

Tactic:
simpa [← NatTrans.comp_app]

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

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ 2 ^ α ≤ #(X ⟶ yp)

Tactic:
apply le_trans (Cardinal.power_le_power_right z)

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(X ⟶ Y) ^ α ≤ #(X ⟶ yp)
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
X : Type (max w u)
f : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j
x : chosenCoend F
x✝¹ x✝ : (j : J) × (F.obj (op j)).obj j
h : Types.coendRel F x✝¹ x✝
⊢ (hom (f x✝¹.fst)) x✝¹.snd = (hom (f x✝.fst)) x✝.snd

Tactic:
by
        cases h with | mk f x => exact ConcreteCategory.congr_hom (hf f) _

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

Goal state before:
pp: case tensorHom_def
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X₁✝ Y₁✝ X₂✝ Y₂✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ (f✝.tensor g✝) = projectMapAux f✝¹ ((f✝.whiskerRight X₂✝).comp (Hom.whiskerLeft Y₁✝ g✝))

Tactic:
| tensorHom_def _ _ =>

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f ≫ 𝟙 Y = g
⊢ f = g

Tactic:
by
  simpa using w

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g ≫ 𝟙 Y
⊢ f = g

Tactic:
by
  simpa using w

Goal state after:
Module: Mathlib.CategoryTheory.Monad.EquivMon

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M : Mon (C ⥤ C)
X : C
⊢ M.X.map (μ.app X) ≫ μ.app X = μ.app (M.X.obj X) ≫ μ.app X

Tactic:
by
    simpa [-MonObj.mul_assoc] using! congrArg (fun t ↦ t.app X) (mul_assoc M.X)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.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
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝² x✝¹ : D
x✝ : x✝² ⟶ x✝¹
⊢ { obj := fun y ↦ X✝ ⊙ₗ y, map := fun {X Y} f ↦ X✝ ⊴ₗ f, map_id := ⋯, map_comp := ⋯ }.map x✝ ≫ f ⊵ₗ x✝¹ =
    f ⊵ₗ x✝² ≫ { obj := fun y ↦ Y✝ ⊙ₗ y, map := fun {X Y} f ↦ Y✝ ⊴ₗ f, map_id := ⋯, map_comp := ⋯ }.map x✝

Tactic:
simp [action_exchange]

Goal state after: