awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Faithful
X_1 Y : Functor.{v₁, v₂, u₁, u₂} C D
a₁ a₂ : X_1 ⟶ Y
hαβ :
  Eq (α := obj (obj (whiskeringRight C D E) F) X_1 ⟶ obj (obj (whiskeringRight C D E) F) Y)
    (map (obj (whiskeringRight C D E) F) a₁) (map (obj (whiskeringRight C D E) F) a₂)
X : C
⊢ a₁.app X = a₂.app X

Tactic:
exact F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X

Premises used: congr_arg, CategoryTheory.Functor.map_injective, congr_fun, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
hF : F.FullyFaithful
C : Type u_1
inst_3 : Category.{v_1, u_1} C
X Y : Functor.{v_1, v₂, u_1, u₂} C D
f : obj (obj (Functor.whiskeringRight C D E) F) X ⟶ obj (obj (Functor.whiskeringRight C D E) F) Y
x x_1 : C
g : x ⟶ x_1
apply : F.map (X.map g ≫ hF.preimage (f.app x_1)) = F.map (hF.preimage (f.app x) ≫ Y.map g)
⊢ X.map g ≫ hF.preimage (f.app x_1) = hF.preimage (f.app x) ≫ Y.map g

Tactic:
apply hF.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
hF : F.FullyFaithful
C : Type u_1
inst_3 : Category.{v_1, u_1} C
X Y : Functor.{v_1, v₂, u_1, u₂} C D
f : obj (obj (Functor.whiskeringRight C D E) F) X ⟶ obj (obj (Functor.whiskeringRight C D E) F) Y
x x_1 : C
g : x ⟶ x_1
dsimp : F.map (X.map g ≫ hF.preimage (f.app x_1)) = F.map (hF.preimage (f.app x) ≫ Y.map g)
⊢ F.map (X.map g ≫ hF.preimage (f.app x_1)) = F.map (hF.preimage (f.app x) ≫ Y.map g)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
hF : F.FullyFaithful
C : Type u_1
inst_3 : Category.{v_1, u_1} C
X Y : Functor.{v_1, v₂, u_1, u₂} C D
f : obj (obj (Functor.whiskeringRight C D E) F) X ⟶ obj (obj (Functor.whiskeringRight C D E) F) Y
x x_1 : C
g : x ⟶ x_1
simp : F.map (X.map g) ≫ f.app x_1 = f.app x ≫ F.map (Y.map g)
⊢ F.map (X.map g ≫ hF.preimage (f.app x_1)) = F.map (hF.preimage (f.app x) ≫ Y.map g)

Tactic:
simp only [map_comp, map_preimage]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.FullyFaithful.map_preimage
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
hF : F.FullyFaithful
C : Type u_1
inst_3 : Category.{v_1, u_1} C
X Y : Functor.{v_1, v₂, u_1, u₂} C D
f : obj (obj (Functor.whiskeringRight C D E) F) X ⟶ obj (obj (Functor.whiskeringRight C D E) F) Y
x x_1 : C
g : x ⟶ x_1
⊢ F.map (X.map g) ≫ f.app x_1 = f.app x ≫ F.map (Y.map g)

Tactic:
apply f.naturality

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
E : Type u₃
inst_1 : Category.{v₃, u₃} E
⊢ Eq (α := Functor.{v₁, v₃, u₁, u₃} C E ⥤ Functor.{v₁, v₃, u₁, u₃} C E) (obj (whiskeringLeft C C E) (𝟭 C))
    (𝟭 (Functor.{v₁, v₃, u₁, u₃} C E))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₄, u₂, u₄} D D'
⊢ Eq (α := Functor.{v₄, v₃, u₄, u₃} D' E ⥤ Functor.{v₁, v₃, u₁, u₃} C E) (obj (whiskeringLeft C D' E) (F ⋙ G))
    (obj (whiskeringLeft D D' E) G ⋙ obj (whiskeringLeft C D E) F)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
E : Type u₃
inst_1 : Category.{v₃, u₃} E
⊢ Eq (α := Functor.{v₃, v₁, u₃, u₁} E C ⥤ Functor.{v₃, v₁, u₃, u₁} E C) (obj (whiskeringRight E C C) (𝟭 C))
    (𝟭 (Functor.{v₃, v₁, u₃, u₁} E C))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₄, u₂, u₄} D D'
⊢ Eq (α := Functor.{v₃, v₁, u₃, u₁} E C ⥤ Functor.{v₃, v₄, u₃, u₄} E D')
    (obj (whiskeringRight E C D) F ⋙ obj (whiskeringRight E D D') G) (obj (whiskeringRight E C D') (F ⋙ G))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Faithful
inst_4 : F.Full
⊢ Full (C := Functor.{v₁, v₂, u₁, u₂} C D) (obj (whiskeringRight C D E) F)

Tactic:
((Functor.FullyFaithful.ofFullyFaithful F).whiskeringRight C).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful, CategoryTheory.Functor.FullyFaithful.whiskeringRight
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
⊢ F.whiskerLeft (NatTrans.id G) = NatTrans.id (F ⋙ G)

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
⊢ F.whiskerLeft (𝟙 G) = 𝟙 (F ⋙ G)

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₃, u₂, u₃} D E
⊢ whiskerRight (NatTrans.id G) F = NatTrans.id (G ⋙ F)

Tactic:
((whiskeringRight C D E).obj F).map_id _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.map_id, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
F : Functor.{v₂, v₃, u₂, u₃} D E
⊢ whiskerRight (𝟙 G) F = 𝟙 (G ⋙ F)

Tactic:
((whiskeringRight C D E).obj F).map_id _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.map_id, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H K : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
β : H ⟶ K
⊢ F.whiskerLeft (α ≫ β) = F.whiskerLeft α ≫ F.whiskerLeft β

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H K : Functor.{v₁, v₂, u₁, u₂} C D
α : G ⟶ H
β : H ⟶ K
F : Functor.{v₂, v₃, u₂, u₃} D E
⊢ whiskerRight (α ≫ β) F = whiskerRight α F ≫ whiskerRight β F

Tactic:
((whiskeringRight C D E).obj F).map_comp α β

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ⟶ G
β : H ⟶ K
w : ∀ (x : C), (F.whiskerLeft β ≫ whiskerRight α K).app x = (whiskerRight α H ≫ G.whiskerLeft β).app x
⊢ F.whiskerLeft β ≫ whiskerRight α K = whiskerRight α H ≫ G.whiskerLeft β

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ⟶ G
β : H ⟶ K
x : C
⊢ (F.whiskerLeft β ≫ whiskerRight α K).app x = (whiskerRight α H ≫ G.whiskerLeft β).app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ⟶ G
β : H ⟶ K
w : ∀ (x : C), (α ◫ β).app x = (F.whiskerLeft β ≫ whiskerRight α K).app x
⊢ α ◫ β = F.whiskerLeft β ≫ whiskerRight α K

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ⟶ G
β : H ⟶ K
x : C
⊢ (α ◫ β).app x = (F.whiskerLeft β ≫ whiskerRight α K).app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ≅ H
⊢ (F.isoWhiskerLeft α).hom = F.whiskerLeft α.hom

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ≅ H
⊢ (F.isoWhiskerLeft α).inv = F.whiskerLeft α.inv

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ≅ H
⊢ (F.isoWhiskerLeft α).symm = F.isoWhiskerLeft α.symm

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.mapIso, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
⊢ F.isoWhiskerLeft (Iso.refl G) = Iso.refl (F ⋙ G)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Iso.refl, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.NatTrans.id, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ≅ H
F : Functor.{v₂, v₃, u₂, u₃} D E
⊢ (isoWhiskerRight α F).hom = whiskerRight α.hom F

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ≅ H
F : Functor.{v₂, v₃, u₂, u₃} D E
⊢ (isoWhiskerRight α F).inv = whiskerRight α.inv F

Tactic:
rfl

Premises used: CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ≅ H
F : Functor.{v₂, v₃, u₂, u₃} D E
⊢ (isoWhiskerRight α F).symm = isoWhiskerRight α.symm F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.mapIso, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
inst_3 : IsIso α
⊢ IsIso (F.whiskerLeft α)

Tactic:
(isoWhiskerLeft F (asIso α)).isIso_hom

Premises used: CategoryTheory.Functor.whiskerLeft, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.isIso_hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ⟶ H
F : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsIso α
⊢ IsIso (whiskerRight α F)

Tactic:
(isoWhiskerRight (asIso α) F).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ⟶ H
F : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsIso α
symm : whiskerRight (inv α) F = inv (whiskerRight α F)
⊢ inv (whiskerRight α F) = whiskerRight (inv α) F

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ⟶ H
F : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsIso α
hom_inv_id : whiskerRight (inv α) F ≫ whiskerRight α F = 𝟙 (H ⋙ F)
⊢ whiskerRight (inv α) F = inv (whiskerRight α F)

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Premises used: CategoryTheory.IsIso.eq_inv_of_inv_hom_id
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ⟶ H
F : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsIso α
⊢ whiskerRight (inv α) F ≫ whiskerRight α F = 𝟙 (H ⋙ F)

Tactic:
simp [← whiskerRight_comp]

Premises used: CategoryTheory.Functor.whiskerRight_comp
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
inst_3 : IsIso α
symm : F.whiskerLeft (inv α) = inv (F.whiskerLeft α)
⊢ inv (F.whiskerLeft α) = F.whiskerLeft (inv α)

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
inst_3 : IsIso α
hom_inv_id : F.whiskerLeft (inv α) ≫ F.whiskerLeft α = 𝟙 (F ⋙ H)
⊢ F.whiskerLeft (inv α) = inv (F.whiskerLeft α)

Tactic:
apply IsIso.eq_inv_of_inv_hom_id

Premises used: CategoryTheory.IsIso.eq_inv_of_inv_hom_id
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
inst_3 : IsIso α
⊢ F.whiskerLeft (inv α) ≫ F.whiskerLeft α = 𝟙 (F ⋙ H)

Tactic:
simp [← whiskerLeft_comp]

Premises used: CategoryTheory.Functor.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G H K : Functor.{v₂, v₃, u₂, u₃} D E
α : G ≅ H
β : H ≅ K
⊢ F.isoWhiskerLeft (α ≪≫ β) = F.isoWhiskerLeft α ≪≫ F.isoWhiskerLeft β

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G H K : Functor.{v₁, v₂, u₁, u₂} C D
α : G ≅ H
β : H ≅ K
F : Functor.{v₂, v₃, u₂, u₃} D E
⊢ isoWhiskerRight (α ≪≫ β) F = isoWhiskerRight α F ≪≫ isoWhiskerRight β F

Tactic:
((whiskeringRight C D E).obj F).mapIso_trans α β

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.mapIso_trans, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ≅ G
β : H ≅ K
w :
  ∀ (x : C),
    (F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K).hom.app x = (isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β).hom.app x
⊢ F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Whiskering
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ≅ G
β : H ≅ K
x : C
⊢ (F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K).hom.app x = (isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β).hom.app x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty.{v₁, u₂} D
inst_1 : P.IsMultiplicative
X Y : InducedWideCategory D F P
f g : X ⟶ Y
eq :
  Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
    (Functor.map (wideInducedFunctor F P) f) (Functor.map (wideInducedFunctor F P) g)
mk :
  ∀ (hom : F X ⟶ F Y) (property : P hom)
    (eq :
      Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
        (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom property)) (Functor.map (wideInducedFunctor F P) g)),
    Hom.mk (P := P) hom property = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty.{v₁, u₂} D
inst_1 : P.IsMultiplicative
X Y : InducedWideCategory D F P
g : X ⟶ Y
hom : F X ⟶ F Y
property : P hom
eq :
  Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
    (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom property)) (Functor.map (wideInducedFunctor F P) g)
mk :
  ∀ (hom_1 : F X ⟶ F Y) (property_1 : P hom_1)
    (eq :
      Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
        (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom property))
        (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom_1 property_1))),
    Hom.mk (P := P) hom property = Hom.mk (P := P) hom_1 property_1
⊢ Hom.mk (P := P) hom property = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty.{v₁, u₂} D
inst_1 : P.IsMultiplicative
X Y : InducedWideCategory D F P
hom : F X ⟶ F Y
property : P hom
hom_1 : F X ⟶ F Y
property_1 : P hom_1
eq :
  Eq (α := Functor.obj (wideInducedFunctor F P) X ⟶ Functor.obj (wideInducedFunctor F P) Y)
    (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom property))
    (Functor.map (wideInducedFunctor F P) (Hom.mk (P := P) hom_1 property_1))
⊢ Hom.mk (P := P) hom property = Hom.mk (P := P) hom_1 property_1

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
inst_1 : P.IsMultiplicative
X Y : WideSubcategory P
f g : X ⟶ Y
h : f.hom (P := P) = g.hom (P := P)
⊢ f = g

Tactic:
InducedWideCategory.Hom.ext h

Premises used: CategoryTheory.InducedWideCategory.Hom.ext
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
inst_1 : P.IsMultiplicative
X : WideSubcategory P
⊢ InducedWideCategory.Hom.hom (P := P) (𝟙 X) = 𝟙 (X.obj (_P := P))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
inst_1 : P.IsMultiplicative
X Y Z : WideSubcategory P
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom (P := P) = f.hom (P := P) ≫ g.hom (P := P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
inst_1 : P.IsMultiplicative
X : WideSubcategory P
⊢ Functor.obj (wideSubcategoryInclusion P) X = X.obj (_P := P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
inst_1 : P.IsMultiplicative
X Y : WideSubcategory P
f : X ⟶ Y
⊢ Functor.map (wideSubcategoryInclusion P) f = f.hom (P := P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Widesubcategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
inst_1 : P.IsMultiplicative
⊢ Functor.Faithful (C := WideSubcategory P) (wideSubcategoryInclusion P)

Tactic:
inferInstanceAs (wideInducedFunctor WideSubcategory.obj P).Faithful

Premises used: _private.0.CategoryTheory.wideSubcategory.faithful._proof_1
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : Hom star (of X)
⊢ False

Tactic:
(f : PEmpty).elim

Premises used: PEmpty.elim
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Eq.{v + 1} (α := X ⟶ X) (down (𝟙 (of X))) (𝟙 X)

Tactic:
rfl

Premises used: CategoryTheory.WithTerminal.id, CategoryTheory.WithTerminal.down, rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : of X ⟶ of Y
g : of Y ⟶ of Z
⊢ down (f ≫ g) = down f ≫ down g

Tactic:
rfl

Premises used: CategoryTheory.WithTerminal.comp, CategoryTheory.WithTerminal.down, rfl
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : star ⟶ of X
⊢ False

Tactic:
(f : PEmpty).elim

Premises used: PEmpty.elim
-- Module: Mathlib.CategoryTheory.WithTerminal.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F G : Functor.{v, v_1, u, u_1} C D
η : F ⟶ G
X Y : WithTerminal C
f_1 : X ⟶ Y
x y : C
f : of x ⟶ of y
⊢ Eq (α := (map F).obj (of x) ⟶ (map G).obj (of y))
    ((map F).map f ≫
      match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) of y with
      | of x => η.app x
      | star => 𝟙 star)
    ((match (motive := (X : WithTerminal C) → (map F).obj X ⟶ (map G).obj X) of x with
      | of x => η.app x
      | star => 𝟙 star) ≫
      (map G).map f)

Tactic:
η.naturality f

Premises used: CategoryTheory.WithTerminal.comp, CategoryTheory.WithTerminal.Hom, CategoryTheory.NatTrans.naturality, CategoryTheory.WithTerminal.down