awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
X : F C
⊢ motive ⟦Hom.ρ_inv X⟧

Tactic:
ρ_inv X
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
X : F C
⊢ motive ⟦Hom.ρ_inv X⟧

Tactic:
exact ρ_inv X
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
X_1 Y_1 Z : F C
f : X_1 ⟶ᵐ Y_1
g : Y_1 ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
⊢ motive ⟦f.comp g⟧

Tactic:
comp _ _ hf hg

Premises used: Quotient.map₂
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
X_1 Y_1 Z : F C
f : X_1 ⟶ᵐ Y_1
g : Y_1 ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
⊢ motive ⟦f.comp g⟧

Tactic:
exact comp _ _ hf hg
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
X Y₁ Y₂ : F C
f : Y₁ ⟶ᵐ Y₂
hf : motive ⟦f⟧
⊢ motive ⟦Hom.whiskerLeft X f⟧

Tactic:
whiskerLeft X _ hf

Premises used: Quot.map
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
X Y₁ Y₂ : F C
f : Y₁ ⟶ᵐ Y₂
hf : motive ⟦f⟧
⊢ motive ⟦Hom.whiskerLeft X f⟧

Tactic:
exact whiskerLeft X _ hf
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
X₁ X₂ : F C
f : X₁ ⟶ᵐ X₂
X : F C
hf : motive ⟦f⟧
⊢ motive ⟦f.whiskerRight X⟧

Tactic:
whiskerRight _ X hf

Premises used: Quot.map
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
X₁ X₂ : F C
f : X₁ ⟶ᵐ X₂
X : F C
hf : motive ⟦f⟧
⊢ motive ⟦f.whiskerRight X⟧

Tactic:
exact whiskerRight _ X hf
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y_1 : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
h :
  ∀
    (this :
      Eq (α := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X ⟶ tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)
        (homMk f ⊗ₘ homMk g) (homMk f ▷ X ≫ Y ◁ homMk g)),
    motive ⟦f.tensor g⟧
⊢ motive ⟦f.tensor g⟧

Tactic:
have : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g :=
        Quotient.sound (HomEquiv.tensorHom_def f g)
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y_1 : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
this :
  Eq (α := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X ⟶ tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)
    (homMk f ⊗ₘ homMk g) (homMk f ▷ X ≫ Y ◁ homMk g)
h : motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X) (homMk f ▷ X ≫ Y ◁ homMk g)
⊢ motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X) (homMk f ⊗ₘ homMk g)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y_1 : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
this :
  Eq (α := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X ⟶ tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)
    (homMk f ⊗ₘ homMk g) (homMk f ▷ X ≫ Y ◁ homMk g)
⊢ motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X) (homMk f ▷ X ≫ Y ◁ homMk g)

Tactic:
comp _ _ (whiskerRight _ _ hf) (whiskerLeft _ _ hg)
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X_1 Y_1 : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
W X Y Z : F C
f : W ⟶ᵐ Y
g : X ⟶ᵐ Z
hf : motive ⟦f⟧
hg : motive ⟦g⟧
this :
  Eq (α := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X ⟶ tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z)
    (homMk f ⊗ₘ homMk g) (homMk f ▷ X ≫ Y ◁ homMk g)
⊢ motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X) (homMk f ▷ X ≫ Y ◁ homMk g)

Tactic:
exact comp _ _ (whiskerRight _ _ hf) (whiskerLeft _ _ hg)
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) (tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) Z)
      (Iso.hom (α_ X Y Z))
α_inv :
  ∀ (X Y Z : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y Z))
      (Iso.inv (α_ X Y Z))
l_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.hom (λ_ X))
l_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)) X)
      (Iso.inv (λ_ X))
ρ_hom :
  ∀ (X : F C),
    motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.hom (ρ_ X))
ρ_inv :
  ∀ (X : F C),
    motive (Y := tensorObj (𝒞 := categoryFreeMonoidalCategory) X ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory)))
      (Iso.inv (ρ_ X))
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft :
  ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y) (X ◁ f)
whiskerRight :
  ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C),
    motive f → motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) X Z) (f ▷ Z)
f : X ⟶ᵐ Y
h : ∀ (X : F C), motive ⟦Hom.id X⟧
h₁ : ∀ (X Y Z : F C), motive ⟦Hom.α_hom X Y Z⟧
h₂ : ∀ (X Y Z : F C), motive ⟦Hom.α_inv X Y Z⟧
h₃ : ∀ (X : F C), motive ⟦Hom.l_hom X⟧
h₄ : ∀ (X : F C), motive ⟦Hom.l_inv X⟧
h₅ : ∀ (X : F C), motive ⟦Hom.ρ_hom X⟧
h₆ : ∀ (X : F C), motive ⟦Hom.ρ_inv X⟧
h₇ : ∀ {X Y Z : F C} (f : X ⟶ᵐ Y) (g : Y ⟶ᵐ Z) (hf : motive ⟦f⟧) (hg : motive ⟦g⟧), motive ⟦f.comp g⟧
h₈ : ∀ (X : F C) {Y₁ Y₂ : F C} (f : Y₁ ⟶ᵐ Y₂) (hf : motive ⟦f⟧), motive ⟦Hom.whiskerLeft X f⟧
h₉ : ∀ {X₁ X₂ : F C} (f : X₁ ⟶ᵐ X₂) (X : F C) (hf : motive ⟦f⟧), motive ⟦f.whiskerRight X⟧
h₁₀ : ∀ {W X Y Z : F C} (f : W ⟶ᵐ Y) (g : X ⟶ᵐ Z) (hf : motive ⟦f⟧) (hg : motive ⟦g⟧), motive ⟦f.tensor g⟧
⊢ motive ⟦f⟧

Tactic:
induction f with
  | id X => exact id X
  | α_hom X Y Z => exact α_hom X Y Z
  | α_inv X Y Z => exact α_inv X Y Z
  | l_hom X => exact l_hom X
  | l_inv X => exact l_inv X
  | ρ_hom X => exact ρ_hom X
  | ρ_inv X => exact ρ_inv X
  | comp f g hf hg => exact comp _ _ hf hg
  | whiskerLeft X f hf => exact whiskerLeft X _ hf
  | whiskerRight f X hf => exact whiskerRight _ X hf
  | @tensor W X Y Z f g hf hg =>
      have : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g :=
        Quotient.sound (HomEquiv.tensorHom_def f g)
      change motive (homMk f ⊗ₘ homMk g)
      rw [this]
      exact comp _ _ (whiskerRight _ _ hf) (whiskerLeft _ _ hg)

Premises used: CategoryTheory.FreeMonoidalCategory.Hom.tensor
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 : F C
f_2 : X_1 ⟶ᵐ Y_1
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f_2)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
D : Type u'
inst : Category.{v', u'} D
inst_1 : MonoidalCategory.{v', u'} D
f_1 : C → D
X Y : F C
f g : X ⟶ᵐ Y
X_1 Y_1 : F C
f_2 g_1 : X_1 ⟶ᵐ Y_1
h : HomEquiv f_2 g_1
hfg' :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 g_1)
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Y_1) (projectMapAux f_1 g_1)
    (projectMapAux f_1 f_2)

Tactic:
hfg'.symm

Premises used: Eq.symm