awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b : FreeBicategory B
f g h : a ⟶ b
θ : g ⟶ h
a_1 : Hom₂ f g
f₁ :
  ∀ (a_2 : Hom₂ g h),
    Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1 ≫ Quot.mk Rel a_2) =
      Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1) ≫ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_2)
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1 ≫ θ) =
    Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1) ≫ Quot.lift (r := Rel) (liftHom₂ F) ⋯ θ
have f₂ : ∀ (a_2 b_1 : Hom₂ g h) (p : Rel a_2 b_1),
  Eq (α :=
    Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1 ≫ Quot.mk Rel b_1) =
      Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1) ≫ Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel b_1))
    sorry sorry
Tactic: induction θ using Quot.rec
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (f ◁ η) =
    Iso.hom (Iso.refl (liftHom F (f ≫ g))) ≫
      liftHom F f ◁ Quot.lift (r := Rel) (liftHom₂ F) ⋯ η ≫ Iso.inv (Iso.refl (liftHom F (f ≫ h)))
have f₁ : ∀ (a_1 : Hom₂ g h),
  Quot.lift (r := Rel) (liftHom₂ F) sorry (f ◁ Quot.mk Rel a_1) =
    Iso.hom (Iso.refl (liftHom F (f ≫ g))) ≫
      liftHom F f ◁ Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1) ≫ Iso.inv (Iso.refl (liftHom F (f ≫ h)))
Tactic: induction η using Quot.rec
Cleared hypotheses: η
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
f₁ :
  ∀ (a_1 : Hom₂ g h),
    Quot.lift (r := Rel) (liftHom₂ F) ⋯ (f ◁ Quot.mk Rel a_1) =
      Iso.hom (Iso.refl (liftHom F (f ≫ g))) ≫
        liftHom F f ◁ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1) ≫ Iso.inv (Iso.refl (liftHom F (f ≫ h)))
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (f ◁ η) =
    Iso.hom (Iso.refl (liftHom F (f ≫ g))) ≫
      liftHom F f ◁ Quot.lift (r := Rel) (liftHom₂ F) ⋯ η ≫ Iso.inv (Iso.refl (liftHom F (f ≫ h)))
have h₁ : ∀ (a_1 b_1 : Hom₂ g h) (p : Rel a_1 b_1), sorry = sorry
Tactic: induction η using Quot.rec
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b c : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (η ▷ h) =
    Iso.hom (Iso.refl (liftHom F (f ≫ h))) ≫
      Quot.lift (r := Rel) (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ Iso.inv (Iso.refl (liftHom F (g ≫ h)))
have dsimp : Quot.lift (r := Rel) (liftHom₂ F) sorry (η ▷ h) =
  𝟙 (liftHom F f ≫ liftHom F h) ≫ Quot.lift (r := Rel) (liftHom₂ F) sorry η ▷ liftHom F h ≫ 𝟙 (liftHom F g ≫ liftHom F h)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b c : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (η ▷ h) =
    𝟙 (liftHom F f ≫ liftHom F h) ≫ Quot.lift (r := Rel) (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ 𝟙 (liftHom F g ≫ liftHom F h)
have f : ∀ (a_1 : Hom₂ f g),
  Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1 ▷ h) =
    𝟙 (liftHom F f ≫ liftHom F h) ≫
      Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel a_1) ▷ liftHom F h ≫ 𝟙 (liftHom F g ≫ liftHom F h)
Tactic: induction η using Quot.rec
Cleared hypotheses: η
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Free (goal)
Goal:
B : Type u₁
inst : Quiver.{v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : Prefunctor.{v₁, v₂, u₁, u₂} B C
a b c : FreeBicategory B
f_1 g : a ⟶ b
η : f_1 ⟶ g
h : b ⟶ c
f :
  ∀ (a_1 : Hom₂ f_1 g),
    Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1 ▷ h) =
      𝟙 (liftHom F f_1 ≫ liftHom F h) ≫
        Quot.lift (r := Rel) (liftHom₂ F) ⋯ (Quot.mk Rel a_1) ▷ liftHom F h ≫ 𝟙 (liftHom F g ≫ liftHom F h)
⊢ Quot.lift (r := Rel) (liftHom₂ F) ⋯ (η ▷ h) =
    𝟙 (liftHom F f_1 ≫ liftHom F h) ≫
      Quot.lift (r := Rel) (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ 𝟙 (liftHom F g ≫ liftHom F h)
have h₁ : ∀ (a_1 b_1 : Hom₂ f_1 g) (p : Rel a_1 b_1),
  Eq (α :=
    Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel b_1 ▷ h) =
      𝟙 (liftHom F f_1 ≫ liftHom F h) ≫
        Quot.lift (r := Rel) (liftHom₂ F) sorry (Quot.mk Rel b_1) ▷ liftHom F h ≫ 𝟙 (liftHom F g ≫ liftHom F h))
    sorry sorry
Tactic: induction η using Quot.rec
-- 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 : LaxFunctor.{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 ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) ≫ F.map₂ (α_ f g h).inv
have rw : F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
  F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ ((α_ f g h).hom ≫ (α_ f g h).inv)
Tactic: rw [← F.map₂_associator_assoc, ← F.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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ (λ_ (F.map f)).hom = F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f ≫ F.map₂ (λ_ f).hom
have rw : (F.map₂Iso (λ_ f)).inv = (λ_ (F.map f)).inv ≫ F.mapId a ▷ F.map f ≫ F.mapComp (𝟙 a) f
Tactic: rw [← PrelaxFunctor.map₂Iso_hom, ← assoc, ← Iso.comp_inv_eq, ← Iso.eq_inv_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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
a b : B
f : a ⟶ b
⊢ (ρ_ (F.map f)).hom = F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b) ≫ F.map₂ (ρ_ f).hom
have rw : (F.map₂Iso (ρ_ f)).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ F.mapId b ≫ F.mapComp f (𝟙 b)
Tactic: rw [← PrelaxFunctor.map₂Iso_hom, ← assoc, ← Iso.comp_inv_eq, ← Iso.eq_inv_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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b : B
f : b ⟶ b
hf : f = 𝟙 b
⊢ 𝟙 b = f
have rw : Eq.{v₁ + 1} (α := b ⟶ b) (𝟙 b) (𝟙 b)
Tactic: rw [hf]
-- 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 : LaxFunctor.{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
⊢ f ≫ g = fg
have rw : fg = fg
Tactic: rw [h]
-- 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 : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
⊢ (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ≫ (F.comp G.toPrelaxFunctor).map₂ (η ▷ g) =
    (F.comp G.toPrelaxFunctor).map₂ η ▷ (F.comp G.toPrelaxFunctor).map g ≫
      G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
have dsimp : (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ≫ G.map₂ (F.map₂ (η ▷ g)) =
  G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
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 c : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
⊢ (G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
have rw : G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g) ≫ G.map₂ (F.map₂ (η ▷ g)) =
  G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_left, G.map₂_comp, 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 : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
rw :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.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.mapComp f g)) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
have rw₁ : G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g ≫ F.map₂ (η ▷ g)) =
  G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_left, G.map₂_comp, 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 : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
rw :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
rw₁ :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g ≫ F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.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.mapComp f g)) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
have rw₂ : G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.map₂ η ▷ F.map g ≫ F.mapComp f' g) =
  G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_left, G.map₂_comp, 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 : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
rw :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
rw₁ :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g ≫ F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
rw₂ :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.map₂ η ▷ F.map g ≫ F.mapComp f' g) =
    G.map₂ (F.map₂ η) ▷ G.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.mapComp f g)) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
have rw₃ : G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.map₂ η ▷ F.map g) ≫ G.map₂ (F.mapComp f' g) =
  G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_left, G.map₂_comp, 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 : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
rw :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
rw₁ :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g ≫ F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
rw₂ :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.map₂ η ▷ F.map g ≫ F.mapComp f' g) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
rw₃ :
  G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.map₂ η ▷ F.map g) ≫ G.map₂ (F.mapComp f' g) =
    G.map₂ (F.map₂ η) ▷ G.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.mapComp f g)) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
have rw₄ : G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g) =
  G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f') (F.map g) ≫ G.map₂ (F.mapComp f' g)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_left, G.map₂_comp, 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 : B
f : a ⟶ b
x x_1 : b ⟶ c
η : x ⟶ x_1
⊢ (G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x)) ≫ (F.comp G.toPrelaxFunctor).map₂ (f ◁ η) =
    (F.comp G.toPrelaxFunctor).map f ◁ (F.comp G.toPrelaxFunctor).map₂ η ≫
      G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
have dsimp : (G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x)) ≫ G.map₂ (F.map₂ (f ◁ η)) =
  G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
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 c : B
f : a ⟶ b
x x_1 : b ⟶ c
η : x ⟶ x_1
⊢ (G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x)) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
have rw : G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x) ≫ G.map₂ (F.map₂ (f ◁ η)) =
  G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_right, G.map₂_comp, mapComp_naturality_right_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 : B
f : a ⟶ b
x x_1 : b ⟶ c
η : x ⟶ x_1
rw :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
⊢ (G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x)) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
have rw₁ : G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x ≫ F.map₂ (f ◁ η)) =
  G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_right, G.map₂_comp, mapComp_naturality_right_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 : B
f : a ⟶ b
x x_1 : b ⟶ c
η : x ⟶ x_1
rw :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
rw₁ :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x ≫ F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
⊢ (G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x)) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
have rw₂ : G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.map f ◁ F.map₂ η ≫ F.mapComp f x_1) =
  G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_right, G.map₂_comp, mapComp_naturality_right_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 : B
f : a ⟶ b
x x_1 : b ⟶ c
η : x ⟶ x_1
rw :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
rw₁ :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x ≫ F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
rw₂ :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.map f ◁ F.map₂ η ≫ F.mapComp f x_1) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
⊢ (G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x)) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
have rw₃ : G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.map f ◁ F.map₂ η) ≫ G.map₂ (F.mapComp f x_1) =
  G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_right, G.map₂_comp, mapComp_naturality_right_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 : B
f : a ⟶ b
x x_1 : b ⟶ c
η : x ⟶ x_1
rw :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
rw₁ :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x ≫ F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
rw₂ :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.map f ◁ F.map₂ η ≫ F.mapComp f x_1) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
rw₃ :
  G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.map f ◁ F.map₂ η) ≫ G.map₂ (F.mapComp f x_1) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
⊢ (G.mapComp (F.map f) (F.map x) ≫ G.map₂ (F.mapComp f x)) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
have rw₄ : G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1) =
  G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x_1) ≫ G.map₂ (F.mapComp f x_1)
Tactic: rw [assoc, ← G.map₂_comp, mapComp_naturality_right, G.map₂_comp, mapComp_naturality_right_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)) ▷ (F.comp G.toPrelaxFunctor).map h ≫
      (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫
        (F.comp G.toPrelaxFunctor).map₂ (α_ f g h).hom =
    (α_ ((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.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 dsimp : (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))
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 c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
| (α_ (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))
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.map f) (F.map g) (F.map h)).hom ≫ G.map₂ (F.map f ◁ F.mapComp g h)
Tactic: rw [Bicategory.whiskerLeft_comp, assoc, ← mapComp_naturality_right, ← map₂_associator_assoc]