awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J_1 : Type w
inst : SmallCategory J_1
inst_1 : FinCategory J_1
inst_2 : SemilatticeSup α
inst_3 : OrderBot α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasColimitsOfShape J α

Tactic:
exact { has_colimit := fun F => HasColimit.mk (finiteColimitCocone F) }
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeInf α
inst_3 : OrderTop α
F : J ⥤ α
⊢ limit F = Finset.inf Finset.univ F.obj

Tactic:
(IsLimit.conePointUniqueUpToIso (limit.isLimit F) (finiteLimitCone F).isLimit).to_eq

Premises used: CategoryTheory.Iso.to_eq, Multiset.foldr, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, Finset.fold, CategoryTheory.Limits.CompleteLattice.finiteLimitCone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, Finset.inf, CategoryTheory.Limits.LimitCone.isLimit, Multiset.fold
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeSup α
inst_3 : OrderBot α
F : J ⥤ α
⊢ colimit F = Finset.sup Finset.univ F.obj

Tactic:
(IsColimit.coconePointUniqueUpToIso (colimit.isColimit F) (finiteColimitCocone F).isColimit).to_eq

Premises used: CategoryTheory.Iso.to_eq, Multiset.foldr, Finset.fold, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone, CategoryTheory.Limits.ColimitCocone.isColimit, Finset.sup, Multiset.fold, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
trans : ∏ᶜ f = Cone.pt (F := Discrete.functor f) (LimitCone.cone (finiteLimitCone (Discrete.functor f)))
trans₁ :
  Cone.pt (F := Discrete.functor f) (LimitCone.cone (finiteLimitCone (Discrete.functor f))) = Finset.inf Finset.univ f
trans₂ : α
⊢ ∏ᶜ f = Finset.inf Finset.univ f

Tactic:
trans
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ ∏ᶜ f = Cone.pt (F := Discrete.functor f) (LimitCone.cone (finiteLimitCone (Discrete.functor f)))

Tactic:
(IsLimit.conePointUniqueUpToIso (limit.isLimit _)
          (finiteLimitCone (Discrete.functor f)).isLimit).to_eq

Premises used: CategoryTheory.Iso.to_eq, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Discrete.functor, CategoryTheory.Limits.CompleteLattice.finiteLimitCone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.LimitCone.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ ∏ᶜ f = Cone.pt (F := Discrete.functor f) (LimitCone.cone (finiteLimitCone (Discrete.functor f)))

Tactic:
exact
      (IsLimit.conePointUniqueUpToIso (limit.isLimit _)
          (finiteLimitCone (Discrete.functor f)).isLimit).to_eq

Premises used: CategoryTheory.Iso.to_eq, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Discrete.functor, CategoryTheory.Limits.CompleteLattice.finiteLimitCone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.LimitCone.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
change :
  Finset.inf (β := Discrete ι) Finset.univ (f ∘ (⇑(Equiv.toEmbedding discreteEquiv) : (a : Discrete ι) → ι)) =
    Finset.inf Fintype.elems f
⊢ Cone.pt (F := Discrete.functor f) (LimitCone.cone (finiteLimitCone (Discrete.functor f))) = Finset.inf Finset.univ f

Tactic:
change Finset.univ.inf (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.inf f

Premises used: Fintype.elems, Finset.univ, Function.comp, Equiv.toEmbedding, Finset.inf, DFunLike.coe, CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
simp : Finset.inf Finset.univ f = Finset.inf Fintype.elems f
⊢ Finset.inf (β := Discrete ι) Finset.univ (f ∘ (⇑(Equiv.toEmbedding discreteEquiv) : (a : Discrete ι) → ι)) =
    Finset.inf Fintype.elems f

Tactic:
simp only [← Finset.inf_map, Finset.univ_map_equiv_to_embedding]

Premises used: Finset.inf_map, Finset.univ_map_equiv_to_embedding
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ Finset.inf Finset.univ f = Finset.inf Fintype.elems f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
trans : ∐ f = Cocone.pt (F := Discrete.functor f) (ColimitCocone.cocone (finiteColimitCocone (Discrete.functor f)))
trans₁ :
  Cocone.pt (F := Discrete.functor f) (ColimitCocone.cocone (finiteColimitCocone (Discrete.functor f))) =
    Finset.sup Finset.univ f
trans₂ : α
⊢ ∐ f = Finset.sup Finset.univ f

Tactic:
trans
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ ∐ f = Cocone.pt (F := Discrete.functor f) (ColimitCocone.cocone (finiteColimitCocone (Discrete.functor f)))

Tactic:
(IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
          (finiteColimitCocone (Discrete.functor f)).isColimit).to_eq

Premises used: CategoryTheory.Iso.to_eq, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone, CategoryTheory.Limits.ColimitCocone.isColimit, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ ∐ f = Cocone.pt (F := Discrete.functor f) (ColimitCocone.cocone (finiteColimitCocone (Discrete.functor f)))

Tactic:
exact
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
          (finiteColimitCocone (Discrete.functor f)).isColimit).to_eq

Premises used: CategoryTheory.Iso.to_eq, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone, CategoryTheory.Limits.ColimitCocone.isColimit, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
change :
  Finset.sup (β := Discrete ι) Finset.univ (f ∘ (⇑(Equiv.toEmbedding discreteEquiv) : (a : Discrete ι) → ι)) =
    Finset.sup Fintype.elems f
⊢ Cocone.pt (F := Discrete.functor f) (ColimitCocone.cocone (finiteColimitCocone (Discrete.functor f))) =
    Finset.sup Finset.univ f

Tactic:
change Finset.univ.sup (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.sup f

Premises used: Fintype.elems, Finset.univ, Function.comp, Equiv.toEmbedding, Finset.sup, DFunLike.coe, CategoryTheory.discreteEquiv
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
simp : Finset.sup Finset.univ f = Finset.sup Fintype.elems f
⊢ Finset.sup (β := Discrete ι) Finset.univ (f ∘ (⇑(Equiv.toEmbedding discreteEquiv) : (a : Discrete ι) → ι)) =
    Finset.sup Fintype.elems f

Tactic:
simp only [← Finset.sup_map, Finset.univ_map_equiv_to_embedding]

Premises used: Finset.univ_map_equiv_to_embedding, Finset.sup_map
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ Finset.sup Finset.univ f = Finset.sup Fintype.elems f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeInf α
inst_3 : OrderTop α
this : ∀ (h : ∀ (J : Type u) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J α), HasFiniteLimits α := ⋯
⊢ ∀ (x y : α), HasLimit (pair x y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeInf α
inst_3 : OrderTop α
⊢ ∀ (x y : α), HasLimit (pair x y)

Tactic:
have : ∀ x y : α, HasLimit (pair x y) := by
    letI := hasFiniteLimits_of_hasFiniteLimits_of_size.{u} α
    infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeInf α
inst_3 : OrderTop α
this : ∀ (x y : α), HasLimit (pair x y)
⊢ HasBinaryProducts α

Tactic:
apply hasBinaryProducts_of_hasLimit_pair

Premises used: CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
x y : α
rw rw₁ : Finset.inf Finset.univ (Functor.obj (pair x y)) = Finset.inf Finset.univ (Functor.obj (pair x y))
⊢ limit (pair x y) = Finset.inf Finset.univ (Functor.obj (pair x y))

Tactic:
rw [finite_limit_eq_finset_univ_inf (pair.{u} x y)]
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
x y : α
rw rw₁ : x ⊓ y = x ⊓ y
⊢ x ⊓ (y ⊓ ⊤) = x ⊓ y

Tactic:
rw [inf_top_eq]

Premises used: inf_top_eq
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeSup α
inst_3 : OrderBot α
this : ∀ (h : ∀ (J : Type u) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape J α), HasFiniteColimits α :=
  ⋯
⊢ ∀ (x y : α), HasColimit (pair x y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeSup α
inst_3 : OrderBot α
⊢ ∀ (x y : α), HasColimit (pair x y)

Tactic:
have : ∀ x y : α, HasColimit (pair x y) := by
    letI := hasFiniteColimits_of_hasFiniteColimits_of_size.{u} α
    infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeSup α
inst_3 : OrderBot α
this : ∀ (x y : α), HasColimit (pair x y)
⊢ HasBinaryCoproducts α

Tactic:
apply hasBinaryCoproducts_of_hasColimit_pair

Premises used: CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
x y : α
rw rw₁ : Finset.sup Finset.univ (Functor.obj (pair x y)) = Finset.sup Finset.univ (Functor.obj (pair x y))
⊢ colimit (pair x y) = Finset.sup Finset.univ (Functor.obj (pair x y))

Tactic:
rw [finite_colimit_eq_finset_univ_sup (pair x y)]

Premises used: CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
x y : α
rw rw₁ : x ⊔ y = x ⊔ y
⊢ x ⊔ (y ⊔ ⊥) = x ⊔ y

Tactic:
rw [sup_bot_eq]

Premises used: sup_bot_eq
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
rw rw₁ : Finset.inf Finset.univ (cospan f g).obj = Finset.inf Finset.univ (cospan f g).obj
⊢ limit (cospan f g) = Finset.inf Finset.univ (cospan f g).obj

Tactic:
rw [finite_limit_eq_finset_univ_inf]

Premises used: CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
rw rw₁ : z ⊓ (x ⊓ y) = z ⊓ (x ⊓ y)
⊢ z ⊓ (x ⊓ (y ⊓ ⊤)) = z ⊓ (x ⊓ y)

Tactic:
rw [inf_top_eq]

Premises used: inf_top_eq
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
rw rw₁ : Finset.sup Finset.univ (span f g).obj = Finset.sup Finset.univ (span f g).obj
⊢ colimit (span f g) = Finset.sup Finset.univ (span f g).obj

Tactic:
rw [finite_colimit_eq_finset_univ_sup]

Premises used: CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
rw rw₁ : z ⊔ (x ⊔ y) = z ⊔ (x ⊔ y)
⊢ z ⊔ (x ⊔ (y ⊔ ⊥)) = z ⊔ (x ⊔ y)

Tactic:
rw [sup_bot_eq]

Premises used: sup_bot_eq
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : CompleteLattice α
J : Type w
inst_1 : Category.{w', w} J
F : Functor.{w', u, w, u} J α
s : Cone F
j : J
⊢ s.pt ≤ F.obj j

Tactic:
(s.π.app j).le

Premises used: CategoryTheory.Limits.Cone.π, Quiver.Hom.le, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : CompleteLattice α
J : Type w
inst_1 : Category.{w', w} J
F : Functor.{w', u, w, u} J α
s : Cone F
j : J
⊢ s.pt ≤ F.obj j

Tactic:
exact (s.π.app j).le

Premises used: CategoryTheory.Limits.Cone.π, Quiver.Hom.le, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : CompleteLattice α
J : Type w
inst_1 : Category.{w', w} J
F : Functor.{w', u, w, u} J α
s : Cocone F
j : J
⊢ F.obj j ≤ s.pt

Tactic:
(s.ι.app j).le

Premises used: Quiver.Hom.le, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : CompleteLattice α
J : Type w
inst_1 : Category.{w', w} J
F : Functor.{w', u, w, u} J α
s : Cocone F
j : J
⊢ F.obj j ≤ s.pt

Tactic:
exact (s.ι.app j).le

Premises used: Quiver.Hom.le, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : CompleteLattice α
J : Type w
inst_1 : Category.{w', w} J
F : Functor.{w', u, w, u} J α
⊢ limit F = iInf F.obj

Tactic:
(IsLimit.conePointUniqueUpToIso (limit.isLimit F) (limitCone F).isLimit).to_eq

Premises used: CategoryTheory.Iso.to_eq, iInf, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.CompleteLattice.limitCone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.LimitCone.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
inst : CompleteLattice α
J : Type w
inst_1 : Category.{w', w} J
F : Functor.{w', u, w, u} J α
⊢ colimit F = iSup F.obj

Tactic:
(IsColimit.coconePointUniqueUpToIso (colimit.isColimit F) (colimitCocone F).isColimit).to_eq

Premises used: CategoryTheory.Iso.to_eq, iSup, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.CompleteLattice.colimitCocone, CategoryTheory.Limits.colimit, CategoryTheory.Limits.ColimitCocone.isColimit, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A B : C
c : BinaryCofan.{v_1, u_1} A B
hc : IsColimit c
⊢ IsSplitMono c.inl

Tactic:
haveI : IsSplitMono c.inl :=
      IsSplitMono.mk' (SplitMono.mk (BinaryCofan.IsColimit.desc hc (𝟙 A) 0) (IsColimit.fac _ _ _))
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
A B : C
c : BinaryCofan.{v_1, u_1} A B
hc : IsColimit c
this : IsSplitMono c.inl
⊢ Mono c.inl

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
inst_1 : MonoCoprod.{v_1, u_1} C
c : BinaryCofan.{v_1, u_1} A B
hc : IsColimit c
⊢ ∀ {T : C} (f : Functor.obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair } ⟶ T)
    (g : Functor.obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair } ⟶ T),
    (BinaryCofan.mk c.inr c.inl).inl ≫
        (fun {T : C}
              (f₁ : Functor.obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair } ⟶ T)
              (f₂ : Functor.obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair } ⟶ T) ↦
            BinaryCofan.IsColimit.desc hc f₂ f₁)
          f g =
      f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
inst_1 : MonoCoprod.{v_1, u_1} C
c : BinaryCofan.{v_1, u_1} A B
hc : IsColimit c
⊢ ∀ {T : C} (f : Functor.obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair } ⟶ T)
    (g : Functor.obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair } ⟶ T),
    (BinaryCofan.mk c.inr c.inl).inr ≫
        (fun {T : C}
              (f₁ : Functor.obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair } ⟶ T)
              (f₂ : Functor.obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair } ⟶ T) ↦
            BinaryCofan.IsColimit.desc hc f₂ f₁)
          f g =
      g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
inst_1 : MonoCoprod.{v_1, u_1} C
c : BinaryCofan.{v_1, u_1} A B
hc : IsColimit c
haveI : ∀ (hc' : IsColimit (BinaryCofan.mk c.inr c.inl)), Mono c.inr
⊢ Mono c.inr

Tactic:
haveI hc' : IsColimit (BinaryCofan.mk c.inr c.inl) :=
    BinaryCofan.IsColimit.mk _
      (fun f₁ f₂ => BinaryCofan.IsColimit.desc (s := c) hc f₂ f₁)
      (by simp) (by simp)
      (fun f₁ f₂ m h₁ h₂ => BinaryCofan.IsColimit.hom_ext hc (by cat_disch) (by cat_disch))
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
inst_1 : MonoCoprod.{v_1, u_1} C
c : BinaryCofan.{v_1, u_1} A B
hc : IsColimit c
hc' : IsColimit (BinaryCofan.mk c.inr c.inl)
⊢ Mono c.inr

Tactic:
binaryCofan_inl _ hc'

Premises used: CategoryTheory.Limits.MonoCoprod.binaryCofan_inl, CategoryTheory.Discrete.functor, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
inst_1 : MonoCoprod.{v_1, u_1} C
c : BinaryCofan.{v_1, u_1} A B
hc : IsColimit c
hc' : IsColimit (BinaryCofan.mk c.inr c.inl)
⊢ Mono c.inr

Tactic:
exact binaryCofan_inl _ hc'

Premises used: CategoryTheory.Limits.MonoCoprod.binaryCofan_inl
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
inst_1 : MonoCoprod.{v_1, u_1} C
inst_2 : HasBinaryCoproduct.{v_1, u_1} A B
⊢ Mono.{v_1, u_1} (C := C) (X := A) (Y := coprod.{v_1, u_1} A B) coprod.inl

Tactic:
binaryCofan_inl _ (colimit.isColimit _)

Premises used: CategoryTheory.Limits.MonoCoprod.binaryCofan_inl, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
inst_1 : MonoCoprod.{v_1, u_1} C
inst_2 : HasBinaryCoproduct.{v_1, u_1} A B
⊢ Mono.{v_1, u_1} (C := C) (X := B) (Y := coprod.{v_1, u_1} A B) coprod.inr

Tactic:
binaryCofan_inr _ (colimit.isColimit _)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.MonoCoprod.binaryCofan_inr, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
c₁ c₂ : BinaryCofan.{v_1, u_1} A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : ∀ (c₁ c₂ : BinaryCofan.{v_1, u_1} A B) (x : IsColimit c₁) (x : IsColimit c₂), Mono c₁.inl → Mono c₂.inl
⊢ Mono c₁.inl ↔ Mono c₂.inl

Tactic:
⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
c₁ c₂ : BinaryCofan.{v_1, u_1} A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : ∀ (c₁ c₂ : BinaryCofan.{v_1, u_1} A B) (x : IsColimit c₁) (x : IsColimit c₂), Mono c₁.inl → Mono c₂.inl
⊢ Mono c₁.inl ↔ Mono c₂.inl

Tactic:
exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
c₁ c₂ : BinaryCofan.{v_1, u_1} A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
c₃ : ∀ (c₁ c₂ : BinaryCofan.{v_1, u_1} A B) (x : IsColimit c₁) (x : IsColimit c₂), Mono c₁.inl → Mono c₂.inl
⊢ Mono c₁.inl ↔ Mono c₂.inl

Tactic:
suffices
    ∀ (c₁ c₂ : BinaryCofan A B) (_ : IsColimit c₁) (_ : IsColimit c₂) (_ : Mono c₁.inl),
      Mono c₂.inl
    by exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
c₁_1 c₂_1 : BinaryCofan.{v_1, u_1} A B
hc₁_1 : IsColimit c₁_1
hc₂_1 : IsColimit c₂_1
c₁ c₂ : BinaryCofan.{v_1, u_1} A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
_ : Mono c₁.inl → Mono c₂.inl
⊢ Mono c₁.inl → Mono c₂.inl

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : C
c₁_1 c₂_1 : BinaryCofan.{v_1, u_1} A B
hc₁_1 : IsColimit c₁_1
hc₂_1 : IsColimit c₂_1
c₁ c₂ : BinaryCofan.{v_1, u_1} A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
h : Mono c₁.inl
⊢ Mono c₂.inl

Tactic:
simpa only [IsColimit.comp_coconePointUniqueUpToIso_hom] using
    mono_comp c₁.inl (hc₁.coconePointUniqueUpToIso hc₂).hom

Premises used: CategoryTheory.mono_comp, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.BinaryCofan.inl, CategoryTheory.Iso.hom, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (A B : C), ∃ (c : BinaryCofan.{v_1, u_1} A B) (x : IsColimit c), Mono c.inl
A B : C
c' : BinaryCofan.{v_1, u_1} A B
hc' : IsColimit c'
obtain : ∀ (c : BinaryCofan.{v_1, u_1} A B) (hc₁ : IsColimit c) (hc₂ : Mono c.inl), Mono c'.inl
⊢ Mono c'.inl

Tactic:
obtain ⟨c, hc₁, hc₂⟩ := h A B
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : ∀ (A B : C), ∃ (c : BinaryCofan.{v_1, u_1} A B) (x : IsColimit c), Mono c.inl
A B : C
c' : BinaryCofan.{v_1, u_1} A B
hc' : IsColimit c'
c : BinaryCofan.{v_1, u_1} A B
hc₁ : IsColimit c
hc₂ : Mono c.inl
⊢ Mono c'.inl

Tactic:
simpa only [mono_inl_iff hc' hc₁] using hc₂

Premises used: CategoryTheory.Limits.MonoCoprod.mono_inl_iff
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : Type u
⊢ ∃ (c : BinaryCofan A B) (x : IsColimit c), Mono c.inl

Tactic:
⟨BinaryCofan.mk (↾(Sum.inl : A → A ⊕ B))
      (↾Sum.inr), ?_, ?_⟩

Premises used: TypeCat.ofHom, Sum.inl, Sum.inr, CategoryTheory.Limits.BinaryCofan.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : Type u
refine_1 : IsColimit (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))
refine_2 :
  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)))
⊢ ∃ (c : BinaryCofan A B) (x : IsColimit c), Mono c.inl

Tactic:
refine ⟨BinaryCofan.mk (↾(Sum.inl : A → A ⊕ B))
      (↾Sum.inr), ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))
inl : (x : A) → T
inr : (x : B) → T
⊢ T

Tactic:
rcases x with x | x
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
x : A
⊢ T

Tactic:
exacts [f₁ x, f₂ x]

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe