awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ Eq (α := F ⟶ obj (const J) Y) ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) f : F ⟶ obj (const J) Y)
    ((h.homEquiv : (a : X ⟶ X) → F ⟶ (const J).obj X) (𝟙 X) ≫ Functor.map (const J) f : F ⟶ obj (const J) Y)
have e_ι : Eq (α := F ⟶ obj (const J) Y) ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) (𝟙 X ≫ f) : F ⟶ obj (const J) Y)
  ((h.homEquiv : (a : X ⟶ X) → F ⟶ (const J).obj X) (𝟙 X) ≫ Functor.map (const J) f : F ⟶ obj (const J) Y)
Tactic: conv_lhs => rw [← Category.id_comp f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (X := s.pt) (homOfCocone h s) = s
have rw : (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt) (homOfCocone h (coconeOfHom h (homOfCocone h s))) =
  coconeOfHom h (homOfCocone h s)
Tactic: rw [← coconeOfHom_homOfCocone h s]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
| (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt) (homOfCocone h (coconeOfHom h (homOfCocone h s)))
have simp : (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt) (homOfCocone h s)
Tactic: simp only [homOfCocone_coconeOfHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt)
      (homOfCocone h (coconeOfHom h (homOfCocone h s))) =
    coconeOfHom h (homOfCocone h s)
have conv_lhs : (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt) (homOfCocone h s) = coconeOfHom h (homOfCocone h s)
Tactic: conv_lhs => simp only [homOfCocone_coconeOfHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
j : J
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h s = s.ι.app j
have h₁ : (colimitCocone h).extend (X := s.pt) (homOfCocone h s) = s
Tactic: have h := cocone_fac h s
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h_1 : F.cocones.CorepresentableBy X
s : Cocone F
j : J
h : (colimitCocone h_1).extend (X := s.pt) (homOfCocone h_1 s) = s
⊢ (colimitCocone h_1).ι.app j ≫ homOfCocone h_1 s = s.ι.app j
have mk : ∀ (pt : C) (ι : F ⟶ obj (const J) pt)
  (h :
    (colimitCocone h_1).extend (X := { pt := pt, ι := ι : Cocone F }.pt)
        (homOfCocone h_1 { pt := pt, ι := ι : Cocone F }) =
      { pt := pt, ι := ι }),
  (colimitCocone h_1).ι.app j ≫ homOfCocone h_1 { pt := pt, ι := ι } = { pt := pt, ι := ι : Cocone F }.ι.app j
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h_1 : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h :
  (colimitCocone h_1).extend (X := { pt := pt, ι := ι : Cocone F }.pt)
      (homOfCocone h_1 { pt := pt, ι := ι : Cocone F }) =
    { pt := pt, ι := ι }
⊢ (colimitCocone h_1).ι.app j ≫ homOfCocone h_1 { pt := pt, ι := ι } = { pt := pt, ι := ι : Cocone F }.ι.app j
have h₁ : { pt := pt, ι := ι : Cocone F }.pt = pt
Tactic: injection h with h₁ h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h_1 : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h :
  (colimitCocone h_1).extend (X := { pt := pt, ι := ι : Cocone F }.pt)
      (homOfCocone h_1 { pt := pt, ι := ι : Cocone F }) =
    { pt := pt, ι := ι }
h₁ : { pt := pt, ι := ι : Cocone F }.pt = pt
⊢ (colimitCocone h_1).ι.app j ≫ homOfCocone h_1 { pt := pt, ι := ι } = { pt := pt, ι := ι : Cocone F }.ι.app j
have h₂ : (colimitCocone h_1).ι ≫ Functor.map (const J) (homOfCocone h_1 { pt := pt, ι := ι }) = ι
Tactic: injection h with h₁ h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h₁ : { pt := pt, ι := ι : Cocone F }.pt = pt
h₂ : (colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) = ι
| { pt := pt, ι := ι : Cocone F }.ι.app j
have rw : NatTrans.app
  (Cocone.ι
    { pt := pt,
      ι := ((colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) : F ⟶ obj (const J) pt) })
  j
Tactic: rw [← h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h₁ : { pt := pt, ι := ι : Cocone F }.pt = pt
h₂ : (colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) = ι
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h { pt := pt, ι := ι } = { pt := pt, ι := ι : Cocone F }.ι.app j
have mk : Eq (α := F.obj j ⟶ { pt := pt, ι := ι : Cocone F }.pt) ((colimitCocone h).ι.app j ≫ homOfCocone h { pt := pt, ι := ι })
  (NatTrans.app
    (Cocone.ι
      { pt := pt,
        ι :=
          ((colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) : F ⟶ obj (const J) pt) })
    j)
Tactic: conv_rhs => rw [← h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ m = homOfCocone h s
have rw : homOfCocone h (coconeOfHom h m) = homOfCocone h s
Tactic: rw [← homOfCocone_coconeOfHom h m]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ homOfCocone h (coconeOfHom h m) = homOfCocone h s
have h₁ : coconeOfHom h m = s
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ coconeOfHom h m = s
have h₁ : (colimitCocone h).extend m = s
Tactic: rw [coconeOfHom_fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ { pt := s.pt, ι := (colimitCocone h).ι ≫ Functor.map (const J) m : Cocone F } = s
have h₁ : ∀ (pt : C) (ι : F ⟶ obj (const J) pt) (m : (colimitCocone h).pt ⟶ { pt := pt, ι := ι : Cocone F }.pt)
  (w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt, ι := ι }.ι.app j),
  { pt := { pt := pt, ι := ι : Cocone F }.pt, ι := (colimitCocone h).ι ≫ Functor.map (const J) m : Cocone F } =
    { pt := pt, ι := ι }
Tactic: cases s
Cleared hypotheses: s, m, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
pt : C
ι : F ⟶ obj (const J) pt
m : (colimitCocone h).pt ⟶ { pt := pt, ι := ι : Cocone F }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt, ι := ι }.ι.app j
⊢ { pt := { pt := pt, ι := ι : Cocone F }.pt, ι := (colimitCocone h).ι ≫ Functor.map (const J) m : Cocone F } =
    { pt := pt, ι := ι }
have h₁ : ∀ (j : J), ((colimitCocone h).ι ≫ Functor.map (const J) m).app j = ι.app j
Tactic: congr with j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ ∏ᶜ f = Finset.inf Finset.univ f
have trans : ∏ᶜ f = Cone.pt (F := Discrete.functor f) (LimitCone.cone (finiteLimitCone (Discrete.functor f)))
Tactic: trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
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)))
⊢ ∏ᶜ f = Finset.inf Finset.univ f
have trans₁ : Cone.pt (F := Discrete.functor f) (LimitCone.cone (finiteLimitCone (Discrete.functor f))) = Finset.inf Finset.univ f
Tactic: trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
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
⊢ ∏ᶜ f = Finset.inf Finset.univ f
have trans₂ : α
Tactic: trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ Cone.pt (F := Discrete.functor f) (LimitCone.cone (finiteLimitCone (Discrete.functor f))) = Finset.inf Finset.univ f
have change : Finset.inf (β := Discrete ι) Finset.univ (f ∘ (⇑(Equiv.toEmbedding discreteEquiv) : (a : Discrete ι) → ι)) =
  Finset.inf Fintype.elems f
Tactic: change Finset.univ.inf (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.inf f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ Finset.inf (β := Discrete ι) Finset.univ (f ∘ (⇑(Equiv.toEmbedding discreteEquiv) : (a : Discrete ι) → ι)) =
    Finset.inf Fintype.elems f
have simp : Finset.inf Finset.univ f = Finset.inf Fintype.elems f
Tactic: simp only [← Finset.inf_map, Finset.univ_map_equiv_to_embedding]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ ∐ f = Finset.sup Finset.univ f
have trans : ∐ f = Cocone.pt (F := Discrete.functor f) (ColimitCocone.cocone (finiteColimitCocone (Discrete.functor f)))
Tactic: trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
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)))
⊢ ∐ f = Finset.sup Finset.univ f
have trans₁ : Cocone.pt (F := Discrete.functor f) (ColimitCocone.cocone (finiteColimitCocone (Discrete.functor f))) =
  Finset.sup Finset.univ f
Tactic: trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
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
⊢ ∐ f = Finset.sup Finset.univ f
have trans₂ : α
Tactic: trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ Cocone.pt (F := Discrete.functor f) (ColimitCocone.cocone (finiteColimitCocone (Discrete.functor f))) =
    Finset.sup Finset.univ f
have change : Finset.sup (β := Discrete ι) Finset.univ (f ∘ (⇑(Equiv.toEmbedding discreteEquiv) : (a : Discrete ι) → ι)) =
  Finset.sup Fintype.elems f
Tactic: change Finset.univ.sup (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.sup f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
ι : Type u
inst_2 : Fintype ι
f : ι → α
⊢ Finset.sup (β := Discrete ι) Finset.univ (f ∘ (⇑(Equiv.toEmbedding discreteEquiv) : (a : Discrete ι) → ι)) =
    Finset.sup Fintype.elems f
have simp : Finset.sup Finset.univ f = Finset.sup Fintype.elems f
Tactic: simp only [← Finset.sup_map, Finset.univ_map_equiv_to_embedding]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (hypothesis)
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeInf α
inst_3 : OrderTop α
⊢ HasBinaryProducts α
have this : ∀ (x y : α), HasLimit (pair x y)
Tactic: have : ∀ x y : α, HasLimit (pair x y) := by
    letI := hasFiniteLimits_of_hasFiniteLimits_of_size.{u} α
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
x y : α
⊢ limit (pair x y) = Finset.inf Finset.univ (Functor.obj (pair x y))
have rw : Finset.inf Finset.univ (Functor.obj (pair x y)) = Finset.inf Finset.univ (Functor.obj (pair x y))
Tactic: rw [finite_limit_eq_finset_univ_inf (pair.{u} x y)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
x y : α
⊢ x ⊓ (y ⊓ ⊤) = x ⊓ y
have rw : x ⊓ y = x ⊓ y
Tactic: rw [inf_top_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (hypothesis)
Goal:
α : Type u
J : Type w
inst : SmallCategory J
inst_1 : FinCategory J
inst_2 : SemilatticeSup α
inst_3 : OrderBot α
⊢ HasBinaryCoproducts α
have this : ∀ (x y : α), HasColimit (pair x y)
Tactic: have : ∀ x y : α, HasColimit (pair x y) := by
    letI := hasFiniteColimits_of_hasFiniteColimits_of_size.{u} α
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
x y : α
⊢ colimit (pair x y) = Finset.sup Finset.univ (Functor.obj (pair x y))
have rw : Finset.sup Finset.univ (Functor.obj (pair x y)) = Finset.sup Finset.univ (Functor.obj (pair x y))
Tactic: rw [finite_colimit_eq_finset_univ_sup (pair x y)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
x y : α
⊢ x ⊔ (y ⊔ ⊥) = x ⊔ y
have rw : x ⊔ y = x ⊔ y
Tactic: rw [sup_bot_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ limit (cospan f g) = Finset.inf Finset.univ (cospan f g).obj
have rw : Finset.inf Finset.univ (cospan f g).obj = Finset.inf Finset.univ (cospan f g).obj
Tactic: rw [finite_limit_eq_finset_univ_inf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : OrderTop α
x y z : α
f : x ⟶ z
g : y ⟶ z
⊢ z ⊓ (x ⊓ (y ⊓ ⊤)) = z ⊓ (x ⊓ y)
have rw : z ⊓ (x ⊓ y) = z ⊓ (x ⊓ y)
Tactic: rw [inf_top_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ colimit (span f g) = Finset.sup Finset.univ (span f g).obj
have rw : Finset.sup Finset.univ (span f g).obj = Finset.sup Finset.univ (span f g).obj
Tactic: rw [finite_colimit_eq_finset_univ_sup]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ z ⊔ (x ⊔ (y ⊔ ⊥)) = z ⊔ (x ⊔ y)
have rw : z ⊔ (x ⊔ y) = z ⊔ (x ⊔ y)
Tactic: rw [sup_bot_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (hypothesis)
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
⊢ Mono c.inl
have this : IsSplitMono c.inl
Tactic: haveI : IsSplitMono c.inl :=
      IsSplitMono.mk' (SplitMono.mk (BinaryCofan.IsColimit.desc hc (𝟙 A) 0) (IsColimit.fac _ _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
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
⊢ Mono c.inr
have haveI : ∀ (hc' : IsColimit (BinaryCofan.mk c.inr c.inl)), 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))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
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₂
⊢ Mono c₁.inl ↔ Mono c₂.inl
have c₃ : ∀ (c₁ c₂ : BinaryCofan.{v_1, u_1} A B) (x : IsColimit c₁) (x : IsColimit c₂), 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₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MonoCoprod (goal)
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'
⊢ Mono c'.inl
have obtain : ∀ (c : BinaryCofan.{v_1, u_1} A B) (hc₁ : IsColimit c) (hc₂ : Mono c.inl), Mono c'.inl
Tactic: obtain ⟨c, hc₁, hc₂⟩ := h A B
-- 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
⊢ ∃ (c : BinaryCofan A B) (x : IsColimit c), Mono c.inl
have refine_1 : IsColimit (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))
Tactic: refine ⟨BinaryCofan.mk (↾(Sum.inl : A → A ⊕ B))
      (↾Sum.inr), ?_, ?_⟩
-- 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
refine_1 : IsColimit (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))
⊢ ∃ (c : BinaryCofan A B) (x : IsColimit c), Mono c.inl
have 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)))
Tactic: refine ⟨BinaryCofan.mk (↾(Sum.inl : A → A ⊕ B))
      (↾Sum.inr), ?_, ?_⟩
-- 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
x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))
⊢ T
have inl : (x : A) → T
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 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
⊢ T
have inr : (x : B) → T
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 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₂
⊢ m =
    (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₂
have h : ∀ (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
Tactic: ext x