awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Colimits (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst_2 : Category.{v_2, u_2} J
inst_3 : Category.{v_3, u_3} J₁
inst_4 : Category.{v_4, u_4} J₂
F₁ F₂ : Functor.{v_2, v_1, u_2, u_1} J C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst_5 : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst_6 : IsSifted.{v_2, u_2} J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
refine_1 : Functor.diag J ⋙ externalProduct F₁ F₂ ≅ tensorObj (𝒞 := Functor.category) F₁ F₂
⊢ IsColimit (F := tensorObj (𝒞 := Functor.category) F₁ F₂) (c₁.tensor c₂)
have refine_2 : Iso (C := Cocone (tensorObj (𝒞 := Functor.category) F₁ F₂))
  (Functor.obj (C := Cocone (Functor.diag J ⋙ externalProduct F₁ F₂))
    (Cocone.precompose
      (Iso.inv (NatIso.ofComponents (fun (x : J) ↦ Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj x)) sorry)))
    (Cocone.whisker (Functor.diag J) (c₁.tensor₂ c₂)))
  (c₁.tensor c₂)
Tactic: refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    ((Functor.Final.isColimitWhiskerEquiv (Functor.diag J) _).2 (hc₁.tensor₂ hc₂))
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ inl ≫ Q ◁ hP.desc h k w) (Q ◁ h)
have rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ (inl ≫ hP.desc h k w)) (Q ◁ h)
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, IsPushout.inl_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ (inl ≫ hP.desc h k w)) (Q ◁ h)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ inl ≫ Q ◁ hP.desc h k w) (Q ◁ h)
have rw₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q X ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ h) (Q ◁ h)
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, IsPushout.inl_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ inr ≫ Q ◁ hP.desc h k w) (Q ◁ k)
have rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ (inr ≫ hP.desc h k w)) (Q ◁ k)
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, IsPushout.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ (inr ≫ hP.desc h k w)) (Q ◁ k)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ inr ≫ Q ◁ hP.desc h k w) (Q ◁ k)
have rw₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) Q Y ⟶ tensorObj.{v, u} (𝒞 := inst) Q W) (Q ◁ k) (Q ◁ k)
Tactic: rw [← MonoidalCategory.whiskerLeft_comp, IsPushout.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (inl ▷ Q ≫ hP.desc h k w ▷ Q) (h ▷ Q)
have rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) ((inl ≫ hP.desc h k w) ▷ Q) (h ▷ Q)
Tactic: rw [← comp_whiskerRight, IsPushout.inl_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) ((inl ≫ hP.desc h k w) ▷ Q) (h ▷ Q)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (inl ▷ Q ≫ hP.desc h k w ▷ Q) (h ▷ Q)
have rw₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) X Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (h ▷ Q) (h ▷ Q)
Tactic: rw [← comp_whiskerRight, IsPushout.inl_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (inr ▷ Q ≫ hP.desc h k w ▷ Q) (k ▷ Q)
have rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) ((inr ≫ hP.desc h k w) ▷ Q) (k ▷ Q)
Tactic: rw [← comp_whiskerRight, IsPushout.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) ((inr ≫ hP.desc h k w) ▷ Q) (k ▷ Q)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (inr ▷ Q ≫ hP.desc h k w ▷ Q) (k ▷ Q)
have rw₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) Y Q ⟶ tensorObj.{v, u} (𝒞 := inst) W Q) (k ▷ Q) (k ▷ Q)
Tactic: rw [← comp_whiskerRight, IsPushout.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ X
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (f ▷ Z ▷ W ≫ Iso.hom (α_ B Z W) ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
have rw : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
    pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
  (Iso.hom (α_ A Z W) ≫ f ▷ tensorObj.{v, u} (𝒞 := inst) Z W ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
  (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
Tactic: rw [associator_naturality_left_assoc, ← whisker_exchange_assoc, pushout.condition,
    ← MonoidalCategory.whiskerLeft_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ X
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ f ▷ tensorObj.{v, u} (𝒞 := inst) Z W ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (f ▷ Z ▷ W ≫ Iso.hom (α_ B Z W) ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
have rw₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
    pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
  (Iso.hom (α_ A Z W) ≫ A ◁ h ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
  (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
Tactic: rw [associator_naturality_left_assoc, ← whisker_exchange_assoc, pushout.condition,
    ← MonoidalCategory.whiskerLeft_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ X
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ f ▷ tensorObj.{v, u} (𝒞 := inst) Z W ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ h ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (f ▷ Z ▷ W ≫ Iso.hom (α_ B Z W) ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
have rw₂ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
    pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
  (Iso.hom (α_ A Z W) ≫ A ◁ h ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g))
  (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
Tactic: rw [associator_naturality_left_assoc, ← whisker_exchange_assoc, pushout.condition,
    ← MonoidalCategory.whiskerLeft_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ X
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ f ▷ tensorObj.{v, u} (𝒞 := inst) Z W ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ h ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ h ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (f ▷ Z ▷ W ≫ Iso.hom (α_ B Z W) ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
have rw₃ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) A Z) W ⟶
    pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
  (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
  (Iso.hom (α_ A Z W) ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g))
Tactic: rw [associator_naturality_left_assoc, ← whisker_exchange_assoc, pushout.condition,
    ← MonoidalCategory.whiskerLeft_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ A
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Z ◁ W ◁ g ≫ Iso.inv (α_ Z W Y) ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
have rw : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
    pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
  (Iso.inv (α_ Z W X) ≫ tensorObj.{v, u} (𝒞 := inst) Z W ◁ g ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
  (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
Tactic: rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ← pushout.condition,
    ← comp_whiskerRight_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ A
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ tensorObj.{v, u} (𝒞 := inst) Z W ◁ g ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Z ◁ W ◁ g ≫ Iso.inv (α_ Z W Y) ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
have rw₁ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
    pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
  (Iso.inv (α_ Z W X) ≫ h ▷ X ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g))
  (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
Tactic: rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ← pushout.condition,
    ← comp_whiskerRight_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ A
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ tensorObj.{v, u} (𝒞 := inst) Z W ◁ g ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ h ▷ X ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Z ◁ W ◁ g ≫ Iso.inv (α_ Z W Y) ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
have rw₂ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
    pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
  (Iso.inv (α_ Z W X) ≫ h ▷ X ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
  (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
Tactic: rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ← pushout.condition,
    ← comp_whiskerRight_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : HasPushouts.{v, u} C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : tensorObj.{v, u} (𝒞 := inst) Z W ⟶ A
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ tensorObj.{v, u} (𝒞 := inst) Z W ◁ g ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
rw₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ h ▷ X ≫ A ◁ g ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ h ▷ X ≫ f ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
      pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
    (Z ◁ W ◁ g ≫ Iso.inv (α_ Z W Y) ≫ h ▷ Y ≫ pushout.inr (f ▷ X) (A ◁ g))
    (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
have rw₃ : Eq (α :=
  tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) W X) ⟶
    pushout (X := tensorObj.{v, u} (𝒞 := inst) A X) (f ▷ X) (A ◁ g))
  (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
  (Iso.inv (α_ Z W X) ≫ (h ≫ f) ▷ X ≫ pushout.inl (f ▷ X) (A ◁ g))
Tactic: rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ← pushout.condition,
    ← comp_whiskerRight_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Linear (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ X ◁ (r • f) =
    HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f)
have a : F.map (X ◁ (r • f)) =
  F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f))
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Linear (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ F.map (X ◁ (r • f)) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f))
have a : CategoryStruct.comp (Y := tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Y)) (Functor.OplaxMonoidal.δ F X Y)
    (F.obj X ◁ F.map (r • f) ≫ Functor.LaxMonoidal.μ F X Z) =
  F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Y ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z) r (X ◁ f))
Tactic: rw [Functor.Monoidal.map_whiskerLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Linear (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ (r • f) ▷ Z =
    HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z)
have a : F.map ((r • f) ▷ Z) =
  F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z))
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Linear (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : MonoidalCategory.{v_1, u_2} C
inst_5 : MonoidalPreadditive.{v_1, u_2} C
inst_6 : MonoidalLinear.{u_1, v_1, u_2} R C
D : Type u_3
inst_7 : Category.{v_2, u_3} D
inst_8 : Preadditive.{v_2, u_3} D
inst_9 : Linear.{u_1, v_2, u_3} R D
inst_10 : MonoidalCategory.{v_2, u_3} D
inst_11 : MonoidalPreadditive.{v_2, u_3} D
F : Functor.{v_2, v_1, u_3, u_2} D C
inst_12 : F.Monoidal
inst_13 : F.Faithful
inst_14 : Functor.Linear R F
r : R
X Y : D
f : X ⟶ Y
Z : D
⊢ F.map ((r • f) ▷ Z) =
    F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z))
have a : CategoryStruct.comp (Y := tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z)) (Functor.OplaxMonoidal.δ F X Z)
    (F.map (r • f) ▷ F.obj Z ≫ Functor.LaxMonoidal.μ F Y Z) =
  F.map (HSMul.hSMul (β := tensorObj.{v_2, u_3} (𝒞 := inst_7) X Z ⟶ tensorObj.{v_2, u_3} (𝒞 := inst_7) Y Z) r (f ▷ Z))
Tactic: rw [Functor.Monoidal.map_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
X : C
h₁ h₂ : ModObj M X
H :
  Eq.{v₁ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
    (@smul _ _ _ _ _ _ _ inst_2 _ _) (@smul _ _ _ _ _ _ _ inst_2 _ _)
⊢ h₁ = h₂
have mk : ∀ (smul : @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
  (one_smul : η ⊵ₗ X ≫ smul = Iso.hom (λₗ X)) (mul_smul : μ ⊵ₗ X ≫ smul = Iso.hom (αₗ M M X) ≫ M ⊴ₗ smul ≫ smul)
  (H :
    Eq.{v₁ + 1} (α :=
      @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
      (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _) (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)),
  { smul := smul, one_smul := one_smul, mul_smul := mul_smul : ModObj M X } = h₂
Tactic: cases h₁
Cleared hypotheses: h₁, H