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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
    ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom

Tactic:
dsimp only [comp_app, comp_naturality]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫
      (α_ (η.app a) (θ.app a ≫ ι.app a) (I.map f)).hom ≫
        η.app a ◁
            ((α_ (θ.app a) (ι.app a) (I.map f)).hom ≫
              θ.app a ◁ ι.naturality f ≫
                (α_ (θ.app a) (H.map f) (ι.app b)).inv ≫
                  θ.naturality f ▷ ι.app b ≫ (α_ (G.map f) (θ.app b) (ι.app b)).hom) ≫
          (α_ (η.app a) (G.map f) (θ.app b ≫ ι.app b)).inv ≫
            η.naturality f ▷ (θ.app b ≫ ι.app b) ≫ (α_ (F.map f) (η.app b) (θ.app b ≫ ι.app b)).hom =
    ((α_ (η.app a ≫ θ.app a) (ι.app a) (I.map f)).hom ≫
        (η.app a ≫ θ.app a) ◁ ι.naturality f ≫
          (α_ (η.app a ≫ θ.app a) (H.map f) (ι.app b)).inv ≫
            ((α_ (η.app a) (θ.app a) (H.map f)).hom ≫
                  η.app a ◁ θ.naturality f ≫
                    (α_ (η.app a) (G.map f) (θ.app b)).inv ≫
                      η.naturality f ▷ θ.app b ≫ (α_ (F.map f) (η.app b) (θ.app b)).hom) ▷
                ι.app b ≫
              (α_ (F.map f) (η.app b ≫ θ.app b) (ι.app b)).hom) ≫
      F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
dsimp only [comp_app, comp_naturality]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫
      (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        η.naturality f ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫ (η ≫ θ ≫ ι).naturality f =
    ((η ≫ θ) ≫ ι).naturality f ≫ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom

Tactic:
dsimp only [comp_app, comp_naturality]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f ≫
      (α_ (η.app a) (θ.app a ≫ ι.app a) (I.map f)).hom ≫
        η.app a ◁
            ((α_ (θ.app a) (ι.app a) (I.map f)).hom ≫
              θ.app a ◁ ι.naturality f ≫
                (α_ (θ.app a) (H.map f) (ι.app b)).inv ≫
                  θ.naturality f ▷ ι.app b ≫ (α_ (G.map f) (θ.app b) (ι.app b)).hom) ≫
          (α_ (η.app a) (G.map f) (θ.app b ≫ ι.app b)).inv ≫
            η.naturality f ▷ (θ.app b ≫ ι.app b) ≫ (α_ (F.map f) (η.app b) (θ.app b ≫ ι.app b)).hom =
    ((α_ (η.app a ≫ θ.app a) (ι.app a) (I.map f)).hom ≫
        (η.app a ≫ θ.app a) ◁ ι.naturality f ≫
          (α_ (η.app a ≫ θ.app a) (H.map f) (ι.app b)).inv ≫
            ((α_ (η.app a) (θ.app a) (H.map f)).hom ≫
                  η.app a ◁ θ.naturality f ≫
                    (α_ (η.app a) (G.map f) (θ.app b)).inv ≫
                      η.naturality f ▷ θ.app b ≫ (α_ (F.map f) (η.app b) (θ.app b)).hom) ▷
                ι.app b ≫
              (α_ (F.map f) (η.app b ≫ θ.app b) (ι.app b)).hom) ≫
      F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫ (θ ≫ ι).naturality f = (η ≫ ι).naturality f ≫ Γ.as.app a ▷ ι.app a ▷ H.map f

Tactic:
dsimp only [comp_app, comp_naturality]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ F.map f ◁ Γ.as.app b ▷ ι.app b ≫
      (α_ (F.map f) (θ.app b) (ι.app b)).inv ≫
        θ.naturality f ▷ ι.app b ≫
          (α_ (θ.app a) (G.map f) (ι.app b)).hom ≫ θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv) ≫
      Γ.as.app a ▷ ι.app a ▷ H.map f
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom ≫ (η ≫ θ ≫ ι).naturality f =
    ((η ≫ θ) ≫ ι).naturality f ≫ (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f

Tactic:
dsimp only [comp_app, comp_naturality]

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ : G ⟶ H
ι : H ⟶ I
a b : B
f : a ⟶ b
⊢ F.map f ◁ (α_ (η.app b) (θ.app b) (ι.app b)).hom ≫
      (α_ (F.map f) (η.app b) (θ.app b ≫ ι.app b)).inv ≫
        η.naturality f ▷ (θ.app b ≫ ι.app b) ≫
          (α_ (η.app a) (G.map f) (θ.app b ≫ ι.app b)).hom ≫
            η.app a ◁
                ((α_ (G.map f) (θ.app b) (ι.app b)).inv ≫
                  θ.naturality f ▷ ι.app b ≫
                    (α_ (θ.app a) (H.map f) (ι.app b)).hom ≫
                      θ.app a ◁ ι.naturality f ≫ (α_ (θ.app a) (ι.app a) (I.map f)).inv) ≫
              (α_ (η.app a) (θ.app a ≫ ι.app a) (I.map f)).inv =
    ((α_ (F.map f) (η.app b ≫ θ.app b) (ι.app b)).inv ≫
        ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
              η.naturality f ▷ θ.app b ≫
                (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
                  η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ▷
            ι.app b ≫
          (α_ (η.app a ≫ θ.app a) (H.map f) (ι.app b)).hom ≫
            (η.app a ≫ θ.app a) ◁ ι.naturality f ≫ (α_ (η.app a ≫ θ.app a) (ι.app a) (I.map f)).inv) ≫
      (α_ (η.app a) (θ.app a) (ι.app a)).hom ▷ I.map f
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
X✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (hom (limit.π (F ⋙ objects) Y✝)) X = (F.map f).toFunctor.obj ((hom (limit.π (F ⋙ objects) X✝)) X)

Tactic:
exact (congr_hom (limit.w (F ⋙ Cat.objects) f) X).symm

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
h : (hom (limit.π (F ⋙ objects) x✝¹)) X ⟶ (hom (limit.π (F ⋙ objects) x✝¹)) Y
this : Category.{v, v} (objects.obj (F.obj Z)) := inferInstance
⊢ (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

Tactic:
simp [Functor.congr_hom congr($(F.map_comp f g).toFunctor) h, eqToHom_map]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (f ⊗ₘ g)

Tactic:
rw [tensorHom_def]
  exact comp_mem _ _ _ (whiskerRight_mem _ _ hf _) (whiskerLeft_mem _ _ _ hg)

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
a b : α
hg :
  (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    ((pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a)) ≫ g₂) ≫
      Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b

Tactic:
rw [(Category.assoc _ _ g₂), pullback.condition] at hg

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
a b : α
hg :
  (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    (pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ Sigma.ι X b) ≫ Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
⊢ φ ≫ φ' = 𝟙 a

Tactic:
have h₁ : IsHomLift p (𝟙 (p.obj a)) (φ ≫ φ') := by
    rw [← IsIso.hom_inv_id (p.map φ)]
    apply IsHomLift.comp

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
⊢ φ ≫ φ' = 𝟙 a
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
⊢ IsFiltered (Grothendieck F)

Tactic:
have : Nonempty (Grothendieck F) := by
    obtain ⟨c⟩ : Nonempty C := IsFiltered.nonempty
    obtain ⟨f⟩ : Nonempty (F.obj c) := IsFiltered.nonempty
    exact ⟨⟨c, f⟩⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFiltered C
inst✝ : ∀ (c : C), IsFiltered ↑(F.obj c)
this : Nonempty (Grothendieck F)
⊢ IsFiltered (Grothendieck F)
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
X Y : C
w : X ⟶ Y
hw : W w
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ F.HasPointwiseLeftDerivedFunctorAt W Y

Tactic:
simp only [F.hasPointwiseLeftDerivedFunctorAt_iff W.Q W]
  exact hasPointwiseRightKanExtensionAt_iff_of_iso W.Q F (Localization.isoOfHom W.Q W w hw)

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : PreGaloisCategory C
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ HasColimitsOfShape (SingleObj G) C

Tactic:
by
  obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.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 : C
⊢ Nonempty (IsInitial X) ↔ IsEmpty (F.obj X).obj

Tactic:
(IsInitial.isInitialIffObj F X).nonempty_congr

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X : C
⊢ Nonempty (IsInitial (F.obj X)) ↔ IsEmpty (F.obj X).obj
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ HasColimitsOfShape (SingleObj G) FintypeCat

Tactic:
by
  obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

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

Goal state before:
pp: case intro
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
ι : Type u_1
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), Nonempty (F.obj (X i)).obj
val✝ : Fintype ι
⊢ Nonempty (F.obj (∏ᶜ X)).obj

Tactic:
let f (i : ι) : FintypeCat.{w} := F.obj (X i)

Goal state after:
case intro
C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
ι : Type u_1
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), Nonempty (F.obj (X i)).obj
val✝ : Fintype ι
f : ι → FintypeCat := fun i ↦ F.obj (X i)
⊢ Nonempty (F.obj (∏ᶜ X)).obj
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ ((IsLimit.lift h fun i ↦
          WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
            (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
            (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯) ≫
        bc.fst) ≫
      c₁.proj val✝ =
    s.proj (Sum.inl val✝)

Tactic:
h.fac

Goal state after:
case inl
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₁
⊢ (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯).π.app
        { as := WalkingPair.left } ≫
      c₁.proj val✝ =
    s.proj (Sum.inl val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ ((IsLimit.lift h fun i ↦
          WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
            (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
            (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯) ≫
        bc.snd) ≫
      c₂.proj val✝ =
    s.proj (Sum.inr val✝)

Tactic:
h.fac

Goal state after:
case inr
C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val✝ : ι₂
⊢ (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.rec c₁.pt c₂.pt i))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) i ⋯).π.app
        { as := WalkingPair.right } ≫
      c₂.proj val✝ =
    s.proj (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inl
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₂)
val✝ : ι₁
⊢ (c₁.inj val✝ ≫
      bc.inl ≫
        IsColimit.desc h fun i ↦
          WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯) =
    s.inj (Sum.inl val✝)

Tactic:
h.fac

Goal state after:
case inl
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₂)
val✝ : ι₁
⊢ c₁.inj val✝ ≫
      (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯).ι.app
        { as := WalkingPair.left } =
    s.inj (Sum.inl val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: case inr
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₂)
val✝ : ι₂
⊢ (c₂.inj val✝ ≫
      bc.inr ≫
        IsColimit.desc h fun i ↦
          WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
            (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯) =
    s.inj (Sum.inr val✝)

Tactic:
h.fac

Goal state after:
case inr
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₂)
val✝ : ι₂
⊢ c₂.inj val✝ ≫
      (mk s.pt fun i ↦
              WalkingPair.rec (motive := fun t ↦ i = t → (WalkingPair.rec c₁.pt c₂.pt i ⟶ s.pt))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₁ fun a ↦ s.inj (Sum.inl a))
                (fun h ↦ ⋯ ▸ IsColimit.desc h₂ fun a ↦ s.inj (Sum.inr a)) i ⋯).ι.app
        { as := WalkingPair.right } =
    s.inj (Sum.inr val✝)
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case convert_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 (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map ((Pi.map' ⇑(fiberPerm h b) fun x ↦ 𝟙 X) ≫ Pi.π (fun x ↦ X) t))) (mkSelfProdFib F X)

Tactic:
Pi.map'_comp_π,

Goal state after:
case convert_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 (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) ((fiberPerm h b) t) ≫ 𝟙 X))) (mkSelfProdFib F 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
X : C
inst✝ : IsGalois X
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).obj

Tactic:
refine ⟨fun x y ↦ ?_⟩
  obtain ⟨(φ : Aut X), h⟩ := MulAction.IsPretransitive.exists_smul_eq (M := Aut X) x y
  obtain ⟨a, ha⟩ := AutGalois.π_surjective F ⟨X, x, inferInstance⟩ φ
  use (autMulEquivAutGalois F).symm ⟨a⟩
  simpa [mulAction_def, ha]

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝¹ : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this✝ : ∀ (i : ι), DiscreteTopology (f i).V.obj
this : ∀ (i : ι), ContinuousSMul G (f i).V.obj
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)

Tactic:
have (i : ι) : ∃ (U : OpenSubgroup (G)), (Nonempty ((f i) ≅ G ⧸ₐ U.toSubgroup)) := by
    obtain ⟨(x : (f i).V)⟩ := nonempty_fiber_of_isConnected (forget₂ _ _) (f i)
    let U : OpenSubgroup (G) := ⟨MulAction.stabilizer (G) x, stabilizer_isOpen (G) x⟩
    exact ⟨U, ⟨FintypeCat.isoQuotientStabilizerOfIsConnected (f i) x⟩⟩

Goal state after:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝² : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this✝¹ : ∀ (i : ι), DiscreteTopology (f i).V.obj
this✝ : ∀ (i : ι), ContinuousSMul G (f i).V.obj
this : ∀ (i : ι), ∃ U, Nonempty (f i ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑U)))
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp.mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
h : S.IsWide
x : C
⊢ x ∈ S.objs

Tactic:
apply mem_objs_of_src S (h.wide x)

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

Goal state before:
pp: case neg
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
h : ¬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 := ⋯ } =
    0

Tactic:
· 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.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
a✝ b✝ c✝ : Cat
f✝ g✝ : a✝ ⟶ b✝
η✝ : f✝ ⟶ g✝
h✝ : b✝ ⟶ c✝
⊢ NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (η✝ ▷ h✝).toNatTrans) =
    (Cat.Hom.isoMk (mapCompRight C f✝.toFunctor h✝.toFunctor)).hom ≫
      NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) η✝.toNatTrans) ▷ (mapPair (𝟭 C) h✝.toFunctor).toCatHom ≫
        (Cat.Hom.isoMk (mapCompRight C g✝.toFunctor h✝.toFunctor)).inv

Tactic:
exact congr($(mapWhiskerLeft_whiskerRight C _ _).toCatHom₂)

Goal state after: