awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : IsMonoidalRightDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
        (coprod.inr :
          tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
        (hom (∂R X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
      tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (coprod.inr ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
have rw : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
    coprod.inr (coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)))
  (coprod.inr ▷ X)
Tactic: rw [rightDistrib_hom, coprod.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : IsMonoidalRightDistrib.{v, u_1} C
X Y Z : C
rw :
  Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (CategoryStruct.comp (Y :=
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X)) coprod.inr
      (coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)))
    (coprod.inr ▷ X)
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
        (coprod.inr :
          tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
        (hom (∂R X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
      tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
    (coprod.inr ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
have rw₁ : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (coprod.inr ▷ X) (coprod.inr ▷ X)
Tactic: rw [rightDistrib_hom, coprod.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : IsMonoidalRightDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
        (coprod.inl ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
        (Iso.inv (∂R X Y Z) :
          tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X)) :
      tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
    (coprod.inl :
      tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
have apply : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
          (coprod.inl ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
          (Iso.inv (∂R X Y Z) :
            tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X ⟶
              coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X)) :
        tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (hom (∂R X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
    tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (coprod.inl :
        tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (hom (∂R X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
    tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
Tactic: apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : IsMonoidalRightDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
        (coprod.inr ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
        (Iso.inv (∂R X Y Z) :
          tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X)) :
      tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
    (coprod.inr :
      tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
have apply : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
          (coprod.inr ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
          (Iso.inv (∂R X Y Z) :
            tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X ⟶
              coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X)) :
        tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (hom (∂R X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
    tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (coprod.inr :
        tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X))
      (hom (∂R X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) Y X) (tensorObj.{v, u_1} (𝒞 := inst) Z X) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X) :
    tensorObj.{v, u_1} (𝒞 := inst) Z X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
Tactic: apply (cancel_iso_hom_right _ _ (∂R X Y Z)).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : MonoidalClosed.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z) ⟶
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
    (Iso.inv (∂L X Y Z) :
      tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z) ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
    (uncurry (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
      tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z) ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
have rw : Eq.{v + 1} (α :=
  coprod.{v, u_1} Y Z ⟶
    Functor.obj.{v, v, u_1, u_1} (ihom X)
      (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
  (curry (Iso.inv (∂L X Y Z)) :
    coprod.{v, u_1} Y Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
  (coprod.desc (curry coprod.inl) (curry coprod.inr) :
    coprod.{v, u_1} Y Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
Tactic: rw [← curry_eq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : MonoidalClosed.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    coprod.{v, u_1} Y Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (curry (Iso.inv (∂L X Y Z)) :
      coprod.{v, u_1} Y Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (coprod.desc (curry coprod.inl) (curry coprod.inr) :
      coprod.{v, u_1} Y Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
have h₁ : Eq.{v + 1} (α :=
  Y ⟶
    Functor.obj.{v, v, u_1, u_1} (ihom X)
      (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
  (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) (coprod.inl : Y ⟶ coprod.{v, u_1} Y Z)
      (curry (Iso.inv (∂L X Y Z)) :
        coprod.{v, u_1} Y Z ⟶
          Functor.obj.{v, v, u_1, u_1} (ihom X)
            (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))) :
    Y ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
  (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) coprod.inl (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
    Y ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Monoidal (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : MonoidalCategory.{v, u_1} C
inst_2 : HasBinaryCoproducts.{v, u_1} C
inst_3 : MonoidalClosed.{v, u_1} C
X Y Z : C
h₁ :
  Eq.{v + 1} (α :=
    Y ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) (coprod.inl : Y ⟶ coprod.{v, u_1} Y Z)
        (curry (Iso.inv (∂L X Y Z)) :
          coprod.{v, u_1} Y Z ⟶
            Functor.obj.{v, v, u_1, u_1} (ihom X)
              (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))) :
      Y ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) coprod.inl (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
      Y ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
⊢ Eq.{v + 1} (α :=
    coprod.{v, u_1} Y Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (curry (Iso.inv (∂L X Y Z)) :
      coprod.{v, u_1} Y Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
    (coprod.desc (curry coprod.inl) (curry coprod.inr) :
      coprod.{v, u_1} Y Z ⟶
        Functor.obj.{v, v, u_1, u_1} (ihom X)
          (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
have h₂ : Eq.{v + 1} (α :=
  Z ⟶
    Functor.obj.{v, v, u_1, u_1} (ihom X)
      (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
  (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) (coprod.inr : Z ⟶ coprod.{v, u_1} Y Z)
      (curry (Iso.inv (∂L X Y Z)) :
        coprod.{v, u_1} Y Z ⟶
          Functor.obj.{v, v, u_1, u_1} (ihom X)
            (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))) :
    Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
  (CategoryStruct.comp (Y := coprod.{v, u_1} Y Z) coprod.inr (coprod.desc (curry coprod.inl) (curry coprod.inr)) :
    Z ⟶
      Functor.obj.{v, v, u_1, u_1} (ihom X)
        (coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : Y ⟶ X
inst_1 : EffectiveEpi f
Z : C
m₁ m₂ : X ⟶ Z
h : f ≫ m₁ = f ≫ m₂
⊢ m₁ = m₂
have rw : m₁ = desc f (f ≫ m₂) sorry
Tactic: rw [show m₂ = desc f (f ≫ m₂) (fun _ _ h => by simp [← assoc, h]) from uniq _ _ _ _ rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ m₂ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯
have hm : ∀ (a : α), π a ≫ m₂ = π a ≫ m₂
Tactic: apply EffectiveEpiFamily.uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
⊢ m₁ = m₂
have this : m₂ = desc X π (fun (a : α) ↦ π a ≫ m₂) sorry
Tactic: have : m₂ = EffectiveEpiFamily.desc X π (fun a => π a ≫ m₂)
      (fun a₁ a₂ g₁ g₂ h => by simp only [← assoc, h]) := by
    apply EffectiveEpiFamily.uniq; intro; rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B W : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
m₁ m₂ : B ⟶ W
h : ∀ (a : α), π a ≫ m₁ = π a ≫ m₂
this : m₂ = desc X π (fun (a : α) ↦ π a ≫ m₂) ⋯
⊢ m₁ = m₂
have rw : m₁ = desc X π (fun (a : α) ↦ π a ≫ m₂) sorry
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
W : C
e : (a : Unit) → X ⟶ W
h :
  ∀ {Z : C} (a₁ a₂ : Unit) (g₁ g₂ : Z ⟶ X),
    Eq (α := Z ⟶ B)
        (g₁ ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a₁ with
          | PUnit.unit => f)
        (g₂ ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a₂ with
          | PUnit.unit => f) →
      g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm :
  ∀ (a : Unit),
    (match (motive := (x : Unit) → (fun (x : Unit) ↦ X) x ⟶ B) a with
        | PUnit.unit => f) ≫
        m =
      e a
⊢ m = desc f (e ()) ⋯
have hm₁ : f ≫ m = e ()
Tactic: apply EffectiveEpi.uniq f (e ()) (h () ())
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ π a ≫ CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Iso.inv (asIso (Sigma.desc π))) (Sigma.desc e) = e a
have this : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Iso.hom (asIso (Sigma.desc π)))
Tactic: have : π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom := by simp only [asIso_hom,
      colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
this : π a = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Iso.hom (asIso (Sigma.desc π)))
⊢ π a ≫ CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Iso.inv (asIso (Sigma.desc π))) (Sigma.desc e) = e a
have rw : CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a)
    (Iso.hom (asIso (Sigma.desc π)) ≫
      CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Iso.inv (asIso (Sigma.desc π))) (Sigma.desc e)) =
  e a
Tactic: rw [this, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
⊢ m = CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Iso.inv (asIso (Sigma.desc π))) (Sigma.desc e)
have simp : Eq (α := sigmaObj.{u_2, v_1, u_1} X ⟶ W) (Sigma.desc π ≫ m) (Sigma.desc e)
Tactic: simp only [asIso_inv, IsIso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
⊢ Eq (α := sigmaObj.{u_2, v_1, u_1} X ⟶ W) (Sigma.desc π ≫ m) (Sigma.desc e)
have h₁ : ∀ (a : α),
  CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π ≫ m) =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
Tactic: ext a
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : IsIso (X := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B ⟶ W
hm : ∀ (a : α), π a ≫ m = e a
a : α
⊢ CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc π ≫ m) =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X a) (Sigma.desc e)
have h₁ : π a ≫ m = e a
Tactic: simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app,
      colimit.ι_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
α' : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
e : α' ≃ α
P :
  EffectiveEpiFamilyStruct.{v_1, u_1, u_3} (C := C) (B := B) (fun (a : α') ↦ X ((e : (a : α') → α) a)) fun (a : α') ↦
    π ((e : (a : α') → α) a)
W : C
x : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x a₁ = g₂ ≫ x a₂
a : α
⊢ π a ≫ P.desc (fun (x_1 : α') ↦ x ((e : (a : α') → α) x_1)) ⋯ = x a
have obtain : ∀ (a : α'),
  Eq (α := X ((e : (a : α') → α) a) ⟶ W)
    (π ((e : (a : α') → α) a) ≫ P.desc (fun (x_1 : α') ↦ x ((e : (a : α') → α) x_1)) sorry) (x ((e : (a : α') → α) a))
Tactic: obtain ⟨a, rfl⟩ := e.surjective a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan.{u_2, v_1, u_1} X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst_1 : EffectiveEpiFamily X π
W : C
e : c.pt ⟶ W
h :
  ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt),
    Eq (α := Z ⟶ (Cofan.mk B π).pt) (g₁ ≫ hc.desc (Cofan.mk B π)) (g₂ ≫ hc.desc (Cofan.mk B π)) → g₁ ≫ e = g₂ ≫ e
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ Eq (α := Z ⟶ W) (g₁ ≫ (fun (a : α) ↦ (c.ι.app { as := a } ≫ e : X a ⟶ W)) a₁)
    (g₂ ≫ (fun (a : α) ↦ (c.ι.app { as := a } ≫ e : X a ⟶ W)) a₂)
have simp : (g₁ ≫ c.ι.app { as := a₁ : Discrete α }) ≫ e = (g₂ ≫ c.ι.app { as := a₂ : Discrete α }) ≫ e
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.EffectiveEpi.Coproduct (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst_1 : HasCoproduct.{u_2, v_1, u_1} X
inst_2 : EffectiveEpiFamily X π
e : EffectiveEpiStruct (Y := (Cofan.mk (sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X)).pt)
  (IsColimit.desc (coproductIsCoproduct X) (Cofan.mk B π)) :=
  effectiveEpiStructIsColimitDescOfEffectiveEpiFamily X (Cofan.mk (sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X))
    (coproductIsCoproduct X) π
⊢ EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
have simp : ∀ (e : EffectiveEpiStruct (Y := sigmaObj.{u_2, v_1, u_1} X) (colimit.desc (Discrete.functor X) (Cofan.mk B π))),
  EffectiveEpi (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.desc π)
Tactic: simp only [Cofan.mk_pt, coproductIsCoproduct, colimit.cocone_x, IsColimit.ofIsoColimit_desc,
    Cocone.ext_inv_hom, Iso.refl_inv, colimit.isColimit_desc, Category.id_comp] at e
Cleared hypotheses: e