mathlib-initiative/mathlib-tactics huggingface dataset:
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

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 G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
by

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 G : C ⥤ D
h : F = G
X : C
⊢ F.obj X = G.obj X

Tactic:
by

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 G : C ⥤ D
h : F = G
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
by

Goal state after:
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
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ F.obj X = G.obj X

Tactic:
by

Goal state after:
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
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ G.obj Y = F.obj Y

Tactic:
by

Goal state after:
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
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ F.obj Y = G.obj Y

Tactic:
by

Goal state after:
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
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ G.obj X = F.obj X

Tactic:
by

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 G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ F.map e.inv = eqToHom ⋯ ≫ G.map e.inv ≫ eqToHom ⋯

Tactic:
by

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 G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : F.map f ≍ G.map f
hg : F.map g ≍ G.map g
⊢ F.map (f ≫ g) ≍ G.map (f ≫ g)

Tactic:
by

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 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:
by

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
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : F.map f ≍ G.map f
⊢ (F ⋙ H).map f ≍ (G ⋙ H).map f

Tactic:
by

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:
by

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 G : C ⥤ D
h : F = G
X Y : C
f : X ⟶ Y
⊢ F.map f ≍ G.map f

Tactic:
by

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
p : X = Y
⊢ F.map (eqToHom p) = eqToHom ⋯

Tactic:
by

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 Z : C
p : X = Y
q : Y = Z
⊢ F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom ⋯)

Tactic:
by

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
p : X = Y
⊢ F.mapIso (eqToIso p) = eqToIso ⋯

Tactic:
by

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 Z : C
p : X = Y
q : Y = Z
⊢ F.mapIso (eqToIso p) ≪≫ F.mapIso (eqToIso q) = F.mapIso (eqToIso ⋯)

Tactic:
by

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 G : C ⥤ D
h : F = G
X : C
⊢ (eqToHom h).app X = eqToHom ⋯

Tactic:
by

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 G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i j : ι
h : i = j
⊢ α i = eqToHom ⋯ ≫ α j ≫ eqToHom ⋯

Tactic:
by

Goal state after:
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 Y : InducedCategory D F
h : X = Y
⊢ F X = F Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_2
D : Type u_3
inst✝ : Category.{u_4, u_3} D
F : C → D
X Y : InducedCategory D F
h : X = Y
⊢ (eqToHom h).hom = eqToHom ⋯

Tactic:
by

Goal state after:
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 Y : P.FullSubcategory
h : X = Y
⊢ X.obj = Y.obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_2
inst✝ : Category.{u_3, u_2} C
P : ObjectProperty C
X Y : P.FullSubcategory
h : X = Y
⊢ (eqToHom h).hom = eqToHom ⋯

Tactic:
by

Goal state after:
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
T : Type u_2
e : T ≃ D
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ e (e.symm X✝) = X✝

Tactic:
by

Goal state after:
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
T : Type u_2
e : T ≃ D
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ Y✝ = e (e.symm Y✝)

Tactic:
by

Goal state after:
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
T : Type u_2
e : T ≃ D
x✝ : InducedCategory D ⇑e
⊢ (𝟭 (InducedCategory D ⇑e)).obj x✝ =
    (inducedFunctor ⇑e ⋙
          { obj := ⇑e.symm, map := fun {X Y} f ↦ InducedCategory.homMk (eqToHom ⋯ ≫ f ≫ eqToHom ⋯), map_id := ⋯,
            map_comp := ⋯ }).obj
      x✝

Tactic:
by

Goal state after:
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
T : Type u_2
e : T ≃ D
x✝ : D
⊢ ({ obj := ⇑e.symm, map := fun {X Y} f ↦ InducedCategory.homMk (eqToHom ⋯ ≫ f ≫ eqToHom ⋯), map_id := ⋯,
            map_comp := ⋯ } ⋙
          inducedFunctor ⇑e).obj
      x✝ =
    (𝟭 D).obj x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Const

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : C ⥤ D
X : C
⊢ ∀ {X_1 Y : J} (f : X_1 ⟶ Y),
    ((F ⋙ const J).obj X).map f ≫ (Iso.refl (((F ⋙ const J).obj X).obj Y)).hom =
      (Iso.refl (((F ⋙ const J).obj X).obj X_1)).hom ≫ ((const J ⋙ (whiskeringRight J C D).obj F).obj X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Const

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
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 ⋙ const J).map f ≫ (NatIso.ofComponents (fun x ↦ Iso.refl (((F ⋙ const J).obj Y).obj x)) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ Iso.refl (((F ⋙ const J).obj X).obj x)) ⋯).hom ≫
        (const J ⋙ (whiskeringRight J C D).obj F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.counitIso.inv.app (e.functor.obj X) ≫ e.functor.map (e.unitIso.inv.app X) = 𝟙 (e.functor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
functor : C ⥤ D
inverse : D ⥤ C
unitIso : 𝟭 C ≅ functor ⋙ inverse
counitIso : inverse ⋙ functor ≅ 𝟭 D
functor_unitIso_comp :
  ∀ (X : C), counitIso.inv.app (functor.obj X) ≫ functor.map (unitIso.inv.app X) = 𝟙 (functor.obj X)
X : C
⊢ functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.unit.app X ≫ e.unitInv.app X = 𝟙 X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.unitInv.app X ≫ e.unit.app X = 𝟙 (e.inverse.obj (e.functor.obj X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.counit.app Y ≫ e.counitInv.app Y = 𝟙 (e.functor.obj (e.inverse.obj Y))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.counitInv.app Y ≫ e.counit.app Y = 𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
⊢ e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)

Tactic:
by

Goal state after:
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
F : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f

Tactic:
by

Goal state after:
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
F : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
⊢ 𝟙 F ◫ α = F.whiskerLeft α

Tactic:
by

Goal state after:
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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f

Tactic:
rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]

Goal state after:
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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f

Tactic:
by

Goal state after:
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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
⊢ α ◫ 𝟙 F = whiskerRight α F

Tactic:
by

Goal state after:
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
⊢ ({ obj := fun G ↦ X✝ ⋙ G, map := fun {X Y} α ↦ X✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.obj H).map f ≫
      H.map (τ.app Y) =
    H.map (τ.app X) ≫
      ({ obj := fun G ↦ Y✝ ⋙ G, map := fun {X Y} α ↦ Y✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.obj H).map f

Tactic:
by

Goal state after:
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 Y : C × D
h : X = Y
⊢ (eqToHom h).1 = eqToHom ⋯

Tactic:
by

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

Tactic:
by

Goal state after:
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 Y : C × D
h : X = Y
⊢ (eqToHom h).2 = eqToHom ⋯

Tactic:
by

Goal state after:
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
⊢ ({ obj := fun F ↦ F ⋙ X✝, map := fun {X Y} α ↦ whiskerRight α X✝, map_id := ⋯, map_comp := ⋯ }.obj F).map f ≫
      τ.app (F.obj Y) =
    τ.app (F.obj X) ≫
      ({ obj := fun F ↦ F ⋙ Y✝, map := fun {X Y} α ↦ whiskerRight α Y✝, map_id := ⋯, map_comp := ⋯ }.obj F).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f ↔ IsIso f.1 ∧ IsIso f.2

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ (braiding C D).functor.IsEquivalence

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C × D
f : x ⟶ y
⊢ f = (𝟙 x.1 ×ₘ f.2) ≫ (f.1 ×ₘ 𝟙 y.2)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C × D
f : x ⟶ y
⊢ f = (f.1 ×ₘ 𝟙 x.2) ≫ (𝟙 y.1 ×ₘ f.2)

Tactic:
by

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

Tactic:
by

Goal state after:
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
F : D ⥤ E
inst✝ : F.Faithful
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

Goal state after:
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
F : D ⥤ E
hF : F.FullyFaithful
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C ⥤ D
f : ((Functor.whiskeringRight C D E).obj F).obj X✝ ⟶ ((Functor.whiskeringRight C D E).obj F).obj Y✝
x✝¹ x✝ : C
g : x✝¹ ⟶ x✝
⊢ X✝.map g ≫ hF.preimage (f.app x✝) = hF.preimage (f.app x✝¹) ≫ Y✝.map g

Tactic:
by

Goal state after:
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
F G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
⊢ F.whiskerLeft β ≫ whiskerRight α K = whiskerRight α H ≫ G.whiskerLeft β

Tactic:
by

Goal state after:
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
F G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
⊢ α ◫ β = F.whiskerLeft β ≫ whiskerRight α K

Tactic:
by

Goal state after:
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
F : C ⥤ D
G : D ⥤ E
⊢ isoWhiskerRight (Iso.refl F) G = Iso.refl (F ⋙ G)

Tactic:
by

Goal state after:
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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
inst✝ : IsIso α
⊢ inv (whiskerRight α F) = whiskerRight (inv α) F

Tactic:
by

Goal state after:
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
F : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
inst✝ : IsIso α
⊢ inv (F.whiskerLeft α) = F.whiskerLeft (inv α)

Tactic:
by

Goal state after:
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
F G : C ⥤ D
H K : D ⥤ E
α : F ≅ G
β : H ≅ K
⊢ F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β

Tactic:
by

Goal state after:
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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
H K : D ⥤ E
α : H ⟶ K
⊢ F.whiskerLeft (G.whiskerLeft α) = (F.associator G H).inv ≫ (F ⋙ G).whiskerLeft α ≫ (F.associator G K).hom

Tactic:
by

Goal state after:
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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
H K : B ⥤ C
F : C ⥤ D
G : D ⥤ E
α : H ⟶ K
⊢ whiskerRight (whiskerRight α F) G = (H.associator F G).hom ≫ whiskerRight α (F ⋙ G) ≫ (K.associator F G).inv

Tactic:
by

Goal state after:
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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G H : C ⥤ D
α : G ⟶ H
K : D ⥤ E
⊢ whiskerRight (F.whiskerLeft α) K = (F.associator G K).hom ≫ F.whiskerLeft (whiskerRight α K) ≫ (F.associator H K).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f

Tactic:
by

Goal state after:
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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
H K : D ⥤ E
α : H ≅ K
⊢ F.isoWhiskerLeft (G.isoWhiskerLeft α) = (F.associator G H).symm ≪≫ (F ⋙ G).isoWhiskerLeft α ≪≫ F.associator G K

Tactic:
by

Goal state after:
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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
H K : B ⥤ C
F : C ⥤ D
G : D ⥤ E
α : H ≅ K
⊢ isoWhiskerRight (isoWhiskerRight α F) G = H.associator F G ≪≫ isoWhiskerRight α (F ⋙ G) ≪≫ (K.associator F G).symm

Tactic:
by

Goal state after:
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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G H : C ⥤ D
α : G ≅ H
K : D ⥤ E
⊢ isoWhiskerRight (F.isoWhiskerLeft α) K =
    F.associator G K ≪≫ F.isoWhiskerLeft (isoWhiskerRight α K) ≪≫ (F.associator H K).symm

Tactic:
by

Goal state after:
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
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G H : C ⥤ D
α : G ≅ H
K : D ⥤ E
⊢ F.isoWhiskerLeft (isoWhiskerRight α K) =
    (F.associator G K).symm ≪≫ isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ F.associator H K

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ f ≫ 𝟙 Y✝ = f

Tactic:
by

Goal state after: