awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ x₂ : X₁ i₁
hx :
  Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
obtain :
  ∀
    (hx :
      Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) :
              (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
            ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁))
                x₁ :
              (fun (X : Type u) ↦ X) (X₂ i₁)) :
          (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) :
              (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
            ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁))
                x₁ :
              (fun (X : Type u) ↦ X) (X₂ i₁)) :
          (fun (X : Type u) ↦ X) (∐ X₂))),
    Eq (α := ∐ X₁)
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
        (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
        (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
⊢ Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)

Tactic:
obtain rfl := h _ (Cofan.inj_injective_of_isColimit (coproductIsCoproduct X₂) i₁ hx)

Premises used: CategoryTheory.Limits.Cofan.inj_injective_of_isColimit, CategoryTheory.Limits.coproductIsCoproduct, rfl
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
hx :
  Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
⊢ Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.UnivLE
Goal:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
obtain : ∀ (a' : Type v) (m : Nonempty (uliftFunctor.{u, v}.obj a' ≅ α)), Small.{v, max u v} α
⊢ Small.{v, max u v} α

Tactic:
obtain ⟨a', m⟩ := w.mem_essImage α

Premises used: CategoryTheory.Functor.EssSurj.mem_essImage
-- Module: Mathlib.CategoryTheory.UnivLE
Goal:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m : Nonempty (uliftFunctor.{u, v}.obj a' ≅ α)
obtain : ∀ (m' : uliftFunctor.{u, v}.obj a' ≅ α), Small.{v, max u v} α
⊢ Small.{v, max u v} α

Tactic:
obtain ⟨m'⟩ := m
-- Module: Mathlib.CategoryTheory.UnivLE
Goal:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m' : uliftFunctor.{u, v}.obj a' ≅ α
⊢ Small.{v, max u v} α

Tactic:
⟨a', ⟨(Iso.toEquiv m').symm.trans Equiv.ulift⟩⟩

Premises used: CategoryTheory.Iso.toEquiv, Equiv.trans, Equiv.ulift, Small.mk, Nonempty.intro, Exists.intro, Equiv.symm
-- Module: Mathlib.CategoryTheory.UnivLE
Goal:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m' : uliftFunctor.{u, v}.obj a' ≅ α
⊢ Small.{v, max u v} α

Tactic:
exact ⟨a', ⟨(Iso.toEquiv m').symm.trans Equiv.ulift⟩⟩
-- Module: Mathlib.CategoryTheory.UnivLE
Goal:
⊢ UnivLE.{max u v, v} ↔ uliftFunctor.{u, v}.EssSurj

Tactic:
⟨fun _ => inferInstance, fun w => UnivLE.ofEssSurj w⟩

Premises used: inferInstance, Iff.intro, UnivLE.ofEssSurj
-- Module: Mathlib.CategoryTheory.UnivLE
Goal:
inst : UnivLE.{max u v, v}
⊢ UnivLE.witness.Faithful

Tactic:
inferInstanceAs <| Functor.Faithful (_ ⋙ _)

Premises used: _private.0.instFaithfulWitness._proof_1
-- Module: Mathlib.CategoryTheory.UnivLE
Goal:
inst : UnivLE.{max u v, v}
⊢ UnivLE.witness.Full

Tactic:
inferInstanceAs <| Functor.Full (_ ⋙ _)

Premises used: _private.0.instFullWitness._proof_1
-- 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
X Y : C
f : X ⟶ Y
rw : G.map (F.map f) ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f
rw₁ : G.map (F.map f) ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ H.map (F.map f)
rw₂ rw₃ : α.app (F.obj X) ≫ H.map (F.map f) = α.app (F.obj X) ≫ H.map (F.map f)
⊢ (F ⋙ G).map f ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f

Tactic:
rw [Functor.comp_map, Functor.comp_map, α.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map
-- 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
w : ∀ (x : C), (𝟙 F ◫ α).app x = (F.whiskerLeft α).app x
⊢ 𝟙 F ◫ α = F.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 : Functor.{v₁, v₂, u₁, u₂} C D
G H : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ H
x : C
⊢ (𝟙 F ◫ α).app x = (F.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
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ⟶ H
F : Functor.{v₂, v₃, u₂, u₃} D E
X Y : C
f : X ⟶ Y
rw : F.map (G.map f) ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f
rw₁ : F.map (G.map f) ≫ F.map (α.app Y) = F.map (α.app X) ≫ F.map (H.map f)
rw₂ : F.map (G.map f ≫ α.app Y) = F.map (α.app X) ≫ F.map (H.map f)
rw₃ : F.map (G.map f ≫ α.app Y) = F.map (α.app X ≫ H.map f)
rw₄ rw₅ : F.map (α.app X ≫ H.map f) = F.map (α.app X ≫ H.map f)
⊢ (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]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- 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
w : ∀ (x : C), (α ◫ 𝟙 F).app x = (whiskerRight α F).app x
⊢ α ◫ 𝟙 F = whiskerRight α F

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
G H : Functor.{v₁, v₂, u₁, u₂} C D
α : G ⟶ H
F : Functor.{v₂, v₃, u₂, u₃} D E
x : C
⊢ (α ◫ 𝟙 F).app x = (whiskerRight α F).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
X_1 Y_1 : Functor.{v₁, v₂, u₁, u₂} C D
τ : X_1 ⟶ Y_1
H : Functor.{v₂, v₃, u₂, u₃} D E
X Y : C
f : X ⟶ Y
dsimp : H.map (X_1.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y_1.map f)
⊢ (obj
            { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ X_1 ⋙ G,
              map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ X_1.whiskerLeft α, map_id := ⋯,
              map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
            H).map
        f ≫
      H.map (τ.app Y) =
    H.map (τ.app X) ≫
      (obj
            { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ Y_1 ⋙ G,
              map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ Y_1.whiskerLeft α, map_id := ⋯,
              map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
            H).map
        f

Tactic:
dsimp
-- 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
X_1 Y_1 : Functor.{v₁, v₂, u₁, u₂} C D
τ : X_1 ⟶ Y_1
H : Functor.{v₂, v₃, u₂, u₃} D E
X Y : C
f : X ⟶ Y
rw : H.map (X_1.map f ≫ τ.app Y) = H.map (τ.app X) ≫ H.map (Y_1.map f)
rw₁ : H.map (X_1.map f ≫ τ.app Y) = H.map (τ.app X ≫ Y_1.map f)
rw₂ rw₃ : H.map (X_1.map f ≫ τ.app Y) = H.map (X_1.map f ≫ τ.app Y)
⊢ H.map (X_1.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y_1.map f)

Tactic:
rw [← H.map_comp, ← H.map_comp, ← τ.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_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
X_1 Y_1 : Functor.{v₁, v₂, u₁, u₂} C D
τ : X_1 ⟶ Y_1
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
w :
  ∀ (x : C),
    Eq (α :=
      (obj
              { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ X_1 ⋙ G,
                map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ X_1.whiskerLeft α, map_id := ⋯,
                map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
              X).obj
          x ⟶
        (obj
              { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ Y_1 ⋙ G,
                map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ Y_1.whiskerLeft α, map_id := ⋯,
                map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
              Y).obj
          x)
      (NatTrans.app
        (map
            { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ X_1 ⋙ G,
              map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ X_1.whiskerLeft α, map_id := ⋯,
              map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
            f ≫
          { app := fun (c : C) ↦ Y.map (τ.app c), naturality := ⋯ })
        x)
      (NatTrans.app
        ({ app := fun (c : C) ↦ X.map (τ.app c), naturality := ⋯ } ≫
          map
            { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ Y_1 ⋙ G,
              map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ Y_1.whiskerLeft α, map_id := ⋯,
              map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
            f)
        x)
⊢ Eq (α :=
    obj
        { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ X_1 ⋙ G,
          map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ X_1.whiskerLeft α, map_id := ⋯, map_comp := ⋯ :
          Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
        X ⟶
      obj
        { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ Y_1 ⋙ G,
          map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ Y_1.whiskerLeft α, map_id := ⋯, map_comp := ⋯ :
          Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
        Y)
    (map
        { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ X_1 ⋙ G,
          map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ X_1.whiskerLeft α, map_id := ⋯, map_comp := ⋯ :
          Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
        f ≫
      { app := fun (c : C) ↦ Y.map (τ.app c), naturality := ⋯ })
    ({ app := fun (c : C) ↦ X.map (τ.app c), naturality := ⋯ } ≫
      map
        { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ Y_1 ⋙ G,
          map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ Y_1.whiskerLeft α, map_id := ⋯, map_comp := ⋯ :
          Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
        f)

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
X_1 Y_1 : Functor.{v₁, v₂, u₁, u₂} C D
τ : X_1 ⟶ Y_1
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
x : C
w : f.app (X_1.obj x) ≫ Y.map (τ.app x) = X.map (τ.app x) ≫ f.app (Y_1.obj x)
⊢ Eq (α :=
    (obj
            { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ X_1 ⋙ G,
              map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ X_1.whiskerLeft α, map_id := ⋯,
              map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
            X).obj
        x ⟶
      (obj
            { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ Y_1 ⋙ G,
              map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ Y_1.whiskerLeft α, map_id := ⋯,
              map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
            Y).obj
        x)
    (NatTrans.app
      (map
          { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ X_1 ⋙ G,
            map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ X_1.whiskerLeft α, map_id := ⋯,
            map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          f ≫
        { app := fun (c : C) ↦ Y.map (τ.app c), naturality := ⋯ })
      x)
    (NatTrans.app
      ({ app := fun (c : C) ↦ X.map (τ.app c), naturality := ⋯ } ≫
        map
          { obj := fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ Y_1 ⋙ G,
            map := fun {X Y : Functor.{v₂, v₃, u₂, u₃} D E} (α : X ⟶ Y) ↦ Y_1.whiskerLeft α, map_id := ⋯,
            map_comp := ⋯ : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          f)
      x)

Tactic:
dsimp
-- 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
X_1 Y_1 : Functor.{v₁, v₂, u₁, u₂} C D
τ : X_1 ⟶ Y_1
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
x : C
w w₁ : f.app (X_1.obj x) ≫ Y.map (τ.app x) = f.app (X_1.obj x) ≫ Y.map (τ.app x)
⊢ f.app (X_1.obj x) ≫ Y.map (τ.app x) = X.map (τ.app x) ≫ f.app (Y_1.obj x)

Tactic:
rw [f.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- 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
X_1 Y_1 : Functor.{v₂, v₃, u₂, u₃} D E
τ : X_1 ⟶ Y_1
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
dsimp : X_1.map (F.map f) ≫ τ.app (F.obj Y) = τ.app (F.obj X) ≫ Y_1.map (F.map f)
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (obj.{v₁, v₃, u₁, u₃}
        (obj
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ X_1,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α X_1, map_id := ⋯,
            map_comp := ⋯ }
          F)
        X)
      (obj.{v₁, v₃, u₁, u₃}
        (obj
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ Y_1,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α Y_1, map_id := ⋯,
            map_comp := ⋯ }
          F)
        Y))
    (map
        (obj
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ X_1,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α X_1, map_id := ⋯,
            map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          F)
        f ≫
      τ.app (F.obj Y))
    (τ.app (F.obj X) ≫
      map
        (obj
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ Y_1,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α Y_1, map_id := ⋯,
            map_comp := ⋯ }
          F)
        f)

Tactic:
dsimp
-- 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
X_1 Y_1 : Functor.{v₂, v₃, u₂, u₃} D E
τ : X_1 ⟶ Y_1
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
rw rw₁ : τ.app (F.obj X) ≫ Y_1.map (F.map f) = τ.app (F.obj X) ≫ Y_1.map (F.map f)
⊢ X_1.map (F.map f) ≫ τ.app (F.obj Y) = τ.app (F.obj X) ≫ Y_1.map (F.map f)

Tactic:
rw [τ.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- 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
X_1 Y_1 : Functor.{v₂, v₃, u₂, u₃} D E
τ : X_1 ⟶ Y_1
X Y : Functor.{v₁, v₂, u₁, u₂} C D
f : X ⟶ Y
w :
  ∀ (x : C),
    Eq.{v₃ + 1} (α :=
      Quiver.Hom.{v₃, u₃} (V := E)
        (obj.{v₁, v₃, u₁, u₃}
          (obj
            { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ X_1,
              map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α X_1, map_id := ⋯,
              map_comp := ⋯ }
            X)
          x)
        (obj.{v₁, v₃, u₁, u₃}
          (obj
            { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ Y_1,
              map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α Y_1, map_id := ⋯,
              map_comp := ⋯ }
            Y)
          x))
      (NatTrans.app
        (map
            { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ X_1,
              map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α X_1, map_id := ⋯,
              map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
            f ≫
          { app := fun (c : C) ↦ τ.app (Y.obj c), naturality := ⋯ })
        x)
      (NatTrans.app
        ({ app := fun (c : C) ↦ τ.app (X.obj c), naturality := ⋯ } ≫
          map
            { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ Y_1,
              map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α Y_1, map_id := ⋯,
              map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
            f)
        x)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₁, v₃, u₁, u₃} C E)
      (obj
        { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ X_1,
          map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α X_1, map_id := ⋯, map_comp := ⋯ }
        X)
      (obj
        { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ Y_1,
          map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α Y_1, map_id := ⋯, map_comp := ⋯ }
        Y))
    (map
        { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ X_1,
          map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α X_1, map_id := ⋯, map_comp := ⋯ :
          Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
        f ≫
      { app := fun (c : C) ↦ τ.app (Y.obj c), naturality := ⋯ })
    ({ app := fun (c : C) ↦ τ.app (X.obj c), naturality := ⋯ } ≫
      map
        { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ Y_1,
          map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α Y_1, map_id := ⋯, map_comp := ⋯ :
          Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
        f)

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
X_1 Y_1 : Functor.{v₂, v₃, u₂, u₃} D E
τ : X_1 ⟶ Y_1
X Y : Functor.{v₁, v₂, u₁, u₂} C D
f : X ⟶ Y
x : C
w : X_1.map (f.app x) ≫ τ.app (Y.obj x) = τ.app (X.obj x) ≫ Y_1.map (f.app x)
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := E)
      (obj.{v₁, v₃, u₁, u₃}
        (obj
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ X_1,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α X_1, map_id := ⋯,
            map_comp := ⋯ }
          X)
        x)
      (obj.{v₁, v₃, u₁, u₃}
        (obj
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ Y_1,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α Y_1, map_id := ⋯,
            map_comp := ⋯ }
          Y)
        x))
    (NatTrans.app
      (map
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ X_1,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α X_1, map_id := ⋯,
            map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          f ≫
        { app := fun (c : C) ↦ τ.app (Y.obj c), naturality := ⋯ })
      x)
    (NatTrans.app
      ({ app := fun (c : C) ↦ τ.app (X.obj c), naturality := ⋯ } ≫
        map
          { obj := fun (F : Functor.{v₁, v₂, u₁, u₂} C D) ↦ F ⋙ Y_1,
            map := fun {X Y : Functor.{v₁, v₂, u₁, u₂} C D} (α : X ⟶ Y) ↦ whiskerRight α Y_1, map_id := ⋯,
            map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          f)
      x)

Tactic:
dsimp
-- 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
X_1 Y_1 : Functor.{v₂, v₃, u₂, u₃} D E
τ : X_1 ⟶ Y_1
X Y : Functor.{v₁, v₂, u₁, u₂} C D
f : X ⟶ Y
x : C
w w₁ : X_1.map (f.app x) ≫ τ.app (Y.obj x) = X_1.map (f.app x) ≫ τ.app (Y.obj x)
⊢ X_1.map (f.app x) ≫ τ.app (Y.obj x) = τ.app (X.obj x) ≫ Y_1.map (f.app x)

Tactic:
rw [← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- 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 Y : Functor.{v₁, v₂, u₁, u₂} C D
a₁ a₂ : X ⟶ Y
hαβ :
  Eq (α := obj (obj (whiskeringRight C D E) F) X ⟶ obj (obj (whiskeringRight C D E) F) Y)
    (map (obj (whiskeringRight C D E) F) a₁) (map (obj (whiskeringRight C D E) F) a₂)
w : ∀ (X_1 : C), a₁.app X_1 = a₂.app X_1
⊢ a₁ = a₂

Tactic:
ext X
-- 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:
F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X

Premises used: congr_arg, CategoryTheory.Functor.map_injective, congr_fun, CategoryTheory.NatTrans.app