awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))
    (Iso.hom (λ_ (F.obj x)) ≫ Iso.inv (λ_ (F.obj x)))
    (Iso.hom (λ_ (F.obj x)) ≫
      F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    Iso.hom (λ_ (F.obj x)) ≫
      F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₂ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    (h.εIso.hom ▷ F.obj x ≫ Iso.hom (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ F.map (Iso.hom (λ_ x))) ≫
      F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₃ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    h.εIso.hom ▷ F.obj x ≫
      (Iso.hom (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ F.map (Iso.hom (λ_ x))) ≫
        F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₄ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    h.εIso.hom ▷ F.obj x ≫
      Iso.hom (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫
        F.map (Iso.hom (λ_ x)) ≫
          F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₅ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    h.εIso.hom ▷ F.obj x ≫
      Iso.hom (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫
        Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
⊢ Iso.inv (λ_ (F.obj x)) =
    F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
have rw₆ : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
  h.εIso.hom ▷ F.obj x ≫ h.εIso.inv ▷ F.obj x
Tactic: rw [← cancel_epi (λ_ _).hom, Iso.hom_inv_id, h.left_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, hom_inv_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))
    (Iso.hom (λ_ (F.obj x)) ≫ Iso.inv (λ_ (F.obj x)))
    (Iso.hom (λ_ (F.obj x)) ≫
      F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    Iso.hom (λ_ (F.obj x)) ≫
      F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₂ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    (h.εIso.hom ▷ F.obj x ≫ Iso.hom (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ F.map (Iso.hom (λ_ x))) ≫
      F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₃ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    h.εIso.hom ▷ F.obj x ≫
      (Iso.hom (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ F.map (Iso.hom (λ_ x))) ≫
        F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₄ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    h.εIso.hom ▷ F.obj x ≫
      Iso.hom (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫
        F.map (Iso.hom (λ_ x)) ≫
          F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₅ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    h.εIso.hom ▷ F.obj x ≫
      Iso.hom (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫
        Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
rw₆ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) =
    h.εIso.hom ▷ F.obj x ≫ h.εIso.inv ▷ F.obj x
⊢ Iso.inv (λ_ (F.obj x)) =
    F.map (Iso.inv (λ_ x)) ≫ Iso.inv (h.μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) ≫ h.εIso.inv ▷ F.obj x
have rw₇ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)))
Tactic: rw [← cancel_epi (λ_ _).hom, Iso.hom_inv_id, h.left_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, hom_inv_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
⊢ Iso.inv (ρ_ (F.obj x)) =
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
have rw : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (Iso.hom (ρ_ (F.obj x)) ≫ Iso.inv (ρ_ (F.obj x)))
  (Iso.hom (ρ_ (F.obj x)) ≫
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv)
Tactic: rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (Iso.hom (ρ_ (F.obj x)) ≫ Iso.inv (ρ_ (F.obj x)))
    (Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv)
⊢ Iso.inv (ρ_ (F.obj x)) =
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
have rw₁ : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
  Iso.hom (ρ_ (F.obj x)) ≫
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
Tactic: rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (Iso.hom (ρ_ (F.obj x)) ≫ Iso.inv (ρ_ (F.obj x)))
    (Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
⊢ Iso.inv (ρ_ (F.obj x)) =
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
have rw₂ : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
  (F.obj x ◁ h.εIso.hom ≫ Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
Tactic: rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (Iso.hom (ρ_ (F.obj x)) ≫ Iso.inv (ρ_ (F.obj x)))
    (Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₂ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    (F.obj x ◁ h.εIso.hom ≫ Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
⊢ Iso.inv (ρ_ (F.obj x)) =
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
have rw₃ : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
  F.obj x ◁ h.εIso.hom ≫
    (Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
Tactic: rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (Iso.hom (ρ_ (F.obj x)) ≫ Iso.inv (ρ_ (F.obj x)))
    (Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₂ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    (F.obj x ◁ h.εIso.hom ≫ Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₃ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      (Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
        F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
⊢ Iso.inv (ρ_ (F.obj x)) =
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
have rw₄ : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
  F.obj x ◁ h.εIso.hom ≫
    Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      F.map (Iso.hom (ρ_ x)) ≫
        F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
Tactic: rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (Iso.hom (ρ_ (F.obj x)) ≫ Iso.inv (ρ_ (F.obj x)))
    (Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₂ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    (F.obj x ◁ h.εIso.hom ≫ Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₃ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      (Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
        F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₄ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        F.map (Iso.hom (ρ_ x)) ≫
          F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
⊢ Iso.inv (ρ_ (F.obj x)) =
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
have rw₅ : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
  F.obj x ◁ h.εIso.hom ≫
    Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
Tactic: rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (Iso.hom (ρ_ (F.obj x)) ≫ Iso.inv (ρ_ (F.obj x)))
    (Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₂ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    (F.obj x ◁ h.εIso.hom ≫ Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₃ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      (Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
        F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₄ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        F.map (Iso.hom (ρ_ x)) ≫
          F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₅ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
⊢ Iso.inv (ρ_ (F.obj x)) =
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
have rw₆ : 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
  F.obj x ◁ h.εIso.hom ≫ F.obj x ◁ h.εIso.inv
Tactic: rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
x : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (Iso.hom (ρ_ (F.obj x)) ≫ Iso.inv (ρ_ (F.obj x)))
    (Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    Iso.hom (ρ_ (F.obj x)) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₂ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    (F.obj x ◁ h.εIso.hom ≫ Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
      F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₃ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      (Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ x))) ≫
        F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₄ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        F.map (Iso.hom (ρ_ x)) ≫
          F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₅ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫
      Iso.hom (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
rw₆ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    F.obj x ◁ h.εIso.hom ≫ F.obj x ◁ h.εIso.inv
⊢ Iso.inv (ρ_ (F.obj x)) =
    F.map (Iso.inv (ρ_ x)) ≫ Iso.inv (h.μIso x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj x ◁ h.εIso.inv
have rw₇ : Eq.{v₂ + 1} (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
  (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
Tactic: rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
⊢ Eq (α :=
    Quiver.Hom (V := D × C') ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C'))
      ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')))
    (CategoryStruct.comp (Y := (F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
      (ε (F.prod G)) (η (F.prod G)))
    (𝟙 ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')))
have h₁ : Eq (α :=
  Quiver.Hom.{v₂, u₂} (V := D) (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').1
    (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').1)
  (CategoryStruct.comp (Y := (F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
      (ε (F.prod G)) (η (F.prod G))).1
  (𝟙 ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C'))).1
Tactic: ext