awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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

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
obj : ∀ (x : B), (comp (id B) F).obj x = F.obj x
map :
  @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (comp (id B) F).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) (comp (id B) 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.toPrelaxFunctorStruct
mapId : (comp (id B) F).mapId ≍ F.mapId
mapComp :
  @LaxFunctor.mapComp B inst C inst_1 (comp (id B) F).toLaxFunctor ≍ @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
⊢ comp (id B) F = 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
⊢ (comp (id B) F).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 (comp (id B) F).toPrefunctor =
    @Prefunctor.map B inst.toQuiver C inst_1.toQuiver F.toPrefunctor
⊢ @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (comp (id B) F).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), (comp (id B) F).map x_2 = F.map x_2
⊢ @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (comp (id B) F).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
⊢ (comp (id B) F).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) (comp (id B) 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.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) (comp (id B) 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.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), (comp (id B) F).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) (comp (id B) 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.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
⊢ (comp (id B) F).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 : (comp (id B) F).mapId = F.mapId
⊢ (comp (id B) F).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), (comp (id B) F).mapId x = F.mapId x
⊢ (comp (id B) F).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
⊢ (comp (id B) F).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 (comp (id B) F).toLaxFunctor = @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
⊢ @LaxFunctor.mapComp B inst C inst_1 (comp (id B) F).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), (comp (id B) F).mapComp x_3 x_4 = F.mapComp x_3 x_4
⊢ @LaxFunctor.mapComp B inst C inst_1 (comp (id B) F).toLaxFunctor = @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor

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 x_2 : B
x_3 : x ⟶ x_1
x_4 : x_1 ⟶ x_2
⊢ (comp (id B) F).mapComp x_3 x_4 = F.mapComp x_3 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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
obj : ∀ (x : B), ((F.comp G).comp H).obj x = (F.comp (G.comp H)).obj x
map :
  @Prefunctor.map B inst.toQuiver E inst_3.toQuiver ((F.comp G).comp H).toPrefunctor ≍
    @Prefunctor.map B inst.toQuiver E inst_3.toQuiver (F.comp (G.comp H)).toPrefunctor
map₂ :
  @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) E inst_3.toQuiver
      (fun (a b : E) ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) E inst_3.toQuiver
      (fun (a b : E) ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).toPrelaxFunctorStruct
mapId : ((F.comp G).comp H).mapId ≍ (F.comp (G.comp H)).mapId
mapComp :
  @LaxFunctor.mapComp B inst E inst_3 ((F.comp G).comp H).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst E inst_3 (F.comp (G.comp H)).toLaxFunctor
⊢ (F.comp G).comp H = F.comp (G.comp H)

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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
x : B
⊢ ((F.comp G).comp H).obj x = (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
map :
  @Prefunctor.map B inst.toQuiver E inst_3.toQuiver ((F.comp G).comp H).toPrefunctor =
    @Prefunctor.map B inst.toQuiver E inst_3.toQuiver (F.comp (G.comp H)).toPrefunctor
⊢ @Prefunctor.map B inst.toQuiver E inst_3.toQuiver ((F.comp G).comp H).toPrefunctor ≍
    @Prefunctor.map B inst.toQuiver E inst_3.toQuiver (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
map : ∀ (x x_1 : B) (x_2 : x ⟶ x_1), ((F.comp G).comp H).map x_2 = (F.comp (G.comp H)).map x_2
⊢ @Prefunctor.map B inst.toQuiver E inst_3.toQuiver ((F.comp G).comp H).toPrefunctor =
    @Prefunctor.map B inst.toQuiver E inst_3.toQuiver (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
x x_1 : B
x_2 : x ⟶ x_1
⊢ ((F.comp G).comp H).map x_2 = (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
map₂ :
  @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) E inst_3.toQuiver
      (fun (a b : E) ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct =
    @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) E inst_3.toQuiver
      (fun (a b : E) ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).toPrelaxFunctorStruct
⊢ @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) E inst_3.toQuiver
      (fun (a b : E) ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct ≍
    @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) E inst_3.toQuiver
      (fun (a b : E) ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
map₂ : ∀ (x x_1 : B) (x_2 x_3 : x ⟶ x_1) (x_4 : x_2 ⟶ x_3), ((F.comp G).comp H).map₂ x_4 = (F.comp (G.comp H)).map₂ x_4
⊢ @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) E inst_3.toQuiver
      (fun (a b : E) ↦ (homCategory a b).toQuiver) ((F.comp G).comp H).toPrelaxFunctorStruct =
    @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) E inst_3.toQuiver
      (fun (a b : E) ↦ (homCategory a b).toQuiver) (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
x x_1 : B
x_2 x_3 : x ⟶ x_1
x_4 : x_2 ⟶ x_3
⊢ ((F.comp G).comp H).map₂ x_4 = (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
mapId : ((F.comp G).comp H).mapId = (F.comp (G.comp H)).mapId
⊢ ((F.comp G).comp H).mapId ≍ (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
mapId : ∀ (x : B), ((F.comp G).comp H).mapId x = (F.comp (G.comp H)).mapId x
⊢ ((F.comp G).comp H).mapId = (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
x : B
⊢ ((F.comp G).comp H).mapId x = (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
mapComp :
  @LaxFunctor.mapComp B inst E inst_3 ((F.comp G).comp H).toLaxFunctor =
    @LaxFunctor.mapComp B inst E inst_3 (F.comp (G.comp H)).toLaxFunctor
⊢ @LaxFunctor.mapComp B inst E inst_3 ((F.comp G).comp H).toLaxFunctor ≍
    @LaxFunctor.mapComp B inst E inst_3 (F.comp (G.comp H)).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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
mapComp :
  ∀ (x x_1 x_2 : B) (x_3 : x ⟶ x_1) (x_4 : x_1 ⟶ x_2),
    ((F.comp G).comp H).mapComp x_3 x_4 = (F.comp (G.comp H)).mapComp x_3 x_4
⊢ @LaxFunctor.mapComp B inst E inst_3 ((F.comp G).comp H).toLaxFunctor =
    @LaxFunctor.mapComp B inst E inst_3 (F.comp (G.comp H)).toLaxFunctor

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
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
E : Type u₄
inst_3 : Bicategory.{w₄, v₄, u₄} E
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictlyUnitaryLaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
H : StrictlyUnitaryLaxFunctor.{w₃, w₄, v₃, v₄, u₃, u₄} D E
x x_1 x_2 : B
x_3 : x ⟶ x_1
x_4 : x_1 ⟶ x_2
⊢ ((F.comp G).comp H).mapComp x_3 x_4 = (F.comp (G.comp H)).mapComp x_3 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
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 ≫ g) ≅ map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    map₂ (f ◁ η) = (mapComp f g).hom ≫ map f ◁ map₂ η ≫ (mapComp f h).inv
map₂_whisker_right :
  ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    map₂ (η ▷ h) = (mapComp f h).hom ≫ map₂ η ▷ map h ≫ (mapComp g h).inv
a b : B
f : a ⟶ b
rw rw₁ : 𝟙 (obj a) ≫ map f = 𝟙 (obj a) ≫ map f
⊢ map (𝟙 a) ≫ map f = 𝟙 (obj 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 ≫ g) ≅ map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    map₂ (f ◁ η) = (mapComp f g).hom ≫ map f ◁ map₂ η ≫ (mapComp f h).inv
map₂_whisker_right :
  ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    map₂ (η ▷ h) = (mapComp f h).hom ≫ map₂ η ▷ map h ≫ (mapComp g h).inv
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = (mapComp (𝟙 a) f).hom ≫ eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
rw rw₁ : map f ≫ 𝟙 (obj b) = map f ≫ 𝟙 (obj b)
⊢ map f ≫ map (𝟙 b) = map f ≫ 𝟙 (obj 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 : StrictlyUnitaryPseudofunctorCore.{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 ◁ η) = (S.mapComp f x).hom ≫ S.map f ◁ S.map₂ η ≫ (S.mapComp f x_1).inv

Tactic:
simpa using S.map₂_whisker_left f η

Premises used: CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_whisker_left
-- 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 : StrictlyUnitaryPseudofunctorCore.{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) = (S.mapComp f_1 f).hom ≫ S.map₂ η ▷ S.map f ≫ (S.mapComp g f).inv

Tactic:
simpa using S.map₂_whisker_right η f

Premises used: CategoryTheory.StrictlyUnitaryPseudofunctorCore.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
S : StrictlyUnitaryPseudofunctorCore.{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 =
    (S.mapComp (f ≫ g) h).hom ≫
      (S.mapComp f g).hom ▷ S.map h ≫
        (α_ (S.map f) (S.map g) (S.map h)).hom ≫ S.map f ◁ (S.mapComp g h).inv ≫ (S.mapComp f (g ≫ h)).inv

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

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

Tactic:
simpa using S.map₂_left_unitor f

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

Tactic:
simpa using S.map₂_right_unitor f

Premises used: CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_right_unitor
-- 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 : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ F.toLax.map (𝟙 x) = 𝟙 (F.toLax.obj x)

Tactic:
simp [F.map_id]

Premises used: CategoryTheory.StrictlyUnitaryPseudofunctor.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 : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ F.toLax.mapId x = eqToHom ⋯

Tactic:
simp [F.mapId_eq_eqToIso]

Premises used: CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso
-- 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 : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ F.toStrictlyUnitaryLaxFunctor.obj x = F.obj x

Tactic:
rfl

Premises used: rfl
-- 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 : StrictlyUnitaryPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x y : B
f : x ⟶ y
⊢ F.toStrictlyUnitaryLaxFunctor.map f = F.map f

Tactic:
rfl

Premises used: rfl