awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₂ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ (F'.mapCompIso f h).hom ≫ (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.map (f ≫ h))
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
rw₂ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ (F'.mapCompIso f h).hom ≫ (F'.mapCompIso f h).inv
rw₃ : F.map₂ (f ◁ η) = F.map₂ (f ◁ η) ≫ 𝟙 (F.map (f ≫ 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.map₂ (f ◁ η)
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 g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
have rw : F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
Tactic: rw [F'.mapCompIso_hom _ h, ← F.mapComp_naturality_left_assoc, ← F'.mapCompIso_hom _ 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 g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
rw : F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
⊢ F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
have rw₁ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ F.mapComp g h ≫ (F'.mapCompIso g h).inv
Tactic: rw [F'.mapCompIso_hom _ h, ← F.mapComp_naturality_left_assoc, ← F'.mapCompIso_hom _ 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 g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
rw : F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
rw₁ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ F.mapComp g h ≫ (F'.mapCompIso g h).inv
⊢ F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
have rw₂ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ (F'.mapCompIso g h).hom ≫ (F'.mapCompIso g h).inv
Tactic: rw [F'.mapCompIso_hom _ h, ← F.mapComp_naturality_left_assoc, ← F'.mapCompIso_hom _ 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 g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
rw : F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
rw₁ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ F.mapComp g h ≫ (F'.mapCompIso g h).inv
rw₂ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ (F'.mapCompIso g h).hom ≫ (F'.mapCompIso g h).inv
⊢ F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
have rw₃ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ 𝟙 (F.map (g ≫ h))
Tactic: rw [F'.mapCompIso_hom _ h, ← F.mapComp_naturality_left_assoc, ← F'.mapCompIso_hom _ 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 g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
rw : F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
rw₁ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ F.mapComp g h ≫ (F'.mapCompIso g h).inv
rw₂ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ (F'.mapCompIso g h).hom ≫ (F'.mapCompIso g h).inv
rw₃ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ 𝟙 (F.map (g ≫ h))
⊢ F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g h).inv
have rw₄ : F.map₂ (η ▷ h) = F.map₂ (η ▷ h)
Tactic: rw [F'.mapCompIso_hom _ h, ← F.mapComp_naturality_left_assoc, ← F'.mapCompIso_hom _ 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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
have rw : F.map₂ (α_ f g h).hom =
  F.mapComp (f ≫ g) h ≫
    (F'.mapCompIso f g).hom ▷ F.map h ≫
      (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
Tactic: rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
have rw₁ : F.map₂ (α_ f g h).hom =
  F.mapComp (f ≫ g) h ≫
    F.mapComp f g ▷ F.map h ≫
      (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
Tactic: rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₁ :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
have rw₂ : F.map₂ (α_ f g h).hom =
  F.map₂ (α_ f g h).hom ≫
    F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
Tactic: rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₁ :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₂ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
have rw₃ : F.map₂ (α_ f g h).hom =
  F.map₂ (α_ f g h).hom ≫
    (F'.mapCompIso f (g ≫ h)).hom ≫
      F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
Tactic: rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₁ :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₂ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₃ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
have rw₄ : F.map₂ (α_ f g h).hom =
  F.map₂ (α_ f g h).hom ≫
    (F'.mapCompIso f (g ≫ h)).hom ≫
      F.map f ◁ (F'.mapCompIso g h).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
Tactic: rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₁ :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₂ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₃ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₄ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ (F'.mapCompIso g h).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
have rw₅ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom ≫ (F'.mapCompIso f (g ≫ h)).hom ≫ (F'.mapCompIso f (g ≫ h)).inv
Tactic: rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₁ :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₂ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₃ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₄ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ (F'.mapCompIso g h).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₅ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom ≫ (F'.mapCompIso f (g ≫ h)).hom ≫ (F'.mapCompIso f (g ≫ h)).inv
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
have rw₆ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom ≫ 𝟙 (F.map (f ≫ g ≫ h))
Tactic: rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
rw :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₁ :
  F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₂ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₃ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₄ :
  F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      (F'.mapCompIso f (g ≫ h)).hom ≫
        F.map f ◁ (F'.mapCompIso g h).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₅ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom ≫ (F'.mapCompIso f (g ≫ h)).hom ≫ (F'.mapCompIso f (g ≫ h)).inv
rw₆ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom ≫ 𝟙 (F.map (f ≫ g ≫ h))
⊢ F.map₂ (α_ f g h).hom =
    (F'.mapCompIso (f ≫ g) h).hom ≫
      (F'.mapCompIso f g).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
have rw₇ : F.map₂ (α_ f g h).hom = F.map₂ (α_ f g h).hom
Tactic: rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
      F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
      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
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = (asIso (F.mapComp f g)).hom ≫ F.map f ◁ F.map₂ η ≫ (asIso (F.mapComp f h)).inv
have dsimp : F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)
Tactic: dsimp
-- 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
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)
have rw : F.map₂ (f ◁ η) = (F.mapComp f g ≫ F.map f ◁ F.map₂ η) ≫ inv (F.mapComp f h)
Tactic: rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_right]
-- 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
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
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₂ η) ≫ inv (F.mapComp f h)
⊢ F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)
have rw₁ : F.map₂ (f ◁ η) ≫ F.mapComp f h = F.mapComp f g ≫ F.map f ◁ F.map₂ η
Tactic: rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_right]
-- 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
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
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₂ η) ≫ inv (F.mapComp f h)
rw₁ : F.map₂ (f ◁ η) ≫ F.mapComp f h = F.mapComp f g ≫ F.map f ◁ F.map₂ η
⊢ F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)
have rw₂ : F.mapComp f g ≫ F.map f ◁ F.map₂ η = F.mapComp f g ≫ F.map f ◁ F.map₂ η
Tactic: rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_right]
-- 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
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ F.map₂ (η ▷ h) = (asIso (F.mapComp f h)).hom ≫ F.map₂ η ▷ F.map h ≫ (asIso (F.mapComp g h)).inv
have dsimp : F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ inv (F.mapComp g h)
Tactic: dsimp
-- 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
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
⊢ F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ inv (F.mapComp g h)
have rw : F.map₂ (η ▷ h) = (F.mapComp f h ≫ F.map₂ η ▷ F.map h) ≫ inv (F.mapComp g h)
Tactic: rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_left]
-- 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
inst_3 : ∀ (a : B), IsIso (F.mapId a)
inst_4 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
rw : F.map₂ (η ▷ h) = (F.mapComp f h ≫ F.map₂ η ▷ F.map h) ≫ inv (F.mapComp g h)
⊢ F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ inv (F.mapComp g h)
have rw₁ : F.map₂ (η ▷ h) ≫ F.mapComp g h = F.mapComp f h ≫ F.map₂ η ▷ F.map h
Tactic: rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_left]