awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val : ι₁
inl :
  Eq (α := Sum.elim f₁ f₂ (Sum.inl val) ⟶ s.pt)
    (c₁.inj val ≫
      NatTrans.app
        (Cocone.ι
          (mk s.pt fun (i : WalkingPair) ↦
            WalkingPair.rec (motive := fun (t : WalkingPair) ↦
              (h : i = t) → WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i ⟶ s.pt)
              (fun (h : i = WalkingPair.left) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                  WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                  (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
              (fun (h : i = WalkingPair.right) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                  WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                  (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
              i ⋯))
        { as := WalkingPair.left })
    (s.inj (Sum.inl val))
⊢ Eq (α := Sum.elim f₁ f₂ (Sum.inl val) ⟶ s.pt)
    (c₁.inj val ≫
      bc.inl ≫
        IsColimit.desc h fun (i : WalkingPair) ↦
          WalkingPair.rec (motive := fun (t : WalkingPair) ↦
            (h : i = t) → WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i ⟶ s.pt)
            (fun (h : i = WalkingPair.left) ↦
              Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
            (fun (h : i = WalkingPair.right) ↦
              Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
            i ⋯)
    (s.inj (Sum.inl val))

Tactic:
erw [h.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val : ι₁
⊢ Eq (α := Sum.elim f₁ f₂ (Sum.inl val) ⟶ s.pt)
    (c₁.inj val ≫
      NatTrans.app
        (Cocone.ι
          (mk s.pt fun (i : WalkingPair) ↦
            WalkingPair.rec (motive := fun (t : WalkingPair) ↦
              (h : i = t) → WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i ⟶ s.pt)
              (fun (h : i = WalkingPair.left) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                  WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                  (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
              (fun (h : i = WalkingPair.right) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                  WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                  (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
              i ⋯))
        { as := WalkingPair.left })
    (s.inj (Sum.inl val))

Tactic:
simp only [Cofan.mk_ι_app, Cofan.IsColimit.fac]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val : ι₂
inr :
  Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
    (c₂.inj val ≫
      bc.inr ≫
        IsColimit.desc h fun (i : WalkingPair) ↦
          WalkingPair.rec (motive := fun (t : WalkingPair) ↦
            (h : i = t) → WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i ⟶ s.pt)
            (fun (h : i = WalkingPair.left) ↦
              Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
            (fun (h : i = WalkingPair.right) ↦
              Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
            i ⋯)
    (s.inj (Sum.inr val))
⊢ Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
    ((mk bc.pt (c₁.combPairHoms c₂ bc)).inj (Sum.inr val) ≫
      (fun (s : Cofan (Sum.elim f₁ f₂)) ↦
          (IsColimit.desc h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
                ⋯ :
            bc.pt ⟶ s.pt))
        s)
    (s.inj (Sum.inr val))

Tactic:
simp only [cofan_mk_inj, combPairHoms, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofan.combPairHoms, CategoryTheory.Limits.cofan_mk_inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val : ι₂
inr :
  Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
    (c₂.inj val ≫
      NatTrans.app
        (Cocone.ι
          (mk s.pt fun (i : WalkingPair) ↦
            WalkingPair.rec (motive := fun (t : WalkingPair) ↦
              (h : i = t) → WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i ⟶ s.pt)
              (fun (h : i = WalkingPair.left) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                  WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                  (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
              (fun (h : i = WalkingPair.right) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                  WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                  (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
              i ⋯))
        { as := WalkingPair.right })
    (s.inj (Sum.inr val))
⊢ Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
    (c₂.inj val ≫
      bc.inr ≫
        IsColimit.desc h fun (i : WalkingPair) ↦
          WalkingPair.rec (motive := fun (t : WalkingPair) ↦
            (h : i = t) → WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i ⟶ s.pt)
            (fun (h : i = WalkingPair.left) ↦
              Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
            (fun (h : i = WalkingPair.right) ↦
              Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
            i ⋯)
    (s.inj (Sum.inr val))

Tactic:
erw [h.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
val : ι₂
⊢ Eq (α := Sum.elim f₁ f₂ (Sum.inr val) ⟶ s.pt)
    (c₂.inj val ≫
      NatTrans.app
        (Cocone.ι
          (mk s.pt fun (i : WalkingPair) ↦
            WalkingPair.rec (motive := fun (t : WalkingPair) ↦
              (h : i = t) → WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i ⟶ s.pt)
              (fun (h : i = WalkingPair.left) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                  WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                  (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
              (fun (h : i = WalkingPair.right) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                  WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x ⟶ s.pt)
                  (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
              i ⋯))
        { as := WalkingPair.right })
    (s.inj (Sum.inr val))

Tactic:
simp only [Cofan.mk_ι_app, Cofan.IsColimit.fac]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
a : ι₁
⊢ c₁.inj a ≫ inj bc WalkingPair.left ≫ m =
    c₁.inj a ≫
      inj bc WalkingPair.left ≫
        (fun (s : Cofan (Sum.elim f₁ f₂)) ↦
            (IsColimit.desc h fun (i : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                  (h : i = t) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt) i
                  (fun (h : i = WalkingPair.left) ↦
                    Eq.ndrec (motive := fun (i : WalkingPair) ↦
                      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                      (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
                  (fun (h : i = WalkingPair.right) ↦
                    Eq.ndrec (motive := fun (i : WalkingPair) ↦
                      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                      (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
                  ⋯ :
              bc.pt ⟶ s.pt))
          s

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
⊢ inj bc WalkingPair.left ≫ m =
    inj bc WalkingPair.left ≫
      (fun (s : Cofan (Sum.elim f₁ f₂)) ↦
          (IsColimit.desc h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
                ⋯ :
            bc.pt ⟶ s.pt))
        s

Tactic:
refine Cofan.IsColimit.hom_ext h₁ _ _ (fun a ↦ by aesop)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
a : ι₂
⊢ c₂.inj a ≫ inj bc WalkingPair.right ≫ m =
    c₂.inj a ≫
      inj bc WalkingPair.right ≫
        (fun (s : Cofan (Sum.elim f₁ f₂)) ↦
            (IsColimit.desc h fun (i : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                  (h : i = t) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt) i
                  (fun (h : i = WalkingPair.left) ↦
                    Eq.ndrec (motive := fun (i : WalkingPair) ↦
                      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                      (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
                  (fun (h : i = WalkingPair.right) ↦
                    Eq.ndrec (motive := fun (i : WalkingPair) ↦
                      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                      (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
                  ⋯ :
              bc.pt ⟶ s.pt))
          s

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Cofan.{u_1, u₂, u₁} f₁
c₂ : Cofan.{u_2, u₂, u₁} f₂
bc : BinaryCofan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsColimit c₁
h₂ : IsColimit c₂
h : IsColimit bc
s : Cofan (Sum.elim f₁ f₂)
m : (mk bc.pt (c₁.combPairHoms c₂ bc)).pt ⟶ s.pt
hm : ∀ (j : ι₁ ⊕ ι₂), (mk bc.pt (c₁.combPairHoms c₂ bc)).inj j ≫ m = s.inj j
⊢ inj bc WalkingPair.right ≫ m =
    inj bc WalkingPair.right ≫
      (fun (s : Cofan (Sum.elim f₁ f₂)) ↦
          (IsColimit.desc h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₁ fun (a : ι₁) ↦ s.inj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt ⟶ s.pt)
                    (IsColimit.desc h₂ fun (a : ι₂) ↦ s.inj (Sum.inr a)) ⋯)
                ⋯ :
            bc.pt ⟶ s.pt))
        s

Tactic:
refine Cofan.IsColimit.hom_ext h₂ _ _ (fun a ↦ by aesop)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
J : Type w
F : J → C
inst_3 : HasProduct.{w, v, u} F
inst_4 : PreservesLimit (Discrete.functor F) (forget C (FC := FC) (CC := CC))
x : ToType (FC := FC) (CC := CC) (piObj.{w, v, u} F)
j : J
⊢ Eq (α := ToType (FC := FC) (CC := CC) (F j))
    ((productEquiv (FC := FC) (CC := CC) F : (a : ToType (∏ᶜ F)) → (j : J) → ToType (F j)) x j :
      ToType (FC := FC) (CC := CC) (F j))
    ((hom (FC := FC) (CC := CC) (Pi.π F j) : (a : CC (∏ᶜ F)) → CC (F j)) x : CC (F j))

Tactic:
congr_hom (piComparison_comp_π (forget C) F j) x

Premises used: CategoryTheory.Limits.piComparison_comp_π, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
J : Type w
F : J → C
inst_3 : HasProduct.{w, v, u} F
inst_4 : PreservesLimit (Discrete.functor F) (forget C (FC := FC) (CC := CC))
x : (j : J) → ToType (FC := FC) (CC := CC) (F j)
j : J
rw :
  (productEquiv (FC := FC) (CC := CC) F : (a : ToType (∏ᶜ F)) → (j : J) → ToType (F j))
      ((Equiv.symm (productEquiv (FC := FC) (CC := CC) F) : (a : (j : J) → ToType (F j)) → ToType (∏ᶜ F)) x :
        ToType (FC := FC) (CC := CC) (piObj.{w, v, u} F))
      j =
    x j
rw₁ rw₂ : x j = x j
⊢ (hom (FC := FC) (CC := CC) (Pi.π F j) : (a : CC (∏ᶜ F)) → CC (F j))
      ((Equiv.symm (productEquiv (FC := FC) (CC := CC) F) : (a : (j : J) → ToType (F j)) → ToType (∏ᶜ F)) x) =
    x j

Tactic:
rw [← productEquiv_apply_apply, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Limits.Concrete.productEquiv_apply_apply
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
f : J → C
inst_1 : HasProduct.{w, v, u} f
D : Type t
inst_2 : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst_4 : ConcreteCategory D FD (CC := DD)
F : Functor.{v, r, u, t} C D
inst_5 : PreservesLimit (Discrete.functor f) F
inst_6 : HasProduct.{w, r, t} (C := D) fun (j : J) ↦ F.obj (f j)
inst_7 : PreservesLimitsOfShape WalkingCospan (forget D (FC := FD) (CC := DD))
inst_8 : PreservesLimit (J := Discrete J) (Discrete.functor fun (b : J) ↦ F.obj (f b)) (forget D (FC := FD) (CC := DD))
x y : ToType (FC := FD) (CC := DD) (F.obj (piObj.{w, v, u} f))
h :
  ∀ (i : J),
    Eq (α := DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) x : DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) y : DD (F.obj (f i)))
a :
  Eq (α := DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
    ((hom (FC := FD) (CC := DD) (Iso.hom (PreservesProduct.iso F f)) :
          (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (j : J) ↦ F.obj (f j)))
        x :
      DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
    ((hom (FC := FD) (CC := DD) (Iso.hom (PreservesProduct.iso F f)) :
          (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (j : J) ↦ F.obj (f j)))
        y :
      DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
⊢ x = y

Tactic:
apply ConcreteCategory.injective_of_mono_of_preservesPullback (PreservesProduct.iso F f).hom

Premises used: CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback, CategoryTheory.Limits.PreservesProduct.iso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
f : J → C
inst_1 : HasProduct.{w, v, u} f
D : Type t
inst_2 : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst_3 : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst_4 : ConcreteCategory D FD (CC := DD)
F : Functor.{v, r, u, t} C D
inst_5 : PreservesLimit (Discrete.functor f) F
inst_6 : HasProduct.{w, r, t} (C := D) fun (j : J) ↦ F.obj (f j)
inst_7 : PreservesLimitsOfShape WalkingCospan (forget D (FC := FD) (CC := DD))
inst_8 : PreservesLimit (J := Discrete J) (Discrete.functor fun (b : J) ↦ F.obj (f b)) (forget D (FC := FD) (CC := DD))
x y : ToType (FC := FD) (CC := DD) (F.obj (piObj.{w, v, u} f))
h :
  ∀ (i : J),
    Eq (α := DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) x : DD (F.obj (f i)))
      ((hom (FC := FD) (CC := DD) (F.map (Pi.π f i)) : (a : DD (F.obj (∏ᶜ f))) → DD (F.obj (f i))) y : DD (F.obj (f i)))
a :
  ∀ (j : Discrete J),
    Eq (α := DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) j))
      ((hom (FC := FD) (CC := DD) (limit.π (Discrete.functor fun (b : J) ↦ F.obj (f b)) j) :
            (a : DD (limit (Discrete.functor fun (b : J) ↦ F.obj (f b)))) →
              DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj j))
          ((hom (FC := FD) (CC := DD) (piComparison F f) : (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (b : J) ↦ F.obj (f b)))
            x) :
        DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) j))
      ((hom (FC := FD) (CC := DD) (limit.π (Discrete.functor fun (b : J) ↦ F.obj (f b)) j) :
            (a : DD (limit (Discrete.functor fun (b : J) ↦ F.obj (f b)))) →
              DD ((Discrete.functor fun (b : J) ↦ F.obj (f b)).obj j))
          ((hom (FC := FD) (CC := DD) (piComparison F f) : (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (b : J) ↦ F.obj (f b)))
            y) :
        DD (Functor.obj.{w, r, w, t} (Discrete.functor fun (b : J) ↦ F.obj (f b)) j))
⊢ Eq (α := DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
    ((hom (FC := FD) (CC := DD) (Iso.hom (PreservesProduct.iso F f)) :
          (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (j : J) ↦ F.obj (f j)))
        x :
      DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))
    ((hom (FC := FD) (CC := DD) (Iso.hom (PreservesProduct.iso F f)) :
          (a : DD (F.obj (∏ᶜ f))) → DD (∏ᶜ fun (j : J) ↦ F.obj (f j)))
        y :
      DD (piObj.{w, r, t} fun (j : J) ↦ F.obj (f j)))

Tactic:
apply Concrete.limit_ext _ (piComparison F _ x) (piComparison F _ y)

Premises used: CategoryTheory.Limits.piComparison, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Concrete.limit_ext, DFunLike.coe