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

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 : C ⥤ D ⥤ E ⥤ E'
e : F ≅ G
X₁ : C
X₂ : D
X₃ : E
⊢ ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 (((F.obj X₁).obj X₂).obj X₃)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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 : C ⥤ D ⥤ E ⥤ E'
e : F ≅ G
X₁ : C
X₂ : D
X₃ : E
⊢ ((e.inv.app X₁).app X₂).app X₃ ≫ ((e.hom.app X₁).app X₂).app X₃ = 𝟙 (((G.obj X₁).obj X₂).obj X₃)

Tactic:
cat_disch

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

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 H : C ⥤ D
I J K : D ⥤ E
α : F ⟶ G
β : G ⟶ H
γ : I ⟶ J
δ : J ⟶ K
⊢ (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ

Tactic:
cat_disch

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

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
e : X ≅ Y
F : C ⥤ D ⥤ E
Z : D
⊢ (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 ((F.obj X).obj Z)

Tactic:
cat_disch

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

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
e : X ≅ Y
F : C ⥤ D ⥤ E
Z : D
⊢ (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 ((F.obj Y).obj Z)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
X : C
⊢ inv (e.inv.app X) = e.hom.app X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
α : F ⟶ G
f : X ⟶ Y
x✝ : IsIso (α.app Y)
⊢ α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
inst✝ : IsIso α
X : C
⊢ (inv α).app X = inv (α.app X)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
⊢ Function.LeftInverse hF.preimageIso F.mapIso

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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 ⥤ E
X Y : C
e : X ≅ Y
Z : D
⊢ inv ((F.map e.inv).app Z) = (F.map e.hom).app Z

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
⊢ Function.RightInverse hF.preimageIso F.mapIso

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
app' : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app' Y).hom = (app' X).hom ≫ G.map f
X : C
⊢ (ofComponents app' naturality).app X = app' X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ F₂.map f ≫ e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X = 𝟙 (F₂.obj X) ∧
    (e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X) ≫ F₂.map f = 𝟙 (F₂.obj Y)

Tactic:
cat_disch

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

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✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
⊢ ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)

Tactic:
by
      intro X
      apply G.map_injective
      grind

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j'

Tactic:
cases w

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j : β
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').hom

Tactic:
cases w

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).hom
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').inv

Tactic:
cases w

Goal state after:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).inv
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ inv (eqToHom h) = eqToHom ⋯

Tactic:
cat_disch

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

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

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

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

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

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✝
⊢ F.map (X✝.map g ≫ hF.preimage (f.app x✝)) = F.map (hF.preimage (f.app x✝¹) ≫ Y✝.map g)

Tactic:
simp only [map_comp, map_preimage]

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
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✝
⊢ F.map (X✝.map g) ≫ f.app x✝ = f.app x✝¹ ≫ F.map (Y✝.map g)
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:
cat_disch

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

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

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

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

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

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

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

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : B ⥤ C
⊢ F.associator (𝟭 B) G ≪≫ F.isoWhiskerLeft G.leftUnitor = isoWhiskerRight F.rightUnitor G

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
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 : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ isoWhiskerRight (F.associator G H) K ≪≫ F.associator (G ⋙ H) K ≪≫ F.isoWhiskerLeft (G.associator H K) =
    (F ⋙ G).associator H K ≪≫ F.associator G (H ⋙ K)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : B ⥤ C
⊢ (F.associator (𝟭 B) G).hom ≫ F.whiskerLeft G.leftUnitor.hom = whiskerRight F.rightUnitor.hom G

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
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 : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ whiskerRight (F.associator G H).hom K ≫ (F.associator (G ⋙ H) K).hom ≫ F.whiskerLeft (G.associator H K).hom =
    ((F ⋙ G).associator H K).hom ≫ (F.associator G (H ⋙ K)).hom

Tactic:
cat_disch

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

Goal state before:
pp: α : Type u₁
⊢ Function.LeftInverse Discrete.mk Discrete.as

Tactic:
cat_disch

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

Goal state before:
pp: α : Type u₁
⊢ Function.RightInverse Discrete.mk Discrete.as

Tactic:
cat_disch

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

Goal state before:
pp: α : Type u₁
inst✝ : Subsingleton α
⊢ ∀ (a b : Discrete α), a = b

Tactic:
cat_disch

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

Goal state before:
pp: α : Type u₁
X Y : Discrete α
h : X.as = Y.as
⊢ X = Y

Tactic:
cat_disch

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
i j : Discrete I
f : i ⟶ j
⊢ f ≫ Discrete.eqToHom ⋯ = 𝟙 i ∧ Discrete.eqToHom ⋯ ≫ f = 𝟙 j

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
i : Discrete I
f : i ⟶ i
⊢ (functor F).map f = 𝟙 (F i.as)

Tactic:
cat_disch

Goal state after:
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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : D ⥤ E
α : F ⟶ G
⊢ NatTrans.op (whiskerRight α H) = (G.opComp H).hom ≫ whiskerRight (NatTrans.op α) H.op ≫ (F.opComp H).inv

Tactic:
cat_disch

Goal state after:
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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : E ⥤ C
α : F ⟶ G
⊢ NatTrans.op (H.whiskerLeft α) = (H.opComp G).hom ≫ H.op.whiskerLeft (NatTrans.op α) ≫ (H.opComp F).inv

Tactic:
cat_disch

Goal state after:
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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : Dᵒᵖ ⥤ Eᵒᵖ
α : F ⟶ G
⊢ NatTrans.unop (whiskerRight α H) = (G.unopComp H).hom ≫ whiskerRight (NatTrans.unop α) H.unop ≫ (F.unopComp H).inv

Tactic:
cat_disch

Goal state after:
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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : Eᵒᵖ ⥤ Cᵒᵖ
α : F ⟶ G
⊢ NatTrans.unop (H.whiskerLeft α) = (H.unopComp G).hom ≫ H.unop.whiskerLeft (NatTrans.unop α) ≫ (H.unopComp F).inv

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F G : Discrete I ⥤ C
f : (i : Discrete I) → F.obj i ≅ G.obj i
i : Discrete I
⊢ (natIso f).app i = f i

Tactic:
cat_disch

Goal state after:
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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : E ⥤ C
α : F ⟶ G
⊢ NatTrans.leftOp (H.whiskerLeft α) = (H.leftOpComp G).hom ≫ H.op.whiskerLeft (NatTrans.leftOp α) ≫ (H.leftOpComp F).inv

Tactic:
cat_disch

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

Goal state before:
pp: J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ f = 𝟙 j

Tactic:
cat_disch

Goal state after:
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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : D ⥤ E
α : F ⟶ G
⊢ NatTrans.rightOp (whiskerRight α H) =
    (G.rightOpComp H).hom ≫ whiskerRight (NatTrans.rightOp α) H.op ≫ (F.rightOpComp H).inv

Tactic:
cat_disch

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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ (f ≫ fun i ↦ inv (f i)) = 𝟙 X

Tactic:
cat_disch

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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
a✝ : ∀ (i : I), IsIso (f i)
⊢ (fun i ↦ inv (f i)) ≫ f = 𝟙 Y

Tactic:
cat_disch

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

Goal state before:
pp: J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Discrete J ⥤ C} (f : X ⟶ Y),
    ({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as, map_id := ⋯,
                map_comp := ⋯ }).map
          f ≫
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                            map_comp := ⋯ } ⋙
                          { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                            map_id := ⋯, map_comp := ⋯ }).obj
                      Y).obj
                  x))
            ⋯).hom =
      (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                            map_comp := ⋯ } ⋙
                          { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                            map_id := ⋯, map_comp := ⋯ }).obj
                      X).obj
                  x))
            ⋯).hom ≫
        (𝟭 (Discrete J ⥤ C)).map f

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
X Y : C
f : X ⟶ Y
⊢ f ≫ eqToHom ⋯ = 𝟙 X ∧ eqToHom ⋯ ≫ f = 𝟙 Y

Tactic:
cat_disch

Goal state after:
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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : D ⥤ E
α : F ≅ G
⊢ NatIso.op (isoWhiskerRight α H) = G.opComp H ≪≫ isoWhiskerRight (NatIso.op α) H.op ≪≫ (F.opComp H).symm

Tactic:
cat_disch

Goal state after:
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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : E ⥤ C
α : F ≅ G
⊢ NatIso.op (H.isoWhiskerLeft α) = H.opComp G ≪≫ H.op.isoWhiskerLeft (NatIso.op α) ≪≫ (H.opComp F).symm

Tactic:
cat_disch

Goal state after:
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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : Dᵒᵖ ⥤ Eᵒᵖ
α : F ≅ G
⊢ NatIso.unop (isoWhiskerRight α H) = G.unopComp H ≪≫ isoWhiskerRight (NatIso.unop α) H.unop ≪≫ (F.unopComp H).symm

Tactic:
cat_disch

Goal state after:
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ᵒᵖ
E : Type u_1
inst✝ : Category.{v_1, u_1} E
H : Eᵒᵖ ⥤ Cᵒᵖ
α : F ≅ G
⊢ NatIso.unop (H.isoWhiskerLeft α) = H.unopComp G ≪≫ H.unop.isoWhiskerLeft (NatIso.unop α) ≪≫ (H.unopComp F).symm

Tactic:
cat_disch

Goal state after:
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 : C ⥤ D
⊢ NatIso.op F.leftUnitor = F.op.leftUnitor.symm ≪≫ isoWhiskerRight (opId C).symm F.op ≪≫ ((𝟭 C).opComp F).symm

Tactic:
cat_disch

Goal state after:
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 : C ⥤ D
⊢ NatIso.op F.rightUnitor = F.op.rightUnitor.symm ≪≫ F.op.isoWhiskerLeft (opId D).symm ≪≫ (F.opComp (𝟭 D)).symm

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u_1
E' : Type u_2
inst✝¹ : Category.{v_1, u_1} E
inst✝ : Category.{v_2, u_2} E'
F : C ⥤ D
G : D ⥤ E
H : E ⥤ E'
⊢ NatIso.op (F.associator G H) =
    F.opComp (G ⋙ H) ≪≫
      F.op.isoWhiskerLeft (G.opComp H) ≪≫
        (F.op.associator G.op H.op).symm ≪≫ isoWhiskerRight (F.opComp G).symm H.op ≪≫ ((F ⋙ G).opComp H).symm

Tactic:
cat_disch

Goal state after:
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 : Cᵒᵖ ⥤ Dᵒᵖ
⊢ NatIso.unop F.leftUnitor =
    F.unop.leftUnitor.symm ≪≫ isoWhiskerRight (unopId C).symm F.unop ≪≫ ((𝟭 Cᵒᵖ).unopComp F).symm

Tactic:
cat_disch

Goal state after:
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 : Cᵒᵖ ⥤ Dᵒᵖ
⊢ NatIso.unop F.rightUnitor =
    F.unop.rightUnitor.symm ≪≫ F.unop.isoWhiskerLeft (unopId D).symm ≪≫ (F.unopComp (𝟭 Dᵒᵖ)).symm

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u_1
E' : Type u_2
inst✝¹ : Category.{v_1, u_1} E
inst✝ : Category.{v_2, u_2} E'
F : Cᵒᵖ ⥤ Dᵒᵖ
G : Dᵒᵖ ⥤ Eᵒᵖ
H : Eᵒᵖ ⥤ E'ᵒᵖ
⊢ NatIso.unop (F.associator G H) =
    F.unopComp (G ⋙ H) ≪≫
      F.unop.isoWhiskerLeft (G.unopComp H) ≪≫
        (F.unop.associator G.unop H.unop).symm ≪≫
          isoWhiskerRight (F.unopComp G).symm H.unop ≪≫ ((F ⋙ G).unopComp H).symm

Tactic:
cat_disch

Goal state after:
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 : F ⟶ G
⊢ (NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop =
    { app := fun X ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
      (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom

Tactic:
cat_disch

Goal state after: