awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y : C
f : X ≅ Y
⊢ F.map f.hom ≫ F.map f.inv = 𝟙 (F.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Iso
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y : C
f : X ≅ Y
⊢ F.map f.inv ≫ F.map f.hom = 𝟙 (F.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.IsomorphismClasses
Goal:
C : Cat
h :
  ∀ (x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop))
              (Cat.Hom.toFunctor (𝟙 C)).obj ⋯))
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))))).toFun
        x
⊢ ↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
        (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (Cat.Hom.toFunctor (𝟙 C)).obj ⋯ =
    𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.IsomorphismClasses
Goal:
C : Cat
x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))
h : ∀ (a b : (↑C : Type u)) (p : (isIsomorphicSetoid (↑C : Type u) : (↑C : Type u) → (↑C : Type u) → Prop) a b), ⋯ = ⋯
h₁ :
  ∀ (a : (↑C : Type u)),
    TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop))
              (Cat.Hom.toFunctor (𝟙 C)).obj ⋯))
        (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a) =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))))).toFun
        (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
            (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (Cat.Hom.toFunctor (𝟙 C)).obj
            ⋯))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))))).toFun
      x

Tactic:
apply @Quot.recOn _ _ _ x

Premises used: Quot.recOn
-- Module: Mathlib.CategoryTheory.IsomorphismClasses
Goal:
C : Cat
x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))
⊢ ∀ (a : (↑C : Type u)),
    TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop))
              (Cat.Hom.toFunctor (𝟙 C)).obj ⋯))
        (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a) =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (𝟙 (Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))))).toFun
        (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a)

Tactic:
all_goals cat_disch
-- Module: Mathlib.CategoryTheory.IsomorphismClasses
Goal:
C D E : Cat
f : C ⟶ D
g : D ⟶ E
h :
  ∀ (x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))),
    Eq (α := Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj ⋯))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
            (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
                (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj ⋯)
            (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
                (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj ⋯)))
        x)
⊢ Eq (α :=
    Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)) ⟶
      Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
    (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
        (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj ⋯)
    (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
      (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
          (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj ⋯)
      (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
          (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj ⋯))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.IsomorphismClasses
Goal:
C D E : Cat
f : C ⟶ D
g : D ⟶ E
x : Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u))
⊢ ∀ (a : (↑C : Type u)),
    Eq (α := Quotient (α := (↑E : Type u)) (isIsomorphicSetoid.{v, u} (↑E : Type u)))
      (TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
              (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) (f ≫ g).toFunctor.obj ⋯))
        (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a))
      (TypeCat.Fun.toFun (X := Quotient (α := (↑C : Type u)) (isIsomorphicSetoid.{v, u} (↑C : Type u)))
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Quotient (α := (↑D : Type u)) (isIsomorphicSetoid.{v, u} (↑D : Type u)))
            (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop)) (rb :=
                (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) f.toFunctor.obj ⋯)
            (↾Quot.map (ra := (⇑(isIsomorphicSetoid (↑D : Type u)) : (↑D : Type u) → (↑D : Type u) → Prop)) (rb :=
                (⇑(isIsomorphicSetoid (↑E : Type u)) : (↑E : Type u) → (↑E : Type u) → Prop)) g.toFunctor.obj ⋯)))
        (Quot.mk (⇑(isIsomorphicSetoid (↑C : Type u)) : (↑C : Type u) → (↑C : Type u) → Prop) a))

Tactic:
all_goals cat_disch
-- Module: Mathlib.CategoryTheory.IsomorphismClasses
Goal:
C : Type u
inst : Groupoid.{v, u} C
X Y : C
⊢ IsIsomorphic.{v, u} X Y ↔ Nonempty.{v + 1} (X ⟶ Y)

Tactic:
(Groupoid.isoEquivHom X Y).nonempty_congr

Premises used: CategoryTheory.IsIsomorphic, CategoryTheory.Groupoid.isoEquivHom, Equiv.nonempty_congr
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
x y : Join.{v₁, v₂, u₁, u₂} C D
f : x.Hom y
left : ∀ (a : C) (f : Hom (Join.left a) y), comp (id (Join.left a)) f = f
right : ∀ (a : D) (f : Hom (Join.right a) y), comp (id (Join.right a)) f = f
⊢ comp x.id f = f

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : C
f : Hom (Join.left a) y
left : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)), comp (id (Join.left a)) f = f
left₁ : ∀ (a_1 : D) (f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)), comp (id (Join.left a)) f = f
⊢ comp (id (Join.left a)) f = f

Tactic:
cases y
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : D
f : Hom (Join.right a) y
right : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)), comp (id (Join.right a)) f = f
right₁ : ∀ (a_1 : D) (f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)), comp (id (Join.right a)) f = f
⊢ comp (id (Join.right a)) f = f

Tactic:
cases y
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)
left : { down := f.down : ULift.{v₂, v₁} (a ⟶ a_1) } = f
⊢ comp (id (Join.left a)) f = f

Tactic:
simp only [Hom, id, comp, Category.id_comp]

Premises used: CategoryTheory.Join.id, CategoryTheory.Join.comp, CategoryTheory.Join.Hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)
right :
  (match (motive :=
      (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
          | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
          | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, Join.right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | Join.right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, Join.right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | Join.right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
            match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, Join.right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | Join.right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
      Join.right a, Join.right a, left a_1, { down := 𝟙 a }, f with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, Join.right _z, x, x_1 => PUnit.unit
    | left _x, Join.right _y, Join.right _z, x, x_1 => PUnit.unit
    | Join.right _x, Join.right _y, Join.right _z, f, g => { down := f.down ≫ g.down }) =
    f
⊢ comp (id (Join.right a)) f = f

Tactic:
simp only [Hom, id, comp, Category.id_comp]

Premises used: CategoryTheory.Join.id, CategoryTheory.Join.comp, CategoryTheory.Join.Hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)
right : { down := f.down : ULift.{v₁, v₂} (a ⟶ a_1) } = f
⊢ comp (id (Join.right a)) f = f

Tactic:
simp only [Hom, id, comp, Category.id_comp]

Premises used: CategoryTheory.Join.id, CategoryTheory.Join.comp, CategoryTheory.Join.Hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a) (left a_1)
⊢ { down := f.down : ULift.{v₂, v₁} (a ⟶ a_1) } = f

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : C
a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (left a) (right a_1)
⊢ PUnit.unit = f

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)
⊢ (match (motive :=
      (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
          | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
            match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
      right a, right a, left a_1, { down := 𝟙 a }, f with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    f

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a) (right a_1)
⊢ { down := f.down : ULift.{v₁, v₂} (a ⟶ a_1) } = f

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
x y : Join.{v₁, v₂, u₁, u₂} C D
f : x.Hom y
left : ∀ (a : C) (f : Hom (Join.left a) y), comp f y.id = f
right : ∀ (a : D) (f : Hom (Join.right a) y), comp f y.id = f
⊢ comp f y.id = f

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : C
f : Hom (Join.left a) y
left : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)), comp f (id (Join.left a_1)) = f
left₁ : ∀ (a_1 : D) (f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)), comp f (id (right a_1)) = f
⊢ comp f y.id = f

Tactic:
cases y
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
y : Join.{v₁, v₂, u₁, u₂} C D
a : D
f : Hom (Join.right a) y
right : ∀ (a_1 : C) (f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)), comp f (id (left a_1)) = f
right₁ :
  ∀ (a_1 : D) (f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)), comp f (id (Join.right a_1)) = f
⊢ comp f y.id = f

Tactic:
cases y
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)
left : { down := f.down : ULift.{v₂, v₁} (a ⟶ a_1) } = f
⊢ comp f (id (Join.left a_1)) = f

Tactic:
simp only [Hom, id, comp, Category.comp_id]

Premises used: CategoryTheory.Join.id, CategoryTheory.Join.comp, CategoryTheory.Category.comp_id, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)
right :
  (match (motive :=
      (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
          | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
          | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, Join.right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | Join.right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, Join.right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | Join.right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
            match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | Join.right x, Join.right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, Join.right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | Join.right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
      Join.right a, left a_1, left a_1, f, { down := 𝟙 a_1 } with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, Join.right _z, x, x_1 => PUnit.unit
    | left _x, Join.right _y, Join.right _z, x, x_1 => PUnit.unit
    | Join.right _x, Join.right _y, Join.right _z, f, g => { down := f.down ≫ g.down }) =
    f
⊢ comp f (id (left a_1)) = f

Tactic:
simp only [Hom, id, comp, Category.comp_id]

Premises used: CategoryTheory.Join.id, CategoryTheory.Join.comp, CategoryTheory.Category.comp_id, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a a_1 : D
f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)
right : { down := f.down : ULift.{v₁, v₂} (a ⟶ a_1) } = f
⊢ comp f (id (Join.right a_1)) = f

Tactic:
simp only [Hom, id, comp, Category.comp_id]

Premises used: CategoryTheory.Join.id, CategoryTheory.Join.comp, CategoryTheory.Category.comp_id, CategoryTheory.Join.Hom
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a : D
a_1 : C
f : Hom.{v₁, v₂, u₁, u₂} (right a) (left a_1)
⊢ (match (motive :=
      (x x_1 x_2 : Join.{v₁, v₂, u₁, u₂} C D) →
        (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_1 with
          | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
          | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
          | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
          | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
          (match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x_1, x_2 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)}) →
            match (motive := Join.{v₁, v₂, u₁, u₂} C D → Join.{v₁, v₂, u₁, u₂} C D → Type (max v₁ v₂)) x, x_2 with
            | left x, left y => ULift.{v₂, v₁} (x ⟶ y)
            | right x, right y => ULift.{v₁, v₂} (x ⟶ y)
            | left a, right a_2 => PUnit.{max (v₁ + 1) (v₂ + 1)}
            | right a, left a_2 => PEmpty.{max (v₁ + 1) (v₂ + 1)})
      right a, left a_1, left a_1, f, { down := 𝟙 a_1 } with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    f

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
a b c d : Join.{v₁, v₂, u₁, u₂} C D
f : a.Hom b
g : b.Hom c
h : c.Hom d
left : ∀ (a : C) (f : Hom (Join.left a) b), comp (comp f g) h = comp f (comp g h)
right : ∀ (a : D) (f : Hom (Join.right a) b), comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases a
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
b c d : Join.{v₁, v₂, u₁, u₂} C D
g : b.Hom c
h : c.Hom d
a : C
f : Hom (Join.left a) b
left :
  ∀ (a_1 : C) (g : Hom (Join.left a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)),
    comp (comp f g) h = comp f (comp g h)
left₁ :
  ∀ (a_1 : D) (g : Hom (right a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases b
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
b c d : Join.{v₁, v₂, u₁, u₂} C D
g : b.Hom c
h : c.Hom d
a : D
f : Hom (Join.right a) b
right :
  ∀ (a_1 : C) (g : Hom (left a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)),
    comp (comp f g) h = comp f (comp g h)
right₁ :
  ∀ (a_1 : D) (g : Hom (Join.right a_1) c) (f : Hom.{v₁, v₂, u₁, u₂} (C := C) (Join.right a) (Join.right a_1)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases b
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a a_1 : C
g : Hom (Join.left a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a) (Join.left a_1)
left :
  ∀ (a_2 : C) (h : Hom (Join.left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (D := D) (Join.left a_1) (Join.left a_2)),
    comp (comp f g) h = comp f (comp g h)
left₁ :
  ∀ (a_2 : D) (h : Hom (right a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (Join.left a_1) (right a_2)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases c
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a : C
a_1 : D
g : Hom (right a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (Join.left a) (right a_1)
left :
  ∀ (a_2 : C) (h : Hom (Join.left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (right a_1) (Join.left a_2)),
    comp (comp f g) h = comp f (comp g h)
left₁ :
  ∀ (a_2 : D) (h : Hom (right a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (C := C) (right a_1) (right a_2)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases c
-- Module: Mathlib.CategoryTheory.Join.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
c d : Join.{v₁, v₂, u₁, u₂} C D
h : c.Hom d
a : D
a_1 : C
g : Hom (left a_1) c
f : Hom.{v₁, v₂, u₁, u₂} (Join.right a) (left a_1)
right :
  ∀ (a_2 : C) (h : Hom (left a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (D := D) (left a_1) (left a_2)),
    comp (comp f g) h = comp f (comp g h)
right₁ :
  ∀ (a_2 : D) (h : Hom (Join.right a_2) d) (g : Hom.{v₁, v₂, u₁, u₂} (left a_1) (Join.right a_2)),
    comp (comp f g) h = comp f (comp g h)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
cases c