awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
        mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom)
    oplaxFunctorOfIsLocallyDiscrete._auto_1
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ map (𝟙 b₀ ≫ f) = map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
        mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom)
    oplaxFunctorOfIsLocallyDiscrete._auto_1
map₂_left_unitor :
  autoParam (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯)
    oplaxFunctorOfIsLocallyDiscrete._auto_2
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ map (f ≫ 𝟙 b₁) = map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b : B
f g : a ⟶ b
φ : f ⟶ g
obtain : ∀ (φ : f ⟶ f), map f = map f
⊢ map f = map g

Tactic:
obtain rfl := obj_ext_of_isDiscrete φ

Premises used: CategoryTheory.obj_ext_of_isDiscrete, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b : B
f : a ⟶ b
φ : f ⟶ f
⊢ map f = map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b c : B
f f' : a ⟶ b
η : f ⟶ f'
obtain : ∀ (η : f ⟶ f) (g : b ⟶ c), eqToHom ⋯ ≫ mapComp f g = mapComp f g ≫ eqToHom ⋯ ▷ map g
⊢ ∀ (g : b ⟶ c), eqToHom ⋯ ≫ mapComp f' g = mapComp f g ≫ eqToHom ⋯ ▷ map g

Tactic:
obtain rfl := obj_ext_of_isDiscrete η

Premises used: CategoryTheory.obj_ext_of_isDiscrete, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b c : B
f : a ⟶ b
η : f ⟶ f
⊢ ∀ (g : b ⟶ c), eqToHom ⋯ ≫ mapComp f g = mapComp f g ≫ eqToHom ⋯ ▷ map g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b c : B
x : a ⟶ b
x_1 x_2 : b ⟶ c
η : x_1 ⟶ x_2
obtain : ∀ (η : x_1 ⟶ x_1), eqToHom ⋯ ≫ mapComp x x_1 = mapComp x x_1 ≫ map x ◁ eqToHom ⋯
⊢ eqToHom ⋯ ≫ mapComp x x_2 = mapComp x x_1 ≫ map x ◁ eqToHom ⋯

Tactic:
obtain rfl := obj_ext_of_isDiscrete η

Premises used: CategoryTheory.obj_ext_of_isDiscrete, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b c : B
x : a ⟶ b
x_1 : b ⟶ c
η : x_1 ⟶ x_1
⊢ eqToHom ⋯ ≫ mapComp x x_1 = mapComp x x_1 ≫ map x ◁ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
x : LocallyDiscrete C
X : C
⊢ Eq.{v_2 + 1} (α :=
    Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
      ((fun (x : LocallyDiscrete C) ↦
          (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
            | { as := X } => { as := F.obj X } :
            LocallyDiscrete D))
        { as := X })
      ((fun (x : LocallyDiscrete C) ↦
          (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
            | { as := X } => { as := F.obj X } :
            LocallyDiscrete D))
        { as := X }))
    ((fun {b b' : LocallyDiscrete C} (x : b ⟶ b') ↦
        (match (motive :=
            (b ⟶ b') →
              Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
                ((fun (x : LocallyDiscrete C) ↦
                    (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                      | { as := X } => { as := F.obj X } :
                      LocallyDiscrete D))
                  b)
                ((fun (x : LocallyDiscrete C) ↦
                    (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                      | { as := X } => { as := F.obj X } :
                      LocallyDiscrete D))
                  b'))
            x with
          | { as := f } => (F.map f).toLoc :
          Quiver.Hom.{v_2, u_2} (V := LocallyDiscrete D)
            ((fun (x : LocallyDiscrete C) ↦
                (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                  | { as := X } => { as := F.obj X } :
                  LocallyDiscrete D))
              b)
            ((fun (x : LocallyDiscrete C) ↦
                (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
                  | { as := X } => { as := F.obj X } :
                  LocallyDiscrete D))
              b')))
      (𝟙 { as := X }))
    (𝟙
      ((fun (x : LocallyDiscrete C) ↦
          (match (motive := LocallyDiscrete C → LocallyDiscrete D) x with
            | { as := X } => { as := F.obj X } :
            LocallyDiscrete D))
        { as := X }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
I : Type u_1
B : Type u_2
inst : Category.{v_1, u_1} I
inst_1 : Bicategory.{u_3, u_4, u_2} B
inst_2 : Strict.{u_3, u_4, u_2} B
F : Functor.{v_1, u_4, u_1, u_2} I B
x : LocallyDiscrete I
X : I
⊢ Eq.{u_4 + 1} (α :=
    Quiver.Hom.{u_4, u_2} (V := B)
      ((fun (x : LocallyDiscrete I) ↦
          (match (motive := LocallyDiscrete I → B) x with
            | { as := X } => F.obj X :
            B))
        { as := X })
      ((fun (x : LocallyDiscrete I) ↦
          (match (motive := LocallyDiscrete I → B) x with
            | { as := X } => F.obj X :
            B))
        { as := X }))
    ((fun {b b' : LocallyDiscrete I} (x : b ⟶ b') ↦
        (match (motive :=
            (b ⟶ b') →
              Quiver.Hom.{u_4, u_2} (V := B)
                ((fun (x : LocallyDiscrete I) ↦
                    (match (motive := LocallyDiscrete I → B) x with
                      | { as := X } => F.obj X :
                      B))
                  b)
                ((fun (x : LocallyDiscrete I) ↦
                    (match (motive := LocallyDiscrete I → B) x with
                      | { as := X } => F.obj X :
                      B))
                  b'))
            x with
          | { as := f } => F.map f :
          Quiver.Hom.{u_4, u_2} (V := B)
            ((fun (x : LocallyDiscrete I) ↦
                (match (motive := LocallyDiscrete I → B) x with
                  | { as := X } => F.obj X :
                  B))
              b)
            ((fun (x : LocallyDiscrete I) ↦
                (match (motive := LocallyDiscrete I → B) x with
                  | { as := X } => F.obj X :
                  B))
              b')))
      (𝟙 { as := X }))
    (𝟙
      ((fun (x : LocallyDiscrete I) ↦
          (match (motive := LocallyDiscrete I → B) x with
            | { as := X } => F.obj X :
            B))
        { as := X }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B₀ : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} B₀
inst_1 : Bicategory.{u_3, u_4, u_2} C
obj : B₀ → C
map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B₀) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
b₀ b₁ b₂ b₃ : B₀
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
h : b₂ ⟶ b₃
⊢ map ((f ≫ g) ≫ h) = map (f ≫ g ≫ h)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B₀ : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} B₀
inst_1 : Bicategory.{u_3, u_4, u_2} C
obj : B₀ → C
map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B₀) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      (mapComp (f ≫ g) h).hom ≫
          (mapComp f g).hom ▷ map h ≫
            (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
        eqToHom ⋯)
    mkPseudofunctor._auto_1
b₀ b₁ : B₀
f : b₀ ⟶ b₁
⊢ map (𝟙 b₀ ≫ f) = map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
Goal:
B₀ : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} B₀
inst_1 : Bicategory.{u_3, u_4, u_2} C
obj : B₀ → C
map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B₀) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B₀} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  autoParam
    (∀ {b₀ b₁ b₂ b₃ : B₀} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
      (mapComp (f ≫ g) h).hom ≫
          (mapComp f g).hom ▷ map h ≫
            (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
        eqToHom ⋯)
    mkPseudofunctor._auto_1
map₂_left_unitor :
  autoParam
    (∀ {b₀ b₁ : B₀} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯)
    mkPseudofunctor._auto_2
b₀ b₁ : B₀
f : b₀ ⟶ b₁
⊢ map (f ≫ 𝟙 b₁) = map f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ (α_ f g h).inv ≫ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom

Tactic:
rw [← F.map₂_associator, ← F.map₂_comp_assoc]

Premises used: CategoryTheory.OplaxFunctor.map₂_associator, CategoryTheory.OplaxFunctor.toPrelaxFunctor, CategoryTheory.PrelaxFunctor.map₂_comp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h =
    F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ (α_ (F.map f) (F.map g) (F.map h)).inv

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

Tactic:
rw [Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
simp : F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom
⊢ (F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f) ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
rw rw₁ : F.map₂ (λ_ f).hom = F.map₂ (λ_ f).hom
⊢ F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom

Tactic:
rw [← F.map₂_leftUnitor]

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

Tactic:
rw [Iso.eq_comp_inv]

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

Tactic:
simp only [Category.assoc]

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

Tactic:
rw [← F.map₂_rightUnitor]

Premises used: CategoryTheory.OplaxFunctor.map₂_rightUnitor
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
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.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b : B
⊢ F.mapId' (𝟙 b) ⋯ = F.mapId b

Tactic:
simp [mapId']

Premises used: CategoryTheory.OplaxFunctor.mapId'
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
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 : OplaxFunctor.{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
rw rw₁ : fg = fg
⊢ fg = f ≫ g

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : OplaxFunctor.{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.OplaxFunctor.mapComp'
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : OplaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
dsimp :
  G.map₂ (F.map₂ (η ▷ g)) ≫ G.map₂ (F.mapComp f' g) ≫ G.mapComp (F.map f') (F.map g) =
    (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
⊢ Eq (α :=
    (F.comp G.toPrelaxFunctor).map (f ≫ g) ⟶ (F.comp G.toPrelaxFunctor).map f' ≫ (F.comp G.toPrelaxFunctor).map g)
    ((F.comp G.toPrelaxFunctor).map₂ (η ▷ g) ≫
      Functor.map (G.mapFunctor (F.obj a) (F.obj c)) (F.mapComp f' g) ≫ G.mapComp (F.map f') (F.map g))
    ((Functor.map (G.mapFunctor (F.obj a) (F.obj c)) (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫
      (F.comp G.toPrelaxFunctor).map₂ η ▷ (F.comp G.toPrelaxFunctor).map g)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : OplaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
rw :
  G.map₂ (F.map₂ (η ▷ g) ≫ F.mapComp f' g) ≫ G.mapComp (F.map f') (F.map g) =
    (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
rw₁ :
  G.map₂ (F.mapComp f g ≫ F.map₂ η ▷ F.map g) ≫ G.mapComp (F.map f') (F.map g) =
    (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
rw₂ :
  G.map₂ (F.mapComp f g) ≫ G.map₂ (F.map₂ η ▷ F.map g) ≫ G.mapComp (F.map f') (F.map g) =
    (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
rw₃ :
  G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g) =
    (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
rw₄ rw₅ :
  G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g) =
    G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
⊢ G.map₂ (F.map₂ (η ▷ g)) ≫ G.map₂ (F.mapComp f' g) ≫ G.mapComp (F.map f') (F.map g) =
    (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)

Tactic:
rw [← G.map₂_comp_assoc, mapComp_naturality_left, G.map₂_comp_assoc, mapComp_naturality_left,
      assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.OplaxFunctor.toPrelaxFunctor, CategoryTheory.OplaxFunctor.mapComp_naturality_left, CategoryTheory.PrelaxFunctor.map₂_comp_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax
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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : OplaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c : B
η : a ⟶ b
dsimp :
  ∀ {g g' : b ⟶ c} (η_1 : g ⟶ g'),
    G.map₂ (F.map₂ (η ◁ η_1)) ≫ G.map₂ (F.mapComp η g') ≫ G.mapComp (F.map η) (F.map g') =
      (G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1)
⊢ ∀ {g g' : b ⟶ c} (η_1 : g ⟶ g'),
    Eq (α :=
      (F.comp G.toPrelaxFunctor).map (η ≫ g) ⟶ (F.comp G.toPrelaxFunctor).map η ≫ (F.comp G.toPrelaxFunctor).map g')
      ((F.comp G.toPrelaxFunctor).map₂ (η ◁ η_1) ≫
        Functor.map (G.mapFunctor (F.obj a) (F.obj c)) (F.mapComp η g') ≫ G.mapComp (F.map η) (F.map g'))
      ((Functor.map (G.mapFunctor (F.obj a) (F.obj c)) (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g)) ≫
        (F.comp G.toPrelaxFunctor).map η ◁ (F.comp G.toPrelaxFunctor).map₂ η_1)

Tactic:
dsimp