awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C ⊕ C'
f g : x ⟶ y
inl :
  ∀ (x y : C) (f : x ⟶ y) (g : Functor.obj (Sum.inl_ C C') x ⟶ Functor.obj (Sum.inl_ C C') y),
    Functor.map (Sum.inl_ C C') f = g
⊢ f = g
have inr : ∀ (x y : C') (f : x ⟶ y) (g : Functor.obj (Sum.inr_ C C') x ⟶ Functor.obj (Sum.inr_ C C') y),
  Functor.map (Sum.inr_ C C') f = g
Tactic: cases f
Cleared hypotheses: x, y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C
f : x ⟶ y
g : Functor.obj (Sum.inl_ C C') x ⟶ Functor.obj (Sum.inl_ C C') y
⊢ Functor.map (Sum.inl_ C C') f = g
have inl : ∀ (f_1 : x ⟶ y),
  Eq (α := Functor.obj (Sum.inl_ C C') x ⟶ Functor.obj (Sum.inl_ C C') y) (Functor.map (Sum.inl_ C C') f)
    (Functor.map (Sum.inl_ C C') f_1)
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C'
f : x ⟶ y
g : Functor.obj (Sum.inr_ C C') x ⟶ Functor.obj (Sum.inr_ C C') y
⊢ Functor.map (Sum.inr_ C C') f = g
have inr : ∀ (f_1 : x ⟶ y),
  Eq (α := Functor.obj (Sum.inr_ C C') x ⟶ Functor.obj (Sum.inr_ C C') y) (Functor.map (Sum.inr_ C C') f)
    (Functor.map (Sum.inr_ C C') f_1)
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C
f g : x ⟶ y
⊢ Eq (α := Functor.obj (Sum.inl_ C C') x ⟶ Functor.obj (Sum.inl_ C C') y) (Functor.map (Sum.inl_ C C') f)
    (Functor.map (Sum.inl_ C C') g)
have rw : Eq (α := Functor.obj (Sum.inl_ C C') x ⟶ Functor.obj (Sum.inl_ C C') y) (Functor.map (Sum.inl_ C C') g)
  (Functor.map (Sum.inl_ C C') g)
Tactic: rw [((by assumption : IsDiscrete C).subsingleton x y).allEq f g]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C'
f g : x ⟶ y
⊢ Eq (α := Functor.obj (Sum.inr_ C C') x ⟶ Functor.obj (Sum.inr_ C C') y) (Functor.map (Sum.inr_ C C') f)
    (Functor.map (Sum.inr_ C C') g)
have rw : Eq (α := Functor.obj (Sum.inr_ C C') x ⟶ Functor.obj (Sum.inr_ C C') y) (Functor.map (Sum.inr_ C C') g)
  (Functor.map (Sum.inr_ C C') g)
Tactic: rw [((by assumption : IsDiscrete C').subsingleton x y).allEq f g]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C
f : x ⟶ y
⊢ Functor.obj (Sum.inl_ C C') x = Functor.obj (Sum.inl_ C C') y
have inl : Functor.obj (Sum.inl_ C C') y = Functor.obj (Sum.inl_ C C') y
Tactic: rw [(by assumption : IsDiscrete C).eq_of_hom f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C'
f : x ⟶ y
⊢ Functor.obj (Sum.inr_ C C') x = Functor.obj (Sum.inr_ C C') y
have inr : Functor.obj (Sum.inr_ C C') y = Functor.obj (Sum.inr_ C C') y
Tactic: rw [(by assumption : IsDiscrete C').eq_of_hom f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C ⊕ C'
f : x ⟶ y
⊢ x = y
have inl : ∀ (x y : C) (f : x ⟶ y), Functor.obj (Sum.inl_ C C') x = Functor.obj (Sum.inl_ C C') y
Tactic: cases f with
    | inl x y f => rw [(by assumption : IsDiscrete C).eq_of_hom f]
    | inr x y f => rw [(by assumption : IsDiscrete C').eq_of_hom f]
Cleared hypotheses: x, y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Discrete.SumsProducts (goal)
Goal:
C : Type u_1
C' : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C'
D : Type u_3
inst_2 : Category.{v_3, u_3} D
inst_3 : IsDiscrete.{v_1, u_1} C
inst_4 : IsDiscrete.{v_2, u_2} C'
inst_5 : IsDiscrete.{v_3, u_3} D
x y : C ⊕ C'
f : x ⟶ y
inl : ∀ (x y : C) (f : x ⟶ y), Functor.obj (Sum.inl_ C C') x = Functor.obj (Sum.inl_ C C') y
⊢ x = y
have inr : ∀ (x y : C') (f : x ⟶ y), Functor.obj (Sum.inr_ C C') x = Functor.obj (Sum.inr_ C C') y
Tactic: cases f with
    | inl x y f => rw [(by assumption : IsDiscrete C).eq_of_hom f]
    | inr x y f => rw [(by assumption : IsDiscrete C').eq_of_hom f]
Cleared hypotheses: x, y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Cartesian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : IsCartesianDistributive.{v, u} C
A B Z : C
f g : Z ⟶ Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }
he :
  Eq (α :=
    Z ⟶
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair A B) (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr)))
        { as := WalkingPair.left : Discrete WalkingPair })
    (f ≫ BinaryCofan.inl (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr))
    (g ≫ BinaryCofan.inl (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr))
ι : A ⟶ coprod.{v, u} A B := coprod.inl
⊢ f = g
have this : Mono (X := tensorObj.{v, u} (𝒞 := inst) Z A) (Z ◁ ι)
Tactic: have : Mono (Z ◁ ι) := SplitMono.mono
        { retraction := (∂L Z A B).inv ≫ coprod.desc (𝟙 _) (fst Z B ≫ lift (𝟙 Z) f) }
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Cartesian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : IsCartesianDistributive.{v, u} C
A B Z : C
f g : Z ⟶ Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }
he :
  Eq (α :=
    Z ⟶
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair A B) (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr)))
        { as := WalkingPair.left : Discrete WalkingPair })
    (f ≫ BinaryCofan.inl (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr))
    (g ≫ BinaryCofan.inl (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr))
ι : A ⟶ coprod.{v, u} A B := coprod.inl
this : Mono (X := tensorObj.{v, u} (𝒞 := inst) Z A) (Z ◁ ι)
⊢ Eq (α :=
    Z ⟶
      tensorObj.{v, u} (𝒞 := inst) Z
        (Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
    (lift (𝟙 Z) f) (lift (𝟙 Z) g)
have rw : Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) Z (coprod.{v, u} A B)) (lift (𝟙 Z) f ≫ Z ◁ ι) (lift (𝟙 Z) g ≫ Z ◁ ι)
Tactic: rw [← cancel_mono (Z ◁ ι)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Distributive.Cartesian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : IsCartesianDistributive.{v, u} C
A B Z : C
f g : Z ⟶ Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }
he :
  Eq (α :=
    Z ⟶
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair A B) (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr)))
        { as := WalkingPair.left : Discrete WalkingPair })
    (f ≫ BinaryCofan.inl (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr))
    (g ≫ BinaryCofan.inl (BinaryCofan.mk (P := coprod.{v, u} A B) coprod.inl coprod.inr))
ι : A ⟶ coprod.{v, u} A B := coprod.inl
this : Mono (X := tensorObj.{v, u} (𝒞 := inst) Z A) (Z ◁ ι)
⊢ f = g
have this₁ : Eq (α :=
  Z ⟶
    tensorObj.{v, u} (𝒞 := inst) Z
      (Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (lift (𝟙 Z) f) (lift (𝟙 Z) g)
Tactic: have : lift (𝟙 Z) f = lift (𝟙 Z) g := by rw [← cancel_mono (Z ◁ ι)]; aesop
-- 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 : IsMonoidalLeftDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (coprod.inl :
          tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (hom (∂L X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (X ◁ coprod.inl : tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
have rw : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
    coprod.inl (coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr)))
  (X ◁ coprod.inl)
Tactic: rw [leftDistrib_hom, coprod.inl_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 : IsMonoidalLeftDistrib.{v, u_1} C
X Y Z : C
rw :
  Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)) coprod.inl
      (coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr)))
    (X ◁ coprod.inl)
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (coprod.inl :
          tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (hom (∂L X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (X ◁ coprod.inl : tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
have rw₁ : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (X ◁ coprod.inl) (X ◁ coprod.inl)
Tactic: rw [leftDistrib_hom, coprod.inl_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 : IsMonoidalLeftDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (coprod.inr :
          tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (hom (∂L X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (X ◁ coprod.inr : tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
have rw : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
    coprod.inr (coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr)))
  (X ◁ coprod.inr)
Tactic: rw [leftDistrib_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 : IsMonoidalLeftDistrib.{v, u_1} C
X Y Z : C
rw :
  Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z)) coprod.inr
      (coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr)))
    (X ◁ coprod.inr)
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (CategoryStruct.comp (Y :=
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (coprod.inr :
          tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
            coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
        (hom (∂L X Y Z) :
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
            tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
    (X ◁ coprod.inr : tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
have rw₁ : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (X ◁ coprod.inr) (X ◁ coprod.inr)
Tactic: rw [leftDistrib_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 : IsMonoidalLeftDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
        (X ◁ coprod.inl : tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y 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)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
    (coprod.inl :
      tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
have apply : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
          (X ◁ coprod.inl : tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y 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)) :
        tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (hom (∂L X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
    tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (coprod.inl :
        tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (hom (∂L X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
    tensorObj.{v, u_1} (𝒞 := inst) X Y ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
Tactic: apply (cancel_iso_hom_right _ _ (∂L 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 : IsMonoidalLeftDistrib.{v, u_1} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
      coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
        (X ◁ coprod.inr : tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y 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)) :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
    (coprod.inr :
      tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
have apply : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
          (X ◁ coprod.inr : tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y 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)) :
        tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (hom (∂L X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
    tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
  (CategoryStruct.comp (Y := coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (coprod.inr :
        tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶
          coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z))
      (hom (∂L X Y Z) :
        coprod.{v, u_1} (tensorObj.{v, u_1} (𝒞 := inst) X Y) (tensorObj.{v, u_1} (𝒞 := inst) X Z) ⟶
          tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z)) :
    tensorObj.{v, u_1} (𝒞 := inst) X Z ⟶ tensorObj.{v, u_1} (𝒞 := inst) X (coprod.{v, u_1} Y Z))
Tactic: apply (cancel_iso_hom_right _ _ (∂L 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) 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)
    (coprod.inl ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
have rw : 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))
    coprod.inl (coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)))
  (coprod.inl ▷ X)
Tactic: rw [rightDistrib_hom, coprod.inl_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) 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
      (coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X)))
    (coprod.inl ▷ X)
⊢ 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))
        (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)
    (coprod.inl ▷ X : tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
have rw₁ : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) Y X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (coprod.{v, u_1} Y Z) X)
  (coprod.inl ▷ X) (coprod.inl ▷ X)
Tactic: rw [rightDistrib_hom, coprod.inl_desc]