awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsDiscrete.{v_1, u_1} C
unop unop_1 : C
f : Opposite.unop (Opposite.op unop_1) ⟶ Opposite.unop (Opposite.op unop)
obtain :
  ∀ (f : Opposite.unop (Opposite.op unop_1) ⟶ Opposite.unop (Opposite.op (Opposite.unop (Opposite.op unop_1)))),
    Opposite.op (Opposite.unop (Opposite.op unop_1)) = Opposite.op unop_1
⊢ Opposite.op unop = Opposite.op unop_1

Tactic:
obtain rfl := obj_ext_of_isDiscrete f

Premises used: CategoryTheory.obj_ext_of_isDiscrete, rfl
-- Module: Mathlib.CategoryTheory.Discrete.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : IsDiscrete.{v_1, u_1} C
unop : C
f : Opposite.unop (Opposite.op unop) ⟶ Opposite.unop (Opposite.op (Opposite.unop (Opposite.op unop)))
⊢ Opposite.op (Opposite.unop (Opposite.op unop)) = Opposite.op unop

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Discrete.StructuredArrow
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
F : Functor.{v, w, u, w} C (Discrete T)
t : T
inst_1 : Subsingleton T
X : C
⊢ { as := t : Discrete T } = F.obj X

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Discrete.StructuredArrow
Goal:
C : Type u
inst : Category.{v, u} C
T : Type w
F : Functor.{v, w, u, w} C (Discrete T)
t : T
inst_1 : Subsingleton T
X : C
⊢ F.obj X = { as := t }

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
Goal:
J : Type u_1
K : Type u_2
X Y : Prod.{u_1, u_2} (Discrete J) (Discrete K)
x : X ⟶ Y
f₁ : X.1 ⟶ Y.1
f₂ : X.2 ⟶ Y.2
⊢ X.1.as = Y.1.as

Tactic:
discrete_cases
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
Goal:
J : Type u_1
K : Type u_2
X Y : Prod.{u_1, u_2} (Discrete J) (Discrete K)
x : X ⟶ Y
f₁ : X.1 ⟶ Y.1
f₂ : X.2 ⟶ Y.2
f₃ : X.1.as = Y.1.as
⊢ X.2.as = Y.2.as

Tactic:
discrete_cases
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
Goal:
J : Type u_1
K : Type u_2
X Y : Prod.{u_1, u_2} (Discrete J) (Discrete K)
x : X ⟶ Y
f₁ : X.1.as = Y.1.as
f₂ : X.2.as = Y.2.as
dsimp : { as := (X.1.as, X.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }
⊢ Eq (α := Discrete (J × K))
    (match (motive := Prod.{u_1, u_2} (Discrete J) (Discrete K) → Discrete (J × K)) X with
      | (x, y) => { as := (x.as, y.as) } :
      Discrete (J × K))
    (match (motive := Prod.{u_1, u_2} (Discrete J) (Discrete K) → Discrete (J × K)) Y with
      | (x, y) => { as := (x.as, y.as) } :
      Discrete (J × K))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
Goal:
J : Type u_1
K : Type u_2
X Y : Prod.{u_1, u_2} (Discrete J) (Discrete K)
x : X ⟶ Y
f₁ : X.1.as = Y.1.as
f₂ : X.2.as = Y.2.as
rw : { as := (Y.1.as, X.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }
rw₁ rw₂ : { as := (Y.1.as, Y.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }
⊢ { as := (X.1.as, X.2.as) : Discrete (J × K) } = { as := (Y.1.as, Y.2.as) }

Tactic:
rw [f₁, f₂]
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
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
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
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)
⊢ Functor.map (Sum.inl_ C C') f = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
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)
⊢ Functor.map (Sum.inr_ C C') f = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
⊢ IsDiscrete.{v_1, u_1} C

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
rw 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)
⊢ 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)

Tactic:
rw [((by assumption : IsDiscrete C).subsingleton x y).allEq f g]

Premises used: Subsingleton.allEq
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
⊢ IsDiscrete.{v_2, u_2} C'

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
rw 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)
⊢ 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)

Tactic:
rw [((by assumption : IsDiscrete C').subsingleton x y).allEq f g]

Premises used: Subsingleton.allEq
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
⊢ IsDiscrete.{v_1, u_1} C

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
inl inl₁ : Functor.obj (Sum.inl_ C C') y = Functor.obj (Sum.inl_ C C') y
⊢ Functor.obj (Sum.inl_ C C') x = Functor.obj (Sum.inl_ C C') y

Tactic:
rw [(by assumption : IsDiscrete C).eq_of_hom f]

Premises used: CategoryTheory.IsDiscrete.eq_of_hom
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
⊢ IsDiscrete.{v_2, u_2} C'

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
inr inr₁ : Functor.obj (Sum.inr_ C C') y = Functor.obj (Sum.inr_ C C') y
⊢ Functor.obj (Sum.inr_ C C') x = Functor.obj (Sum.inr_ C C') y

Tactic:
rw [(by assumption : IsDiscrete C').eq_of_hom f]

Premises used: CategoryTheory.IsDiscrete.eq_of_hom
-- Module: Mathlib.CategoryTheory.Discrete.SumsProducts
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
inr : ∀ (x y : C') (f : x ⟶ y), Functor.obj (Sum.inr_ C C') x = Functor.obj (Sum.inr_ C C') y
⊢ x = 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]

Premises used: CategoryTheory.IsDiscrete.eq_of_hom
-- Module: Mathlib.CategoryTheory.Distributive.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : IsMonoidalLeftDistrib.{v, u} C
⊢ IsCartesianDistributive.{v, u} C

Tactic:
letI : BraidedCategory C := Nonempty.some inferInstance
  SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib

Premises used: CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib
-- Module: Mathlib.CategoryTheory.Distributive.Cartesian
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
⊢ 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) }
-- Module: Mathlib.CategoryTheory.Distributive.Cartesian
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 ◁ ι)
rw : Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) Z (coprod.{v, u} A B)) (lift (𝟙 Z) f ≫ Z ◁ ι) (lift (𝟙 Z) g ≫ 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)

Tactic:
rw [← cancel_mono (Z ◁ ι)]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Distributive.Cartesian
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 (coprod.{v, u} A B)) (lift (𝟙 Z) f ≫ Z ◁ ι) (lift (𝟙 Z) g ≫ Z ◁ ι)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Distributive.Cartesian
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)

Tactic:
have : lift (𝟙 Z) f = lift (𝟙 Z) g := by rw [← cancel_mono (Z ◁ ι)]; aesop
-- Module: Mathlib.CategoryTheory.Distributive.Cartesian
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_1 : Mono (X := tensorObj.{v, u} (𝒞 := inst) Z A) (Z ◁ ι)
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)
⊢ f = g

Tactic:
simpa only [lift_snd] using this =≫ snd _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.CartesianMonoidalCategory.lift_snd
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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} (α :=
    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))
    (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))
    (coprod.desc (X ◁ coprod.inl) (X ◁ coprod.inr) :
      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))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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)
rw₁ 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)
⊢ 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))

Tactic:
rw [leftDistrib_hom, coprod.inl_desc]

Premises used: CategoryTheory.Limits.coprod.inl_desc, CategoryTheory.leftDistrib_hom
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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)
rw₁ 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)
⊢ 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))

Tactic:
rw [leftDistrib_hom, coprod.inr_desc]

Premises used: CategoryTheory.Limits.coprod.inr_desc, CategoryTheory.leftDistrib_hom
-- Module: Mathlib.CategoryTheory.Distributive.Monoidal
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
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))
⊢ 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))

Tactic:
apply (cancel_iso_hom_right _ _ (∂L X Y Z)).mp

Premises used: CategoryTheory.leftDistrib, CategoryTheory.Iso.cancel_iso_hom_right, Iff.mp