mathlib-initiative/mathlib-tactics huggingface dataset:
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
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasFunctorEnrichedHom V F₁ F₂
inst✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
k : Under j'
⊢ (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))) ≫
      enrichedComp V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃) ≫
        end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k =
    enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)) ≫
        end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k

Tactic:
enrichedComp_π

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
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasFunctorEnrichedHom V F₁ F₂
inst✝¹ : HasFunctorEnrichedHom V F₂ F₃
inst✝ : HasFunctorEnrichedHom V F₁ F₃
j j' : J
f : j ⟶ j'
k : Under j'
⊢ (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))) ≫
      (end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂)) k ⊗ₘ
          end_.π (diagram V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)) k) ≫
        eComp V (Opposite.unop ((Under.forget j' ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j' ⋙ F₂).obj k)
          ((Under.forget j' ⋙ F₃).obj k) =
    enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)) ≫
        end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k
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₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫
        enrichedComp V F₁ F₂ F₃ ≫
          enrichedHomπ V F₁ F₃ ((Under.forget j).obj k) ≫
            eHomWhiskerRight V ((Iso.refl (Under.forget j ⋙ F₁)).inv.app k) (F₃.obj ((Under.forget j).obj k)) ≫
              eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj k) ((Iso.refl (Under.forget j ⋙ F₃)).hom.app k) =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗ₘ
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ≫
          end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k

Tactic:
enrichedComp_π

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₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ⊗ₘ (homEquiv V) g) ≫
        enrichedComp V F₁ F₂ F₃ ≫
          enrichedHomπ V F₁ F₃ ((Under.forget j).obj k) ≫
            eHomWhiskerRight V ((Iso.refl (Under.forget j ⋙ F₁)).inv.app k) (F₃.obj ((Under.forget j).obj k)) ≫
              eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj k) ((Iso.refl (Under.forget j ⋙ F₃)).hom.app k) =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗ₘ
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k ⊗ₘ
            end_.π (diagram V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) k) ≫
          eComp V (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₂).obj k)
            ((Under.forget j ⋙ F₃).obj k)
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₂)) ≫ β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) = β.app X₂

Tactic:
← eq₃,

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 (adj.unit.app (F.obj X₂)) ≫ L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app 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 : AutGalois F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom
        (F.map
          ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ })
              (MulOpposite.unop ((autMulEquivAutGalois F) ((autMulEquivAutGalois F).symm { unop' := x })))).hom))
      a =
    (ConcreteCategory.hom (F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom)) a

Tactic:
MulEquiv.apply_symm_apply

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
x : AutGalois F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom
        (F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop { unop' := x })).hom))
      a =
    (ConcreteCategory.hom (F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom)) a
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
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i ↦ F.obj (X i)).obj ≃ ((i : ι) → (F.obj (X i)).obj) := FintypeCat.productEquiv fun i ↦ F.obj (X i)
px : (F.obj P).obj := (ConcreteCategory.hom is₁.inv) (is₂.symm x)
hpx : ∀ (i : ι), (ConcreteCategory.hom (F.map (Pi.π X i))) px = x i
A : C
f : A ⟶ P
a : (F.obj A).obj
left✝ : IsGalois A
hfa : (ConcreteCategory.hom (F.map f)) a = px
g : G
hg : ∀ (x : (F.obj A).obj), g • x = (ConcreteCategory.hom (t.hom.app A)) x
i : ι
y : (F.obj (X i)).obj
⊢ g • x i = (ConcreteCategory.hom (t.hom.app (X i))) (x i)

Tactic:
← hpx i,

Goal state after:
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
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i ↦ F.obj (X i)).obj ≃ ((i : ι) → (F.obj (X i)).obj) := FintypeCat.productEquiv fun i ↦ F.obj (X i)
px : (F.obj P).obj := (ConcreteCategory.hom is₁.inv) (is₂.symm x)
hpx : ∀ (i : ι), (ConcreteCategory.hom (F.map (Pi.π X i))) px = x i
A : C
f : A ⟶ P
a : (F.obj A).obj
left✝ : IsGalois A
hfa : (ConcreteCategory.hom (F.map f)) a = px
g : G
hg : ∀ (x : (F.obj A).obj), g • x = (ConcreteCategory.hom (t.hom.app A)) x
i : ι
y : (F.obj (X i)).obj
⊢ g • (ConcreteCategory.hom (F.map (Pi.π X i))) px =
    (ConcreteCategory.hom (t.hom.app (X i))) ((ConcreteCategory.hom (F.map (Pi.π X i))) px)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ ∀ {X Y : Symmetrify V} (f : X ⟶ Y),
    (Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (reverse f) =
      reverse ((Paths.of (Symmetrify V) ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)

Tactic:
rintro X Y f
    simp only [← Functor.toPrefunctor_comp, Prefunctor.comp_map, Paths.of_map]
    change Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
      Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
    have := Functor.map_inv Φ ((Quotient.functor redStep).toPrefunctor.map f.toPath)
    convert! this <;> simp only [Groupoid.inv_eq_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Category.{v_2, u_1} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenCoendsOfShape J C
G H : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
g : G ⟶ H
⊢ map f ≫ map g = map (f ≫ g)

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Chosen.End

Goal state before:
pp: J : Type u_3
C : Type u_4
inst✝² : Category.{v_3, u_4} C
inst✝¹ : Category.{v_4, u_3} J
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : ChosenEndsOfShape J C
G H : Jᵒᵖ ⥤ J ⥤ C
f : F ⟶ G
g : G ⟶ H
⊢ map f ≫ map g = map (f ≫ g)

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : C ⥤ Type u
f : F ⟶ G
H : MonoFactorisation f
X Y : C
g : X ⟶ Y
⊢ ((monoFactorisation f).I.map g ≫
      ↾fun x ↦
        match x with
        | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app Y)) (Exists.choose hx)) =
    (↾fun x ↦
        match x with
        | ⟨x, hx⟩ => (ConcreteCategory.hom (H.e.app X)) (Exists.choose hx)) ≫
      H.I.map g

Tactic:
by
      ext
      apply injective_of_mono (H.m.app Y)
      simp
      grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type t
inst✝ : HasProductsOfShape α C
⊢ powerMap (𝟙 U) α = 𝟙 (U.power α)

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type t
inst✝ : HasProductsOfShape α C
⊢ U.mapPower id = 𝟙 (U.power α)

Tactic:
by
  cat_disch

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 : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x y z : C ⋆ D
f : x ⟶ y
g : y ⟶ z
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (f ≫ g) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) f ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) g

Tactic:
cases f <;> cases g
    · simp [← Functor.map_comp]
    · case left.edge f d => simpa using! (α.naturality <| (Prod.sectL _ d).map f).symm
    · simp [← Functor.map_comp]
    · case edge.right c _ _ f => simpa using! α.naturality <| (Prod.sectR c _).map f

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ₗ Hₗ : C ⥤ E
α : Fₗ ⟶ Gₗ
β : Gₗ ⟶ Hₗ
H : D ⥤ E'
⊢ mapWhiskerRight (α ≫ β) H = mapWhiskerRight α H ≫ mapWhiskerRight β H

Tactic:
by
  cat_disch

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ₗ : C ⥤ E
H : D ⥤ E'
⊢ mapWhiskerRight (𝟙 Fₗ) H = 𝟙 (mapPair Fₗ H)

Tactic:
by
  cat_disch

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ᵣ Hᵣ : D ⥤ E'
H : C ⥤ E
α : Fᵣ ⟶ Gᵣ
β : Gᵣ ⟶ Hᵣ
⊢ mapWhiskerLeft H (α ≫ β) = mapWhiskerLeft H α ≫ mapWhiskerLeft H β

Tactic:
by
  cat_disch

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'
H : C ⥤ E
Fᵣ : D ⥤ E'
⊢ mapWhiskerLeft H (𝟙 Fᵣ) = 𝟙 (mapPair H Fᵣ)

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.FinCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a : Option C
⊢ (fun x ↦
        match x with
        | of a => some a
        | star => none)
      ((fun x ↦
          match x with
          | some a => of a
          | none => star)
        a) =
    a

Tactic:
by cases a <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.FinCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a : WithTerminal C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        a) =
    a

Tactic:
by cases a <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.FinCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a : WithInitial C
⊢ (fun x ↦
        match x with
        | some a => of a
        | none => star)
      ((fun x ↦
          match x with
          | of a => some a
          | star => none)
        a) =
    a

Tactic:
by cases a <;> simp

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

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝³ : Category.{v_1, u_1} C
X : I → C
P : I → Prop
inst✝² : HasProduct X
inst✝¹ : HasProduct fun i ↦ X ↑i
inst✝ : HasProduct fun i ↦ X ↑i
⊢ HasBinaryProduct (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)

Tactic:
exact ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ = ⋯.lift h.p₁ h.p₂ ⋯

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ = ⋯.lift h.p₂ h.p₃ ⋯

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₃ = ⋯.lift h.p₁ h.p₃ ⋯

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case mk
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
m : (cowedge F).pt ⟶ s.pt
h : ∀ (j : WalkingMultispan (multispanShapeCoend J)), (cowedge F).ι.app j ≫ m = s.ι.app j
x✝ : (cowedge F).pt
j : (j : J) × (F.obj (op j)).obj j
⊢ (hom m).toFun (Quot.mk (coendRel F) j) =
    (hom (↾Quot.lift (fun x ↦ (hom (Multicofork.π s x.fst)) x.snd) ⋯)).toFun (Quot.mk (coendRel F) j)

Tactic:
exact ConcreteCategory.congr_hom (h (.right j.fst)) j.snd

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝¹¹ : Category.{v₁, u₁} A
inst✝¹⁰ : Category.{v₂, u₂} B
inst✝⁹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁸ : Category.{v₄, u₄} A'
inst✝⁷ : Category.{v₅, u₅} B'
inst✝⁶ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁵ : Category.{v₇, u₇} A''
inst✝⁴ : Category.{v₈, u₈} B''
inst✝³ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝² : Category.{v₁₀, u₁₀} A'''
inst✝¹ : Category.{v₁₁, u₁₁} B'''
inst✝ : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
τ : CatCospanTransform F'' G'' F''' G'''
⊢ η ▷ φ.comp τ = (α_ ψ φ τ).inv ≫ η ▷ φ ▷ τ ≫ (α_ ψ' φ τ).hom

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝¹¹ : Category.{v₁, u₁} A
inst✝¹⁰ : Category.{v₂, u₂} B
inst✝⁹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁸ : Category.{v₄, u₄} A'
inst✝⁷ : Category.{v₅, u₅} B'
inst✝⁶ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁵ : Category.{v₇, u₇} A''
inst✝⁴ : Category.{v₈, u₈} B''
inst✝³ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝² : Category.{v₁₀, u₁₀} A'''
inst✝¹ : Category.{v₁₁, u₁₁} B'''
inst✝ : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
⊢ ψ.comp φ ◁ γ = (α_ ψ φ τ).hom ≫ ψ ◁ φ ◁ γ ≫ (α_ ψ φ τ').inv

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝¹⁴ : Category.{v₁, u₁} A
inst✝¹³ : Category.{v₂, u₂} B
inst✝¹² : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝¹¹ : Category.{v₄, u₄} A'
inst✝¹⁰ : Category.{v₅, u₅} B'
inst✝⁹ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁸ : Category.{v₇, u₇} A''
inst✝⁷ : Category.{v₈, u₈} B''
inst✝⁶ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝⁵ : Category.{v₁₀, u₁₀} A'''
inst✝⁴ : Category.{v₁₁, u₁₁} B'''
inst✝³ : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
τ : CatCospanTransform F'' G'' F''' G'''
A'''' : Type u₁₃
B'''' : Type u₁₄
C'''' : Type u₁₅
inst✝² : Category.{v₁₃, u₁₃} A''''
inst✝¹ : Category.{v₁₄, u₁₄} B''''
inst✝ : Category.{v₁₅, u₁₅} C''''
F'''' : A'''' ⥤ B''''
G'''' : C'''' ⥤ B''''
σ : CatCospanTransform F''' G''' F'''' G''''
⊢ (α_ ψ φ τ).hom ▷ σ ≫ (α_ ψ (φ.comp τ) σ).hom ≫ ψ ◁ (α_ φ τ σ).hom = (α_ (ψ.comp φ) τ σ).hom ≫ (α_ ψ φ (τ.comp σ)).hom

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
⊢ (α_ ψ (id F' G') φ).hom ≫ ψ ◁ (λ_ φ).hom = (ρ_ ψ).hom ▷ φ

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ : CatCospanTransform F' G' F'' G''
⊢ (α_ ψ (id F' G') φ).inv ≫ (ρ_ ψ).hom ▷ φ = ψ ◁ (λ_ φ).hom

Tactic:
by
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
W : J ⥤ Type w
F : J ⥤ C
inst✝ : HasWeightedLimit W F
⊢ W.weightedLimObjMap (𝟙 F) = 𝟙 (W.weightedLimObjObj F)

Tactic:
by
  cat_disch

Goal state after: