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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ (eqToIso p ≪≫ eqToIso q).hom = (eqToIso ⋯).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ (eqToIso p ≪≫ eqToIso q).hom = (eqToIso ⋯).hom
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map : ∀ (X Y : C) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
⊢ F = G

Tactic:
by
  match F, G with
  | mk F_obj _ _ _, mk G_obj _ _ _ =>
    obtain rfl : F_obj = G_obj := by
      ext X
      apply h_obj
    congr
    funext X Y f
    simpa using h_map X Y f

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
⊢ F.map (f ≫ g) ≍ G.map (f ≫ g)

Tactic:
rw [Functor.hext hobj fun _ _ => hmap]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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
F G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f
⊢ (F ⋙ H).map f ≍ (G ⋙ H).map f

Tactic:
rw [Functor.hext hobj fun _ _ => hmap]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ F.map (eqToHom ⋯) = eqToHom ⋯

Tactic:
;

Goal state after:
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ F.map (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ (F.mapIso (eqToIso p)).hom = (eqToIso ⋯).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ (F.mapIso (eqToIso p)).hom = (eqToIso ⋯).hom
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (F.mapIso (eqToIso ⋯)).hom = (eqToIso ⋯).hom

Tactic:
;

Goal state after:
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (F.mapIso (eqToIso ⋯)).hom = (eqToIso ⋯).hom
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (eqToHom ⋯).app X = eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (eqToHom ⋯).app X = eqToHom ⋯
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
C : Type u_2
D : Type u_3
inst✝ : Category.{?u.12, u_3} D
F : C → D
X : InducedCategory D F
⊢ F X = F X

Tactic:
;

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
C : Type u_2
D : Type u_3
inst✝ : Category.{?u.12, u_3} D
F : C → D
X : InducedCategory D F
⊢ F X = F X
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u_2
inst✝ : Category.{?u.11, u_2} C
P : ObjectProperty C
X : P.FullSubcategory
⊢ X.obj = X.obj

Tactic:
;

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u_2
inst✝ : Category.{?u.11, u_2} C
P : ObjectProperty C
X : P.FullSubcategory
⊢ X.obj = X.obj
Module: Mathlib.CategoryTheory.Whiskering

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
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y✝.map f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y✝.map f)
Module: Mathlib.CategoryTheory.Whiskering

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
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ ({ obj := fun G ↦ X✝ ⋙ G, map := fun {X Y} α ↦ X✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.map f ≫
          { app := fun c ↦ Y.map (τ.app c), naturality := ⋯ }).app
      x✝ =
    ({ app := fun c ↦ X.map (τ.app c), naturality := ⋯ } ≫
          { obj := fun G ↦ Y✝ ⋙ G, map := fun {X Y} α ↦ Y✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.map f).app
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ ({ obj := fun G ↦ X✝ ⋙ G, map := fun {X Y} α ↦ X✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.map f ≫
          { app := fun c ↦ Y.map (τ.app c), naturality := ⋯ }).app
      x✝ =
    ({ app := fun c ↦ X.map (τ.app c), naturality := ⋯ } ≫
          { obj := fun G ↦ Y✝ ⋙ G, map := fun {X Y} α ↦ Y✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.map f).app
      x✝
Module: Mathlib.CategoryTheory.Whiskering

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
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ f.app (X✝.obj x✝) ≫ Y.map (τ.app x✝) = X.map (τ.app x✝) ≫ f.app (Y✝.obj x✝)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ f.app (X✝.obj x✝) ≫ Y.map (τ.app x✝) = X.map (τ.app x✝) ≫ f.app (Y✝.obj x✝)
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X : C × D
⊢ (eqToHom ⋯).1 = eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X : C × D
⊢ (eqToHom ⋯).1 = eqToHom ⋯
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X : C × D
⊢ (eqToHom ⋯).2 = eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X : C × D
⊢ (eqToHom ⋯).2 = eqToHom ⋯
Module: Mathlib.CategoryTheory.Whiskering

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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ X✝.map (F.map f) ≫ τ.app (F.obj Y) = τ.app (F.obj X) ≫ Y✝.map (F.map f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ X✝.map (F.map f) ≫ τ.app (F.obj Y) = τ.app (F.obj X) ≫ Y✝.map (F.map f)
Module: Mathlib.CategoryTheory.Whiskering

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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ ({ obj := fun F ↦ F ⋙ X✝, map := fun {X Y} α ↦ whiskerRight α X✝, map_id := ⋯, map_comp := ⋯ }.map f ≫
          { app := fun c ↦ τ.app (Y.obj c), naturality := ⋯ }).app
      x✝ =
    ({ app := fun c ↦ τ.app (X.obj c), naturality := ⋯ } ≫
          { obj := fun F ↦ F ⋙ Y✝, map := fun {X Y} α ↦ whiskerRight α Y✝, map_id := ⋯, map_comp := ⋯ }.map f).app
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ ({ obj := fun F ↦ F ⋙ X✝, map := fun {X Y} α ↦ whiskerRight α X✝, map_id := ⋯, map_comp := ⋯ }.map f ≫
          { app := fun c ↦ τ.app (Y.obj c), naturality := ⋯ }).app
      x✝ =
    ({ app := fun c ↦ τ.app (X.obj c), naturality := ⋯ } ≫
          { obj := fun F ↦ F ⋙ Y✝, map := fun {X Y} α ↦ whiskerRight α Y✝, map_id := ⋯, map_comp := ⋯ }.map f).app
      x✝
Module: Mathlib.CategoryTheory.Whiskering

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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ X✝.map (f.app x✝) ≫ τ.app (Y.obj x✝) = τ.app (X.obj x✝) ≫ Y✝.map (f.app x✝)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ X✝.map (f.app x✝) ≫ τ.app (Y.obj x✝) = τ.app (X.obj x✝) ≫ Y✝.map (f.app x✝)
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ (({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
        f' ≫
      fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ fun i ↦ f' (g (f i))

Tactic:
;

Goal state after:
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ (({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
        f' ≫
      fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ fun i ↦ f' (g (f i))
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ (({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
          f' ≫
        fun b ↦ 𝟙 (Y (g (f b))))
      x✝ =
    ((fun b ↦ 𝟙 (X (g (f b)))) ≫ fun i ↦ f' (g (f i))) x✝

Tactic:
;

Goal state after:
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ (({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
          f' ≫
        fun b ↦ 𝟙 (Y (g (f b))))
      x✝ =
    ((fun b ↦ 𝟙 (X (g (f b)))) ≫ fun i ↦ f' (g (f i))) x✝
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_obj
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I✝ : Type u₁
G F : Discrete I✝ ⥤ C
h : ∀ (i : I✝), G.obj { as := i } = F.obj { as := i }
I : Discrete I✝
⊢ G.obj I = F.obj I

Tactic:
;

Goal state after:
case h_obj
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I✝ : Type u₁
G F : Discrete I✝ ⥤ C
h : ∀ (i : I✝), G.obj { as := i } = F.obj { as := i }
I : Discrete I✝
⊢ G.obj I = F.obj I
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((fun i ↦ f' (g (f i))) ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫
      ({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
        f'

Tactic:
;

Goal state after:
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((fun i ↦ f' (g (f i))) ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫
      ({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
        f'
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
p : { as := X }.as = { as := Y }.as
⊢ G.map { down := { down := p } } = eqToHom ⋯ ≫ F.map { down := { down := p } } ≫ eqToHom ⋯

Tactic:
;

Goal state after:
case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
p : { as := X }.as = { as := Y }.as
⊢ G.map { down := { down := p } } = eqToHom ⋯ ≫ F.map { down := { down := p } } ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
p : X = Y
⊢ G.map { down := { down := p } } = eqToHom ⋯ ≫ F.map { down := { down := p } } ≫ eqToHom ⋯

Tactic:
;

Goal state after:
case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
p : X = Y
⊢ G.map { down := { down := p } } = eqToHom ⋯ ≫ F.map { down := { down := p } } ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ ((fun i ↦ f' (g (f i))) ≫ fun b ↦ 𝟙 (Y (g (f b)))) x✝ =
    ((fun b ↦ 𝟙 (X (g (f b)))) ≫
        ({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
          f')
      x✝

Tactic:
;

Goal state after:
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ ((fun i ↦ f' (g (f i))) ≫ fun b ↦ 𝟙 (Y (g (f b)))) x✝ =
    ((fun b ↦ 𝟙 (X (g (f b)))) ≫
        ({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
          f')
      x✝
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: case h_map.refl
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
⊢ G.map { down := { down := ⋯ } } = eqToHom ⋯ ≫ F.map { down := { down := ⋯ } } ≫ eqToHom ⋯

Tactic:
;

Goal state after:
case h_map.refl
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X Y : I
⊢ G.map { down := { down := ⋯ } } = eqToHom ⋯ ≫ F.map { down := { down := ⋯ } } ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  (G ⋙ F).map (F.map (η.inv.app X)) ≫ ε.hom.app (F.obj ((𝟭 C).obj X)) =
    ε.hom.app (F.obj ((F ⋙ G).obj X)) ≫ (𝟭 D).map (F.map (η.inv.app X))
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) =
    𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  (G ⋙ F).map (F.map (η.inv.app X)) ≫ ε.hom.app (F.obj ((𝟭 C).obj X)) =
    ε.hom.app (F.obj ((F ⋙ G).obj X)) ≫ (𝟭 D).map (F.map (η.inv.app X))
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) =
    𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) ext._auto_1

pp: case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ ∀ (X : A), f.obj X = f'.obj X

Tactic:
;

Goal state after:
case h_map
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam (∀ (X Y : A) (f_1 : X ⟶ Y), f.map f_1 = eqToHom ⋯ ≫ f'.map f_1 ≫ eqToHom ⋯) ext._auto_1

case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ ∀ (X : A), f.obj X = f'.obj X
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  (G ⋙ F).map (ε.inv.app (F.obj X)) ≫ ε.hom.app ((G ⋙ F).obj (F.obj X)) =
    ε.hom.app ((𝟭 D).obj (F.obj X)) ≫ (𝟭 D).map (ε.inv.app (F.obj X))
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  (G ⋙ F).map (ε.inv.app (F.obj X)) ≫ ε.hom.app ((G ⋙ F).obj (F.obj X)) =
    ε.hom.app ((𝟭 D).obj (F.obj X)) ≫ (𝟭 D).map (ε.inv.app (F.obj X))
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op.hom = f.hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op.hom = f.hom
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop.hom = f.hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop.hom = f.hom
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.op α.hom ≫ NatTrans.op α.inv).app x✝ = (𝟙 G.op).app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.op α.hom ≫ NatTrans.op α.inv).app x✝ = (𝟙 G.op).app x✝