awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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)
⊢ 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)
have 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)
Tactic: rw [← G.map₂_comp_assoc, mapComp_naturality_left, G.map₂_comp_assoc, mapComp_naturality_left,
      assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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
⊢ ∀ {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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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
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)
have rw : G.map₂ (F.map₂ (η ◁ η_1) ≫ 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)
Tactic: rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc,
      mapComp_naturality_right, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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
g g' : b ⟶ c
η_1 : g ⟶ g'
rw :
  G.map₂ (F.map₂ (η ◁ η_1) ≫ 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.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)
have rw₁ : G.map₂ (F.mapComp η g ≫ F.map η ◁ F.map₂ η_1) ≫ 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)
Tactic: rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc,
      mapComp_naturality_right, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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
g g' : b ⟶ c
η_1 : g ⟶ g'
rw :
  G.map₂ (F.map₂ (η ◁ η_1) ≫ 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)
rw₁ :
  G.map₂ (F.mapComp η g ≫ F.map η ◁ F.map₂ η_1) ≫ 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.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)
have rw₂ : G.map₂ (F.mapComp η g) ≫ G.map₂ (F.map η ◁ F.map₂ η_1) ≫ 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)
Tactic: rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc,
      mapComp_naturality_right, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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
g g' : b ⟶ c
η_1 : g ⟶ g'
rw :
  G.map₂ (F.map₂ (η ◁ η_1) ≫ 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)
rw₁ :
  G.map₂ (F.mapComp η g ≫ F.map η ◁ F.map₂ η_1) ≫ 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)
rw₂ :
  G.map₂ (F.mapComp η g) ≫ G.map₂ (F.map η ◁ F.map₂ η_1) ≫ 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.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)
have rw₃ : G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1) =
  (G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1)
Tactic: rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc,
      mapComp_naturality_right, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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
g g' : b ⟶ c
η_1 : g ⟶ g'
rw :
  G.map₂ (F.map₂ (η ◁ η_1) ≫ 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)
rw₁ :
  G.map₂ (F.mapComp η g ≫ F.map η ◁ F.map₂ η_1) ≫ 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)
rw₂ :
  G.map₂ (F.mapComp η g) ≫ G.map₂ (F.map η ◁ F.map₂ η_1) ≫ 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)
rw₃ :
  G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1) =
    (G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g)) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1)
⊢ 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)
have rw₄ : G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1) =
  G.map₂ (F.mapComp η g) ≫ G.mapComp (F.map η) (F.map g) ≫ G.map (F.map η) ◁ G.map₂ (F.map₂ η_1)
Tactic: rw [← G.map₂_comp_assoc, mapComp_naturality_right, G.map₂_comp_assoc,
      mapComp_naturality_right, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ Eq (α :=
    (F.comp G.toPrelaxFunctor).map ((f ≫ g) ≫ h) ⟶
      (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map g ≫ (F.comp G.toPrelaxFunctor).map h)
    ((F.comp G.toPrelaxFunctor).map₂ (α_ f g h).hom ≫
      CategoryStruct.comp (Y := (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map (g ≫ h))
        (Functor.map (G.mapFunctor (F.obj a) (F.obj d)) (F.mapComp f (g ≫ h)) ≫ G.mapComp (F.map f) (F.map (g ≫ h)) :
          (F.comp G.toPrelaxFunctor).map (f ≫ g ≫ h) ⟶
            (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map (g ≫ h))
        ((F.comp G.toPrelaxFunctor).map f ◁
            (Functor.map (G.mapFunctor (F.obj b) (F.obj d)) (F.mapComp g h) ≫ G.mapComp (F.map g) (F.map h)) :
          (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map (g ≫ h) ⟶
            (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map g ≫ (F.comp G.toPrelaxFunctor).map h))
    (CategoryStruct.comp (Y := (F.comp G.toPrelaxFunctor).map (f ≫ g) ≫ (F.comp G.toPrelaxFunctor).map h)
      (Functor.map (G.mapFunctor (F.obj a) (F.obj d)) (F.mapComp (f ≫ g) h) ≫ G.mapComp (F.map (f ≫ g)) (F.map h) :
        (F.comp G.toPrelaxFunctor).map ((f ≫ g) ≫ h) ⟶
          (F.comp G.toPrelaxFunctor).map (f ≫ g) ≫ (F.comp G.toPrelaxFunctor).map h)
      ((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 h ≫
          (α_ ((F.comp G.toPrelaxFunctor).map f) ((F.comp G.toPrelaxFunctor).map g)
              ((F.comp G.toPrelaxFunctor).map h)).hom :
        (F.comp G.toPrelaxFunctor).map (f ≫ g) ≫ (F.comp G.toPrelaxFunctor).map h ⟶
          (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map g ≫ (F.comp G.toPrelaxFunctor).map h))
have dsimp : G.map₂ (F.map₂ (α_ f g h).hom) ≫
    (G.map₂ (F.mapComp f (g ≫ h)) ≫ G.mapComp (F.map f) (F.map (g ≫ h))) ≫
      G.map (F.map f) ◁ (G.map₂ (F.mapComp g h) ≫ G.mapComp (F.map g) (F.map h)) =
  (G.map₂ (F.mapComp (f ≫ g) h) ≫ G.mapComp (F.map (f ≫ g)) (F.map h)) ≫
    (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ▷ G.map (F.map h) ≫
      (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ G.map₂ (F.map₂ (α_ f g h).hom) ≫
      (G.map₂ (F.mapComp f (g ≫ h)) ≫ G.mapComp (F.map f) (F.map (g ≫ h))) ≫
        G.map (F.map f) ◁ (G.map₂ (F.mapComp g h) ≫ G.mapComp (F.map g) (F.map h)) =
    (G.map₂ (F.mapComp (f ≫ g) h) ≫ G.mapComp (F.map (f ≫ g)) (F.map h)) ≫
      (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ▷ G.map (F.map h) ≫
        (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom
have simp : G.map₂ (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom) ≫
    G.mapComp (F.map f) (F.map g ≫ F.map h) ≫ G.map (F.map f) ◁ G.mapComp (F.map g) (F.map h) =
  G.map₂ (F.mapComp (f ≫ g) h) ≫
    G.mapComp (F.map (f ≫ g)) (F.map h) ≫
      (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ▷ G.map (F.map h) ≫
        (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom
Tactic: simp only [map₂_associator, ← PrelaxFunctor.map₂_comp_assoc, ← mapComp_naturality_right_assoc,
      whiskerLeft_comp, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
F_1 F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : OplaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b : B
f : a ⟶ b
⊢ (F.comp G.toPrelaxFunctor).map₂ (λ_ f).hom =
    CategoryStruct.comp (Y := (F.comp G.toPrelaxFunctor).map (𝟙 a) ≫ (F.comp G.toPrelaxFunctor).map f)
      (Functor.map (G.mapFunctor (F.obj a) (F.obj b)) (F.mapComp (𝟙 a) f) ≫ G.mapComp (F.map (𝟙 a)) (F.map f) :
        (F.comp G.toPrelaxFunctor).map (𝟙 a ≫ f) ⟶
          (F.comp G.toPrelaxFunctor).map (𝟙 a) ≫ (F.comp G.toPrelaxFunctor).map f)
      ((Functor.map (G.mapFunctor (F.obj a) (F.obj a)) (F.mapId a) ≫ G.mapId (F.obj a)) ▷
            (F.comp G.toPrelaxFunctor).map f ≫
          (λ_ ((F.comp G.toPrelaxFunctor).map f)).hom :
        (F.comp G.toPrelaxFunctor).map (𝟙 a) ≫ (F.comp G.toPrelaxFunctor).map f ⟶ (F.comp G.toPrelaxFunctor).map f)
have dsimp : G.map₂ (F.map₂ (λ_ f).hom) =
  (G.map₂ (F.mapComp (𝟙 a) f) ≫ G.mapComp (F.map (𝟙 a)) (F.map f)) ≫
    (G.map₂ (F.mapId a) ≫ G.mapId (F.obj a)) ▷ G.map (F.map f) ≫ (λ_ (G.map (F.map f))).hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Oplax (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
F_1 F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : OplaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b : B
f : a ⟶ b
⊢ (F.comp G.toPrelaxFunctor).map₂ (ρ_ f).hom =
    CategoryStruct.comp (Y := (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map (𝟙 b))
      (Functor.map (G.mapFunctor (F.obj a) (F.obj b)) (F.mapComp f (𝟙 b)) ≫ G.mapComp (F.map f) (F.map (𝟙 b)) :
        (F.comp G.toPrelaxFunctor).map (f ≫ 𝟙 b) ⟶
          (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map (𝟙 b))
      ((F.comp G.toPrelaxFunctor).map f ◁
            (Functor.map (G.mapFunctor (F.obj b) (F.obj b)) (F.mapId b) ≫ G.mapId (F.obj b)) ≫
          (ρ_ ((F.comp G.toPrelaxFunctor).map f)).hom :
        (F.comp G.toPrelaxFunctor).map f ≫ (F.comp G.toPrelaxFunctor).map (𝟙 b) ⟶ (F.comp G.toPrelaxFunctor).map f)
have dsimp : G.map₂ (F.map₂ (ρ_ f).hom) =
  (G.map₂ (F.mapComp f (𝟙 b)) ≫ G.mapComp (F.map f) (F.map (𝟙 b))) ≫
    G.map (F.map f) ◁ (G.map₂ (F.mapId b) ≫ G.mapId (F.obj b)) ≫ (ρ_ (G.map (F.map f))).hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst_2 : IsIso η
⊢ F.map₂ (inv η) = inv (F.map₂ η)
have hom_inv_id : F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f)
Tactic: apply IsIso.eq_inv_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f)
have rw : F.map₂ (η.hom ≫ η.inv) = 𝟙 (F.map f)
Tactic: rw [← F.map₂_comp, Iso.hom_inv_id, F.map₂_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f g : a ⟶ b
η : f ≅ g
rw : F.map₂ (η.hom ≫ η.inv) = 𝟙 (F.map f)
⊢ F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f)
have rw₁ : F.map₂ (𝟙 f) = 𝟙 (F.map f)
Tactic: rw [← F.map₂_comp, Iso.hom_inv_id, F.map₂_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f g : a ⟶ b
η : f ≅ g
rw : F.map₂ (η.hom ≫ η.inv) = 𝟙 (F.map f)
rw₁ : F.map₂ (𝟙 f) = 𝟙 (F.map f)
⊢ F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f)
have rw₂ : 𝟙 (F.map f) = 𝟙 (F.map f)
Tactic: rw [← F.map₂_comp, Iso.hom_inv_id, F.map₂_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)
have rw : F.map₂ (η.inv ≫ η.hom) = 𝟙 (F.map g)
Tactic: rw [← F.map₂_comp, Iso.inv_hom_id, F.map₂_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f g : a ⟶ b
η : f ≅ g
rw : F.map₂ (η.inv ≫ η.hom) = 𝟙 (F.map g)
⊢ F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)
have rw₁ : F.map₂ (𝟙 g) = 𝟙 (F.map g)
Tactic: rw [← F.map₂_comp, Iso.inv_hom_id, F.map₂_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f g : a ⟶ b
η : f ≅ g
rw : F.map₂ (η.inv ≫ η.hom) = 𝟙 (F.map g)
rw₁ : F.map₂ (𝟙 g) = 𝟙 (F.map g)
⊢ F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)
have rw₂ : 𝟙 (F.map g) = 𝟙 (F.map g)
Tactic: rw [← F.map₂_comp, Iso.inv_hom_id, F.map₂_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (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
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map f = F.map g
have rw : F.map f = F.map f
Tactic: rw [← hfg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map₂ (eqToHom hfg) = eqToHom ⋯
have subst : F.map₂ (eqToHom sorry) = eqToHom sorry
Tactic: subst hfg
Cleared hypotheses: g, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Prelax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map₂Iso (eqToIso hfg) = eqToIso ⋯
have subst : F.map₂Iso (eqToIso sorry) = eqToIso sorry
Tactic: subst hfg
Cleared hypotheses: g, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (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
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.map₂ (λ_ f).inv = (λ_ (F.map f)).inv ≫ (F.mapId a).inv ▷ F.map f ≫ (F.mapComp (𝟙 a) f).inv
have rw : (λ_ (F.map f)).hom = ((F.mapId a).inv ▷ F.map f ≫ (F.mapComp (𝟙 a) f).inv) ≫ (F.map₂Iso (λ_ f)).hom
Tactic: rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (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
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.map₂ (ρ_ f).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b).inv ≫ (F.mapComp f (𝟙 b)).inv
have rw : (ρ_ (F.map f)).hom = (F.map f ◁ (F.mapId b).inv ≫ (F.mapComp f (𝟙 b)).inv) ≫ (F.map₂Iso (ρ_ f)).hom
Tactic: rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (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
F_1 F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b_1 b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ f = 𝟙 b
have rw : Eq.{v₁ + 1} (α := b ⟶ b) (𝟙 b) (𝟙 b)
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (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
F_1 F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = f ≫ g
have rw : fg = fg
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (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
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
have rw : F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
Tactic: rw [F'.mapCompIso_hom f g, ← F.mapComp_naturality_right_assoc, ← F'.mapCompIso_hom f h,
      hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (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
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
rw : F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
have rw₁ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ F.mapComp f h ≫ (F'.mapCompIso f h).inv
Tactic: rw [F'.mapCompIso_hom f g, ← F.mapComp_naturality_right_assoc, ← F'.mapCompIso_hom f h,
      hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (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
F_1 : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
rw : F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
rw₁ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ F.mapComp f h ≫ (F'.mapCompIso f h).inv
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
have rw₂ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ (F'.mapCompIso f h).hom ≫ (F'.mapCompIso f h).inv
Tactic: rw [F'.mapCompIso_hom f g, ← F.mapComp_naturality_right_assoc, ← F'.mapCompIso_hom f h,
      hom_inv_id, comp_id]