awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
this_1 :
  ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape J (Functor.obj coyoneda (op X))
A : Set X
hA : HasCardinalLT (↑A : Type u) κ
f :
  (HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X)).obj
    (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)
hf :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := HasCardinalLT.Set X κ)
        (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
          (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
            (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
        (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ)))
              (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)) :
          (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (HasCardinalLT.Set X κ)).obj
                    ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                ⟨A, hA⟩))
        f :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := HasCardinalLT.Set X κ)
          (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
            (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
              (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
          (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) A hA)))
    (𝟙 X : X ⟶ X)
x : X
this : (↑((hom (FC := TypeCat.Fun) f : (a : X) → (↑A : Type u)) x) : X) = x
⊢ (↑((hom (FC := TypeCat.Fun) f : (a : X) → (↑A : Type u)) x) : X) ∈ A ↔
    Membership.mem (γ := Set X) Set.univ (↑((hom (FC := TypeCat.Fun) f : (a : X) → (↑A : Type u)) x) : X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape J (Functor.obj coyoneda (op X))
hA : HasCardinalLT (↑Set.univ : Type u) κ
f :
  (HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X)).obj
    (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ hA)
hf :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := HasCardinalLT.Set X κ)
        (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
          (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
            (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
        (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ hA)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ)))
              (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ hA)) :
          (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨Set.univ, hA⟩)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (HasCardinalLT.Set X κ)).obj
                    ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                ⟨Set.univ, hA⟩))
        f :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := HasCardinalLT.Set X κ)
          (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
            (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
              (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
          (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ hA)))
    (𝟙 X : X ⟶ X)
⊢ HasCardinalLT X κ

Tactic:
(hasCardinalLT_iff_of_equiv (Equiv.Set.univ X) _).1 hA

Premises used: hasCardinalLT_iff_of_equiv, Iff.mp, Equiv.Set.univ
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
inst : Fact κ.IsRegular
h : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst_1 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape J (Functor.obj coyoneda (op X))
hA : HasCardinalLT (↑Set.univ : Type u) κ
f :
  (HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X)).obj
    (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ hA)
hf :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := HasCardinalLT.Set X κ)
        (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
          (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
            (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
        (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ hA)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ)))
              (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ hA)) :
          (a : (fun (X : Type u) ↦ X) ((HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨Set.univ, hA⟩)) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (HasCardinalLT.Set X κ)).obj
                    ((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).pt).obj
                ⟨Set.univ, hA⟩))
        f :
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := HasCardinalLT.Set X κ)
          (Functor.obj (Functor.const (HasCardinalLT.Set X κ))
            (Cocone.pt (F := HasCardinalLT.Set.functor X κ ⋙ Functor.obj coyoneda (op X))
              (Functor.mapCocone (Functor.obj coyoneda (op X)) (HasCardinalLT.Set.cocone X κ))))
          (Subtype.mk (p := fun (A : Set X) ↦ HasCardinalLT (↑A : Type u) κ) Set.univ hA)))
    (𝟙 X : X ⟶ X)
⊢ HasCardinalLT X κ

Tactic:
exact (hasCardinalLT_iff_of_equiv (Equiv.Set.univ X) _).1 hA

Premises used: hasCardinalLT_iff_of_equiv, Iff.mp, Equiv.Set.univ
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X_1 X : Type u
obtain : ∀ (κ : Cardinal.{u}) (hκ : κ.IsRegular) (hX : HasCardinalLT X κ), IsPresentable.{u, u, u + 1} X
⊢ IsPresentable.{u, u, u + 1} X

Tactic:
obtain ⟨κ, hκ, hX⟩ := HasCardinalLT.exists_regular_cardinal.{u} X
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X_1 X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
⊢ Fact κ.IsRegular

Tactic:
have : Fact κ.IsRegular := ⟨hκ⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X_1 X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
this : Fact κ.IsRegular
⊢ IsCardinalPresentable X κ

Tactic:
have := hX.isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X_1 X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
this_1 : Fact κ.IsRegular
this : IsCardinalPresentable X κ
⊢ IsPresentable.{u, u, u + 1} X

Tactic:
isPresentable_of_isCardinalPresentable X κ

Premises used: CategoryTheory.isPresentable_of_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X_1 X : Type u
κ : Cardinal.{u}
hκ : κ.IsRegular
hX : HasCardinalLT X κ
this_1 : Fact κ.IsRegular
this : IsCardinalPresentable X κ
⊢ IsPresentable.{u, u, u + 1} X

Tactic:
exact isPresentable_of_isCardinalPresentable X κ

Premises used: CategoryTheory.isPresentable_of_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Products.Associator
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
⊢ Functor.IsEquivalence (Equivalence.functor (associativity C D E))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Products.Associator
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
⊢ Functor.IsEquivalence (Equivalence.inverse (associativity C D E))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst_1 : CategoryStruct.{v₂, u₂} D
X Y : C × D
f g : X ⟶ Y
h₁ : f.1 = g.1
h₂ : f.2 = g.2
⊢ f = g

Tactic:
Prod.ext h₁ h₂

Premises used: Prod.ext
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst_1 : CategoryStruct.{v₂, u₂} D
X₁ X₂ : C
Y₁ Y₂ : D
f f' : X₁ ⟶ X₂
g g' : Y₁ ⟶ Y₂
⊢ f ×ₘ g = f' ×ₘ g' ↔ f = f' ∧ g = g'

Tactic:
Prod.hom_ext_iff

Premises used: CategoryTheory.Prod.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst_1 : CategoryStruct.{v₂, u₂} D
X : C
Y : D
⊢ Eq (α := (X, Y) ⟶ (X, Y)) (𝟙 (X, Y)) (𝟙 X ×ₘ 𝟙 Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst_1 : CategoryStruct.{v₂, u₂} D
X : C
Y : D
⊢ Eq (α := (X, Y) ⟶ (X, Y)) (𝟙 (X, Y)) (𝟙 X, 𝟙 Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst_1 : CategoryStruct.{v₂, u₂} D
P Q R : C
S T U : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (R, U)
⊢ f ≫ g = f.1 ≫ g.1 ×ₘ f.2 ≫ g.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
mp : IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f → IsIso f.1 ∧ IsIso f.2
mpr : IsIso f.1 ∧ IsIso f.2 → IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f
⊢ IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f ↔ IsIso f.1 ∧ IsIso f.2

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
⊢ (f ≫ g).1 = (𝟙 (P, S)).1

Tactic:
rcases Prod.hom_ext_iff.1 hfg with ⟨hfg₁, hfg₂⟩

Premises used: CategoryTheory.Prod.hom_ext_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
⊢ (f ≫ g).2 = (𝟙 (P, S)).2

Tactic:
rcases Prod.hom_ext_iff.1 hfg with ⟨hfg₁, hfg₂⟩

Premises used: CategoryTheory.Prod.hom_ext_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
hfg₂ : (f ≫ g).2 = (𝟙 (P, S)).2
⊢ (g ≫ f).1 = (𝟙 (Q, T)).1

Tactic:
rcases Prod.hom_ext_iff.1 hgf with ⟨hgf₁, hgf₂⟩

Premises used: CategoryTheory.Prod.hom_ext_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
hfg₂ : (f ≫ g).2 = (𝟙 (P, S)).2
hgf₁ : (g ≫ f).1 = (𝟙 (Q, T)).1
⊢ (g ≫ f).2 = (𝟙 (Q, T)).2

Tactic:
rcases Prod.hom_ext_iff.1 hgf with ⟨hgf₁, hgf₂⟩

Premises used: CategoryTheory.Prod.hom_ext_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
hfg₂ : (f ≫ g).2 = (𝟙 (P, S)).2
hgf₁ : (g ≫ f).1 = (𝟙 (Q, T)).1
hgf₂ : (g ≫ f).2 = (𝟙 (Q, T)).2
⊢ IsIso f.1 ∧ IsIso f.2

Tactic:
⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩

Premises used: Prod.fst, And.intro, Exists.intro, CategoryTheory.IsIso.mk, Prod.snd
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
hfg₁ : (f ≫ g).1 = (𝟙 (P, S)).1
hfg₂ : (f ≫ g).2 = (𝟙 (P, S)).2
hgf₁ : (g ≫ f).1 = (𝟙 (Q, T)).1
hgf₂ : (g ≫ f).2 = (𝟙 (Q, T)).2
⊢ IsIso f.1 ∧ IsIso f.2

Tactic:
exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ IsIso (C := C × D) (X := (P, S)) (Y := (Q, T)) f

Tactic:
refine ⟨⟨(g₁, g₂), by aesop_cat, by aesop_cat⟩⟩
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ IsEquivalence (Equivalence.functor (braiding C D))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : A ⥤ Functor.{v₂, v₃, u₂, u₃} B C
a : A
⊢ F.flip ⋙ obj (evaluation A C) a = F.obj a

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : A ⥤ Functor.{v₂, v₃, u₂, u₃} B C
b : B
⊢ F ⋙ obj (evaluation B C) b = F.flip.obj b

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
a : A
⊢ Eq (α := Functor.{v₂, v₃, u₂, u₃} B C ⥤ C) (obj (whiskeringLeft A B C) F ⋙ obj (evaluation A C) a)
    (obj (evaluation B C) (F.obj a))

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Products.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₂, v₃, u₂, u₃} B C
a : A
⊢ Eq (α := Functor.{v₁, v₂, u₁, u₂} A B ⥤ C) (obj (whiskeringRight A B C) F ⋙ obj (evaluation A C) a)
    (obj (evaluation A B) a ⋙ F)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Products.Bifunctor
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 X ×ₘ 𝟙 Y) = 𝟙 (F.obj (X, Y))

Tactic:
F.map_id (X, Y)

Premises used: Prod.mk, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Products.Bifunctor
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
rw : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f) ≫ (𝟙 W ×ₘ g))
rw₁ : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f).1 ≫ (𝟙 W ×ₘ g).1 ×ₘ (𝟙 W ×ₘ f).2 ≫ (𝟙 W ×ₘ g).2)
rw₂ rw₃ : F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f).1 ×ₘ (𝟙 W ×ₘ f).2 ≫ (𝟙 W ×ₘ g).2)
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.prod_comp
-- Module: Mathlib.CategoryTheory.Products.Bifunctor
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
rw : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W) ≫ (g ×ₘ 𝟙 W))
rw₁ : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W).1 ≫ (g ×ₘ 𝟙 W).1 ×ₘ (f ×ₘ 𝟙 W).2 ≫ (g ×ₘ 𝟙 W).2)
rw₂ rw₃ : F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W).1 ≫ (g ×ₘ 𝟙 W).1 ×ₘ (f ×ₘ 𝟙 W).2)
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.prod_comp
-- Module: Mathlib.CategoryTheory.Products.Bifunctor
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
rw : F.map ((𝟙 X ×ₘ g) ≫ (f ×ₘ 𝟙 Y')) = F.map (f ×ₘ g)
rw₁ : F.map ((𝟙 X ×ₘ g).1 ≫ (f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2 ≫ (f ×ₘ 𝟙 Y').2) = F.map (f ×ₘ g)
rw₂ : F.map ((f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2 ≫ (f ×ₘ 𝟙 Y').2) = F.map (f ×ₘ g)
rw₃ rw₄ : F.map ((f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2) = F.map (f ×ₘ g)
⊢ F.map (𝟙 X ×ₘ g) ≫ F.map (f ×ₘ 𝟙 Y') = F.map (f ×ₘ g)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.prod_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Products.Bifunctor
Goal:
C : Type u₁
D : Type u₂
E : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
rw : F.map ((f ×ₘ 𝟙 Y) ≫ (𝟙 X' ×ₘ g)) = F.map (f ×ₘ g)
rw₁ : F.map ((f ×ₘ 𝟙 Y).1 ≫ (𝟙 X' ×ₘ g).1 ×ₘ (f ×ₘ 𝟙 Y).2 ≫ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
rw₂ : F.map ((f ×ₘ 𝟙 Y).1 ≫ (𝟙 X' ×ₘ g).1 ×ₘ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
rw₃ rw₄ : F.map ((f ×ₘ 𝟙 Y).1 ×ₘ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
⊢ F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.prod_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Products.Unitor
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Functor.IsEquivalence (leftUnitor C)

Tactic:
(leftUnitorEquivalence C).isEquivalence_functor

Premises used: CategoryTheory.prod.leftUnitor, CategoryTheory.prod.leftUnitorEquivalence, CategoryTheory.Equivalence.isEquivalence_functor
-- Module: Mathlib.CategoryTheory.Products.Unitor
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Functor.IsEquivalence (rightUnitor C)

Tactic:
(rightUnitorEquivalence C).isEquivalence_functor

Premises used: CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.prod.rightUnitorEquivalence, CategoryTheory.prod.rightUnitor
-- Module: Mathlib.CategoryTheory.Profunctor.Basic
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X : C
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
nth_rw : P.map (𝟙 X ≫ 𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g
⊢ P.map (𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g

Tactic:
nth_rw 1 [← Category.id_comp (𝟙 X)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Profunctor.Basic
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X : C
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ P.map (𝟙 X ≫ 𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g

Tactic:
simp only [P.map_comp]

Premises used: CategoryTheory.ProfunctorCore.map_comp
-- Module: Mathlib.CategoryTheory.Profunctor.Basic
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X X' X'' : C
Y : D
f : X ⟶ X'
f' : X' ⟶ X''
nth_rw : P.map (f ≫ f') (𝟙 Y ≫ 𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y)
⊢ P.map (f ≫ f') (𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y)

Tactic:
nth_rw 1 [← Category.id_comp (𝟙 Y)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Profunctor.Basic
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X X' X'' : C
Y : D
f : X ⟶ X'
f' : X' ⟶ X''
⊢ P.map (f ≫ f') (𝟙 Y ≫ 𝟙 Y) = P.map f (𝟙 Y) ≫ P.map f' (𝟙 Y)

Tactic:
simp only [P.map_comp]

Premises used: CategoryTheory.ProfunctorCore.map_comp
-- Module: Mathlib.CategoryTheory.Profunctor.Basic
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X X' : C
Y Y' : D
f : X ⟶ X'
g : Y ⟶ Y'
⊢ P.map (𝟙 X) g ≫ P.map f (𝟙 Y) = P.map f g

Tactic:
simp [← P.map_comp]

Premises used: CategoryTheory.ProfunctorCore.map_comp
-- Module: Mathlib.CategoryTheory.Profunctor.Basic
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X X' : C
Y Y' : D
f : X ⟶ X'
g : Y ⟶ Y'
⊢ P.map f (𝟙 Y') ≫ P.map (𝟙 X') g = P.map f g

Tactic:
simp [← P.map_comp]

Premises used: CategoryTheory.ProfunctorCore.map_comp
-- Module: Mathlib.CategoryTheory.Quotient.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : HomRel.CompClosure r f₁ f₂
⊢ r f₁ f₂

Tactic:
simp only [HomRel.compClosure_eq_self] at h₁₂

Premises used: CategoryTheory.HomRel.compClosure_eq_self
-- Module: Mathlib.CategoryTheory.Quotient.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
a₁ : HomRel.CompClosure r (a • f₁) (a • f₂)
⊢ Eq (α := X ⟶ Y) (Quot.mk (HomRel.CompClosure r) (a • f₁)) (Quot.mk (HomRel.CompClosure r) (a • f₂))

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.CategoryTheory.Quotient.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
a₁ : r (a • f₁) (a • f₂)
⊢ HomRel.CompClosure r (a • f₁) (a • f₂)

Tactic:
rw [HomRel.compClosure_eq_self]

Premises used: CategoryTheory.HomRel.compClosure_eq_self
-- Module: Mathlib.CategoryTheory.Quotient.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
⊢ r (a • f₁) (a • f₂)

Tactic:
hr _ _ _ h₁₂
-- Module: Mathlib.CategoryTheory.Quotient.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
X Y : Quotient r
a : R
f₁ f₂ : X.as (r := r) ⟶ Y.as (r := r)
h₁₂ : r f₁ f₂
⊢ r (a • f₁) (a • f₂)

Tactic:
exact hr _ _ _ h₁₂
-- Module: Mathlib.CategoryTheory.Quotient.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
r : HomRel.{u_2, v_1} C
inst_4 : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
a : R
X Y : C
f : X ⟶ Y
⊢ a • (functor r).map f = (functor r).map (a • f)

Tactic:
rfl

Premises used: rfl