awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
n : ℕ
⊢ Fintype.card.{u_1} (incl.obj (mk n)).obj = n
have h : Fintype.card.{u_1} (incl.obj (mk n)).obj = Finset.card (α := Fin n) Finset.univ
Tactic: convert! Finset.card_fin n
-- Lean 4 proof step from Mathlib.CategoryTheory.FintypeCat (goal)
Goal:
n : ℕ
⊢ Fintype.card.{u_1} (incl.obj (mk n)).obj = Finset.card (α := Fin n) Finset.univ
have h : Fintype.card.{u_1} (ULift.{u_1, 0} (Fin n)) = Fintype.card (Fin n)
Tactic: dsimp [incl, mk, len]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g
have rw : F.map g = F.map g
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F.toPrefunctor = G.toPrefunctor
⊢ F = G
have obtain : ∀ (obj : C → D) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X))
  (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
  (h :
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
      G.toPrefunctor),
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } = G
Tactic: obtain ⟨obj, map, _, _⟩ := F
Cleared hypotheses: F, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    G.toPrefunctor
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } = G
have obtain : ∀ (obj' : C → D) (map' : {X Y : C} → (X ⟶ Y) → (obj' X ⟶ obj' Y)) (map_id_1 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj' X))
  (map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g)
  (h :
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
      { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor),
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }
Tactic: obtain ⟨obj', map', _, _⟩ := G
Cleared hypotheses: G, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj' : C → D
map' : {X Y : C} → (X ⟶ Y) → (obj' X ⟶ obj' Y)
map_id_1 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj' X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := obj', map := @map', map_id := map_id_1, map_comp := @map_comp_1 }
have obtain : ∀ (map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id_2 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X))
  (map_comp_2 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g)
  (h :
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
      { obj := obj, map := @map', map_id := map_id_2, map_comp := @map_comp_2 }.toPrefunctor),
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := obj, map := @map', map_id := map_id_2, map_comp := @map_comp_2 }
Tactic: obtain rfl : obj = obj' := congr_arg Prefunctor.obj h
Cleared hypotheses: obj', map', map_id_1, map_comp_1, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map' : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id_1 : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj X)
map_comp_1 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
    { obj := obj, map := @map', map_id := map_id_1, map_comp := @map_comp_1 }.toPrefunctor
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := obj, map := @map', map_id := map_id_1, map_comp := @map_comp_1 }
have obtain : ∀ (map_id_2 : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X))
  (map_comp_2 : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
  (h :
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D }.toPrefunctor =
      { obj := obj, map := @map, map_id := map_id_2, map_comp := @map_comp_2 }.toPrefunctor),
  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₂, u₁, u₂} C D } =
    { obj := obj, map := @map, map_id := map_id_2, map_comp := @map_comp_2 }
Tactic: obtain rfl : @map = @map' := by simpa [Functor.toPrefunctor] using h
Cleared hypotheses: map', map_id_1, map_comp_1, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α β : F ⟶ G
h : α = β
X : C
⊢ α.app X = β.app X
have rw : β.app X = β.app X
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst_2 : IsIso (α.app X)
inst_3 : IsIso (α.app Y)
⊢ inv (α.app X) ≫ F.map f = G.map f ≫ inv (α.app Y)
have rw : F.map f ≫ α.app Y = α.app X ≫ G.map f
Tactic: rw [IsIso.inv_comp_eq, ← Category.assoc, IsIso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
inst_2 : ∀ (X : C), Epi (α.app X)
Z : Functor.{v₁, v₂, u₁, u₂} C D
g h : G ⟶ Z
eq : α ≫ g = α ≫ h
⊢ g = h
have w : ∀ (X : C), g.app X = h.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
inst_2 : ∀ (X : C), Epi (α.app X)
Z : Functor.{v₁, v₂, u₁, u₂} C D
g h : G ⟶ Z
eq : α ≫ g = α ≫ h
X : C
⊢ g.app X = h.app X
have w : α.app X ≫ g.app X = α.app X ≫ h.app X
Tactic: rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
inst_2 : ∀ (X : C), Epi (α.app X)
Z : Functor.{v₁, v₂, u₁, u₂} C D
g h : G ⟶ Z
eq : α ≫ g = α ≫ h
X : C
w : α.app X ≫ g.app X = α.app X ≫ h.app X
⊢ g.app X = h.app X
have w₁ : (α ≫ g).app X = α.app X ≫ h.app X
Tactic: rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
inst_2 : ∀ (X : C), Epi (α.app X)
Z : Functor.{v₁, v₂, u₁, u₂} C D
g h : G ⟶ Z
eq : α ≫ g = α ≫ h
X : C
w : α.app X ≫ g.app X = α.app X ≫ h.app X
w₁ : (α ≫ g).app X = α.app X ≫ h.app X
⊢ g.app X = h.app X
have w₂ : (α ≫ h).app X = α.app X ≫ h.app X
Tactic: rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
inst_2 : ∀ (X : C), Epi (α.app X)
Z : Functor.{v₁, v₂, u₁, u₂} C D
g h : G ⟶ Z
eq : α ≫ g = α ≫ h
X : C
w : α.app X ≫ g.app X = α.app X ≫ h.app X
w₁ : (α ≫ g).app X = α.app X ≫ h.app X
w₂ : (α ≫ h).app X = α.app X ≫ h.app X
⊢ g.app X = h.app X
have w₃ : α.app X ≫ h.app X = α.app X ≫ h.app X
Tactic: rw [← cancel_epi (α.app X), ← comp_app, eq, comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
α β : Quiver.Hom (V := Functor.{v₁, v₁, u₁, u₁} C C) (𝟭 C) (𝟭 C)
⊢ α ≫ β = β ≫ α
have w : ∀ (X : C), (α ≫ β).app X = (β ≫ α).app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (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 I : Functor.{v₂, v₃, u₂, u₃} D E
α : G ⟶ F
β : I ⟶ H
⊢ { app := fun (X : C) ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ : NatTrans (G ⋙ I) (F ⋙ H) } =
    mk' (fun (X : C) ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯
have w : ∀ (x : C),
  { app := fun (X : C) ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := sorry : NatTrans (G ⋙ I) (F ⋙ H) }.app x =
    (mk' (fun (X : C) ↦ I.map (α.app X) ≫ β.app (F.obj X)) sorry).app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Category (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 H : Functor.{v₁, v₂, u₁, u₂} C D
I J K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ⟶ G
β : G ⟶ H
γ : I ⟶ J
δ : J ⟶ K
⊢ (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ
have w : ∀ (x : C), ((α ≫ β) ◫ (γ ≫ δ)).app x = ((α ◫ γ) ≫ β ◫ δ).app x
Tactic: cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
X Y Z : C × D
f : X ⟶ Y
g : Y ⟶ Z
⊢ (F.map (f ≫ g).1).app X.2 ≫ (F.obj Z.1).map (f ≫ g).2 =
    ((F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2) ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
have simp : (F.map f.1).app X.2 ≫ (F.map g.1).app X.2 ≫ (F.obj Z.1).map f.2 ≫ (F.obj Z.1).map g.2 =
  (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
Tactic: simp only [prod_comp_fst, prod_comp_snd, Functor.map_comp, NatTrans.comp_app,
          Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
X Y Z : C × D
f : X ⟶ Y
g : Y ⟶ Z
| (F.map g.1).app X.2 ≫ (F.obj Z.1).map f.2
have a : (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2
Tactic: rw [← NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
X Y Z : C × D
f : X ⟶ Y
g : Y ⟶ Z
⊢ (F.map f.1).app X.2 ≫ (F.map g.1).app X.2 ≫ (F.obj Z.1).map f.2 ≫ (F.obj Z.1).map g.2 =
    (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
have slice_lhs : (F.map f.1).app X.2 ≫ ((F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2) ≫ (F.obj Z.1).map g.2 =
  (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
Tactic: slice_lhs 2 3 => rw [← NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
X Y Z : C × D
f : X ⟶ Y
g : Y ⟶ Z
⊢ (F.map f.1).app X.2 ≫ ((F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2) ≫ (F.obj Z.1).map g.2 =
    (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
have rw : (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2 =
  (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
⊢ Eq.{v₄ + 1} (α :=
    Quiver.Hom.{v₄, u₄} (V := E)
      (obj
        { obj := fun (X : C × D) ↦ (X_1.obj X.1).obj X.2,
          map := fun {X Y : C × D} (f : X ⟶ Y) ↦ (X_1.map f.1).app X.2 ≫ (X_1.obj Y.1).map f.2, map_id := ⋯,
          map_comp := ⋯ }
        X)
      (obj
        { obj := fun (X : C × D) ↦ (Y_1.obj X.1).obj X.2,
          map := fun {X Y : C × D} (f : X ⟶ Y) ↦ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2, map_id := ⋯,
          map_comp := ⋯ }
        Y))
    (map
        { obj := fun (X : C × D) ↦ (X_1.obj X.1).obj X.2,
          map := fun {X Y : C × D} (f : X ⟶ Y) ↦ (X_1.map f.1).app X.2 ≫ (X_1.obj Y.1).map f.2, map_id := ⋯,
          map_comp := ⋯ : C × D ⥤ E }
        f ≫
      NatTrans.app (T.app Y.1) Y.2)
    (NatTrans.app (T.app X.1) X.2 ≫
      map
        { obj := fun (X : C × D) ↦ (Y_1.obj X.1).obj X.2,
          map := fun {X Y : C × D} (f : X ⟶ Y) ↦ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2, map_id := ⋯,
          map_comp := ⋯ }
        f)
have simp : (X_1.map f.1).app X.2 ≫ (X_1.obj Y.1).map f.2 ≫ NatTrans.app (T.app Y.1) Y.2 =
  NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
| (X_1.obj Y.1).map f.2 ≫ NatTrans.app (T.app Y.1) Y.2
have a : NatTrans.app (T.app Y.1) X.2 ≫ (Y_1.obj Y.1).map f.2
Tactic: rw [NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
⊢ (X_1.map f.1).app X.2 ≫ (X_1.obj Y.1).map f.2 ≫ NatTrans.app (T.app Y.1) Y.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
have slice_lhs : (X_1.map f.1).app X.2 ≫ NatTrans.app (T.app Y.1) X.2 ≫ (Y_1.obj Y.1).map f.2 =
  NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
Tactic: slice_lhs 2 3 => rw [NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
| (X_1.map f.1).app X.2 ≫ NatTrans.app (T.app Y.1) X.2
have a : NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2
Tactic: rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
⊢ (X_1.map f.1).app X.2 ≫ NatTrans.app (T.app Y.1) X.2 ≫ (Y_1.obj Y.1).map f.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
have slice_lhs : (NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2) ≫ (Y_1.obj Y.1).map f.2 =
  NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
Tactic: slice_lhs 1 2 => rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
⊢ (NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2) ≫ (Y_1.obj Y.1).map f.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
have rw : NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2 =
  NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 X ×ₘ 𝟙 Y) = 𝟙 (F.obj (X, Y))
have rw : F.map (𝟙 (X, Y)) = 𝟙 (F.obj (X, Y))
Tactic: rw [← prod_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₃, v₄, u₃, u₄} D E)
      { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
        map_comp := ⋯ })
    { app := fun (Y : D) ↦ F.map (𝟙 X ×ₘ 𝟙 Y), naturality := ⋯ }
    (𝟙
      { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
        map_comp := ⋯ })
have w : ∀ (Y : D),
  Eq.{v₄ + 1} (α :=
    Quiver.Hom.{v₄, u₄} (V := E)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := sorry,
          map_comp := sorry }
        Y)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := sorry,
          map_comp := sorry }
        Y))
    (NatTrans.app { app := fun (Y : D) ↦ F.map (𝟙 X ×ₘ 𝟙 Y), naturality := sorry } Y)
    (NatTrans.app
      (𝟙
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := sorry,
          map_comp := sorry })
      Y)
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₃, v₄, u₃, u₄} D E)
      { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun (Y : D) ↦ F.obj (Z, Y), map := fun {X Y : D} (g : X ⟶ Y) ↦ F.map (𝟙 Z ×ₘ g), map_id := ⋯,
        map_comp := ⋯ })
    { app := fun (Y_1 : D) ↦ F.map (f ≫ g ×ₘ 𝟙 Y_1), naturality := ⋯ }
    (CategoryStruct.comp (Y :=
      { obj := fun (Y_1 : D) ↦ F.obj (Y, Y_1), map := fun {X Y_1 : D} (g : X ⟶ Y_1) ↦ F.map (𝟙 Y ×ₘ g), map_id := ⋯,
        map_comp := ⋯ })
      { app := fun (Y_1 : D) ↦ F.map (f ×ₘ 𝟙 Y_1), naturality := ⋯ }
      { app := fun (Y_1 : D) ↦ F.map (g ×ₘ 𝟙 Y_1), naturality := ⋯ })
have w : ∀ (Y_1 : D),
  Eq.{v₄ + 1} (α :=
    Quiver.Hom.{v₄, u₄} (V := E)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := sorry,
          map_comp := sorry }
        Y_1)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (Z, Y), map := fun {X Y : D} (g : X ⟶ Y) ↦ F.map (𝟙 Z ×ₘ g), map_id := sorry,
          map_comp := sorry }
        Y_1))
    (NatTrans.app { app := fun (Y_2 : D) ↦ F.map (f ≫ g ×ₘ 𝟙 Y_2), naturality := sorry } Y_1)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        { obj := fun (Y_2 : D) ↦ F.obj (Y, Y_2), map := fun {X Y_2 : D} (g : X ⟶ Y_2) ↦ F.map (𝟙 Y ×ₘ g), map_id := sorry,
          map_comp := sorry })
        { app := fun (Y_2 : D) ↦ F.map (f ×ₘ 𝟙 Y_2), naturality := sorry }
        { app := fun (Y_2 : D) ↦ F.map (g ×ₘ 𝟙 Y_2), naturality := sorry })
      Y_1)
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C × D ⥤ E
T : X_1 ⟶ Y_1
X : C
Y Y' : D
g : Y ⟶ Y'
⊢ (X_1.curryObj.obj X).map g ≫ T.app (X, Y') = T.app (X, Y) ≫ (Y_1.curryObj.obj X).map g
have dsimp : X_1.map (𝟙 X ×ₘ g) ≫ T.app (X, Y') = T.app (X, Y) ≫ Y_1.map (𝟙 X ×ₘ g)
Tactic: dsimp [curryObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C × D ⥤ E
T : X_1 ⟶ Y_1
X : C
Y Y' : D
g : Y ⟶ Y'
⊢ X_1.map (𝟙 X ×ₘ g) ≫ T.app (X, Y') = T.app (X, Y) ≫ Y_1.map (𝟙 X ×ₘ g)
have rw : T.app (X, Y) ≫ Y_1.map (𝟙 X ×ₘ g) = T.app (X, Y) ≫ Y_1.map (𝟙 X ×ₘ g)
Tactic: rw [NatTrans.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Currying (goal)
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y : C × D ⥤ E
T : X_1 ⟶ Y
X X' : C
f : X ⟶ X'
⊢ X_1.curryObj.map f ≫ { app := fun (Y_1 : D) ↦ T.app (X', Y_1), naturality := ⋯ } =
    { app := fun (Y_1 : D) ↦ T.app (X, Y_1), naturality := ⋯ : NatTrans (X_1.curryObj.obj X) (Y.curryObj.obj X) } ≫
      Y.curryObj.map f
have w : ∀ (x : D),
  NatTrans.app (X_1.curryObj.map f ≫ { app := fun (Y_1 : D) ↦ T.app (X', Y_1), naturality := sorry }) x =
    NatTrans.app
      ({ app := fun (Y_1 : D) ↦ T.app (X, Y_1), naturality := sorry : NatTrans (X_1.curryObj.obj X) (Y.curryObj.obj X) } ≫
        Y.curryObj.map f)
      x
Tactic: ext