awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⟧
h₅ : ∀ (X : F C), motive ⟦Hom.ρ_hom X⟧
⊢ motive ⟦f⟧
have h₆ : ∀ (X : F C), motive ⟦Hom.ρ_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⟧
h₅ : ∀ (X : F C), motive ⟦Hom.ρ_hom X⟧
h₆ : ∀ (X : F C), motive ⟦Hom.ρ_inv X⟧
⊢ motive ⟦f⟧
have h₇ : ∀ {X Y Z : F C} (f : X ⟶ᵐ Y) (g : Y ⟶ᵐ Z) (hf : motive ⟦f⟧) (hg : motive ⟦g⟧), motive ⟦f.comp g⟧
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⟧
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⟧
⊢ motive ⟦f⟧
have h₈ : ∀ (X : F C) {Y₁ Y₂ : F C} (f : Y₁ ⟶ᵐ Y₂) (hf : motive ⟦f⟧), motive ⟦Hom.whiskerLeft X 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)
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⟧
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⟧
⊢ motive ⟦f⟧
have h₉ : ∀ {X₁ X₂ : F C} (f : X₁ ⟶ᵐ X₂) (X : F C) (hf : motive ⟦f⟧), motive ⟦f.whiskerRight 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⟧
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⟧
⊢ motive ⟦f⟧
have h₁₀ : ∀ {W X Y Z : F C} (f : W ⟶ᵐ Y) (g : X ⟶ᵐ Z) (hf : motive ⟦f⟧) (hg : motive ⟦g⟧), motive ⟦f.tensor g⟧
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
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 Z : F C
f_2 f' : X_1 ⟶ᵐ Y_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hf :
  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')
hg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 (f_2.comp g_1))
    (projectMapAux f_1 (f'.comp g'))
have comp : Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
  (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1) (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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 Z : F C
f_2 f' : X_1 ⟶ᵐ Y_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hf :
  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')
hg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
    (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1) (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
have comp : Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
  (projectMapAux f_1 f' ≫ projectMapAux f_1 g_1) (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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 Z : F C
f_2 f' : X_1 ⟶ᵐ Y_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hf :
  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')
hg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
comp :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
    (projectMapAux f_1 f' ≫ projectMapAux f_1 g_1) (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
    (projectMapAux f_1 f_2 ≫ projectMapAux f_1 g_1) (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
have comp₁ : Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 X_1 ⟶ projectObj.{v', u, u'} f_1 Z)
  (projectMapAux f_1 f' ≫ projectMapAux f_1 g') (projectMapAux f_1 f' ≫ projectMapAux f_1 g')
Tactic: rw [hf, hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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 Z : F C
f_2 f' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (X_1.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 (Hom.whiskerLeft X_1 f_2)) (projectMapAux f_1 (Hom.whiskerLeft X_1 f'))
have whiskerLeft : Eq.{v' + 1} (α :=
  tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) ⟶
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Z))
  (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f_2) (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f')
Tactic: dsimp only [projectMapAux, projectObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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 Z : F C
f_2 f' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
⊢ Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Z))
    (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f_2) (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f')
have whiskerLeft : Eq.{v' + 1} (α :=
  tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Y_1) ⟶
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 X_1) (projectObj.{v', u, u'} f_1 Z))
  (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f') (projectObj.{v', u, u'} f_1 X_1 ◁ projectMapAux f_1 f')
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
Y_1 Z : F C
f_2 f' : Y_1 ⟶ᵐ Z
X_1 : F C
h : HomEquiv f_2 f'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (Y_1.tensor X_1) ⟶ projectObj.{v', u, u'} f_1 (Z.tensor X_1))
    (projectMapAux f_1 (f_2.whiskerRight X_1)) (projectMapAux f_1 (f'.whiskerRight X_1))
have whiskerRight : Eq.{v' + 1} (α :=
  tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 X_1) ⟶
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Z) (projectObj.{v', u, u'} f_1 X_1))
  (projectMapAux f_1 f_2 ▷ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f' ▷ projectObj.{v', u, u'} f_1 X_1)
Tactic: dsimp only [projectMapAux, projectObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
Y_1 Z : F C
f_2 f' : Y_1 ⟶ᵐ Z
X_1 : F C
h : HomEquiv f_2 f'
hf :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
⊢ Eq.{v' + 1} (α :=
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 X_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Z) (projectObj.{v', u, u'} f_1 X_1))
    (projectMapAux f_1 f_2 ▷ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f' ▷ projectObj.{v', u, u'} f_1 X_1)
have whiskerRight : Eq.{v' + 1} (α :=
  tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Y_1) (projectObj.{v', u, u'} f_1 X_1) ⟶
    tensorObj.{v', u'} (𝒞 := inst) (projectObj.{v', u, u'} f_1 Z) (projectObj.{v', u, u'} f_1 X_1))
  (projectMapAux f_1 f' ▷ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f' ▷ projectObj.{v', u, u'} f_1 X_1)
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
W X_1 Y_1 Z : F C
f_2 f' : W ⟶ᵐ X_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hfg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 W ⟶ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
hfg' :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 (f_2.tensor g_1)) (projectMapAux f_1 (f'.tensor g'))
have tensor : Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
  (projectMapAux f_1 f_2 ⊗ₘ projectMapAux f_1 g_1) (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
Tactic: dsimp only [projectMapAux]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
W X_1 Y_1 Z : F C
f_2 f' : W ⟶ᵐ X_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hfg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 W ⟶ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
hfg' :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 f_2 ⊗ₘ projectMapAux f_1 g_1) (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
have tensor : Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
  (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g_1) (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
Tactic: rw [hfg, hfg']
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Free.Basic (goal)
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
W X_1 Y_1 Z : F C
f_2 f' : W ⟶ᵐ X_1
g_1 g' : Y_1 ⟶ᵐ Z
h : HomEquiv f_2 f'
h_1 : HomEquiv g_1 g'
hfg :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 W ⟶ projectObj.{v', u, u'} f_1 X_1) (projectMapAux f_1 f_2)
    (projectMapAux f_1 f')
hfg' :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 Y_1 ⟶ projectObj.{v', u, u'} f_1 Z) (projectMapAux f_1 g_1)
    (projectMapAux f_1 g')
tensor :
  Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g_1) (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
⊢ Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
    (projectMapAux f_1 f_2 ⊗ₘ projectMapAux f_1 g_1) (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
have tensor₁ : Eq.{v' + 1} (α := projectObj.{v', u, u'} f_1 (W.tensor Y_1) ⟶ projectObj.{v', u, u'} f_1 (X_1.tensor Z))
  (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g') (projectMapAux f_1 f' ⊗ₘ projectMapAux f_1 g')
Tactic: rw [hfg, hfg']