awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
simp : η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom
simp₁ : (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ.hom
⊢ η.hom = θ.hom

Tactic:
calc
    η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_η)]
    _ = θ.hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_θ)]

Premises used: CategoryTheory.Bicategory.leftUnitor, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g f' : a ⟶ b
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
Hη : η'.hom = η
Hθ : θ'.hom = θ
Hη' : 𝟙 a ◁ η' ≪≫ η_g = η_f
Hθ' : 𝟙 a ◁ θ' ≪≫ η_g = η_f
⊢ η'.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hη')]

Premises used: congrArg, CategoryTheory.Iso.hom
-- Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g f' : a ⟶ b
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
Hη : η'.hom = η
Hθ : θ'.hom = θ
Hη' : 𝟙 a ◁ η' ≪≫ η_g = η_f
Hθ' : 𝟙 a ◁ θ' ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ'.hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hθ')]

Premises used: congrArg, CategoryTheory.Iso.hom
-- Module: Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f g h i : a ⟶ b
inst_1 : LiftHom f
inst_2 : LiftHom g
inst_3 : LiftHom h
η : f ⟶ g
θ : g ⟶ h
ι : h ⟶ i
inst_4 : LiftHom₂ η
inst_5 : LiftHom₂ θ
⊢ η ≫ θ ≫ ι = (η ≫ θ) ≫ ι

Tactic:
(Category.assoc _ _ _).symm

Premises used: CategoryTheory.Category.assoc, Eq.symm
-- Module: Mathlib.Tactic.CategoryTheory.Coherence.Basic
Goal:
α : Type u_1
a b a' b' : α
ha : a = a'
hb : b = b'
h : a' = b'
⊢ a = b

Tactic:
simp [h, ha, hb]
-- Module: Mathlib.Tactic.CategoryTheory.Coherence.Basic
Goal:
C : Type u
inst : CategoryStruct.{v, u} C
f₁ f₂ f₃ f₄ : C
α α' : f₁ ⟶ f₂
η η' : f₂ ⟶ f₃
ηs ηs' : f₃ ⟶ f₄
e_α : α = α'
e_η : η = η'
e_ηs : ηs = ηs'
⊢ α ≫ η ≫ ηs = α' ≫ η' ≫ ηs'

Tactic:
simp [e_α, e_η, e_ηs]
-- Module: Mathlib.Tactic.CategoryTheory.Coherence
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
inst_1 : LiftObj W
inst_2 : LiftObj X
inst_3 : LiftObj Y
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
inst_4 : LiftHom f
inst_5 : LiftHom g
⊢ f ≫ g ≫ h = (f ≫ g) ≫ h

Tactic:
(Category.assoc _ _ _).symm

Premises used: CategoryTheory.Category.assoc, Eq.symm
-- Module: Mathlib.Tactic.CategoryTheory.Coherence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f ≫ 𝟙 Y = g
⊢ f = g

Tactic:
simpa using w
-- Module: Mathlib.Tactic.CategoryTheory.Coherence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g ≫ 𝟙 Y
⊢ f = g

Tactic:
simpa using w
-- Module: Mathlib.Tactic.CategoryTheory.Elementwise
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
x_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_1 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
X Y : C
f g : X ⟶ Y
h : f = g
x : CC X
rw rw₁ :
  Eq (α := CC Y) ((ConcreteCategory.hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)
⊢ Eq (α := CC Y) ((ConcreteCategory.hom (FC := FC) (CC := CC) f : (a : CC X) → CC Y) x : CC Y)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) g : (a : CC X) → CC Y) x : CC Y)

Tactic:
rw [h]
-- Module: Mathlib.Tactic.CategoryTheory.IsoReassoc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ≅ Y
w : f = g
Z : C
h : Y ≅ Z
rw rw₁ : g ≪≫ h = g ≪≫ h
⊢ f ≪≫ h = g ≪≫ h

Tactic:
rw [w]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Goal:
C : Type u
inst : Category.{v, u} C
f g h : C
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : g ⟶ h
θ' : g ≅ h
ih_θ : θ'.hom = θ
⊢ (η' ≪≫ θ').hom = η ≫ θ

Tactic:
simp [ih_η, ih_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Goal:
C : Type u
inst : Category.{v, u} C
f g h i : C
inst_1 : MonoidalCoherence g h
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : h ⟶ i
θ' : h ≅ i
ih_θ : θ'.hom = θ
⊢ (η' ≪⊗≫ θ').hom = η ⊗≫ θ

Tactic:
simp [ih_η, ih_θ, monoidalIsoComp, monoidalComp]

Premises used: CategoryTheory.monoidalComp, CategoryTheory.monoidalIsoComp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h : C
η : g ⟶ h
η' : g ≅ h
ih_η : η'.hom = η
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) f g ⟶ tensorObj.{v, u} (𝒞 := inst) f h) (Iso.hom (f ◁ᵢ η')) (f ◁ η)

Tactic:
simp [ih_η]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h : C
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) f h ⟶ tensorObj.{v, u} (𝒞 := inst) g h) (Iso.hom (η' ▷ᵢ h)) (η ▷ h)

Tactic:
simp [ih_η]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f₁ g₁ f₂ g₂ : C
η : f₁ ⟶ g₁
η' : f₁ ≅ g₁
ih_η : η'.hom = η
θ : f₂ ⟶ g₂
θ' : f₂ ≅ g₂
ih_θ : θ'.hom = θ
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) f₁ f₂ ⟶ tensorObj.{v, u} (𝒞 := inst) g₁ g₂) (Iso.hom (η' ⊗ᵢ θ')) (η ⊗ₘ θ)

Tactic:
simp [ih_η, ih_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
f g h : C
α : f ≅ g
β : g ≅ h
⊢ (α ≪≫ β).hom = (α ≪≫ β).hom

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
f g h i j : C
α : f ≅ g
β : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
⊢ α.hom ≫ β.hom ≫ η ≫ ηs = (α ≪≫ β).hom ≫ η ≫ ηs

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
simp [e_ι]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
f g h : C
η η' : f ⟶ g
θ θ' : g ⟶ h
ι : f ⟶ h
e_η : η = η'
e_θ : θ = θ'
e_ηθ : η' ≫ θ' = ι
⊢ η ≫ θ = ι

Tactic:
simp [e_η, e_θ, e_ηθ]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
f g : C
η : f ⟶ g
⊢ η = Iso.hom (Iso.refl f) ≫ η ≫ Iso.hom (Iso.refl g)

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
f g h i : C
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
simp [e_η, e_θ, e_αθ, e_ηαθ]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h : C
α : g ≅ h
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) f g ⟶ tensorObj.{v, u} (𝒞 := inst) f h) (Iso.hom (f ◁ᵢ α)) (Iso.hom (f ◁ᵢ α))

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i j : C
α : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
θ : tensorObj.{v, u} (𝒞 := inst) f i ⟶ tensorObj.{v, u} (𝒞 := inst) f j
e_θ : f ◁ ηs = θ
⊢ f ◁ (α.hom ≫ η ≫ ηs) = Iso.hom (f ◁ᵢ α) ≫ f ◁ η ≫ θ

Tactic:
simp [e_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i : C
η : h ⟶ i
η₁ : tensorObj.{v, u} (𝒞 := inst) g h ⟶ tensorObj.{v, u} (𝒞 := inst) g i
η₂ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g h) ⟶
    tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g i)
η₃ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g h) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) i
η₄ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) h ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ Iso.inv (α_ f g i) = η₃
e_η₄ : Iso.hom (α_ f g h) ≫ η₃ = η₄
⊢ tensorObj.{v, u} (𝒞 := inst) f g ◁ η = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g : C
η : f ⟶ g
η₁ : f ⟶ tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g
η₂ :
  tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g
e_η₁ : η ≫ Iso.inv (λ_ g) = η₁
e_η₂ : Iso.hom (λ_ f) ≫ η₁ = η₂
⊢ tensorUnit.{v, u} C (𝒞 := inst) ◁ η = η₂

Tactic:
simp [e_η₁, e_η₂]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h : C
η η' : g ⟶ h
θ : tensorObj.{v, u} (𝒞 := inst) f g ⟶ tensorObj.{v, u} (𝒞 := inst) f h
e_η : η = η'
e_θ : f ◁ η' = θ
⊢ f ◁ η = θ

Tactic:
simp [e_η, e_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h : C
η η' : f ⟶ g
θ : tensorObj.{v, u} (𝒞 := inst) f h ⟶ tensorObj.{v, u} (𝒞 := inst) g h
e_η : η = η'
e_θ : η' ▷ h = θ
⊢ η ▷ h = θ

Tactic:
simp [e_η, e_θ]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i : C
η η' : f ⟶ g
θ θ' : h ⟶ i
ι : tensorObj.{v, u} (𝒞 := inst) f h ⟶ tensorObj.{v, u} (𝒞 := inst) g i
e_η : η = η'
e_θ : θ = θ'
e_ι : η' ⊗ₘ θ' = ι
⊢ η ⊗ₘ θ = ι

Tactic:
simp [e_η, e_θ, e_ι]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g : C
α : f ≅ g
h : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) f h ⟶ tensorObj.{v, u} (𝒞 := inst) g h) (Iso.hom (α ▷ᵢ h)) (Iso.hom (α ▷ᵢ h))

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : tensorObj.{v, u} (𝒞 := inst) h j ⟶ tensorObj.{v, u} (𝒞 := inst) i j
η₁ : tensorObj.{v, u} (𝒞 := inst) g j ⟶ tensorObj.{v, u} (𝒞 := inst) h j
η₂ : tensorObj.{v, u} (𝒞 := inst) g j ⟶ tensorObj.{v, u} (𝒞 := inst) i j
η₃ : tensorObj.{v, u} (𝒞 := inst) f j ⟶ tensorObj.{v, u} (𝒞 := inst) i j
e_ηs₁ : ηs ▷ j = ηs₁
e_η₁ : η ▷ j = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : Iso.hom (α ▷ᵢ j) ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ j = η₃

Tactic:
simp_all
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i j k : C
α : g ≅ tensorObj.{v, u} (𝒞 := inst) f h
η : h ⟶ i
ηs : tensorObj.{v, u} (𝒞 := inst) f i ⟶ j
η₁ : tensorObj.{v, u} (𝒞 := inst) h k ⟶ tensorObj.{v, u} (𝒞 := inst) i k
η₂ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h k) ⟶
    tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) i k)
ηs₁ : tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f i) k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
ηs₂ : tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) i k) ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₃ : tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h k) ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₄ : tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₅ : tensorObj.{v, u} (𝒞 := inst) g k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
e_η₁ : (Iso.hom (Iso.refl h) ≫ η ≫ Iso.hom (Iso.refl i)) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : Iso.inv (α_ f i k) ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : Iso.hom (α_ f h k) ≫ η₃ = η₄
e_η₅ : Iso.hom (α ▷ᵢ k) ≫ η₄ = η₅
⊢ η ▷ k = η₁

Tactic:
simp at e_η₁ e_η₅
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i j k : C
α : g ≅ tensorObj.{v, u} (𝒞 := inst) f h
η : h ⟶ i
ηs : tensorObj.{v, u} (𝒞 := inst) f i ⟶ j
η₁ : tensorObj.{v, u} (𝒞 := inst) h k ⟶ tensorObj.{v, u} (𝒞 := inst) i k
η₂ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h k) ⟶
    tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) i k)
ηs₁ : tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f i) k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
ηs₂ : tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) i k) ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₃ : tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h k) ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₄ : tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
η₅ : tensorObj.{v, u} (𝒞 := inst) g k ⟶ tensorObj.{v, u} (𝒞 := inst) j k
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : Iso.inv (α_ f i k) ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : Iso.hom (α_ f h k) ≫ η₃ = η₄
e_η₅ : α.hom ▷ k ≫ η₄ = η₅
e_η₁ : η ▷ k = η₁
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp [e_η₁, e_η₂, e_ηs₁, e_ηs₂, e_η₃, e_η₄, e_η₅]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g h : C
η : f ⟶ f'
η₁ : tensorObj.{v, u} (𝒞 := inst) f g ⟶ tensorObj.{v, u} (𝒞 := inst) f' g
η₂ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) h ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f' g) h
η₃ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) h ⟶
    tensorObj.{v, u} (𝒞 := inst) f' (tensorObj.{v, u} (𝒞 := inst) g h)
η₄ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g h) ⟶
    tensorObj.{v, u} (𝒞 := inst) f' (tensorObj.{v, u} (𝒞 := inst) g h)
e_η₁ : η ▷ g = η₁
e_η₂ : η₁ ▷ h = η₂
e_η₃ : η₂ ≫ Iso.hom (α_ f' g h) = η₃
e_η₄ : Iso.inv (α_ f g h) ≫ η₃ = η₄
⊢ η ▷ tensorObj.{v, u} (𝒞 := inst) g h = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g : C
η : f ⟶ g
η₁ : f ⟶ tensorObj.{v, u} (𝒞 := inst) g (tensorUnit.{v, u} C (𝒞 := inst))
η₂ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
    tensorObj.{v, u} (𝒞 := inst) g (tensorUnit.{v, u} C (𝒞 := inst))
e_η₁ : η ≫ Iso.inv (ρ_ g) = η₁
e_η₂ : Iso.hom (ρ_ f) ≫ η₁ = η₂
⊢ η ▷ tensorUnit.{v, u} C (𝒞 := inst) = η₂

Tactic:
simp [e_η₁, e_η₂]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g : C
η : f ⟶ g
h : C
⊢ η ▷ h =
    Iso.hom (Iso.refl (tensorObj.{v, u} (𝒞 := inst) f h)) ≫
      η ▷ h ≫ Iso.hom (Iso.refl (tensorObj.{v, u} (𝒞 := inst) g h))

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i j : C
η : g ⟶ h
ηs : i ⟶ j
ηs' : tensorObj.{v, u} (𝒞 := inst) i f ⟶ tensorObj.{v, u} (𝒞 := inst) j f
η₁ :
  tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) i f) ⟶
    tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) j f)
η₂ :
  tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) i f) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) h j) f
η₃ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g i) f ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) h j) f
e_ηs' : ηs ▷ f = ηs'
e_η₁ : Iso.hom (Iso.refl g) ≫ η ≫ Iso.hom (Iso.refl h) ⊗ₘ ηs' = η₁
e_η₂ : η₁ ≫ Iso.inv (α_ h j f) = η₂
e_η₃ : Iso.hom (α_ g i f) ≫ η₂ = η₃
⊢ (η ⊗ₘ ηs) ▷ f = η₃

Tactic:
simp [← e_ηs', ← e_η₁, ← e_η₂, ← e_η₃, MonoidalCategory.tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g h i : C
α : f' ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : tensorObj.{v, u} (𝒞 := inst) h f ⟶ tensorObj.{v, u} (𝒞 := inst) i f
η₁ : tensorObj.{v, u} (𝒞 := inst) g f ⟶ tensorObj.{v, u} (𝒞 := inst) h f
η₂ : tensorObj.{v, u} (𝒞 := inst) g f ⟶ tensorObj.{v, u} (𝒞 := inst) i f
η₃ : tensorObj.{v, u} (𝒞 := inst) f' f ⟶ tensorObj.{v, u} (𝒞 := inst) i f
e_ηs₁ : ηs ▷ f = ηs₁
e_η₁ : η ▷ f = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : Iso.hom (α ▷ᵢ f) ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ f = η₃

Tactic:
simp_all
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i : C
η : f ⟶ g
θ : h ⟶ i
⊢ η ⊗ₘ θ =
    Iso.hom (Iso.refl (tensorObj.{v, u} (𝒞 := inst) f h)) ≫
      (η ⊗ₘ θ) ≫ Iso.hom (Iso.refl (tensorObj.{v, u} (𝒞 := inst) g i))

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h i : C
η : f ⟶ g
ηs : f' ⟶ g'
θ : h ⟶ i
ηθ : tensorObj.{v, u} (𝒞 := inst) f' h ⟶ tensorObj.{v, u} (𝒞 := inst) g' i
η₁ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) f' h) ⟶
    tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) g' i)
ηθ₁ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) f' h) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g g') i
ηθ₂ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f f') h ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g g') i
e_ηθ : ηs ⊗ₘ θ = ηθ
e_η₁ : Iso.hom (Iso.refl f) ≫ η ≫ Iso.hom (Iso.refl g) ⊗ₘ ηθ = η₁
e_ηθ₁ : η₁ ≫ Iso.inv (α_ g g' i) = ηθ₁
e_ηθ₂ : Iso.hom (α_ f f' h) ≫ ηθ₁ = ηθ₂
⊢ (η ⊗ₘ ηs) ⊗ₘ θ = ηθ₂

Tactic:
simp_all
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
ηθ : tensorObj.{v, u} (𝒞 := inst) g f' ⟶ tensorObj.{v, u} (𝒞 := inst) h g'
η₁ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g f') ⟶
    tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h g')
η₂ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g f') ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g'
η₃ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g'
e_ηθ : η ⊗ₘ θ = ηθ
e_η₁ : f ◁ ηθ = η₁
e_η₂ : η₁ ≫ Iso.inv (α_ f h g') = η₂
e_η₃ : Iso.hom (α_ f g f') ≫ η₂ = η₃
simp :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) f' ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g')
    (f ◁ η ⊗ₘ θ) (Iso.hom (α_ f g f') ≫ f ◁ (η ⊗ₘ θ) ≫ Iso.inv (α_ f h g'))
⊢ f ◁ η ⊗ₘ θ = η₃

Tactic:
simp only [← e_ηθ, ← e_η₁, ← e_η₂, ← e_η₃]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
ηθ : tensorObj.{v, u} (𝒞 := inst) g f' ⟶ tensorObj.{v, u} (𝒞 := inst) h g'
η₁ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g f') ⟶
    tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) h g')
η₂ :
  tensorObj.{v, u} (𝒞 := inst) f (tensorObj.{v, u} (𝒞 := inst) g f') ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g'
η₃ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g'
e_ηθ : η ⊗ₘ θ = ηθ
e_η₁ : f ◁ ηθ = η₁
e_η₂ : η₁ ≫ Iso.inv (α_ f h g') = η₂
e_η₃ : Iso.hom (α_ f g f') ≫ η₂ = η₃
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f g) f' ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) f h) g')
    (f ◁ η ⊗ₘ θ) (Iso.hom (α_ f g f') ≫ f ◁ (η ⊗ₘ θ) ≫ Iso.inv (α_ f h g'))

Tactic:
simp [MonoidalCategory.tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : tensorObj.{v, u} (𝒞 := inst) g f ⟶ tensorObj.{v, u} (𝒞 := inst) h f
ηθ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g f) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) h f) g'
ηθ₁ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g f) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g')
ηθ₂ :
  tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) f f') ⟶
    tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g')
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ₘ Iso.hom (Iso.refl f') ≫ θ ≫ Iso.hom (Iso.refl g') = ηθ
e_ηθ₁ : ηθ ≫ Iso.hom (α_ h f g') = ηθ₁
e_ηθ₂ : Iso.inv (α_ g f f') ≫ ηθ₁ = ηθ₂
simp :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) f f') ⟶
      tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g'))
    (η ⊗ₘ f ◁ θ)
    (Iso.inv (α_ g f f') ≫ (η ▷ f ⊗ₘ Iso.hom (Iso.refl f') ≫ θ ≫ Iso.hom (Iso.refl g')) ≫ Iso.hom (α_ h f g'))
⊢ η ⊗ₘ f ◁ θ = ηθ₂

Tactic:
simp only [← e_η₁, ← e_ηθ, ← e_ηθ₁, ← e_ηθ₂]
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h : C
η : g ⟶ h
θ : f' ⟶ g'
η₁ : tensorObj.{v, u} (𝒞 := inst) g f ⟶ tensorObj.{v, u} (𝒞 := inst) h f
ηθ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g f) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) h f) g'
ηθ₁ :
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) g f) f' ⟶
    tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g')
ηθ₂ :
  tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) f f') ⟶
    tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g')
e_η₁ : η ▷ f = η₁
e_ηθ : η₁ ⊗ₘ Iso.hom (Iso.refl f') ≫ θ ≫ Iso.hom (Iso.refl g') = ηθ
e_ηθ₁ : ηθ ≫ Iso.hom (α_ h f g') = ηθ₁
e_ηθ₂ : Iso.inv (α_ g f f') ≫ ηθ₁ = ηθ₂
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) g (tensorObj.{v, u} (𝒞 := inst) f f') ⟶
      tensorObj.{v, u} (𝒞 := inst) h (tensorObj.{v, u} (𝒞 := inst) f g'))
    (η ⊗ₘ f ◁ θ)
    (Iso.inv (α_ g f f') ≫ (η ▷ f ⊗ₘ Iso.hom (Iso.refl f') ≫ θ ≫ Iso.hom (Iso.refl g')) ≫ Iso.hom (α_ h f g'))

Tactic:
simp [MonoidalCategory.tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g h i : C
α : f ≅ g
β : h ≅ i
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) f h ⟶ tensorObj.{v, u} (𝒞 := inst) g i) (Iso.hom (α ⊗ᵢ β)) (Iso.hom (α ⊗ᵢ β))

Tactic:
simp
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h i : C
α : f ≅ g
β : f' ≅ g'
η : g' ⟶ h
ηs : h ⟶ i
η₁ : tensorObj.{v, u} (𝒞 := inst) g g' ⟶ tensorObj.{v, u} (𝒞 := inst) g h
ηs₁ : tensorObj.{v, u} (𝒞 := inst) g h ⟶ tensorObj.{v, u} (𝒞 := inst) g i
η₂ : tensorObj.{v, u} (𝒞 := inst) g g' ⟶ tensorObj.{v, u} (𝒞 := inst) g i
η₃ : tensorObj.{v, u} (𝒞 := inst) f f' ⟶ tensorObj.{v, u} (𝒞 := inst) g i
e_η₁ : g ◁ (Iso.hom (Iso.refl g') ≫ η ≫ Iso.hom (Iso.refl h)) = η₁
e_ηs₁ : g ◁ ηs = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : Iso.hom (α ⊗ᵢ β) ≫ η₂ = η₃
⊢ α.hom ⊗ₘ β.hom ≫ η ≫ ηs = η₃

Tactic:
simp_all [MonoidalCategory.tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f f' g g' h i : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
β : f' ≅ g'
η₁ : tensorObj.{v, u} (𝒞 := inst) g g' ⟶ tensorObj.{v, u} (𝒞 := inst) h g'
ηs₁ : tensorObj.{v, u} (𝒞 := inst) h g' ⟶ tensorObj.{v, u} (𝒞 := inst) i g'
η₂ : tensorObj.{v, u} (𝒞 := inst) g g' ⟶ tensorObj.{v, u} (𝒞 := inst) i g'
η₃ : tensorObj.{v, u} (𝒞 := inst) f f' ⟶ tensorObj.{v, u} (𝒞 := inst) i g'
e_η₁ : (Iso.hom (Iso.refl g) ≫ η ≫ Iso.hom (Iso.refl h)) ▷ g' = η₁
e_ηs₁ : ηs ▷ g' = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : Iso.hom (α ⊗ᵢ β) ≫ η₂ = η₃
⊢ α.hom ≫ η ≫ ηs ⊗ₘ β.hom = η₃

Tactic:
simp_all [MonoidalCategory.tensorHom_def']

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def'