awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension (goal)
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
D : Type u₂
D' : Type u₃
E : Type u₄
inst_2 : Category.{v₂, u₂} D
inst_3 : Category.{v₃, u₃} D'
inst_4 : Category.{v₄, u₄} E
H : Functor.{v₂, v₁, u₂, u₁} D V
L : Functor.{v₂, v₃, u₂, u₃} D D'
H' : Functor.{v₃, v₁, u₃, u₁} D' V
α : H ⟶ L ⋙ H'
K : Functor.{v₄, v₁, u₄, u₁} E V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst_5 : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (J := CostructuredArrow (Functor.prod (𝟭 E) L) (e, d))
  (CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d ≌
  CostructuredArrow (Functor.prod (𝟭 E) L) (e, d) :=
  Equivalence.symm (CostructuredArrow.prodEquivalence (𝟭 E) L e d)
I : CostructuredArrow L d ⥤ CostructuredArrow.{v₄, v₄, u₄, u₄} (𝟭 E) e × CostructuredArrow L d :=
  Equivalence.inverse (prod.leftUnitorEquivalence (CostructuredArrow L d)) ⋙
    Functor.prod (Functor.fromPUnit (CostructuredArrow.mk (𝟙 (Functor.obj.{v₄, v₄, u₄, u₄} (𝟭 E) e))))
      (𝟭 (CostructuredArrow L d))
this : I.Final := ⋯
diag_iso : (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e) ≅
  I ⋙ equiv.functor ⋙ CostructuredArrow.proj (Functor.prod (𝟭 E) L) (e, d) ⋙ K ⊠ H :=
  NatIso.ofComponents
    (fun (x : CostructuredArrow L d) ↦ Iso.refl (((CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e)).obj x)) ⋯
⊢ Limits.IsColimit (Limits.Cocone.whisker I (Limits.Cocone.whisker equiv.functor cone))
have apply : Limits.IsColimit (F := (CostructuredArrow.proj L d ⋙ H) ⋙ tensorLeft (K.obj e))
  (Functor.mapCocone (tensorLeft (K.obj e)) ((Functor.LeftExtension.mk H' α).coconeAt d))
Tactic: apply Limits.IsColimit.equivOfNatIsoOfIso diag_iso
    (d := Limits.Cocone.whisker I <| Limits.Cocone.whisker equiv.functor cone)
    (c := (tensorLeft <| K.obj e).mapCocone <| (Functor.LeftExtension.mk H' α).coconeAt d)
    (Limits.Cocone.ext <| .refl _) |>.toFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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)
⊢ motive t
have h : ∀ (f : X ⟶ᵐ Y), motive ⟦f⟧
Tactic: induction t using Quotient.inductionOn with | _ f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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⟧
⊢ motive ⟦f.tensor g⟧
have 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⟧
Tactic: have : homMk f ⊗ₘ homMk g = homMk f ▷ X ≫ Y ◁ homMk g :=
        Quotient.sound (HomEquiv.tensorHom_def f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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 ⊗ₘ homMk g)
have h : motive (X := tensorObj (𝒞 := categoryFreeMonoidalCategory) W X) (homMk f ▷ X ≫ Y ◁ homMk g)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
⊢ motive ⟦f⟧
have h : ∀ (X : F C), motive ⟦Hom.id X⟧
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)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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⟧
⊢ motive ⟦f⟧
have h₁ : ∀ (X Y Z : F C), motive ⟦Hom.α_hom X Y Z⟧
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)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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⟧
⊢ motive ⟦f⟧
have h₂ : ∀ (X Y Z : F C), motive ⟦Hom.α_inv X Y Z⟧
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)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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⟧
⊢ motive ⟦f⟧
have h₃ : ∀ (X : F C), motive ⟦Hom.l_hom X⟧
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)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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⟧
⊢ motive ⟦f⟧
have h₄ : ∀ (X : F C), motive ⟦Hom.l_inv X⟧
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)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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⟧
⊢ motive ⟦f⟧
have h₅ : ∀ (X : F C), motive ⟦Hom.ρ_hom X⟧
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)
Cleared hypotheses: f