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
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)
rw₁ : F.map₂ (η ▷ h) ≫ F.mapComp g h = F.mapComp f h ≫ F.map₂ η ▷ F.map h
⊢ F.map₂ (η ▷ h) = F.mapComp f h ≫ F.map₂ η ▷ F.map h ≫ inv (F.mapComp g h)
have rw₂ : F.mapComp f h ≫ F.map₂ η ▷ F.map h = F.mapComp f h ≫ F.map₂ η ▷ F.map 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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.map₂ (α_ f g h).hom =
    (asIso (F.mapComp (f ≫ g) h)).hom ≫
      (asIso (F.mapComp f g)).hom ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫
          F.map f ◁ (asIso (F.mapComp g h)).inv ≫ (asIso (F.mapComp f (g ≫ h))).inv
have dsimp : 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 ◁ inv (F.mapComp g h) ≫ inv (F.mapComp f (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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ 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 ◁ inv (F.mapComp g h) ≫ inv (F.mapComp f (g ≫ h))
have simp : 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 ◁ inv (F.mapComp g h)) ≫
    inv (F.mapComp f (g ≫ h))
Tactic: simp only [← assoc]
-- 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 d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ 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 ◁ inv (F.mapComp g h)) ≫
      inv (F.mapComp f (g ≫ h))
have rw : (F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h)) ≫ F.map f ◁ F.mapComp g h =
  (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom
Tactic: rw [IsIso.eq_comp_inv, ← Bicategory.inv_whiskerLeft, IsIso.eq_comp_inv]
-- 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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ 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'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ F.mapComp f h
Tactic: rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_right, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]
-- 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 : LaxFunctor.{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'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ F.mapComp 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'.mapCompIso f g).hom ≫ F.mapComp f g ≫ F.map₂ (f ◁ η)
Tactic: rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_right, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]
-- 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 : LaxFunctor.{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'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ F.mapComp f h
rw₁ : F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.mapComp f g ≫ F.map₂ (f ◁ η)
⊢ F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ (F'.mapCompIso f h).inv
have rw₂ : F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ (F'.mapCompIso f g).inv ≫ F.map₂ (f ◁ η)
Tactic: rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_right, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]
-- 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 : LaxFunctor.{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'.mapCompIso f g).hom ≫ F.map f ◁ F.map₂ η ≫ F.mapComp f h
rw₁ : F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ F.mapComp f g ≫ F.map₂ (f ◁ η)
rw₂ : F.map₂ (f ◁ η) = (F'.mapCompIso f g).hom ≫ (F'.mapCompIso f g).inv ≫ F.map₂ (f ◁ η)
⊢ 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_inv, ← LaxFunctor.mapComp_naturality_right, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]
-- 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 : LaxFunctor.{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'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ F.mapComp g h
Tactic: rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_left, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]
-- 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 : LaxFunctor.{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'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ F.mapComp 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'.mapCompIso f h).hom ≫ F.mapComp f h ≫ F.map₂ (η ▷ h)
Tactic: rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_left, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]
-- 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 : LaxFunctor.{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'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ F.mapComp g h
rw₁ : F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.mapComp f h ≫ F.map₂ (η ▷ 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'.mapCompIso f h).hom ≫ (F'.mapCompIso f h).inv ≫ F.map₂ (η ▷ h)
Tactic: rw [F'.mapCompIso_inv, ← LaxFunctor.mapComp_naturality_left, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]
-- 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 : LaxFunctor.{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'.mapCompIso f h).hom ≫ F.map₂ η ▷ F.map h ≫ F.mapComp g h
rw₁ : F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ F.mapComp f h ≫ F.map₂ (η ▷ h)
rw₂ : F.map₂ (η ▷ h) = (F'.mapCompIso f h).hom ≫ (F'.mapCompIso f h).inv ≫ F.map₂ (η ▷ 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_inv, ← LaxFunctor.mapComp_naturality_left, ← F'.mapCompIso_inv,
      hom_inv_id_assoc]
-- 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 : LaxFunctor.{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 : inv ((F'.mapCompIso f g).hom ▷ F.map h) ≫ (F'.mapCompIso (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom =
  (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h)
Tactic: rw [F'.mapCompIso_inv, F'.mapCompIso_inv, ← inv_comp_eq, ← IsIso.inv_comp_eq]
-- 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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (λ_ f).hom = (F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom
have rw : F.map₂ (inv (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)
Tactic: rw [← IsIso.inv_eq_inv, ← F.map₂_inv]
-- 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 : LaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (ρ_ f).hom = (F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom
have rw : F.map₂ (inv (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)
Tactic: rw [← IsIso.inv_eq_inv, ← F.map₂_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor (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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : Prefunctor.{v₁, v₂, u₁, u₂} B C := { obj := obj, map := @map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrefunctor := toPrefunctor, map₂ := @map₂ }
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
toPrelaxFunctor : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := @map₂_id, map₂_comp := @map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) = map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := @map_comp,
    map₂_whisker_left := @map₂_whisker_left, map₂_whisker_right := @map₂_whisker_right }
a b : B
f : a ⟶ b
⊢ map (𝟙 a ≫ f) = 𝟙 (obj a) ≫ map f
have rw : map (𝟙 a) ≫ map f = 𝟙 (obj a) ≫ map f
Tactic: rw [map_comp (𝟙 a) f, map_id a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor (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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : Prefunctor.{v₁, v₂, u₁, u₂} B C := { obj := obj, map := @map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrefunctor := toPrefunctor, map₂ := @map₂ }
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
toPrelaxFunctor : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := @map₂_id, map₂_comp := @map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) = map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := @map_comp,
    map₂_whisker_left := @map₂_whisker_left, map₂_whisker_right := @map₂_whisker_right }
a b : B
f : a ⟶ b
rw : map (𝟙 a) ≫ map f = 𝟙 (obj a) ≫ map f
⊢ map (𝟙 a ≫ f) = 𝟙 (obj a) ≫ map f
have rw₁ : 𝟙 (obj a) ≫ map f = 𝟙 (obj a) ≫ map f
Tactic: rw [map_comp (𝟙 a) f, map_id a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor (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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : Prefunctor.{v₁, v₂, u₁, u₂} B C := { obj := obj, map := @map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrefunctor := toPrefunctor, map₂ := @map₂ }
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
toPrelaxFunctor : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := @map₂_id, map₂_comp := @map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) = map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := @map_comp,
    map₂_whisker_left := @map₂_whisker_left, map₂_whisker_right := @map₂_whisker_right }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
⊢ map (f ≫ 𝟙 b) = map f ≫ 𝟙 (obj b)
have rw : map f ≫ map (𝟙 b) = map f ≫ 𝟙 (obj b)
Tactic: rw [map_comp f (𝟙 b), map_id b]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor (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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
toPrefunctor : Prefunctor.{v₁, v₂, u₁, u₂} B C := { obj := obj, map := @map }
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
toPrelaxFunctorStruct : PrelaxFunctorStruct.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrefunctor := toPrefunctor, map₂ := @map₂ }
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
toPrelaxFunctor : PrelaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := @map₂_id, map₂_comp := @map₂_comp }
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) = map f ≫ map g
map₂_whisker_left :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), map₂ (f ◁ η) = eqToHom ⋯ ≫ map f ◁ map₂ η ≫ eqToHom ⋯
map₂_whisker_right :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), map₂ (η ▷ g) = eqToHom ⋯ ≫ map₂ η ▷ map g ≫ eqToHom ⋯
toStrictPseudofunctorPreCore : StrictPseudofunctorPreCore.{w₁, w₂, v₁, v₂, u₁, u₂} B C :=
  { toPrelaxFunctor := toPrelaxFunctor, map_id := map_id, map_comp := @map_comp,
    map₂_whisker_left := @map₂_whisker_left, map₂_whisker_right := @map₂_whisker_right }
map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).hom = eqToHom ⋯ ≫ (λ_ (map f)).hom
a b : B
f : a ⟶ b
rw : map f ≫ map (𝟙 b) = map f ≫ 𝟙 (obj b)
⊢ map (f ≫ 𝟙 b) = map f ≫ 𝟙 (obj b)
have rw₁ : map f ≫ 𝟙 (obj b) = map f ≫ 𝟙 (obj b)
Tactic: rw [map_comp f (𝟙 b), map_id b]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
D : Type u₃
inst_2 : Bicategory.{w₃, v₃, u₃} D
F_1 F : StrictPseudofunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
G : StrictPseudofunctor.{w₂, w₃, v₂, v₃, u₂, u₃} C D
a b c : B
x : a ⟶ b
x_1 : b ⟶ c
⊢ (F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x x_1 = eqToIso ⋯
have w : ((F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x x_1).hom = Iso.hom (eqToIso sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map f ≫ map g ⟶ map (f ≫ g)
mapComp_naturality_left :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), mapComp f g ≫ map₂ (η ▷ g) = map₂ η ▷ map g ≫ mapComp f' g
mapComp_naturality_right :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), mapComp f g ≫ map₂ (f ◁ η) = map f ◁ map₂ η ≫ mapComp f g'
a b : B
f : a ⟶ b
⊢ 𝟙 (obj a) ≫ map f = map (𝟙 a) ≫ map f
have rw : 𝟙 (obj a) ≫ map f = 𝟙 (obj a) ≫ map f
Tactic: rw [map_id a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (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
obj : B → C
map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : B), map (𝟙 X) = 𝟙 (obj X)
map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g)
map₂_id : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f)
map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), map₂ (η ≫ θ) = map₂ η ≫ map₂ θ
mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → map f ≫ map g ⟶ map (f ≫ g)
mapComp_naturality_left :
  ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), mapComp f g ≫ map₂ (η ▷ g) = map₂ η ▷ map g ≫ mapComp f' g
mapComp_naturality_right :
  ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), mapComp f g ≫ map₂ (f ◁ η) = map f ◁ map₂ η ≫ mapComp f g'
map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), map₂ (λ_ f).inv = (λ_ (map f)).inv ≫ eqToHom ⋯ ≫ mapComp (𝟙 a) f
a b : B
f : a ⟶ b
⊢ map f ≫ 𝟙 (obj b) = map f ≫ map (𝟙 b)
have rw : map f ≫ 𝟙 (obj b) = map f ≫ 𝟙 (obj b)
Tactic: rw [map_id b]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (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 : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
x : B
⊢ IsIso (F.mapId x)
have rw : IsIso (eqToHom sorry)
Tactic: rw [mapId_eq_eqToHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
⊢ F.comp (id C) = F
have obj : ∀ (x : B), (F.comp (id C)).obj x = F.obj x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
obj : ∀ (x : B), (F.comp (id C)).obj x = F.obj x
⊢ F.comp (id C) = F
have map : @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (F.comp (id C)).toPrefunctor ≍
  @Prefunctor.map B inst.toQuiver C inst_1.toQuiver F.toPrefunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary (goal)
Goal:
B : Type u₁
inst : Bicategory.{w₁, v₁, u₁} B
C : Type u₂
inst_1 : Bicategory.{w₂, v₂, u₂} C
F : StrictlyUnitaryLaxFunctor.{w₁, w₂, v₁, v₂, u₁, u₂} B C
obj : ∀ (x : B), (F.comp (id C)).obj x = F.obj x
map :
  @Prefunctor.map B inst.toQuiver C inst_1.toQuiver (F.comp (id C)).toPrefunctor ≍
    @Prefunctor.map B inst.toQuiver C inst_1.toQuiver F.toPrefunctor
⊢ F.comp (id C) = F
have map₂ : @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
    (fun (a b : C) ↦ (homCategory a b).toQuiver) (F.comp (id C)).toPrelaxFunctorStruct ≍
  @PrelaxFunctorStruct.map₂ B inst.toQuiver (fun (a b : B) ↦ (homCategory a b).toQuiver) C inst_1.toQuiver
    (fun (a b : C) ↦ (homCategory a b).toQuiver) F.toPrelaxFunctorStruct
Tactic: ext