awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F_1 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : LaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫
      (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) =
    (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom ≫
      G.map (F.map f) ◁ (G.mapComp (F.map g) (F.map h) ≫ G.map₂ (F.mapComp g h)) ≫
        G.mapComp (F.map f) (F.map (g ≫ h)) ≫ G.map₂ (F.mapComp f (g ≫ h))
have slice_rhs : (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫
    (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) =
  (G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
      G.mapComp (F.map f ≫ F.map g) (F.map h) ≫
        G.map₂ (α_ (F.map f) (F.map g) (F.map h)).hom ≫ G.map₂ (F.map f ◁ F.mapComp g h)) ≫
    G.map₂ (F.mapComp f (g ≫ h))
Tactic: slice_rhs 1 3 =>
      rw [Bicategory.whiskerLeft_comp, assoc, ← mapComp_naturality_right, ← map₂_associator_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F_1 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : LaxFunctor.{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) (F.map g) (F.map h)).hom ≫ G.map₂ (F.map f ◁ F.mapComp g h) ≫ G.map₂ (F.mapComp f (g ≫ h))
have a : G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h) ≫ G.map₂ (F.map₂ (α_ f g h).hom)
Tactic: rw [← G.map₂_comp, ← G.map₂_comp, ← F.map₂_associator, G.map₂_comp, G.map₂_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F_1 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : LaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫
      (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) =
    (G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
        G.mapComp (F.map f ≫ F.map g) (F.map h) ≫
          G.map₂ (α_ (F.map f) (F.map g) (F.map h)).hom ≫ G.map₂ (F.map f ◁ F.mapComp g h)) ≫
      G.map₂ (F.mapComp f (g ≫ h))
have slice_rhs : (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫
    (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) =
  G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
    G.mapComp (F.map f ≫ F.map g) (F.map h) ≫
      G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h) ≫ G.map₂ (F.map₂ (α_ f g h).hom)
Tactic: slice_rhs 3 5 =>
      rw [← G.map₂_comp, ← G.map₂_comp, ← F.map₂_associator, G.map₂_comp, G.map₂_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F_1 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : LaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
| (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫
    G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)
have a : G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
  G.mapComp (F.map f ≫ F.map g) (F.map h) ≫ G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)
Tactic: rw [comp_whiskerRight, assoc, ← G.mapComp_naturality_left_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F_1 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : LaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫
      (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) =
    G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
      G.mapComp (F.map f ≫ F.map g) (F.map h) ≫
        G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h) ≫ G.map₂ (F.map₂ (α_ f g h).hom)
have slice_lhs : (G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
      G.mapComp (F.map f ≫ F.map g) (F.map h) ≫ G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫
    G.map₂ (F.map₂ (α_ f g h).hom) =
  G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
    G.mapComp (F.map f ≫ F.map g) (F.map h) ≫
      G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h) ≫ G.map₂ (F.map₂ (α_ f g h).hom)
Tactic: slice_lhs 1 3 =>
      rw [comp_whiskerRight, assoc, ← G.mapComp_naturality_left_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F_1 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : LaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b : B
f : a ⟶ b
⊢ (F.comp G.toPrelaxFunctor).map₂ (λ_ f).inv =
    (λ_ ((F.comp G.toPrelaxFunctor).map f)).inv ≫
      (G.mapId (F.obj a) ≫ G.map₂ (F.mapId a)) ▷ (F.comp G.toPrelaxFunctor).map f ≫
        G.mapComp (F.map (𝟙 a)) (F.map f) ≫ G.map₂ (F.mapComp (𝟙 a) f)
have dsimp : G.map₂ (F.map₂ (λ_ f).inv) =
  (λ_ (G.map (F.map f))).inv ≫
    (G.mapId (F.obj a) ≫ G.map₂ (F.mapId a)) ▷ G.map (F.map f) ≫
      G.mapComp (F.map (𝟙 a)) (F.map f) ≫ G.map₂ (F.mapComp (𝟙 a) f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F_1 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : LaxFunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b : B
f : a ⟶ b
⊢ (F.comp G.toPrelaxFunctor).map₂ (ρ_ f).inv =
    (ρ_ ((F.comp G.toPrelaxFunctor).map f)).inv ≫
      (F.comp G.toPrelaxFunctor).map f ◁ (G.mapId (F.obj b) ≫ G.map₂ (F.mapId b)) ≫
        G.mapComp (F.map f) (F.map (𝟙 b)) ≫ G.map₂ (F.mapComp f (𝟙 b))
have dsimp : G.map₂ (F.map₂ (ρ_ f).inv) =
  (ρ_ (G.map (F.map f))).inv ≫
    G.map (F.map f) ◁ (G.mapId (F.obj b) ≫ G.map₂ (F.mapId b)) ≫
      G.mapComp (F.map f) (F.map (𝟙 b)) ≫ G.map₂ (F.mapComp f (𝟙 b))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete (goal)
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (mapComp (f ≫ g) h).hom ≫
        (mapComp f g).hom ▷ map h ≫
          (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
      eqToHom ⋯
map₂_left_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b : B
f g : a ⟶ b
φ : f ⟶ g
⊢ map f = map g
have obtain : ∀ (φ : f ⟶ f), map f = map f
Tactic: obtain rfl := obj_ext_of_isDiscrete φ
Cleared hypotheses: g, φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete (goal)
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (mapComp (f ≫ g) h).hom ≫
        (mapComp f g).hom ▷ map h ≫
          (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
      eqToHom ⋯
map₂_left_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b c : B
x : a ⟶ b
x_1 x_2 : b ⟶ c
η : x_1 ⟶ x_2
⊢ eqToHom ⋯ = (mapComp x x_1).hom ≫ map x ◁ eqToHom ⋯ ≫ (mapComp x x_2).inv
have obtain : ∀ (η : x_1 ⟶ x_1), eqToHom sorry = (mapComp x x_1).hom ≫ map x ◁ eqToHom sorry ≫ (mapComp x x_1).inv
Tactic: obtain rfl := obj_ext_of_isDiscrete η
Cleared hypotheses: x_2, η
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete (goal)
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (mapComp (f ≫ g) h).hom ≫
        (mapComp f g).hom ▷ map h ≫
          (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
      eqToHom ⋯
map₂_left_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b c : B
f g : a ⟶ b
η : f ⟶ g
x : b ⟶ c
⊢ eqToHom ⋯ = (mapComp f x).hom ≫ eqToHom ⋯ ▷ map x ≫ (mapComp g x).inv
have obtain : ∀ (η : f ⟶ f), eqToHom sorry = (mapComp f x).hom ≫ eqToHom sorry ▷ map x ≫ (mapComp f x).inv
Tactic: obtain rfl := obj_ext_of_isDiscrete η
Cleared hypotheses: g, η
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete (goal)
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b : B
f g : a ⟶ b
φ : f ⟶ g
⊢ map f = map g
have obtain : ∀ (φ : f ⟶ f), map f = map f
Tactic: obtain rfl := obj_ext_of_isDiscrete φ
Cleared hypotheses: g, φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete (goal)
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b c : B
f f' : a ⟶ b
η : f ⟶ f'
⊢ ∀ (g : b ⟶ c), eqToHom ⋯ ≫ mapComp f' g = mapComp f g ≫ eqToHom ⋯ ▷ map g
have obtain : ∀ (η : f ⟶ f) (g : b ⟶ c), eqToHom sorry ≫ mapComp f g = mapComp f g ≫ eqToHom sorry ▷ map g
Tactic: obtain rfl := obj_ext_of_isDiscrete η
Cleared hypotheses: f', η
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete (goal)
Goal:
B : Type u_1
C : Type u_2
inst : Bicategory.{u_3, u_4, u_1} B
inst_1 : IsLocallyDiscrete.{u_1, u_3, u_4} B
inst_2 : Bicategory.{u_5, u_6, u_2} C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a b c : B
x : a ⟶ b
x_1 x_2 : b ⟶ c
η : x_1 ⟶ x_2
⊢ eqToHom ⋯ ≫ mapComp x x_2 = mapComp x x_1 ≫ map x ◁ eqToHom ⋯
have obtain : ∀ (η : x_1 ⟶ x_1), eqToHom sorry ≫ mapComp x x_1 = mapComp x x_1 ≫ map x ◁ eqToHom sorry
Tactic: obtain rfl := obj_ext_of_isDiscrete η
Cleared hypotheses: x_2, η
-- 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
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
    F.map₂ (α_ f g h).inv ≫ F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom
have rw : F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h =
  F.map₂ ((α_ f g h).inv ≫ (α_ f g h).hom) ≫ F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h
Tactic: rw [← F.map₂_associator, ← F.map₂_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
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f = F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv
have rw : (F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f) ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom
Tactic: rw [Iso.eq_comp_inv]
-- 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
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ (F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f) ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom
have simp : F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom
Tactic: simp only [Category.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
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.mapComp (𝟙 a) f ≫ F.mapId a ▷ F.map f ≫ (λ_ (F.map f)).hom = F.map₂ (λ_ f).hom
have rw : F.map₂ (λ_ f).hom = F.map₂ (λ_ f).hom
Tactic: rw [← F.map₂_leftUnitor]
-- 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
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b = F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv
have rw : (F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b) ≫ (ρ_ (F.map f)).hom = F.map₂ (ρ_ f).hom
Tactic: rw [Iso.eq_comp_inv]
-- 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
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ (F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b) ≫ (ρ_ (F.map f)).hom = F.map₂ (ρ_ f).hom
have simp : F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b ≫ (ρ_ (F.map f)).hom = F.map₂ (ρ_ f).hom
Tactic: simp only [Category.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
F : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b ≫ (ρ_ (F.map f)).hom = F.map₂ (ρ_ f).hom
have rw : F.map₂ (ρ_ f).hom = F.map₂ (ρ_ f).hom
Tactic: rw [← F.map₂_rightUnitor]
-- 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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
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.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 : OplaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = f ≫ g
have rw : fg = fg
Tactic: rw [h]
-- 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
⊢ Eq (α :=
    (F.comp G.toPrelaxFunctor).map (f ≫ g) ⟶ (F.comp G.toPrelaxFunctor).map f' ≫ (F.comp G.toPrelaxFunctor).map g)
    ((F.comp G.toPrelaxFunctor).map₂ (η ▷ g) ≫
      Functor.map (G.mapFunctor (F.obj a) (F.obj c)) (F.mapComp f' g) ≫ G.mapComp (F.map f') (F.map g))
    ((Functor.map (G.mapFunctor (F.obj a) (F.obj c)) (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫
      (F.comp G.toPrelaxFunctor).map₂ η ▷ (F.comp G.toPrelaxFunctor).map g)
have dsimp : G.map₂ (F.map₂ (η ▷ g)) ≫ G.map₂ (F.mapComp f' g) ≫ G.mapComp (F.map f') (F.map g) =
  (G.map₂ (F.mapComp f g) ≫ G.mapComp (F.map f) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)
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
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
⊢ 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.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)
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
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)
⊢ 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 ≫ 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)
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
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)
⊢ 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.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)
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
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)
⊢ 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]