awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ (F.mapComp f (𝟙 b)).inv = F.map f ◁ (F.mapId b).hom ≫ (ρ_ (F.map f)).hom ≫ F.map₂ (ρ_ f).inv

Tactic:
simp [mapComp_id_right]

Premises used: CategoryTheory.Pseudofunctor.mapComp_id_right
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.map f ◁ᵢ F.mapId b = (F.mapComp f (𝟙 b)).symm ≪≫ F.map₂Iso (ρ_ f) ≪≫ (ρ_ (F.map f)).symm

Tactic:
simp [mapComp_id_right]

Premises used: CategoryTheory.Pseudofunctor.mapComp_id_right
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.map f ◁ (F.mapId b).hom = (F.mapComp f (𝟙 b)).inv ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.map f ◁ (F.mapId b).inv = (ρ_ (F.map f)).hom ≫ F.map₂ (ρ_ f).inv ≫ (F.mapComp f (𝟙 b)).hom

Tactic:
simpa using congrArg (·.inv) (F.whiskerLeftIso_mapId f)

Premises used: congrArg, CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b_1 b : B
f : b ⟶ b
hf : f = 𝟙 b
rw rw₁ : Eq.{v₁ + 1} (α := b ⟶ b) (𝟙 b) (𝟙 b)
⊢ f = 𝟙 b

Tactic:
rw [hf]
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b : B
⊢ F.mapId' (𝟙 b) ⋯ = F.mapId b

Tactic:
simp [mapId']

Premises used: CategoryTheory.Pseudofunctor.mapId'
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ F.toLax.mapId' f hf = (F.mapId' f hf).inv

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.LaxFunctor.mapId', CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ F.toOplax.mapId' f hf = (F.mapId' f hf).hom

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.OplaxFunctor.mapId', CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
rw rw₁ : fg = fg
⊢ fg = f ≫ g

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
⊢ F.mapComp' f g (f ≫ g) ⋯ = F.mapComp f g

Tactic:
simp [mapComp']

Premises used: CategoryTheory.Pseudofunctor.mapComp'
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ F.toLax.mapComp' f g fg h = (F.mapComp' f g fg h).inv

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.LaxFunctor.mapComp', rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ F.toOplax.mapComp' f g fg h = (F.mapComp' f g fg h).hom

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.OplaxFunctor.mapComp', rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
rw : F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
rw₁ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ F.mapComp f h ≫ (F'.mapCompIso f h).inv
rw₂ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ (F'.mapCompIso f h).hom ≫ (F'.mapCompIso f h).inv
rw₃ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ 𝟙 (F.map (f ≫ h))
rw₄ rw₅ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η)
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv

Tactic:
rw [F'.mapCompIso_hom f g, ← F.mapComp_naturality_right_assoc, ← F'.mapCompIso_hom f h,
      hom_inv_id, comp_id]

Premises used: CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc, CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
rw : F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
rw₁ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ F.mapComp g h ≫ (F'.mapCompIso g h).inv
rw₂ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ (F'.mapCompIso g h).hom ≫ (F'.mapCompIso g h).inv
rw₃ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ 𝟙 (F.map (g ≫ h))
rw₄ rw₅ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h)
⊢ F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv

Tactic:
rw [F'.mapCompIso_hom _ h, ← F.mapComp_naturality_left_assoc, ← F'.mapCompIso_hom _ h,
      hom_inv_id, comp_id]

Premises used: CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₁ :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₂ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₃ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₄ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ (F'.mapCompIso g h).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₅ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom ≫ (F'.mapCompIso f (g ≫ h)).hom ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₆ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom ≫ 𝟙 (F.map (f ≫ g ≫ h))
rw₇ rw₈ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv

Tactic:
rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      hom_inv_id, comp_id]

Premises used: CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.OplaxFunctor.map₂_associator_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Bicategory.whiskerLeft_hom_inv_assoc, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
dsimp : F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)
⊢ F.map₂ (f ◁ η) = (asIso (F.mapComp f g)).hom ≫ F.map f ◁ F.map₂ η ≫ (asIso (F.mapComp f h)).inv

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
rw : F.map₂ (f ◁ η) = (F.mapComp f g ≫ F.map f ◁ F.map₂ η) ≫ inv (F.mapComp f h)
rw₁ : F.map₂ (f ◁ η) ≫ F.mapComp f h = F.mapComp f g ≫ F.map f ◁ F.map₂ η
rw₂ rw₃ : F.mapComp f g ≫ F.map f ◁ F.map₂ η = F.mapComp f g ≫ F.map f ◁ F.map₂ η
⊢ F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)

Tactic:
rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.OplaxFunctor.mapComp_naturality_right
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
dsimp : F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ inv (F.mapComp g h)
⊢ F.map₂ (η ▷ h) = (asIso (F.mapComp f h)).hom ≫ F.map₂ η ▷ F.map h ≫ (asIso (F.mapComp g h)).inv

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
rw : F.map₂ (η ▷ h) = (F.mapComp f h ≫ F.map₂ η ▷ F.map h) ≫ inv (F.mapComp g h)
rw₁ : F.map₂ (η ▷ h) ≫ F.mapComp g h = F.mapComp f h ≫ F.map₂ η ▷ F.map h
rw₂ rw₃ : F.mapComp f h ≫ F.map₂ η ▷ F.map h = F.mapComp f h ≫ F.map₂ η ▷ F.map h
⊢ F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ inv (F.mapComp g h)

Tactic:
rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.OplaxFunctor.mapComp_naturality_left, CategoryTheory.IsIso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
dsimp :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ inv (F.mapComp g h) ≫ inv (F.mapComp f (g ≫ h))
⊢ F.map₂ (α_ f g h).hom =
    (asIso (F.mapComp (f ≫ g) h)).hom ≫
      (asIso (F.mapComp f g)).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫
          F.map f ◁ (asIso (F.mapComp g h)).inv ≫ (asIso (F.mapComp f (g ≫ h))).inv

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
simp :
  F.map₂ (α_ f g h).hom =
    (((F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom) ≫
        F.map f ◁ inv (F.mapComp g h)) ≫
      inv (F.mapComp f (g ≫ h))
⊢ F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ inv (F.mapComp g h) ≫ inv (F.mapComp f (g ≫ h))

Tactic:
simp only [← assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  (F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h)) ≫ F.map f ◁ F.mapComp g h =
    (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom
⊢ F.map₂ (α_ f g h).hom =
    (((F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom) ≫
        F.map f ◁ inv (F.mapComp g h)) ≫
      inv (F.mapComp f (g ≫ h))

Tactic:
rw [IsIso.eq_comp_inv, ← Bicategory.inv_whiskerLeft, IsIso.eq_comp_inv]

Premises used: CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.Bicategory.inv_whiskerLeft
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h)) ≫ F.map f ◁ F.mapComp g h =
    (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom

Tactic:
simp only [assoc, F.map₂_associator]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.OplaxFunctor.map₂_associator
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
rw : F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ F.mapComp f h
rw₁ : F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.mapComp f g ≫ F.map₂ (f ◁ η)
rw₂ : F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ (F'.mapCompIso f g).inv ≫ F.map₂ (f ◁ η)
rw₃ rw₄ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η)
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv

Tactic:
rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_right, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]

Premises used: CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_right
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
rw : F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ F.mapComp g h
rw₁ : F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.mapComp f h ≫ F.map₂ (η ▷ h)
rw₂ : F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ (F'.mapCompIso f h).inv ≫ F.map₂ (η ▷ h)
rw₃ rw₄ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h)
⊢ F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv

Tactic:
rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_left, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]

Premises used: CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.LaxFunctor.mapComp_naturality_left
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  inv ((F'.mapCompIso f g).hom ▷ F.map h) ≫ (F'.mapCompIso (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv

Tactic:
rw [F'.mapCompIso_inv, F'.mapCompIso_inv, ← inv_comp_eq, ← IsIso.inv_comp_eq]

Premises used: CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv, CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ inv ((F'.mapCompIso f g).hom ▷ F.map h) ≫ (F'.mapCompIso (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b : B
f : a ⟶ b
rw : F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)
⊢ F.map₂ (λ_ f).hom = (F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom

Tactic:
rw [← IsIso.inv_eq_inv, ← F.map₂_inv]

Premises used: CategoryTheory.PrelaxFunctor.map₂_inv, CategoryTheory.LaxFunctor.toPrelaxFunctor, CategoryTheory.IsIso.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b : B
f : a ⟶ b
rw : F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)
⊢ F.map₂ (ρ_ f).hom = (F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom

Tactic:
rw [← IsIso.inv_eq_inv, ← F.map₂_inv]

Premises used: CategoryTheory.PrelaxFunctor.map₂_inv, CategoryTheory.LaxFunctor.toPrelaxFunctor, CategoryTheory.IsIso.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : Prefunctor.{v₁, v₂, u₁, u₂} B C := { obj := obj, map := @map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrefunctor := toPrefunctor, map₂ := @map₂ }
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
toPrelaxFunctor : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := @map₂_id, map₂_comp := @map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) = map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := @map_comp,
    map₂_whisker_left := @map₂_whisker_left, map₂_whisker_right := @map₂_whisker_right }
a b : B
f : a ⟶ b
rw : map (𝟙 a) ≫ map f = 𝟙 (obj a) ≫ map f
rw₁ rw₂ : 𝟙 (obj a) ≫ map f = 𝟙 (obj a) ≫ map f
⊢ map (𝟙 a ≫ f) = 𝟙 (obj a) ≫ map f

Tactic:
rw [map_comp (𝟙 a) f, map_id a]

Premises used: CategoryTheory.CategoryStruct.id