awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ (F ⋙ G).map f ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f
have rw₁ : G.map (F.map f) ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ H.map (F.map f)
Tactic: rw [Functor.comp_map, Functor.comp_map, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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)
⊢ (F ⋙ G).map f ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f
have rw₂ : α.app (F.obj X) ≫ H.map (F.map f) = α.app (F.obj X) ≫ H.map (F.map f)
Tactic: rw [Functor.comp_map, Functor.comp_map, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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 ◫ α = F.whiskerLeft α
have w : ∀ (x : C), (𝟙 F ◫ α).app x = (F.whiskerLeft α).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f
have rw : F.map (G.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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f
have rw₁ : F.map (G.map f) ≫ F.map (α.app Y) = F.map (α.app X) ≫ F.map (H.map f)
Tactic: rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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)
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f
have rw₂ : F.map (G.map f ≫ α.app Y) = F.map (α.app X) ≫ F.map (H.map f)
Tactic: rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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)
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f
have rw₃ : F.map (G.map f ≫ α.app Y) = F.map (α.app X ≫ H.map f)
Tactic: rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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)
⊢ (G ⋙ F).map f ≫ F.map (α.app Y) = F.map (α.app X) ≫ (H ⋙ F).map f
have rw₄ : F.map (α.app X ≫ H.map f) = F.map (α.app X ≫ H.map f)
Tactic: rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ α ◫ 𝟙 F = whiskerRight α F
have w : ∀ (x : C), (α ◫ 𝟙 F).app x = (whiskerRight α F).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ (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
have dsimp : H.map (X_1.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y_1.map f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ H.map (X_1.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y_1.map f)
have rw : H.map (X_1.map f ≫ τ.app Y) = H.map (τ.app X) ≫ H.map (Y_1.map f)
Tactic: rw [← H.map_comp, ← H.map_comp, ← τ.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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)
⊢ H.map (X_1.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y_1.map f)
have rw₁ : H.map (X_1.map f ≫ τ.app Y) = H.map (τ.app X ≫ Y_1.map f)
Tactic: rw [← H.map_comp, ← H.map_comp, ← τ.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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)
⊢ H.map (X_1.map f) ≫ H.map (τ.app Y) = H.map (τ.app X) ≫ H.map (Y_1.map f)
have rw₂ : H.map (X_1.map f ≫ τ.app Y) = H.map (X_1.map f ≫ τ.app Y)
Tactic: rw [← H.map_comp, ← H.map_comp, ← τ.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ 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)
have 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 := sorry,
              map_comp := sorry : 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 := sorry,
              map_comp := sorry : 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 := sorry,
            map_comp := sorry : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          f ≫
        { app := fun (c : C) ↦ Y.map (τ.app c), naturality := sorry })
      x)
    (NatTrans.app
      ({ app := fun (c : C) ↦ X.map (τ.app c), naturality := sorry } ≫
        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 := sorry,
            map_comp := sorry : Functor.{v₂, v₃, u₂, u₃} D E ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          f)
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ 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)
have w : f.app (X_1.obj x) ≫ Y.map (τ.app x) = X.map (τ.app x) ≫ f.app (Y_1.obj x)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ f.app (X_1.obj x) ≫ Y.map (τ.app x) = X.map (τ.app x) ≫ f.app (Y_1.obj x)
have w : f.app (X_1.obj x) ≫ Y.map (τ.app x) = f.app (X_1.obj x) ≫ Y.map (τ.app x)
Tactic: rw [f.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ 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)
have dsimp : X_1.map (F.map f) ≫ τ.app (F.obj Y) = τ.app (F.obj X) ≫ Y_1.map (F.map f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ X_1.map (F.map f) ≫ τ.app (F.obj Y) = τ.app (F.obj X) ≫ Y_1.map (F.map f)
have rw : τ.app (F.obj X) ≫ Y_1.map (F.map f) = τ.app (F.obj X) ≫ Y_1.map (F.map f)
Tactic: rw [τ.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ 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)
have 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 := sorry,
            map_comp := sorry }
          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 := sorry,
            map_comp := sorry }
          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 := sorry,
            map_comp := sorry : Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          f ≫
        { app := fun (c : C) ↦ τ.app (Y.obj c), naturality := sorry })
      x)
    (NatTrans.app
      ({ app := fun (c : C) ↦ τ.app (X.obj c), naturality := sorry } ≫
        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 := sorry,
            map_comp := sorry : Functor.{v₁, v₂, u₁, u₂} C D ⥤ Functor.{v₁, v₃, u₁, u₃} C E }
          f)
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ 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)
have w : X_1.map (f.app x) ≫ τ.app (Y.obj x) = τ.app (X.obj x) ≫ Y_1.map (f.app x)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ X_1.map (f.app x) ≫ τ.app (Y.obj x) = τ.app (X.obj x) ≫ Y_1.map (f.app x)
have w : X_1.map (f.app x) ≫ τ.app (Y.obj x) = X_1.map (f.app x) ≫ τ.app (Y.obj x)
Tactic: rw [← NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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₂)
⊢ a₁ = a₂
have w : ∀ (X_1 : C), a₁.app X_1 = a₂.app X_1
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ X.map g ≫ hF.preimage (f.app x_1) = hF.preimage (f.app x) ≫ Y.map g
have apply : F.map (X.map g ≫ hF.preimage (f.app x_1)) = F.map (hF.preimage (f.app x) ≫ Y.map g)
Tactic: apply hF.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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 ≫ hF.preimage (f.app x_1)) = F.map (hF.preimage (f.app x) ≫ Y.map g)
have dsimp : F.map (X.map g ≫ hF.preimage (f.app x_1)) = F.map (hF.preimage (f.app x) ≫ Y.map g)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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 ≫ hF.preimage (f.app x_1)) = F.map (hF.preimage (f.app x) ≫ Y.map g)
have simp : F.map (X.map g) ≫ f.app x_1 = f.app x ≫ F.map (Y.map g)
Tactic: simp only [map_comp, map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ F.whiskerLeft β ≫ whiskerRight α K = whiskerRight α H ≫ G.whiskerLeft β
have w : ∀ (x : C), (F.whiskerLeft β ≫ whiskerRight α K).app x = (whiskerRight α H ≫ G.whiskerLeft β).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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
⊢ α ◫ β = F.whiskerLeft β ≫ whiskerRight α K
have w : ∀ (x : C), (α ◫ β).app x = (F.whiskerLeft β ≫ whiskerRight α K).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Whiskering (goal)
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 α
⊢ inv (whiskerRight α F) = whiskerRight (inv α) F
have symm : whiskerRight (inv α) F = inv (whiskerRight α F)
Tactic: symm