awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
rw : map f ≫ map (𝟙 b) = map f ≫ 𝟙 (obj b)
rw₁ rw₂ : map f ≫ 𝟙 (obj b) = map f ≫ 𝟙 (obj b)
⊢ map (f ≫ 𝟙 b) = map f ≫ 𝟙 (obj b)

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

Premises used: CategoryTheory.CategoryStruct.id
-- 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 }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
map₂_right_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (ρ_ f).hom = eqToHom ⋯ ≫ (ρ_ (map f)).hom
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ map ((f ≫ g) ≫ h) = (map f ≫ map g) ≫ map h

Tactic:
simp only [map_comp]
-- 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 }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
map₂_right_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (ρ_ f).hom = eqToHom ⋯ ≫ (ρ_ (map f)).hom
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ map f ≫ map g ≫ map h = map (f ≫ g ≫ h)

Tactic:
simp only [map_comp]
-- 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
S : StrictPseudofunctorCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c : B
f : a ⟶ b
x x_1 : b ⟶ c
η : x ⟶ x_1
⊢ S.map₂ (f ◁ η) = Iso.hom (eqToIso ⋯) ≫ S.map f ◁ S.map₂ η ≫ Iso.inv (eqToIso ⋯)

Tactic:
simpa using S.map₂_whisker_left f η

Premises used: CategoryTheory.StrictPseudofunctorCore.toStrictPseudofunctorPreCore, CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left
-- 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
S : StrictPseudofunctorCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c : B
f_1 g : a ⟶ b
η : f_1 ⟶ g
f : b ⟶ c
⊢ S.map₂ (η ▷ f) = Iso.hom (eqToIso ⋯) ≫ S.map₂ η ▷ S.map f ≫ Iso.inv (eqToIso ⋯)

Tactic:
simpa using S.map₂_whisker_right η f

Premises used: CategoryTheory.StrictPseudofunctorCore.toStrictPseudofunctorPreCore, CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right
-- 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
S : StrictPseudofunctorCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ S.map₂ (α_ f g h).hom =
    Iso.hom (eqToIso ⋯) ≫
      Iso.hom (eqToIso ⋯) ▷ S.map h ≫
        (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ Iso.inv (eqToIso ⋯) ≫ Iso.inv (eqToIso ⋯)

Tactic:
simpa using S.map₂_associator f g h

Premises used: CategoryTheory.StrictPseudofunctorCore.map₂_associator
-- 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
S : StrictPseudofunctorCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ S.map₂ (λ_ f).hom = Iso.hom (eqToIso ⋯) ≫ Iso.hom (eqToIso ⋯) ▷ S.map f ≫ (λ_ (S.map f)).hom

Tactic:
simpa using S.map₂_left_unitor f

Premises used: CategoryTheory.StrictPseudofunctorCore.map₂_left_unitor
-- 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
S : StrictPseudofunctorCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ S.map₂ (ρ_ f).hom = Iso.hom (eqToIso ⋯) ≫ S.map f ◁ Iso.hom (eqToIso ⋯) ≫ (ρ_ (S.map f)).hom

Tactic:
simpa using S.map₂_right_unitor f

Premises used: CategoryTheory.StrictPseudofunctorCore.map₂_right_unitor
-- 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
F_1 F : StrictPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictPseudofunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c : B
x : a ⟶ b
⊢ ∀ (g : b ⟶ c),
    (F.comp G.toStrictlyUnitaryPseudofunctor).map (x ≫ g) =
      (F.comp G.toStrictlyUnitaryPseudofunctor).map x ≫ (F.comp G.toStrictlyUnitaryPseudofunctor).map g

Tactic:
simp [StrictPseudofunctor.map_comp]

Premises used: CategoryTheory.StrictPseudofunctor.map_comp
-- 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
F_1 F : StrictPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictPseudofunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c : B
x : a ⟶ b
x_1 : b ⟶ c
w : ((F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x x_1).hom = Iso.hom (eqToIso ⋯)
⊢ (F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x x_1 = eqToIso ⋯

Tactic:
ext
-- 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
F_1 F : StrictPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictPseudofunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c : B
x : a ⟶ b
x_1 : b ⟶ c
⊢ ((F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x x_1).hom = Iso.hom (eqToIso ⋯)

Tactic:
simp [StrictPseudofunctor.mapComp_eq_eqToIso,
      PrelaxFunctor.map₂_eqToHom]

Premises used: CategoryTheory.PrelaxFunctor.map₂_eqToHom, CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso
-- 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
inst_3 : Strict.{w₁, v₁, u₁} B
inst_4 : Strict.{w₂, v₂, u₂} C
S : StrictPseudofunctorPreCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c : B
f : a ⟶ b
x x_1 : b ⟶ c
η : x ⟶ x_1
⊢ S.map₂ (f ◁ η) = Iso.hom (eqToIso ⋯) ≫ S.map f ◁ S.map₂ η ≫ Iso.inv (eqToIso ⋯)

Tactic:
simpa using S.map₂_whisker_left f η

Premises used: CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_left
-- 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
inst_3 : Strict.{w₁, v₁, u₁} B
inst_4 : Strict.{w₂, v₂, u₂} C
S : StrictPseudofunctorPreCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c : B
f_1 g : a ⟶ b
η : f_1 ⟶ g
f : b ⟶ c
⊢ S.map₂ (η ▷ f) = Iso.hom (eqToIso ⋯) ≫ S.map₂ η ▷ S.map f ≫ Iso.inv (eqToIso ⋯)

Tactic:
simpa using S.map₂_whisker_right η f

Premises used: CategoryTheory.StrictPseudofunctorPreCore.map₂_whisker_right
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
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₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map f ≫ map g ⟶ map (f ≫ g)
mapComp_naturality_left :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), mapComp f g ≫ map₂ (η ▷ g) = map₂ η ▷ map g ≫ mapComp f' g
mapComp_naturality_right :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), mapComp f g ≫ map₂ (f ◁ η) = map f ◁ map₂ η ≫ mapComp f g'
a b : B
f : a ⟶ b
rw rw₁ : 𝟙 (obj a) ≫ map f = 𝟙 (obj a) ≫ map f
⊢ 𝟙 (obj a) ≫ map f = map (𝟙 a) ≫ map f

Tactic:
rw [map_id a]
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
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₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map f ≫ map g ⟶ map (f ≫ g)
mapComp_naturality_left :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), mapComp f g ≫ map₂ (η ▷ g) = map₂ η ▷ map g ≫ mapComp f' g
mapComp_naturality_right :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), mapComp f g ≫ map₂ (f ◁ η) = map f ◁ map₂ η ≫ mapComp f g'
map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).inv = (λ_ (map f)).inv ≫ eqToHom ⋯ ≫ mapComp (𝟙 a) f
a b : B
f : a ⟶ b
rw rw₁ : map f ≫ 𝟙 (obj b) = map f ≫ 𝟙 (obj b)
⊢ map f ≫ 𝟙 (obj b) = map f ≫ map (𝟙 b)

Tactic:
rw [map_id b]
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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
S : StrictlyUnitaryLaxFunctorCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ S.mapComp f g ▷ S.map h ≫ S.mapComp (f ≫ g) h ≫ S.map₂ (α_ f g h).hom =
    (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ S.mapComp g h ≫ S.mapComp f (g ≫ h)

Tactic:
simpa using S.map₂_associator f g h

Premises used: CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_associator
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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
S : StrictlyUnitaryLaxFunctorCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ S.map₂ (λ_ f).inv = (λ_ (S.map f)).inv ≫ eqToHom ⋯ ▷ S.map f ≫ S.mapComp (𝟙 a) f

Tactic:
simpa using S.map₂_leftUnitor f

Premises used: CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_leftUnitor
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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
S : StrictlyUnitaryLaxFunctorCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ S.map₂ (ρ_ f).inv = (ρ_ (S.map f)).inv ≫ S.map f ◁ eqToHom ⋯ ≫ S.mapComp f (𝟙 b)

Tactic:
simpa using S.map₂_rightUnitor f

Premises used: CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_rightUnitor
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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 : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
rw : IsIso (eqToHom ⋯)
⊢ IsIso (F.mapId x)

Tactic:
rw [mapId_eq_eqToHom]

Premises used: CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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 : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ IsIso (eqToHom ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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 : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ F.mapId x ≫ eqToHom ⋯ = 𝟙 (𝟙 (F.obj x))

Tactic:
simp [F.mapId_eq_eqToHom]

Premises used: CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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 : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ eqToHom ⋯ ≫ F.mapId x = 𝟙 (F.map (𝟙 x))

Tactic:
simp [F.mapId_eq_eqToHom]

Premises used: CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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 : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
x : B
⊢ (F.comp G.toLaxFunctor).map (𝟙 x) = 𝟙 ((F.comp G.toLaxFunctor).obj x)

Tactic:
simp [StrictlyUnitaryLaxFunctor.map_id]

Premises used: CategoryTheory.StrictlyUnitaryLaxFunctor.map_id
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
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 : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
x : B
⊢ (F.comp G.toLaxFunctor).mapId x = eqToHom ⋯

Tactic:
simp [StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom,
      PrelaxFunctor.map₂_eqToHom]

Premises used: CategoryTheory.PrelaxFunctor.map₂_eqToHom, CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
obj : ∀ (x : B), (F.comp (id C)).obj x = F.obj x
map :
  @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (F.comp (id C)).toPrefunctor ≍
    @Prefunctor.map B inst.toQuiver C inst_1.toQuiver F.toPrefunctor
map₂ :
  @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
      (fun (a b : C) ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
      (fun (a b : C) ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct
mapId : (F.comp (id C)).mapId ≍ F.mapId
mapComp :
  @LaxFunctor.mapComp B inst C inst_1 (F.comp (id C)).toLaxFunctor ≍ @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
⊢ F.comp (id C) = F

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ (F.comp (id C)).obj x = F.obj x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
map :
  @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (F.comp (id C)).toPrefunctor =
    @Prefunctor.map B inst.toQuiver C inst_1.toQuiver F.toPrefunctor
⊢ @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (F.comp (id C)).toPrefunctor ≍
    @Prefunctor.map B inst.toQuiver C inst_1.toQuiver F.toPrefunctor

Tactic:
rw [heq_iff_eq]

Premises used: heq_iff_eq
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
map : ∀ (x x_1 : B) (x_2 : x ⟶ x_1), (F.comp (id C)).map x_2 = F.map x_2
⊢ @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (F.comp (id C)).toPrefunctor =
    @Prefunctor.map B inst.toQuiver C inst_1.toQuiver F.toPrefunctor

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x x_1 : B
x_2 : x ⟶ x_1
⊢ (F.comp (id C)).map x_2 = F.map x_2

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
map₂ :
  @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
      (fun (a b : C) ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct =
    @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
      (fun (a b : C) ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct
⊢ @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
      (fun (a b : C) ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
      (fun (a b : C) ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

Tactic:
rw [heq_iff_eq]

Premises used: heq_iff_eq
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
map₂ : ∀ (x x_1 : B) (x_2 x_3 : x ⟶ x_1) (x_4 : x_2 ⟶ x_3), (F.comp (id C)).map₂ x_4 = F.map₂ x_4
⊢ @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
      (fun (a b : C) ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct =
    @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
      (fun (a b : C) ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x x_1 : B
x_2 x_3 : x ⟶ x_1
x_4 : x_2 ⟶ x_3
⊢ (F.comp (id C)).map₂ x_4 = F.map₂ x_4

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
mapId : (F.comp (id C)).mapId = F.mapId
⊢ (F.comp (id C)).mapId ≍ F.mapId

Tactic:
rw [heq_iff_eq]

Premises used: heq_iff_eq
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
mapId : ∀ (x : B), (F.comp (id C)).mapId x = F.mapId x
⊢ (F.comp (id C)).mapId = F.mapId

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ (F.comp (id C)).mapId x = F.mapId x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
mapComp :
  @LaxFunctor.mapComp B inst C inst_1 (F.comp (id C)).toLaxFunctor = @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
⊢ @LaxFunctor.mapComp B inst C inst_1 (F.comp (id C)).toLaxFunctor ≍ @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor

Tactic:
rw [heq_iff_eq]

Premises used: heq_iff_eq
-- Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
mapComp : ∀ (x x_1 x_2 : B) (x_3 : x ⟶ x_1) (x_4 : x_1 ⟶ x_2), (F.comp (id C)).mapComp x_3 x_4 = F.mapComp x_3 x_4
⊢ @LaxFunctor.mapComp B inst C inst_1 (F.comp (id C)).toLaxFunctor = @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor

Tactic:
ext