awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
m : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T
h₁ : BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₂
x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
            (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                  (fun (x : A) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                        (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                      x)
                  fun (x : B) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                      (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                    x :
              Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
          f₁ f₂))
      x
have h : ∀ (x : A),
  (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sum.inl x) =
    TypeCat.Fun.toFun (X := Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
            (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                  (fun (x : A) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                        (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                      x)
                  fun (x : B) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                      (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                    x :
              Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
          f₁ f₂))
      (Sum.inl x)
Tactic: rcases x with x | x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : Type u
⊢ Mono.{u, u + 1} (X := Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
    Functor.obj
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
      { as := WalkingPair.left : Discrete WalkingPair })
    (BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
have refine_2 : Function.Injective (α :=
  (fun (X : Type u) ↦ X) (Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair })) (β :=
  (fun (X : Type u) ↦ X)
    (Functor.obj
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
      { as := WalkingPair.left : Discrete WalkingPair }))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))) :
    (a : (fun (X : Type u) ↦ X) ((pair A B).obj { as := WalkingPair.left })) →
      (fun (X : Type u) ↦ X)
        (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).pt).obj
          { as := WalkingPair.left }))
Tactic: rw [mono_iff_injective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan.{u_2, v_1, u_1} (X ∘ Sum.inl)
c₂ : Cofan.{u_3, v_1, u_1} (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
T : C
f₁ : c₁.pt ⟶ T
f₂ : c₂.pt ⟶ T
m : (binaryCofanSum c c₁ c₂ hc₁ hc₂).pt ⟶ T
hm₁ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl ≫ m = f₁
hm₂ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr ≫ m = f₂
⊢ m =
    (fun {T : C} (f₁ : c₁.pt ⟶ T) (f₂ : c₂.pt ⟶ T) ↦
        (Cofan.IsColimit.desc hc fun (i : I₁ ⊕ I₂) ↦
            match (motive := (i : I₁ ⊕ I₂) → X i ⟶ T) i with
            | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
            | Sum.inr i₂ => c₂.inj i₂ ≫ f₂ :
          c.pt ⟶ T))
      f₁ f₂
have h : ∀ (i : I₁ ⊕ I₂),
  c.inj i ≫ m =
    c.inj i ≫
      (fun {T : C} (f₁ : c₁.pt ⟶ T) (f₂ : c₂.pt ⟶ T) ↦
          (Cofan.IsColimit.desc hc fun (i : I₁ ⊕ I₂) ↦
              match (motive := (i : I₁ ⊕ I₂) → X i ⟶ T) i with
              | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
              | Sum.inr i₂ => c₂.inj i₂ ≫ f₂ :
            c.pt ⟶ T))
        f₁ f₂
Tactic: apply Cofan.IsColimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan.{u_2, v_1, u_1} (X ∘ Sum.inl)
c₂ : Cofan.{u_3, v_1, u_1} (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst_1 : MonoCoprod.{v_1, u_1} C
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
this : inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
⊢ Mono inl
have rw : Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan.{u_2, v_1, u_1} (X ∘ Sum.inl)
c₂ : Cofan.{u_3, v_1, u_1} (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst_1 : MonoCoprod.{v_1, u_1} C
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
⊢ Mono inl
have suffices : inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
Tactic: suffices inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl by
    rw [this]
    exact MonoCoprod.binaryCofan_inl _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan.{u_2, v_1, u_1} (X ∘ Sum.inl)
c₂ : Cofan.{u_3, v_1, u_1} (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst_1 : MonoCoprod.{v_1, u_1} C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
this : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono inr
have rw : Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan.{u_2, v_1, u_1} (X ∘ Sum.inl)
c₂ : Cofan.{u_3, v_1, u_1} (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst_1 : MonoCoprod.{v_1, u_1} C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
⊢ Mono inr
have suffices : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
Tactic: suffices inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr by
    rw [this]
    exact MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan.{u_2, v_1, u_1} X
c₁ : Cofan.{u_3, v_1, u_1} (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
hc₂ : IsColimit c₂
e : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2) ≃ I :=
  Equiv.trans ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl (↑(Set.range ι)ᶜ : Type u_2)))
    (Equiv.Set.sumCompl (Set.range ι))
⊢ Mono (Y := c.pt) (Cofan.IsColimit.desc hc₁ fun (i : J) ↦ c.inj (ι i))
have refine : IsColimit (J := Discrete (Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2))) (F :=
  Discrete.functor fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
    X ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
  (Cofan.mk c.pt fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
    c.inj ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
Tactic: refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
    hc₁ hc₂ _ (by simp [e])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan.{u_2, v_1, u_1} X
c₁ : Cofan.{u_3, v_1, u_1} (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
hc₂ : IsColimit c₂
let let₁ let₂ : Mono (Y := c.pt) (Cofan.IsColimit.desc hc₁ fun (i : J) ↦ c.inj (ι i))
⊢ Mono (Y := c.pt) (Cofan.IsColimit.desc hc₁ fun (i : J) ↦ c.inj (ι i))
have let₃ : let e :=
  Equiv.trans ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl (↑(Set.range ι)ᶜ : Type u_2)))
    (Equiv.Set.sumCompl (Set.range ι));
IsColimit (J := Discrete (Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2))) (F :=
  Discrete.functor fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
    X ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
  (Cofan.mk c.pt fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
    c.inj ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
Tactic: classical
  let e := ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl _)).trans (Equiv.Set.sumCompl _)
  refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
    hc₁ hc₂ _ (by simp [e])
  exact IsColimit.ofIsoColimit ((IsColimit.ofCoconeEquiv (Cocone.equivalenceOfReindexing
    (Discrete.equivalence e) (Iso.refl _))).symm hc) (Cocone.ext (Iso.refl _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
⊢ Mono.{v_1, u_1} (C := C) (X := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Y := sigmaObj.{u_2, v_1, u_1} X)
    (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j))
have h : Eq.{v_1 + 1} (α := sigmaObj.{u_3, v_1, u_1} (X ∘ ι) ⟶ sigmaObj.{u_2, v_1, u_1} X)
  (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j)) (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j))
Tactic: convert! mono_of_injective' X ι hι
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
⊢ Eq.{v_1 + 1} (α := sigmaObj.{u_3, v_1, u_1} (X ∘ ι) ⟶ sigmaObj.{u_2, v_1, u_1} X)
    (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j)) (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j))
have h : ∀ (b : J),
  Eq.{v_1 + 1} (α := (X ∘ ι) b ⟶ sigmaObj.{u_2, v_1, u_1} X)
    (CategoryStruct.comp (Y := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Sigma.ι (X ∘ ι) b)
      (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j)))
    (CategoryStruct.comp (Y := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Sigma.ι (X ∘ ι) b)
      (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j)))
Tactic: apply Sigma.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
j : J
⊢ Eq.{v_1 + 1} (α := (X ∘ ι) j ⟶ sigmaObj.{u_2, v_1, u_1} X)
    (CategoryStruct.comp (Y := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Sigma.ι (X ∘ ι) j)
      (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j)))
    (CategoryStruct.comp (Y := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Sigma.ι (X ∘ ι) j)
      (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j)))
have h : Eq.{v_1 + 1} (α := (X ∘ ι) j ⟶ sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X (ι j))
  (NatTrans.app (Cocone.ι (Cofan.mk (sigmaObj.{u_2, v_1, u_1} X) fun (j : J) ↦ Sigma.ι X (ι j))) { as := j })
Tactic: rw [Sigma.ι_comp_map', id_comp, colimit.ι_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
X : I → C
c : Cofan.{u_2, v_1, u_1} X
h : IsColimit c
i : I
inst_2 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range fun (x : Unit) ↦ i)ᶜ : Type u_2)) ↦ X (↑k : I)
ι : Unit → I := fun (x : Unit) ↦ i
⊢ Mono (c.inj i)
have hι : Function.Injective ι
Tactic: have hι : Function.Injective ι := fun _ _ _ ↦ rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
⊢ Mono c.inl
have apply : Mono (F.map c.inl)
Tactic: apply mono_of_mono_map F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
⊢ Mono (F.map c.inl)
have change : Mono c'.inl
Tactic: change Mono c'.inl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
⊢ Mono c'.inl
have x : IsColimit c'
Tactic: apply MonoCoprod.binaryCofan_inl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
⊢ IsColimit c'
have x : IsColimit (BinaryCofan.mk c.inl c.inr)
Tactic: apply mapIsColimitOfPreservesOfIsColimit F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
⊢ IsColimit (BinaryCofan.mk c.inl c.inr)
have x : c ≅ BinaryCofan.mk c.inl c.inr
Tactic: apply IsColimit.ofIsoColimit h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
⊢ c ≅ BinaryCofan.mk c.inl c.inr
have x : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ Iso.hom (eqToIso sorry) = (BinaryCofan.mk c.inl c.inr).ι.app j
Tactic: refine Cocone.ext (φ := eqToIso rfl) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : C
inst_1 : HasCoproducts.{u, v_1, u_1} C
inst_2 : MonoCoprod.{v_1, u_1} C
J I : Type u
ι : J ⟶ I
hι : Mono ι
⊢ Mono.{v_1, u_1} (X := Functor.obj.{u, v_1, u + 1, u_1} (Functor.obj sigmaConst A) J)
    (Functor.map (Functor.obj sigmaConst A) ι)
have hι₁ : Function.Injective (α := (fun (X : Type u) ↦ X) J) (β := (fun (X : Type u) ↦ X) I)
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ι) : (a : (fun (X : Type u) ↦ X) J) → (fun (X : Type u) ↦ X) I)
Tactic: rw [mono_iff_injective] at hι
Cleared hypotheses: hι
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MorphismProperty (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
J : Type u_3
inst_2 : Category.{v_3, u_3} J
P : MorphismProperty.{v_1, u_1} T
inst_3 : P.RespectsIso
inst_4 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
⊢ Y.hom =
    hd.desc
      { pt := X,
        ι :=
          {
            app := fun (j : J) ↦
              (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
            naturality := ⋯ } }
have refine : ∀ (j : J),
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
      Y.hom =
    ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
      hd.desc
        { pt := X,
          ι :=
            {
              app := fun (j : J) ↦
                (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
              naturality := sorry } }
Tactic: refine hd.hom_ext fun j ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MorphismProperty (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
J : Type u_3
inst_2 : Category.{v_3, u_3} J
P : MorphismProperty.{v_1, u_1} T
inst_3 : P.RespectsIso
inst_4 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
j : J
⊢ ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
      Y.hom =
    ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
      hd.desc
        { pt := X,
          ι :=
            {
              app := fun (j : J) ↦
                (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
              naturality := ⋯ } }
have simp : ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone).ι.app j ≫
    Y.hom =
  (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom
Tactic: simp only [Functor.const_obj_obj, IsColimit.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MorphismProperty (hypothesis)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
A : Type u_2
inst_1 : Category.{v_2, u_2} A
L : Functor.{v_2, v_1, u_2, u_1} A T
J : Type u_3
inst_2 : Category.{v_3, u_3} J
P : MorphismProperty.{v_1, u_1} T
inst_3 : P.RespectsIso
inst_4 : PreservesColimitsOfShape.{v_3, u_3, v_2, v_1, u_2, u_1} J L
inst_5 : HasColimitsOfShape.{v_3, u_3, v_2, u_2} J A
c : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [HasColimit D] → Cocone D
hc : (D : Functor.{v_3, v_1, u_3, u_1} J T) → [inst_6 : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : Functor.{v_3, v_1, u_3, u_1} J T) [inst_6 : HasColimit D] {X : T} (s : D ⟶ Functor.obj (Functor.const J) X),
    (∀ (j : J), P (s.app j)) →
      P (X := (c D).pt) (Y := { pt := X, ι := s : Cocone D }.pt) (IsColimit.desc (hc D) { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : ObjectProperty.ColimitOfShape (MorphismProperty.costructuredArrowObj L P) J Y
hd : IsColimit
  ((proj L X ⋙ L).mapCocone d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).cocone) :=
  isColimitOfPreserves (proj L X ⋙ L) d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).isColimit
⊢ MorphismProperty.costructuredArrowObj L P Y
have heq : Y.hom =
  hd.desc
    { pt := X,
      ι :=
        {
          app := fun (j : J) ↦
            (d.toColimitPresentation (P := MorphismProperty.costructuredArrowObj L P).diag.obj j).hom,
          naturality := sorry } }
Tactic: have heq : Y.hom = hd.desc { pt := X, ι := { app j := (d.diag.obj j).hom } } := by
      refine hd.hom_ext fun j ↦ ?_
      simp only [Functor.const_obj_obj, IsColimit.fac]
      simp