awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ F.comp (id C) = F
have mapId : (F.comp (id C)).mapId ≍ F.mapId
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ F.comp (id C) = F
have mapComp : @LaxFunctor.mapComp B inst C inst_1 (F.comp (id C)).toLaxFunctor ≍ @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have map : ∀ (x x_1 : B) (x_2 : x ⟶ x_1), (F.comp (id C)).map x_2 = F.map x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (F.comp (id C)).mapId ≍ F.mapId
have mapId : (F.comp (id C)).mapId = F.mapId
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (F.comp (id C)).mapId = F.mapId
have mapId : ∀ (x : B), (F.comp (id C)).mapId x = F.mapId x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @LaxFunctor.mapComp B inst C inst_1 (F.comp (id C)).toLaxFunctor ≍ @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
have mapComp : @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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @LaxFunctor.mapComp B inst C inst_1 (F.comp (id C)).toLaxFunctor = @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ comp (id B) F = F
have obj : ∀ (x : B), (comp (id B) F).obj x = F.obj x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ comp (id B) F = F
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ comp (id B) F = F
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ comp (id B) F = F
have mapId : (comp (id B) F).mapId ≍ F.mapId
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ comp (id B) F = F
have mapComp : @LaxFunctor.mapComp B inst C inst_1 (comp (id B) F).toLaxFunctor ≍ @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have map : ∀ (x x_1 : B) (x_2 : x ⟶ x_1), (comp (id B) F).map x_2 = F.map x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (comp (id B) F).mapId ≍ F.mapId
have mapId : (comp (id B) F).mapId = F.mapId
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (comp (id B) F).mapId = F.mapId
have mapId : ∀ (x : B), (comp (id B) F).mapId x = F.mapId x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @LaxFunctor.mapComp B inst C inst_1 (comp (id B) F).toLaxFunctor ≍ @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
have mapComp : @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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @LaxFunctor.mapComp B inst C inst_1 (comp (id B) F).toLaxFunctor = @LaxFunctor.mapComp B inst C inst_1 F.toLaxFunctor
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (F.comp G).comp H = F.comp (G.comp H)
have obj : ∀ (x : B), ((F.comp G).comp H).obj x = (F.comp (G.comp H)).obj x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (F.comp G).comp H = F.comp (G.comp H)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (F.comp G).comp H = F.comp (G.comp H)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (F.comp G).comp H = F.comp (G.comp H)
have mapId : ((F.comp G).comp H).mapId ≍ (F.comp (G.comp H)).mapId
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ (F.comp G).comp H = F.comp (G.comp H)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: rw [heq_iff_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ @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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
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
⊢ ((F.comp G).comp H).mapId ≍ (F.comp (G.comp H)).mapId
have mapId : ((F.comp G).comp H).mapId = (F.comp (G.comp H)).mapId
Tactic: rw [heq_iff_eq]