awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
T : C
hT : IsTerminal.{v₁, u₁} T
⊢ IsSubterminal.{v₁, u₁} T

Tactic:
fun _ _ _ =>
  hT.hom_ext _ _

Premises used: CategoryTheory.IsSubterminal, CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasTerminal.{v₁, u₁} C
x : C
x_1 x_2 : x ⟶ terminal.{v₁, u₁} C
⊢ x_1 = x_2

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
hA : IsSubterminal.{v₁, u₁} A
inst_1 : HasBinaryProduct.{v₁, u₁} A A
⊢ Eq.{v₁ + 1} (α := A ⟶ A) (CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A A) (diag A) prod.fst) (𝟙 A)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
hA : IsSubterminal.{v₁, u₁} A
inst_1 : HasBinaryProduct.{v₁, u₁} A A
rw :
  ∀ (hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g) [inst_2 : HasBinaryProduct.{v₁, u₁} A A],
    prod.fst ≫ diag A = 𝟙 (Limits.prod.{v₁, u₁} A A)
⊢ prod.fst ≫ diag A = 𝟙 (Limits.prod.{v₁, u₁} A A)

Tactic:
rw [IsSubterminal.def] at hA

Premises used: CategoryTheory.IsSubterminal.def
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasBinaryProduct.{v₁, u₁} A A
inst_2 : IsIso.{v₁, u₁} (Y := Limits.prod.{v₁, u₁} A A) (diag A)
Z : C
f g : Z ⟶ A
⊢ Eq.{v₁ + 1} (α := Limits.prod.{v₁, u₁} A A ⟶ A) prod.fst prod.snd

Tactic:
simp [← cancel_epi (diag A)]

Premises used: CategoryTheory.Limits.diag, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasBinaryProduct.{v₁, u₁} A A
inst_2 : IsIso.{v₁, u₁} (Y := Limits.prod.{v₁, u₁} A A) (diag A)
Z : C
f g : Z ⟶ A
⊢ Eq.{v₁ + 1} (α := Limits.prod.{v₁, u₁} A A ⟶ A) prod.fst prod.snd

Tactic:
have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd := by simp [← cancel_epi (diag A)]
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasBinaryProduct.{v₁, u₁} A A
inst_2 : IsIso.{v₁, u₁} (Y := Limits.prod.{v₁, u₁} A A) (diag A)
Z : C
f g : Z ⟶ A
this : Eq.{v₁ + 1} (α := Limits.prod.{v₁, u₁} A A ⟶ A) prod.fst prod.snd
rw : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A A) (prod.lift f g) prod.fst = g
rw₁ : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A A) (prod.lift f g) prod.snd = g
rw₂ rw₃ : g = g
⊢ f = g

Tactic:
rw [← prod.lift_fst f g, this, prod.lift_snd]

Premises used: CategoryTheory.Limits.prod.lift_fst, CategoryTheory.Limits.prod.lift_snd
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
hA : IsSubterminal.{v₁, u₁} A
inst_1 : HasBinaryProduct.{v₁, u₁} A A
this : IsIso.{v₁, u₁} (Y := Limits.prod.{v₁, u₁} A A) (diag A) := ⋯
⊢ Limits.prod.{v₁, u₁} A A ≅ A

Tactic:
apply (asIso (diag A)).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.diag, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
A : C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
⊢ Functor.Full.{v₁, v₁, u₁, u₁} (C := Subterminals.{v₁, u₁} C) (subterminalInclusion C)

Tactic:
ObjectProperty.full_ι _

Premises used: CategoryTheory.subterminalInclusion, CategoryTheory.ObjectProperty.full_ι, CategoryTheory.Subterminals
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
A : C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
⊢ Functor.Faithful.{v₁, v₁, u₁, u₁} (C := Subterminals.{v₁, u₁} C) (subterminalInclusion C)

Tactic:
ObjectProperty.faithful_ι _

Premises used: CategoryTheory.subterminalInclusion, CategoryTheory.ObjectProperty.faithful_ι, CategoryTheory.Subterminals
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
X Y : Subterminals.{v₁, u₁} C
f : X ⟶ Y
⊢ Eq (α :=
    Over.left.{v₁, u₁} (X := terminal.{v₁, u₁} C)
        (ObjectProperty.FullSubcategory.obj (P := Over.isMono (terminal.{v₁, u₁} C))
          (ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
            (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯)) ⟶
      terminal.{v₁, u₁} C)
    (f.hom ≫
      MonoOver.arrow
        (ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
          (Over.mk (terminal.from (Y.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯))
    (MonoOver.arrow
      (ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
        (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯))

Tactic:
ext1 ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
X : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)
Z : C
f g : Z ⟶ X.obj (P := Over.isMono (terminal.{v₁, u₁} C)).left
rw : f ≫ X.arrow = g ≫ X.arrow
⊢ f = g

Tactic:
rw [← cancel_mono X.arrow]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.MonoOver.arrow
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
X : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)
Z : C
f g : Z ⟶ X.obj (P := Over.isMono (terminal.{v₁, u₁} C)).left
⊢ f ≫ X.arrow = g ≫ X.arrow

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : C
inst_1 : HasTerminal.{v₁, u₁} C
⊢ ∀ {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 (Subterminals.{v₁, u₁} C)) X ⟶
        Functor.obj.{v₁, v₁, u₁, u₁}
          (Functor.comp (D := MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))
            {
              obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                  (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
              map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
              map_comp := ⋯ }
            {
              obj := fun (X : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)) ↦
                ObjectProperty.FullSubcategory.mk (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)
                  X.obj (P := Over.isMono (terminal.{v₁, u₁} C)).left ⋯,
              map := fun {X Y : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)} (f : X ⟶ Y) ↦
                ObjectProperty.homMk (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A) f.hom.left,
              map_id := ⋯, map_comp := ⋯ })
          Y)
      (Functor.map (𝟭 (Subterminals.{v₁, u₁} C)) f ≫
        Iso.hom ((fun (X : Subterminals.{v₁, u₁} C) ↦ (Iso.refl X : X ≅ X)) Y))
      (Iso.hom ((fun (X : Subterminals.{v₁, u₁} C) ↦ (Iso.refl X : X ≅ X)) X) ≫
        Functor.map
          (Functor.comp (D := MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C))
            {
              obj := fun (X : Subterminals.{v₁, u₁} C) ↦
                ObjectProperty.FullSubcategory.mk (P := Over.isMono (terminal.{v₁, u₁} C))
                  (Over.mk (terminal.from (X.obj (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)))) ⋯,
              map := fun {X Y : Subterminals.{v₁, u₁} C} (f : X ⟶ Y) ↦ MonoOver.homMk f.hom ⋯, map_id := ⋯,
              map_comp := ⋯ : Subterminals.{v₁, u₁} C ⥤ MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C) }
            {
              obj := fun (X : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)) ↦
                ObjectProperty.FullSubcategory.mk (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A)
                  X.obj (P := Over.isMono (terminal.{v₁, u₁} C)).left ⋯,
              map := fun {X Y : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C)} (f : X ⟶ Y) ↦
                ObjectProperty.homMk (P := fun (A : C) ↦ IsSubterminal.{v₁, u₁} A) f.hom.left,
              map_id := ⋯, map_comp := ⋯ : MonoOver.{v₁, u₁} (terminal.{v₁, u₁} C) ⥤ Subterminals.{v₁, u₁} C })
          f)

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasTerminal.{v₁, u₁} C
⊢ Equivalence.functor (subterminalsEquivMonoOverTerminal C) ⋙
      MonoOver.forget (terminal.{v₁, u₁} C) ⋙ Over.forget (terminal.{v₁, u₁} C) =
    subterminalInclusion C

Tactic:
rfl

Premises used: CategoryTheory.subterminalInclusion, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.comp, CategoryTheory.inducedFunctor, CategoryTheory.InducedCategory, CategoryTheory.Subterminals, rfl
-- Module: Mathlib.CategoryTheory.Subterminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasTerminal.{v₁, u₁} C
⊢ Equivalence.inverse (subterminalsEquivMonoOverTerminal C) ⋙ subterminalInclusion C =
    MonoOver.forget (terminal.{v₁, u₁} C) ⋙ Over.forget (terminal.{v₁, u₁} C)

Tactic:
rfl

Premises used: CategoryTheory.Over, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.comp, CategoryTheory.CostructuredArrow, CategoryTheory.inducedFunctor, rfl
-- Module: Mathlib.CategoryTheory.Sums.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
X : C
⊢ obj (associator C D E) (inl (inl X)) = inl X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
X : D
⊢ obj (associator C D E) (inl (inr X)) = inr (inl X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
X : E
⊢ obj (associator C D E) (inr X) = inr (inr X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    obj (associator C D E) (obj (inl_ (C ⊕ D) E) (obj (inl_ C D) X)) ⟶
      obj (associator C D E) (obj (inl_ (C ⊕ D) E) (obj (inl_ C D) Y)))
    (Functor.map (associator C D E) (Functor.map (inl_ (C ⊕ D) E) (Functor.map (inl_ C D) f)))
    (Functor.map (inl_ C (D ⊕ E)) f)

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Sums.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
X Y : D
f : X ⟶ Y
⊢ Eq (α :=
    obj (associator C D E) (obj (inl_ (C ⊕ D) E) (obj (inr_ C D) X)) ⟶
      obj (associator C D E) (obj (inl_ (C ⊕ D) E) (obj (inr_ C D) Y)))
    (Functor.map (associator C D E) (Functor.map (inl_ (C ⊕ D) E) (Functor.map (inr_ C D) f)))
    (Functor.map (inr_ C (D ⊕ E)) (Functor.map (inl_ D E) f))

Tactic:
simp [associator]

Premises used: CategoryTheory.sum.associator
-- Module: Mathlib.CategoryTheory.Sums.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
X Y : E
f : X ⟶ Y
⊢ Eq (α := obj (associator C D E) (obj (inr_ (C ⊕ D) E) X) ⟶ obj (associator C D E) (obj (inr_ (C ⊕ D) E) Y))
    (Functor.map (associator C D E) (Functor.map (inr_ (C ⊕ D) E) f))
    (Functor.map (inr_ C (D ⊕ E)) (Functor.map (inr_ D E) f))

Tactic:
simp [associator]

Premises used: CategoryTheory.sum.associator
-- Module: Mathlib.CategoryTheory.Sums.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
X : C
⊢ obj (inverseAssociator C D E) (inl X) = inl (inl X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
X : D
⊢ obj (inverseAssociator C D E) (inr (inl X)) = inl (inr X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
X : E
⊢ obj (inverseAssociator C D E) (inr (inr X)) = inr X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.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
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    obj (inverseAssociator C D E) (obj (inl_ C (D ⊕ E)) X) ⟶ obj (inverseAssociator C D E) (obj (inl_ C (D ⊕ E)) Y))
    (Functor.map (inverseAssociator C D E) (Functor.map (inl_ C (D ⊕ E)) f))
    (Functor.map (inl_ (C ⊕ D) E) (Functor.map (inl_ C D) f))

Tactic:
simp [inverseAssociator]

Premises used: CategoryTheory.sum.inverseAssociator
-- Module: Mathlib.CategoryTheory.Sums.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
X Y : D
f : X ⟶ Y
⊢ Eq (α :=
    obj (inverseAssociator C D E) (obj (inr_ C (D ⊕ E)) (obj (inl_ D E) X)) ⟶
      obj (inverseAssociator C D E) (obj (inr_ C (D ⊕ E)) (obj (inl_ D E) Y)))
    (Functor.map (inverseAssociator C D E) (Functor.map (inr_ C (D ⊕ E)) (Functor.map (inl_ D E) f)))
    (Functor.map (inl_ (C ⊕ D) E) (Functor.map (inr_ C D) f))

Tactic:
simp [inverseAssociator]

Premises used: CategoryTheory.sum.inverseAssociator
-- Module: Mathlib.CategoryTheory.Sums.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
X Y : E
f : X ⟶ Y
⊢ Eq (α :=
    obj (inverseAssociator C D E) (obj (inr_ C (D ⊕ E)) (obj (inr_ D E) X)) ⟶
      obj (inverseAssociator C D E) (obj (inr_ C (D ⊕ E)) (obj (inr_ D E) Y)))
    (Functor.map (inverseAssociator C D E) (Functor.map (inr_ C (D ⊕ E)) (Functor.map (inr_ D E) f)))
    (Functor.map (inr_ (C ⊕ D) E) f)

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Sums.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
⊢ IsEquivalence (Equivalence.functor (associativity C D E))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sums.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
⊢ IsEquivalence (Equivalence.inverse (associativity C D E))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
Y : D
f : inl X ⟶ inr Y
⊢ False

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
Y : D
f : inr X ⟶ inl Y
⊢ False

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : {x y : C ⊕ D} → (x ⟶ y) → Sort u_1
inl : (x y : C) → (f : x ⟶ y) → P (x := obj (inl_ C D) x) (map (inl_ C D) f)
inr : (x y : D) → (f : x ⟶ y) → P (x := obj (inr_ C D) x) (map (inr_ C D) f)
x y : C
f : x ⟶ y
⊢ homInduction (P := fun (x x_1 : C ⊕ D) (x_2 : x ⟶ x_1) ↦ P x_2) inl inr (map (inl_ C D) f) = inl x y f

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
P : {x y : C ⊕ D} → (x ⟶ y) → Sort u_1
inl : (x y : C) → (f : x ⟶ y) → P (x := obj (inl_ C D) x) (map (inl_ C D) f)
inr : (x y : D) → (f : x ⟶ y) → P (x := obj (inr_ C D) x) (map (inr_ C D) f)
x y : D
f : x ⟶ y
⊢ homInduction (P := fun (x x_1 : C ⊕ D) (x_2 : x ⟶ x_1) ↦ P x_2) inl inr (map (inr_ C D) f) = inr x y 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 C
G : Functor.{v₂, v₃, u₂, u₃} B C
val : A
inl :
  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
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) x_1 with
          | Sum.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 := Sum.inl val)
      (𝟙 (Sum.inl val)) =
    F.map (𝟙 val)
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) Sum.inl val with
        | Sum.inl X => F.obj X
        | inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) Sum.inl val with
        | Sum.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
            | Sum.inl X => F.obj X
            | inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | Sum.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 := Sum.inl val)
        (𝟙 (Sum.inl val)) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) Sum.inl val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) Sum.inl val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))
    (𝟙
        (match (motive := A ⊕ B → C) Sum.inl val with
        | Sum.inl X => F.obj X
        | inr X => G.obj X) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) Sum.inl val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) Sum.inl val with
          | Sum.inl X => F.obj X
          | inr X => G.obj X :
          C))

Tactic:
simp only [← map_id]

Premises used: CategoryTheory.Functor.map_id
-- 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
val : A
⊢ 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 := inl val) (𝟙 (inl val)) =
    F.map (𝟙 val)

Tactic:
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 C
G : Functor.{v₂, v₃, u₂, u₃} B C
val : B
inr :
  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
          | Sum.inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) x_1 with
          | inl X => F.obj X
          | Sum.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 := Sum.inr val)
      (𝟙 (Sum.inr val)) =
    G.map (𝟙 val)
⊢ Eq.{v₃ + 1} (α :=
    Quiver.Hom.{v₃, u₃} (V := C)
      (match (motive := A ⊕ B → C) Sum.inr val with
        | inl X => F.obj X
        | Sum.inr X => G.obj X :
        C)
      (match (motive := A ⊕ B → C) Sum.inr val with
        | inl X => F.obj X
        | Sum.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
            | Sum.inr X => G.obj X :
            C)
          (match (motive := A ⊕ B → C) x_1 with
            | inl X => F.obj X
            | Sum.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 := Sum.inr val)
        (𝟙 (Sum.inr val)) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) Sum.inr val with
          | inl X => F.obj X
          | Sum.inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) Sum.inr val with
          | inl X => F.obj X
          | Sum.inr X => G.obj X :
          C))
    (𝟙
        (match (motive := A ⊕ B → C) Sum.inr val with
        | inl X => F.obj X
        | Sum.inr X => G.obj X) :
      Quiver.Hom.{v₃, u₃} (V := C)
        (match (motive := A ⊕ B → C) Sum.inr val with
          | inl X => F.obj X
          | Sum.inr X => G.obj X :
          C)
        (match (motive := A ⊕ B → C) Sum.inr val with
          | inl X => F.obj X
          | Sum.inr X => G.obj X :
          C))

Tactic:
simp only [← map_id]

Premises used: CategoryTheory.Functor.map_id
-- 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
val : B
⊢ 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 := inr val) (𝟙 (inr val)) =
    G.map (𝟙 val)

Tactic:
rfl