mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
u : A ⟶ X
v : B ⟶ X
h : (ConcreteCategory.hom (F.map u)) a = (ConcreteCategory.hom (F.map v)) b
⊢ ∃ k f g,
    (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) u =
      (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) v

Tactic:
obtain ⟨⟨Z, z, _⟩, ⟨f, hf⟩, ⟨g, hg⟩, _⟩ :=
      IsFilteredOrEmpty.cocone_objs (C := (PointedGaloisObject F)ᵒᵖ)
        ⟨{ obj := A, pt := a}⟩ ⟨{obj := B, pt := b}⟩

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝² : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝¹ : IsGalois B
u : A ⟶ X
v : B ⟶ X
h : (ConcreteCategory.hom (F.map u)) a = (ConcreteCategory.hom (F.map v)) b
Z : C
z : (F.obj Z).obj
isGalois✝ : IsGalois Z
f :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj
hf :
  (ConcreteCategory.hom (F.map f)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).pt
h✝ : True
g :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).obj
hg :
  (ConcreteCategory.hom (F.map g)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).pt
⊢ ∃ k f g,
    (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) u =
      (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) v
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
⊢ (ConcreteCategory.hom
        (F.map
          (↑(((sectionsFunctor (PointedGaloisObject F)).mapIso (autIsoFibers F)).symm.toEquiv
                  ((endEquivSectionsFibers F) f))
              A).hom))
      A.pt =
    (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
change F.map ((((sectionsFunctor _).map (autIsoFibers F).inv) _).val A).hom A.pt = _

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
        (F.map
          (↑((ConcreteCategory.hom ((sectionsFunctor (PointedGaloisObject F)).map (autIsoFibers F).inv))
                  ((endEquivSectionsFibers F) f))
              A).hom))
      A.pt =
    (ConcreteCategory.hom (f.app A.obj)) A.pt
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 g : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom (f.app A.obj)) ((ConcreteCategory.hom (g.app A.obj)) A.pt) =
    (ConcreteCategory.hom (F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom))
      ((ConcreteCategory.hom (f.app A.obj)) A.pt)

Tactic:
change f.app A (g.app A A.pt) =
    (f.app A ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom) A.pt

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f g : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom (f.app A.obj)) ((ConcreteCategory.hom (g.app A.obj)) A.pt) =
    (ConcreteCategory.hom (f.app A.obj ≫ F.map ((AutGalois.π F A) ((endEquivAutGalois F) g)).hom)) 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
x✝¹ : C
x✝ : (F.obj x✝¹).obj
⊢ 1 • x✝ = (ConcreteCategory.hom ((Iso.hom 1).app x✝¹)) x✝

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : X.HasTensor Y
inst✝² : Y.HasTensor X
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : Y ⟶ Z
⊢ (whiskerLeft X f ≫ fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) =
    (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) ≫ whiskerRight f X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝⁷ : AddCommMonoid I
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝⁴ : BraidedCategory C
inst✝³ : Y.HasTensor Z
inst✝² : Z.HasTensor Y
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : X ⟶ Y
⊢ (whiskerRight f Z ≫ fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (Y i) (Z j)).hom ≫ ιTensorObj Z Y j i k ⋯) =
    (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) ≫ whiskerLeft Z f

Tactic:
cat_disch

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

Goal state before:
pp: case map_id
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
x✝¹ x✝ : Quiver.FreeGroupoid C
f g : x✝¹ ⟶ x✝
this :
  ∀ {X Y : C} (f : X ⟶ Y),
    Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) ⋯ ⋯ =
      φ.toPrefunctor.map f
X✝ : C
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map ((Quiver.FreeGroupoid.of C).map (𝟙 X✝)) =
    (Quiver.FreeGroupoid.lift φ.toPrefunctor).map (𝟙 ((Quiver.FreeGroupoid.of C).obj X✝))

Tactic:
cat_disch

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

Goal state before:
pp: case map_comp
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
x✝¹ x✝ : Quiver.FreeGroupoid C
f g : x✝¹ ⟶ x✝
this :
  ∀ {X Y : C} (f : X ⟶ Y),
    Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) ⋯ ⋯ =
      φ.toPrefunctor.map f
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map ((Quiver.FreeGroupoid.of C).map (f✝ ≫ g✝)) =
    (Quiver.FreeGroupoid.lift φ.toPrefunctor).map
      ((Quiver.FreeGroupoid.of C).map f✝ ≫ (Quiver.FreeGroupoid.of C).map g✝)

Tactic:
cat_disch

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d

pp: case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e

Tactic:
· rintro h
    suffices (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d by
      simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this
    apply S.mul h (S.inv hg)

Goal state after:
case mpr
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sw : S.IsWide
c d : C
h : c = d
⊢ eqToHom h ∈ S.arrows c d

Tactic:
cases h; simp only [eqToHom_refl]; apply Sw.id_mem c

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
x✝ : op (left a✝¹) ⟶ op (left a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (left a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (left a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
x✝ : op (right a✝¹) ⟶ op (left a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (left a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (right a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
x✝ : op (right a✝¹) ⟶ op (right a✝)
⊢ (𝟭 (C ⋆ D)ᵒᵖ).map x✝ ≫
      (match op (right a✝) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom =
    (match op (right a✝¹) with
        | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
        | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a)))).hom ≫
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp ⋙
            mkFunctor (inclRight C D).op (inclLeft C D).op
              { app := fun x ↦ (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                naturality := ⋯ }).map
        x✝

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝ : C
⊢ (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.map
        ((NatIso.ofComponents
                (fun x ↦
                  match x with
                  | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
                  | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a))))
                ⋯).hom.app
          (op (left a✝))) ≫
      (NatIso.ofComponents
              (fun x ↦
                match x with
                | left a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (left a))
                | right a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (right a)))
              ⋯).hom.app
        ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp.obj
          (op (left a✝))) =
    𝟙
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.obj
        (op (left a✝)))

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
a✝ : D
⊢ (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.map
        ((NatIso.ofComponents
                (fun x ↦
                  match x with
                  | op (left a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (left a)))
                  | op (right a) => Iso.refl ((𝟭 (C ⋆ D)ᵒᵖ).obj (op (right a))))
                ⋯).hom.app
          (op (right a✝))) ≫
      (NatIso.ofComponents
              (fun x ↦
                match x with
                | left a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (left a))
                | right a =>
                  Iso.refl
                    ((mkFunctor (inclRight C D).op (inclLeft C D).op
                            {
                              app := fun x ↦
                                (edge (unop ((Prod.snd Dᵒᵖ Cᵒᵖ).obj x)) (unop ((Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                              naturality := ⋯ } ⋙
                          (mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                                naturality := ⋯ }).leftOp).obj
                      (right a)))
              ⋯).hom.app
        ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp.obj
          (op (right a✝))) =
    𝟙
      ((mkFunctor (inclRight Dᵒᵖ Cᵒᵖ).rightOp (inclLeft Dᵒᵖ Cᵒᵖ).rightOp
              { app := fun x ↦ (edge (op ((Prod.snd C D).obj x)) (op ((Prod.fst C D).obj x))).op,
                naturality := ⋯ }).leftOp.obj
        (op (right a✝)))

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝⁵ : AddCommMonoid I
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : MonoidalCategory C
X Y : GradedObject I C
inst✝² : SymmetricCategory C
inst✝¹ : X.HasTensor Y
inst✝ : Y.HasTensor X
⊢ ((fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) ≫ fun k ↦
      tensorObjDesc fun i j hij ↦ (β_ (Y i) (X j)).hom ≫ ιTensorObj X Y j i k ⋯) =
    𝟙 (tensorObj X Y)

Tactic:
cat_disch

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
⊢ map (𝟙 F) = 𝟙 (chosenCoend F)

Tactic:
cat_disch

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:
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
⊢ map (𝟙 F) = 𝟙 (chosenEnd F)

Tactic:
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:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Tactic:
obtain ⟨j'', H⟩ := H

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J) (x : j'' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
            (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
      { as := WalkingPair.left } =
    (Iso.refl
          ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt).hom ≫
      (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone).π.app { as := WalkingPair.left }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
            (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
      { as := WalkingPair.right } =
    (Iso.refl
          ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt).hom ≫
      (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone).π.app { as := WalkingPair.right }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: case left
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
    (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app { as := WalkingPair.left }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: case right
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
    (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app { as := WalkingPair.right }

Tactic:
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
⊢ powerMap (𝟙 U) α = 𝟙 (U.power α)

Tactic:
cat_disch

Goal state after:
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
x✝ : (U.power α).I
⊢ (powerMap (f ≫ g) α).f x✝ = (powerMap f α ≫ powerMap g α).f x✝

Tactic:
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:
cat_disch

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

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
U : FormalCoproduct C
α β γ : Type t
inst✝² : HasProductsOfShape α C
inst✝¹ : HasProductsOfShape β C
inst✝ : HasProductsOfShape γ C
f : α → β
g : β → γ
x✝ : (U.power γ).I
⊢ (U.mapPower (g ∘ f)).f x✝ = (U.mapPower g ≫ U.mapPower f).f x✝

Tactic:
cat_disch

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

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
U V : FormalCoproduct C
f : U ⟶ V
α β : Type t
inst✝¹ : HasProductsOfShape α C
inst✝ : HasProductsOfShape β C
g : α → β
x✝ : (U.power β).I
⊢ (U.mapPower g ≫ powerMap f α).f x✝ = (powerMap f β ≫ V.mapPower g).f x✝

Tactic:
cat_disch

Goal state after: