awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
rw :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
          F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
have rw₁ : F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
    F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
      (ρ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
  (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
Tactic: rw [Category.assoc, F.mapComp_id_right, F.map₂_inv_hom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
F : OplaxFunctor.{0, w, 0, v, 0, u} (LocallyDiscrete (Discrete Unit)) B
rw :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ≫
        F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
          F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
rw₁ :
  F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
      F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).hom ≫
        (ρ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })).inv ≫
        F.mapComp (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })
          (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) })) ≫
      F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }) ◁
        F.mapId { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) } =
    (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
have rw₂ : (ρ_ (F.map (𝟙 { as := { as := () : Discrete Unit } : LocallyDiscrete (Discrete Unit) }))).inv =
  (ρ_ (F.map (𝟙 { as := { as := () } }))).inv
Tactic: rw [Category.assoc, F.mapComp_id_right, F.map₂_inv_hom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 a : B
t : a ⟶ a
inst_1 : Comonad t
a_2 b c d : LocallyDiscrete (Discrete Unit)
x : a_2 ⟶ b
x_1 : b ⟶ c
x_2 : c ⟶ d
⊢ 𝟙 t ≫ Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom
have rw : Δ ≫ t ◁ Δ = Δ ≫ Δ ▷ t ≫ (α_ t t t).hom
Tactic: rw [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Monad.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a : B
t : a ⟶ a
inst_1 : Comonad t
⊢ Eq.{w + 1} (α := (mkOfComonad t).hom ⟶ (mkOfComonad t).hom ≫ (mkOfComonad t).hom) Δ Δ
have change : 𝟙 t ≫ Δ = Δ
Tactic: change 𝟙 t ≫ Δ = Δ
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ θ.naturality f ⊗≫ (η.naturality f ≫ F.map₂ β ▷ η.app b) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)
have rw : 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
    η.app a ◁ θ.naturality f ⊗≫ (η.app a ◁ G.map₂ β ≫ η.naturality g) ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
  𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
    η.app a ◁ (θ.naturality f ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b)
Tactic: rw [naturality_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
      η.app a ◁ (θ.naturality f ≫ G.map₂ β ▷ θ.app b) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
    η.vCompApp θ a ◁ H.map₂ β ≫ η.vCompNaturality θ g
have rw : 𝟙 ((η.app a ≫ θ.app a) ≫ H.map f) ⊗≫
    η.app a ◁ (θ.app a ◁ H.map₂ β ≫ θ.naturality g) ⊗≫ η.naturality g ▷ θ.app b ⊗≫ 𝟙 (F.map g ≫ η.vCompApp θ b) =
  η.vCompApp θ a ◁ H.map₂ β ≫ η.vCompNaturality θ g
Tactic: rw [naturality_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ θ.naturality (𝟙 a)) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)
have rw : 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
    η.app a ◁ ((ρ_ (θ.app a)).hom ≫ (λ_ (θ.app a)).inv ≫ G.mapId a ▷ θ.app a) ⊗≫
      η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
  𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
    (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)
Tactic: rw [naturality_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a
have rw : 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
    ((ρ_ (η.app a)).hom ≫ (λ_ (η.app a)).inv ≫ F.mapId a ▷ η.app a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
  (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a
Tactic: rw [naturality_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapComp f g ≫ θ.naturality (f ≫ g)) ⊗≫
        η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
have rw : 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
    η.app a ◁
        ((α_ (θ.app a) (H.map f) (H.map g)).inv ≫
          θ.naturality f ▷ H.map g ≫
            (α_ (G.map f) (θ.app b) (H.map g)).hom ≫
              G.map f ◁ θ.naturality g ≫ (α_ (G.map f) (G.map g) (θ.app c)).inv ≫ G.mapComp f g ▷ θ.app c) ⊗≫
      η.naturality (f ≫ g) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
  𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
    η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
      (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
Tactic: rw [naturality_comp θ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
have rw : 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
    η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
      ((α_ (η.app a) (G.map f) (G.map g)).inv ≫
            η.naturality f ▷ G.map g ≫
              (α_ (F.map f) (η.app b) (G.map g)).hom ≫
                F.map f ◁ η.naturality g ≫ (α_ (F.map f) (F.map g) (η.app c)).inv ≫ F.mapComp f g ▷ η.app c) ▷
          θ.app c ⊗≫
        𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
  𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
    η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
      ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
        F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
Tactic: rw [naturality_comp η]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
      η.vCompNaturality θ f ▷ H.map g ≫
        (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
          F.map f ◁ η.vCompNaturality θ g ≫
            (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv ≫ F.mapComp f g ▷ η.vCompApp θ c
have rw : 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
    η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
      (η.naturality f ▷ (θ.app b ≫ H.map g) ≫ (F.map f ≫ η.app b) ◁ θ.naturality g) ⊗≫
        F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
          F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
  (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
    η.vCompNaturality θ f ▷ H.map g ≫
      (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
        F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv ≫ F.mapComp f g ▷ η.vCompApp θ c
Tactic: rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
have rw : 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
    (η.naturality f ≫ η.app a ◁ G.map₂ β) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
  𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
    η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
Tactic: rw [η.naturality_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β
have rw : 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
    η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (θ.naturality f ≫ θ.app a ◁ H.map₂ β) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
  η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β
Tactic: rw [θ.naturality_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ F.map₂ β ▷ η.vCompApp θ b ≫ η.vCompNaturality θ g = η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β
have _ : F.map₂ β ▷ η.vCompApp θ b ≫ η.vCompNaturality θ g =
  𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
    (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫
          η.app a ◁ θ.naturality g ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫
          η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 _ := by
      rw [η.naturality_naturality]
      bicategory
    _ = _ := by
      rw [θ.naturality_naturality]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
_ :
  F.map₂ β ▷ η.vCompApp θ b ≫ η.vCompNaturality θ g =
    𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
⊢ F.map₂ β ▷ η.vCompApp θ b ≫ η.vCompNaturality θ g = η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β
have _₁ : 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
    (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
  𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
    η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫
          η.app a ◁ θ.naturality g ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫
          η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 _ := by
      rw [η.naturality_naturality]
      bicategory
    _ = _ := by
      rw [θ.naturality_naturality]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
_ :
  F.map₂ β ▷ η.vCompApp θ b ≫ η.vCompNaturality θ g =
    𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
_₁ :
  𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫ η.app a ◁ θ.naturality g ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g)
⊢ F.map₂ β ▷ η.vCompApp θ b ≫ η.vCompNaturality θ g = η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β
have _₂ : 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
    η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
  η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.map₂ β ▷ η.app b ≫ η.naturality g) ▷ θ.app b ⊗≫
          η.app a ◁ θ.naturality g ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫
          η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 _ := by
      rw [η.naturality_naturality]
      bicategory
    _ = _ := by
      rw [θ.naturality_naturality]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
        η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
have rw : 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
    ((λ_ (η.app a)).hom ≫ (ρ_ (η.app a)).inv ≫ η.app a ◁ G.mapId a) ▷ θ.app a ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
  𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
    η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
Tactic: rw [η.naturality_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a
have rw : 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
    η.app a ◁ ((λ_ (θ.app a)).hom ≫ (ρ_ (θ.app a)).inv ≫ θ.app a ◁ H.mapId a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
  (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a
Tactic: rw [θ.naturality_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
⊢ F.mapId a ▷ η.vCompApp θ a ≫ η.vCompNaturality θ (𝟙 a) =
    (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a
have _ : F.mapId a ▷ η.vCompApp θ a ≫ η.vCompNaturality θ (𝟙 a) =
  𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
    (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
          η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_id]
      bicategory
    _ = _ := by
      rw [θ.naturality_id]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
_ :
  F.mapId a ▷ η.vCompApp θ a ≫ η.vCompNaturality θ (𝟙 a) =
    𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
        η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
⊢ F.mapId a ▷ η.vCompApp θ a ≫ η.vCompNaturality θ (𝟙 a) =
    (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a
have _₁ : 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
    (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
      η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
  𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
    η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
          η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_id]
      bicategory
    _ = _ := by
      rw [θ.naturality_id]
      bicategory
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G H : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
η : OplaxTrans F G
θ : OplaxTrans G H
a : B
_ :
  F.mapId a ▷ η.vCompApp θ a ≫ η.vCompNaturality θ (𝟙 a) =
    𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
        η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
_₁ :
  𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
        η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
    𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
      η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a))
⊢ F.mapId a ▷ η.vCompApp θ a ≫ η.vCompNaturality θ (𝟙 a) =
    (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a
have _₂ : 𝟙 (𝟙 (F.obj a) ≫ η.vCompApp θ a) ⊗≫
    η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map (𝟙 a)) =
  (λ_ (η.vCompApp θ a)).hom ≫ (ρ_ (η.vCompApp θ a)).inv ≫ η.vCompApp θ a ◁ H.mapId a
Tactic: calc
    _ = 𝟙 _ ⊗≫ (F.mapId a ▷ η.app a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫
          η.app a ◁ θ.naturality (𝟙 a) ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (G.mapId a ▷ θ.app a ≫ θ.naturality (𝟙 a)) ⊗≫ 𝟙 _ := by
      rw [η.naturality_id]
      bicategory
    _ = _ := by
      rw [θ.naturality_id]
      bicategory