awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X : C
hX : Eq.{v₁ + 1} (α := X ⟶ X) (𝟙 X) 0
rw : F.map (𝟙 X) = 0
rw₁ : Eq (α := F.obj X ⟶ F.obj X) (F.map 0) 0
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) 0
have rw₂ : Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) 0 0
Tactic: rw [← F.map_id, hX, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have calc_1 : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
Tactic: calc
      dsimp% F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
      _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
      _ = 0 := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
calc_1 : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have calc_2 : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
  (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
    (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))
Tactic: calc
      dsimp% F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
      _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
      _ = 0 := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
calc_1 : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
calc_2 :
  Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
      (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have calc_3 : Eq (α := F.obj X ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) (F.obj Y))
  (CategoryStruct.comp (Y := F.obj (F.rightAdjoint.obj (F.obj X))) (F.map 0)
    (F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)))
  0
Tactic: calc
      dsimp% F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
      _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
      _ = 0 := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y))
have calc_1 : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0 ≫ 𝟙 (F.obj Y))
Tactic: rw [Adjunction.left_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) 0
have calc_1 : Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
Tactic: calc
      G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 := ?_
      _ = adj.unit.app (G.obj X) ≫ G.map ((leftAdjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 := ?_
      _ = 0 := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
calc_1 : Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
⊢ Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) 0
have calc_2 : Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
  (adj.unit.app (G.obj X) ≫
    CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))
Tactic: calc
      G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 := ?_
      _ = adj.unit.app (G.obj X) ≫ G.map ((leftAdjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 := ?_
      _ = 0 := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
calc_1 : Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
calc_2 :
  Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
    (adj.unit.app (G.obj X) ≫
      CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))
⊢ Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) 0
have calc_3 : Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y)
  (adj.unit.app (G.obj X) ≫
    CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))
  0
Tactic: calc
      G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 := ?_
      _ = adj.unit.app (G.obj X) ≫ G.map ((leftAdjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 := ?_
      _ = 0 := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
have calc_1 : Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (G.map 0)
Tactic: rw [Adjunction.right_triangle_components_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Full
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map (CategoryStruct.comp (Y := Y) 0 (F.preimage 0)))
have rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0)
Tactic: rw [zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Full
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := Y) 0 (F.preimage 0))) 0
have rw : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (F.map (F.preimage 0))) 0
Tactic: rw [F.map_comp, F.map_preimage, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Full
X Y : C
rw : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (F.map (F.preimage 0))) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := Y) 0 (F.preimage 0))) 0
have rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj Y) (F.map 0) 0) 0
Tactic: rw [F.map_comp, F.map_preimage, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Full
X Y : C
rw : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (F.map (F.preimage 0))) 0
rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj Y) (F.map 0) 0) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := Y) 0 (F.preimage 0))) 0
have rw₂ : Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj Y) 0 0
Tactic: rw [F.map_comp, F.map_preimage, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.PreservesZeroMorphisms
⊢ Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 (F.obj 0))
have rw : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map (𝟙 0))
Tactic: rw [← F.map_id, id_zero, F.map_zero, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.PreservesZeroMorphisms
rw : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map (𝟙 0))
⊢ Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 (F.obj 0))
have rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map 0)
Tactic: rw [← F.map_id, id_zero, F.map_zero, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.PreservesZeroMorphisms
rw : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map (𝟙 0))
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map 0)
⊢ Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 (F.obj 0))
have rw₂ : Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) 0
Tactic: rw [← F.map_id, id_zero, F.map_zero, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.PreservesZeroMorphisms
rw : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map (𝟙 0))
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map 0)
rw₂ : Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) 0
⊢ Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 (F.obj 0))
have rw₃ : Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) 0 0
Tactic: rw [← F.map_id, id_zero, F.map_zero, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.PreservesZeroMorphisms
⊢ Eq.{v₂ + 1} (α := Quiver.Hom.{v₂, u₂} (V := D) 0 0) (CategoryStruct.comp (Y := F.obj 0) 0 0) (𝟙 0)
have rw : Eq.{v₂ + 1} (α := Quiver.Hom.{v₂, u₂} (V := D) 0 0) (CategoryStruct.comp (Y := F.obj 0) 0 0) 0
Tactic: rw [id_zero, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (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
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.PreservesZeroMorphisms
rw : Eq.{v₂ + 1} (α := Quiver.Hom.{v₂, u₂} (V := D) 0 0) (CategoryStruct.comp (Y := F.obj 0) 0 0) 0
⊢ Eq.{v₂ + 1} (α := Quiver.Hom.{v₂, u₂} (V := D) 0 0) (CategoryStruct.comp (Y := F.obj 0) 0 0) (𝟙 0)
have rw₁ : Eq.{v₂ + 1} (α := Quiver.Hom.{v₂, u₂} (V := D) 0 0) 0 0
Tactic: rw [id_zero, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
i : F.obj 0 ≅ 0
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
have rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map (CategoryStruct.comp (Y := 0) 0 0))
Tactic: rw [← Functor.map_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
i : F.obj 0 ≅ 0
X Y : C
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map (CategoryStruct.comp (Y := 0) 0 0))
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
have rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0)
Tactic: rw [← Functor.map_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
i : F.obj 0 ≅ 0
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
    (F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0)
have rw : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0)) (F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0)
Tactic: rw [Iso.hom_inv_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
i : F.obj 0 ≅ 0
X Y : C
rw :
  Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0)) (F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0)
⊢ Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
    (F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0)
have rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
  (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
Tactic: rw [Iso.hom_inv_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : IsZero G
J : Type u_1
inst_4 : Category.{v_1, u_1} J
K : Functor.{v_1, v₁, u_1, u₁} J C
c : Cone K
x : IsLimit c
⊢ IsLimit (G.mapCone c)
have rw : (hG : ∀ (X : C), IsZero.{v₂, u₂} (G.obj X)) →
  (J : Type u_1) →
    [inst_5 : Category.{v_1, u_1} J] →
      {K : Functor.{v_1, v₁, u_1, u₁} J C} → {c : Cone K} → IsLimit c → IsLimit (G.mapCone c)
Tactic: rw [Functor.isZero_iff] at hG
Cleared hypotheses: hG, J, inst_4, K, c, x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : IsZero G
J : Type u_1
inst_4 : Category.{v_1, u_1} J
K : Functor.{v_1, v₁, u_1, u₁} J C
c : Cocone K
x : IsColimit c
⊢ IsColimit (G.mapCocone c)
have rw : (hG : ∀ (X : C), IsZero.{v₂, u₂} (G.obj X)) →
  (J : Type u_1) →
    [inst_5 : Category.{v_1, u_1} J] →
      {K : Functor.{v_1, v₁, u_1, u₁} J C} → {c : Cocone K} → IsColimit c → IsColimit (G.mapCocone c)
Tactic: rw [Functor.isZero_iff] at hG
Cleared hypotheses: hG, J, inst_4, K, c, x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc : IsColimit c
⊢ IsColimit.{v', v, u', u} (F := K ⋙ Functor.obj sigmaConst R) (Functor.mapCocone (Functor.obj sigmaConst R) c)
have hc₁ : Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
  ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
Tactic: replace hc := (Types.isColimit_iff_coconeTypesIsColimit ..).1 ⟨hc⟩
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
j j' : J
g : j ⟶ j'
⊢ Eq (α := K.obj j → (R ⟶ s.pt))
    ((fun (k : K.obj j') ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j') ↦ R) k ≫ s.ι.app j') ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (K.map g)) :
        (a : (fun (X : Type w) ↦ X) (K.obj j)) → (fun (X : Type w) ↦ X) (K.obj j')))
    fun (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j
have h : ∀ (x_1 : (fun (X : Type w) ↦ X) (K.obj j)),
  ((fun (k : K.obj j') ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j') ↦ R) k ≫ s.ι.app j') ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (K.map g)) :
          (a : (fun (X : Type w) ↦ X) (K.obj j)) → (fun (X : Type w) ↦ X) (K.obj j')))
      x_1 =
    Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) x_1 ≫ s.ι.app j
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
j : J
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v', v, u', u}
        (Functor.obj (Functor.const J)
          (Cocone.pt.{v', v, u', u} (F := K ⋙ Functor.obj sigmaConst R)
            (Functor.mapCocone (Functor.obj sigmaConst R) c)))
        j)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj sigmaConst R) c)) j)
      (Sigma.desc (hc.desc (coconeTypes s))) =
    s.ι.app j
have dsimp : CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
    (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : K.obj j) → c.pt) fun (x : K.obj j) ↦
      𝟙 R)
    (Sigma.desc (hc.desc (coconeTypes s))) =
  s.ι.app j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
j : J
⊢ CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
      (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : K.obj j) → c.pt) fun (x : K.obj j) ↦
        𝟙 R)
      (Sigma.desc (hc.desc (coconeTypes s))) =
    s.ι.app j
have h : ∀ (k : K.obj j),
  CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : K.obj j) ↦ R)
      (Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
        (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : K.obj j) → c.pt) fun (x : K.obj j) ↦
          𝟙 R)
        (Sigma.desc (hc.desc (coconeTypes s)))) =
    Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j
Tactic: ext k