awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F G : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
α : F ⟶ G
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ α.naturality (f ≫ g) =
    F.mapComp f g ▷ᵢ α.app c ≪≫
      α_ (F.map f) (F.map g) (α.app c) ≪≫
        F.map f ◁ᵢ α.naturality g ≪≫
          (α_ (F.map f) (α.app b) (G.map g)).symm ≪≫
            α.naturality f ▷ᵢ G.map g ≪≫ α_ (α.app a) (G.map f) (G.map g) ≪≫ α.app a ◁ᵢ (G.mapComp f g).symm
have w : (α.naturality (f ≫ g)).hom =
  (F.mapComp f g ▷ᵢ α.app c ≪≫
      α_ (F.map f) (F.map g) (α.app c) ≪≫
        F.map f ◁ᵢ α.naturality g ≪≫
          (α_ (F.map f) (α.app b) (G.map g)).symm ≪≫
            α.naturality f ▷ᵢ G.map g ≪≫ α_ (α.app a) (G.map f) (G.map g) ≪≫ α.app a ◁ᵢ (G.mapComp f g).symm).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g = h
⊢ f ◁ eqToHom η = eqToHom ⋯
have refl : f ◁ eqToHom sorry = eqToHom sorry
Tactic: cases η
Cleared hypotheses: h, η
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Basic (goal)
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f = g
h : b ⟶ c
⊢ eqToHom η ▷ h = eqToHom ⋯
have refl : eqToHom sorry ▷ h = eqToHom sorry
Tactic: cases η
Cleared hypotheses: g, η
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.mapComp' f (𝟙 b₁) f ⋯ = (ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm
have w : (F.mapComp' f (𝟙 b₁) f sorry).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.map₂Iso (eqToIso ⋯) ≪≫ F.mapComp f (𝟙 b₁)).hom = ((ρ_ (F.map f)).symm ≪≫ F.map f ◁ᵢ (F.mapId b₁).symm).hom
have w : F.map₂ (eqToHom sorry) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
have w : F.map₂ (eqToHom sorry) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
  (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
have w₁ : F.map₂ (eqToHom sorry) ≫ F.map₂ (Iso.hom (eqToIso sorry)) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
  (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
have w₂ : F.map₂ (eqToHom sorry) ≫ F.map₂ (eqToHom sorry) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
  (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
have w₃ : F.map₂ (eqToHom sorry ≫ eqToHom sorry) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
  (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
have w₄ : F.map₂ (eqToHom sorry) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₄ :
  F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
have w₅ : F.map₂ (𝟙 f) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₄ :
  F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₅ : F.map₂ (𝟙 f) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
have w₆ : 𝟙 (F.map f) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv =
    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₄ :
  F.map₂ (eqToHom ⋯) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₅ : F.map₂ (𝟙 f) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
w₆ : 𝟙 (F.map f) ≫ (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp f (𝟙 b₁)).hom = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
have w₇ : (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b₁).inv
Tactic: rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.mapComp' (𝟙 b₀) f f ⋯ = (λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f
have w : (F.mapComp' (𝟙 b₀) f f sorry).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ (F.map₂Iso (eqToIso ⋯) ≪≫ F.mapComp (𝟙 b₀) f).hom = ((λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f).hom
have w : F.map₂ (eqToHom sorry) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
have w : F.map₂ (eqToHom sorry) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
  (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
have w₁ : F.map₂ (eqToHom sorry) ≫ F.map₂ (Iso.hom (eqToIso sorry)) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
  (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
have w₂ : F.map₂ (eqToHom sorry) ≫ F.map₂ (eqToHom sorry) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
  (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
have w₃ : F.map₂ (eqToHom sorry ≫ eqToHom sorry) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
  (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
have w₄ : F.map₂ (eqToHom sorry) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₄ :
  F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
have w₅ : F.map₂ (𝟙 f) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₄ :
  F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₅ : F.map₂ (𝟙 f) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
have w₆ : 𝟙 (F.map f) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ : B
f : b₀ ⟶ b₁
w :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₁ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (Iso.hom (eqToIso ⋯)) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₂ :
  F.map₂ (eqToHom ⋯) ≫ F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₃ :
  F.map₂ (eqToHom ⋯ ≫ eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f =
    (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₄ :
  F.map₂ (eqToHom ⋯) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₅ : F.map₂ (𝟙 f) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
w₆ : 𝟙 (F.map f) ≫ (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
⊢ F.map₂ (eqToHom ⋯) ≫ (F.mapComp (𝟙 b₀) f).hom = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
have w₇ : (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f = (λ_ (F.map f)).inv ≫ (F.mapId b₀).inv ▷ F.map f
Tactic: rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor (goal)
Goal:
B : Type u₁
C : Type u₂
inst : Bicategory.{w₁, v₁, u₁} B
inst_1 : Strict.{w₁, v₁, u₁} B
inst_2 : Bicategory.{w₂, v₂, u₂} C
F : Pseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
have subst : (F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) sorry).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) sorry).hom =
  (F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) sorry).hom ≫
    (F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) sorry).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
Tactic: subst h₀₂ h₁₃ hf
Cleared hypotheses: f₀₂, f₁₃, f, h₀₂, h₁₃, hf