awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} A C
G : Functor.{v₂, v₃, u₂, u₃} B C
x y : A
f : x ⟶ y
y_1 : A
f_1 : y ⟶ y_1
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) x with
        | inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) y_1 with
        | inl X => F.obj X
        | inr X => G.obj X :
        C))
    (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) x with
            | inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | inl X => F.obj X
            | inr X => G.obj X :
            C))
        (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := obj (Sum.inl_ A B) x)
        (map (Sum.inl_ A B) f ≫ map (Sum.inl_ A B) f_1) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) x with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) y_1 with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := A ⊕ B → C) obj (Sum.inl_ A B) y with
        | inl X => F.obj X
        | inr X => G.obj X)
        (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
          Quiver.Hom.{v₃, u₃} (V := C)
            (match (motive := A ⊕ B → C) x with
              | inl X => F.obj X
              | inr X => G.obj X :
              C)
            (match (motive := A ⊕ B → C) x_1 with
              | inl X => F.obj X
              | inr X => G.obj X :
              C))
          (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := obj (Sum.inl_ A B) x)
          (map (Sum.inl_ A B) f))
        (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
          Quiver.Hom.{v₃, u₃} (V := C)
            (match (motive := A ⊕ B → C) x with
              | inl X => F.obj X
              | inr X => G.obj X :
              C)
            (match (motive := A ⊕ B → C) x_1 with
              | inl X => F.obj X
              | inr X => G.obj X :
              C))
          (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := obj (Sum.inl_ A B) y)
          (map (Sum.inl_ A B) f_1)) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) x with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) obj (Sum.inl_ A B) y_1 with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} A C
G : Functor.{v₂, v₃, u₂, u₃} B C
x y : B
f : x ⟶ y
y_1 : B
f_1 : y ⟶ y_1
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) x with
        | inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) y_1 with
        | inl X => F.obj X
        | inr X => G.obj X :
        C))
    (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
        Quiver.Hom.{v₃, u₃} (V := C)
          (match (motive := A ⊕ B → C) x with
            | inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | inl X => F.obj X
            | inr X => G.obj X :
            C))
        (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := obj (Sum.inr_ A B) x)
        (map (Sum.inr_ A B) f ≫ map (Sum.inr_ A B) f_1) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) x with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) y_1 with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))
    (CategoryStruct.comp (Y :=
        match (motive := A ⊕ B → C) obj (Sum.inr_ A B) y with
        | inl X => F.obj X
        | inr X => G.obj X)
        (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
          Quiver.Hom.{v₃, u₃} (V := C)
            (match (motive := A ⊕ B → C) x with
              | inl X => F.obj X
              | inr X => G.obj X :
              C)
            (match (motive := A ⊕ B → C) x_1 with
              | inl X => F.obj X
              | inr X => G.obj X :
              C))
          (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := obj (Sum.inr_ A B) x)
          (map (Sum.inr_ A B) f))
        (Sum.homInduction (P := fun (x x_1 : A ⊕ B) (x_2 : x ⟶ x_1) ↦
          Quiver.Hom.{v₃, u₃} (V := C)
            (match (motive := A ⊕ B → C) x with
              | inl X => F.obj X
              | inr X => G.obj X :
              C)
            (match (motive := A ⊕ B → C) x_1 with
              | inl X => F.obj X
              | inr X => G.obj X :
              C))
          (fun (x x_1 : A) (f : x ⟶ x_1) ↦ F.map f) fun (x x_1 : B) (g : x ⟶ x_1) ↦ G.map g (x := obj (Sum.inr_ A B) y)
          (map (Sum.inr_ A B) f_1)) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) x with
          | inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) obj (Sum.inr_ A B) y_1 with
          | inl X => F.obj X
          | inr X => G.obj X :
          C))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sums.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 C
G : Functor.{v₂, v₃, u₂, u₃} B C
a : A
⊢ (F.sum' G).obj (inl a) = F.obj a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 C
G : Functor.{v₂, v₃, u₂, u₃} B C
b : B
⊢ (F.sum' G).obj (inr b) = G.obj b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 C
G : Functor.{v₂, v₃, u₂, u₃} B C
a a' : A
f : a ⟶ a'
⊢ (F.sum' G).map (map (Sum.inl_ A B) f) = F.map f

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Sums.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 C
G : Functor.{v₂, v₃, u₂, u₃} B C
b b' : B
f : b ⟶ b'
⊢ (F.sum' G).map (map (Sum.inr_ A B) f) = G.map f

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₄, u₃, u₄} C D
a : A
⊢ (F.sum G).obj (inl a) = inl (F.obj a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₄, u₃, u₄} C D
c : C
⊢ (F.sum G).obj (inr c) = inr (G.obj c)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₄, u₃, u₄} C D
a a' : A
f : a ⟶ a'
⊢ Eq (α := (F.sum G).obj (obj (Sum.inl_ A C) a) ⟶ (F.sum G).obj (obj (Sum.inl_ A C) a'))
    ((F.sum G).map (map (Sum.inl_ A C) f)) (map (Sum.inl_ B D) (F.map f))

Tactic:
simp [sum]

Premises used: CategoryTheory.Functor.sum
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₄, u₃, u₄} C D
c c' : C
f : c ⟶ c'
⊢ Eq (α := (F.sum G).obj (obj (Sum.inr_ A C) c) ⟶ (F.sum G).obj (obj (Sum.inr_ A C) c'))
    ((F.sum G).map (map (Sum.inr_ A C) f)) (map (Sum.inr_ B D) (G.map f))

Tactic:
simp [sum]

Premises used: CategoryTheory.Functor.sum
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x y : A ⊕ B
f : x ⟶ y
inl :
  ∀ (x y : A) (f : x ⟶ y),
    Eq (α := F.obj (obj (Sum.inl_ A B) x) ⟶ G.obj (obj (Sum.inl_ A B) y))
      (F.map (map (Sum.inl_ A B) f) ≫
        Iso.hom
          ((fun (x : A ⊕ B) ↦
              (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
                | Sum.inl x => e₁.app x
                | Sum.inr x => e₂.app x :
                F.obj x ≅ G.obj x))
            (obj (Sum.inl_ A B) y)))
      (Iso.hom
          ((fun (x : A ⊕ B) ↦
              (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
                | Sum.inl x => e₁.app x
                | Sum.inr x => e₂.app x :
                F.obj x ≅ G.obj x))
            (obj (Sum.inl_ A B) x)) ≫
        G.map (map (Sum.inl_ A B) f))
inr :
  ∀ (x y : B) (f : x ⟶ y),
    Eq (α := F.obj (obj (Sum.inr_ A B) x) ⟶ G.obj (obj (Sum.inr_ A B) y))
      (F.map (map (Sum.inr_ A B) f) ≫
        Iso.hom
          ((fun (x : A ⊕ B) ↦
              (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
                | Sum.inl x => e₁.app x
                | Sum.inr x => e₂.app x :
                F.obj x ≅ G.obj x))
            (obj (Sum.inr_ A B) y)))
      (Iso.hom
          ((fun (x : A ⊕ B) ↦
              (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
                | Sum.inl x => e₁.app x
                | Sum.inr x => e₂.app x :
                F.obj x ≅ G.obj x))
            (obj (Sum.inr_ A B) x)) ≫
        G.map (map (Sum.inr_ A B) f))
⊢ F.map f ≫
      Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | Sum.inl x => e₁.app x
              | Sum.inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          y) =
    Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | Sum.inl x => e₁.app x
              | Sum.inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          x) ≫
      G.map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x y : A
f : x ⟶ y
⊢ Eq (α := F.obj (obj (Sum.inl_ A B) x) ⟶ G.obj (obj (Sum.inl_ A B) y))
    (F.map (map (Sum.inl_ A B) f) ≫
      Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          (obj (Sum.inl_ A B) y)))
    (Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          (obj (Sum.inl_ A B) x)) ≫
      G.map (map (Sum.inl_ A B) f))

Tactic:
simpa using e₁.hom.naturality _

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
x y : B
f : x ⟶ y
⊢ Eq (α := F.obj (obj (Sum.inr_ A B) x) ⟶ G.obj (obj (Sum.inr_ A B) y))
    (F.map (map (Sum.inr_ A B) f) ≫
      Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          (obj (Sum.inr_ A B) y)))
    (Iso.hom
        ((fun (x : A ⊕ B) ↦
            (match (motive := (x : A ⊕ B) → F.obj x ≅ G.obj x) x with
              | inl x => e₁.app x
              | inr x => e₂.app x :
              F.obj x ≅ G.obj x))
          (obj (Sum.inr_ A B) x)) ≫
      G.map (map (Sum.inr_ A B) f))

Tactic:
simpa using e₂.hom.naturality _

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Sums.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 G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
a : A
⊢ (sumIsoExt e₁ e₂).hom.app (inl a) = e₁.hom.app a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
b : B
⊢ (sumIsoExt e₁ e₂).hom.app (inr b) = e₂.hom.app b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
a : A
⊢ (sumIsoExt e₁ e₂).inv.app (inl a) = e₁.inv.app a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 G : A ⊕ B ⥤ C
e₁ : Sum.inl_ A B ⋙ F ≅ Sum.inl_ A B ⋙ G
e₂ : Sum.inr_ A B ⋙ F ≅ Sum.inr_ A B ⋙ G
b : B
⊢ (sumIsoExt e₁ e₂).inv.app (inr b) = e₂.inv.app b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 ⊕ B ⥤ C
a : A
⊢ F.isoSum.hom.app (inl a) = 𝟙 (F.obj (inl a))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 ⊕ B ⥤ C
b : B
⊢ F.isoSum.hom.app (inr b) = 𝟙 (F.obj (inr b))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 ⊕ B ⥤ C
a : A
⊢ Eq (α := ((Sum.inl_ A B ⋙ F).sum' (Sum.inr_ A B ⋙ F)).obj (inl a) ⟶ F.obj (inl a)) (F.isoSum.inv.app (inl a))
    (𝟙 (F.obj (inl a)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 ⊕ B ⥤ C
b : B
⊢ Eq (α := ((Sum.inl_ A B ⋙ F).sum' (Sum.inr_ A B ⋙ F)).obj (inr b) ⟶ F.obj (inr b)) (F.isoSum.inv.app (inr b))
    (𝟙 (F.obj (inr b)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₃, u₁, u₃} A C
H I : Functor.{v₂, v₃, u₂, u₃} B C
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ B
f : X ⟶ Y
inl :
  ∀ (x y : A) (f : x ⟶ y),
    Eq (α := (F.sum' H).obj (obj (Sum.inl_ A B) x) ⟶ (G.sum' I).obj (obj (Sum.inl_ A B) y))
      ((F.sum' H).map (map (Sum.inl_ A B) f) ≫
        match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inl_ A B) y with
        | Sum.inl X => α.app X
        | Sum.inr X => β.app X)
      ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inl_ A B) x with
        | Sum.inl X => α.app X
        | Sum.inr X => β.app X) ≫
        (G.sum' I).map (map (Sum.inl_ A B) f))
inr :
  ∀ (x y : B) (f : x ⟶ y),
    Eq (α := (F.sum' H).obj (obj (Sum.inr_ A B) x) ⟶ (G.sum' I).obj (obj (Sum.inr_ A B) y))
      ((F.sum' H).map (map (Sum.inr_ A B) f) ≫
        match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inr_ A B) y with
        | Sum.inl X => α.app X
        | Sum.inr X => β.app X)
      ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inr_ A B) x with
        | Sum.inl X => α.app X
        | Sum.inr X => β.app X) ≫
        (G.sum' I).map (map (Sum.inr_ A B) f))
⊢ Eq (α := (F.sum' H).obj X ⟶ (G.sum' I).obj Y)
    ((F.sum' H).map f ≫
      match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) Y with
      | Sum.inl X => α.app X
      | Sum.inr X => β.app X)
    ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) X with
      | Sum.inl X => α.app X
      | Sum.inr X => β.app X) ≫
      (G.sum' I).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₃, u₁, u₃} A C
H I : Functor.{v₂, v₃, u₂, u₃} B C
α : F ⟶ G
β : H ⟶ I
x y : A
f : x ⟶ y
⊢ Eq (α := (F.sum' H).obj (obj (Sum.inl_ A B) x) ⟶ (G.sum' I).obj (obj (Sum.inl_ A B) y))
    ((F.sum' H).map (map (Sum.inl_ A B) f) ≫
      match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inl_ A B) y with
      | inl X => α.app X
      | inr X => β.app X)
    ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inl_ A B) x with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map (map (Sum.inl_ A B) f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₃, u₁, u₃} A C
H I : Functor.{v₂, v₃, u₂, u₃} B C
α : F ⟶ G
β : H ⟶ I
x y : B
f : x ⟶ y
⊢ Eq (α := (F.sum' H).obj (obj (Sum.inr_ A B) x) ⟶ (G.sum' I).obj (obj (Sum.inr_ A B) y))
    ((F.sum' H).map (map (Sum.inr_ A B) f) ≫
      match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inr_ A B) y with
      | inl X => α.app X
      | inr X => β.app X)
    ((match (motive := (X : A ⊕ B) → (F.sum' H).obj X ⟶ (G.sum' I).obj X) obj (Sum.inr_ A B) x with
      | inl X => α.app X
      | inr X => β.app X) ≫
      (G.sum' I).map (map (Sum.inr_ A B) f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sums.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 G : Functor.{v₁, v₃, u₁, u₃} A C
H I : Functor.{v₂, v₃, u₂, u₃} B C
α : F ⟶ G
β : H ⟶ I
a : A
⊢ (sum' α β).app (inl a) = α.app a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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 G : Functor.{v₁, v₃, u₁, u₃} A C
H I : Functor.{v₂, v₃, u₂, u₃} B C
α : F ⟶ G
β : H ⟶ I
b : B
⊢ (sum' α β).app (inr b) = β.app b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₂, u₁, u₂} A B
H I : Functor.{v₃, v₄, u₃, u₄} C D
α : F ⟶ G
β : H ⟶ I
X Y : A ⊕ C
f : X ⟶ Y
inl :
  ∀ (x y : A) (f : x ⟶ y),
    Eq (α := (F.sum H).obj (obj (Sum.inl_ A C) x) ⟶ (G.sum I).obj (obj (Sum.inl_ A C) y))
      ((F.sum H).map (map (Sum.inl_ A C) f) ≫
        match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inl_ A C) y with
        | Sum.inl X => map (Sum.inl_ B D) (α.app X)
        | Sum.inr X => map (Sum.inr_ B D) (β.app X))
      ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inl_ A C) x with
        | Sum.inl X => map (Sum.inl_ B D) (α.app X)
        | Sum.inr X => map (Sum.inr_ B D) (β.app X)) ≫
        (G.sum I).map (map (Sum.inl_ A C) f))
inr :
  ∀ (x y : C) (f : x ⟶ y),
    Eq (α := (F.sum H).obj (obj (Sum.inr_ A C) x) ⟶ (G.sum I).obj (obj (Sum.inr_ A C) y))
      ((F.sum H).map (map (Sum.inr_ A C) f) ≫
        match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inr_ A C) y with
        | Sum.inl X => map (Sum.inl_ B D) (α.app X)
        | Sum.inr X => map (Sum.inr_ B D) (β.app X))
      ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inr_ A C) x with
        | Sum.inl X => map (Sum.inl_ B D) (α.app X)
        | Sum.inr X => map (Sum.inr_ B D) (β.app X)) ≫
        (G.sum I).map (map (Sum.inr_ A C) f))
⊢ Eq (α := (F.sum H).obj X ⟶ (G.sum I).obj Y)
    ((F.sum H).map f ≫
      match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) Y with
      | Sum.inl X => map (Sum.inl_ B D) (α.app X)
      | Sum.inr X => map (Sum.inr_ B D) (β.app X))
    ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) X with
      | Sum.inl X => map (Sum.inl_ B D) (α.app X)
      | Sum.inr X => map (Sum.inr_ B D) (β.app X)) ≫
      (G.sum I).map f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Sums.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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₂, u₁, u₂} A B
H I : Functor.{v₃, v₄, u₃, u₄} C D
α : F ⟶ G
β : H ⟶ I
x y : A
f : x ⟶ y
⊢ Eq (α := (F.sum H).obj (obj (Sum.inl_ A C) x) ⟶ (G.sum I).obj (obj (Sum.inl_ A C) y))
    ((F.sum H).map (map (Sum.inl_ A C) f) ≫
      match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inl_ A C) y with
      | inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X))
    ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inl_ A C) x with
      | inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X)) ≫
      (G.sum I).map (map (Sum.inl_ A C) f))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp