awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
f_1 : X ⟶ Y
f : X ⟶ᵐ Y
⊢ Eq.{u + 1} (α := X.tensor unit ⟶ Y)
    (CategoryStruct.comp (Y := Y.tensor unit)
      (Quot.map (ra := HomEquiv) (rb :=
        (⇑((X.tensor unit).setoidHom (Y.tensor unit)) :
          (X.tensor unit ⟶ᵐ Y.tensor unit) → (X.tensor unit ⟶ᵐ Y.tensor unit) → Prop))
        (fun (f : X ⟶ᵐ Y) ↦ f.whiskerRight unit) ⋯ (Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f))
      (Iso.hom { hom := ⟦Hom.ρ_hom Y⟧, inv := ⟦Hom.ρ_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }))
    (Iso.hom { hom := ⟦Hom.ρ_hom X⟧, inv := ⟦Hom.ρ_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      Quot.mk (⇑(X.setoidHom Y) : (X ⟶ᵐ Y) → (X ⟶ᵐ Y) → Prop) f)

Tactic:
exact Quotient.sound (ρ_naturality _)

Premises used: Quotient.sound
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y Z : F C
f : X ⟶ᵐ Y
g : Y ⟶ᵐ Z
⊢ ⟦f.comp g⟧ = ⟦f⟧ ≫ ⟦g⟧

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X₁ Y₁ X₂ Y₂ : F C
f : X₁ ⟶ᵐ Y₁
g : X₂ ⟶ᵐ Y₂
⊢ Eq (α :=
    Quotient (α := X₁.tensor X₂ ⟶ᵐ Y₁.tensor Y₂)
      ((tensorObj (𝒞 := categoryFreeMonoidalCategory) X₁ X₂).setoidHom
        (tensorObj (𝒞 := categoryFreeMonoidalCategory) Y₁ Y₂)))
    ⟦f.tensor g⟧ (⟦f⟧ ⊗ₘ ⟦g⟧)

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y₁ Y₂ : F C
f : Y₁ ⟶ᵐ Y₂
⊢ ⟦Hom.whiskerLeft X f⟧ = X ◁ ⟦f⟧

Tactic:
rfl

Premises used: Quot.map, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X₁ X₂ : F C
f : X₁ ⟶ᵐ X₂
Y : F C
⊢ ⟦f.whiskerRight Y⟧ = ⟦f⟧ ▷ Y

Tactic:
rfl

Premises used: Quot.map, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X : F C
⊢ ⟦Hom.id X⟧ = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y Z : F C
⊢ ⟦Hom.α_hom X Y Z⟧ = Iso.hom (α_ X Y Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y Z : F C
⊢ ⟦Hom.α_inv X Y Z⟧ = Iso.inv (α_ X Y Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X : F C
⊢ ⟦Hom.ρ_hom X⟧ = Iso.hom (ρ_ X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X : F C
⊢ ⟦Hom.ρ_inv X⟧ = Iso.inv (ρ_ X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X : F C
⊢ ⟦Hom.l_hom X⟧ = Iso.hom (λ_ X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X : F C
⊢ ⟦Hom.l_inv X⟧ = Iso.inv (λ_ X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
X Y : F C
⊢ X.tensor Y = tensorObj (𝒞 := categoryFreeMonoidalCategory) X Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
⊢ Eq.{u + 1} (α := F C) unit ((𝟙_ (F C)) (𝒞 := categoryFreeMonoidalCategory))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Free.Basic
Goal:
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
t : X ⟶ Y
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)
h : ∀ (f : X ⟶ᵐ Y), motive ⟦f⟧
⊢ motive t

Tactic:
induction t using Quotient.inductionOn with | _ f
-- 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.id X⟧

Tactic:
id 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.id X⟧

Tactic:
exact id X
-- 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)
X Y Z : F C
⊢ motive ⟦Hom.α_hom X Y Z⟧

Tactic:
α_hom X Y Z
-- 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)
X Y Z : F C
⊢ motive ⟦Hom.α_hom X Y Z⟧

Tactic:
exact α_hom X Y Z
-- 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)
X Y Z : F C
⊢ motive ⟦Hom.α_inv X Y Z⟧

Tactic:
α_inv X Y Z
-- 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)
X Y Z : F C
⊢ motive ⟦Hom.α_inv X Y Z⟧

Tactic:
exact α_inv X Y Z
-- 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.l_hom X⟧

Tactic:
l_hom 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.l_hom X⟧

Tactic:
exact l_hom 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.l_inv X⟧

Tactic:
l_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.l_inv X⟧

Tactic:
exact l_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.ρ_hom X⟧

Tactic:
ρ_hom 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.ρ_hom X⟧

Tactic:
exact ρ_hom X