awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
c' : CoconeTypes.{w₂, w₀', v, u} G
j : J
rw :
  Function.comp.{w₀' + 1, w₁ + 1, w₂ + 1} (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      ((fun (j : J) ↦ (c.ι j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) : G.obj j → c.pt)) j) =
    c'.ι j
rw₁ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) ∘ c.ι j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₂ :
  ι (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) j ∘
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₃ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      ((fun (j : J) ↦ (c'.ι j ∘ (⇑(e j).symm : (a : F.obj j) → G.obj j) : F.obj j → c'.pt)) j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₄ :
  c'.ι j ∘
      Function.comp.{w₀' + 1, w₀ + 1, w₀' + 1} (β := F.obj j) (⇑(e j).symm : (a : F.obj j) → G.obj j)
        (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
⊢ Function.comp (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      (ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j) =
    c'.ι j
have rw₅ : c'.ι j ∘ id = c'.ι j
Tactic: rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
c' : CoconeTypes.{w₂, w₀', v, u} G
j : J
rw :
  Function.comp.{w₀' + 1, w₁ + 1, w₂ + 1} (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      ((fun (j : J) ↦ (c.ι j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) : G.obj j → c.pt)) j) =
    c'.ι j
rw₁ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) ∘ c.ι j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₂ :
  ι (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) j ∘
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₃ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      ((fun (j : J) ↦ (c'.ι j ∘ (⇑(e j).symm : (a : F.obj j) → G.obj j) : F.obj j → c'.pt)) j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₄ :
  c'.ι j ∘
      Function.comp.{w₀' + 1, w₀ + 1, w₀' + 1} (β := F.obj j) (⇑(e j).symm : (a : F.obj j) → G.obj j)
        (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₅ : c'.ι j ∘ id = c'.ι j
⊢ Function.comp (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      (ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j) =
    c'.ι j
have rw₆ : c'.ι j = c'.ι j
Tactic: rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
T : Type w₂
f g : pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) → T
h :
  ∀ (j : J),
    f ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j =
      g ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j
j : J
⊢ f ∘ c.ι j = g ∘ c.ι j
have h₁ : ∀ (x : F.obj j), (f ∘ c.ι j) x = (g ∘ c.ι j) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
T : Type w₂
f g : pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) → T
h :
  ∀ (j : J),
    f ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j =
      g ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j
j : J
x : F.obj j
⊢ (f ∘ c.ι j) x = (g ∘ c.ι j) x
have h₁ : ∀ (y : G.obj j), (f ∘ c.ι j) ((e j : (a : G.obj j) → F.obj j) y) = (g ∘ c.ι j) ((e j : (a : G.obj j) → F.obj j) y)
Tactic: obtain ⟨y, rfl⟩ := (e j).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
y : F.ColimitType
⊢ hc.down.desc F.coconeTypes (F.descColimitType c y) = y
have obtain : ∀ (j : J) (x : F.obj j), hc.down.desc F.coconeTypes (F.descColimitType c (F.ιColimitType j x)) = F.ιColimitType j x
Tactic: obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
j : J
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j
have rw : (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = c.ι j
Tactic: rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
j : J
rw : (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = c.ι j
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j
have rw₁ : F.descColimitType c ∘ hc.down.desc F.coconeTypes ∘ c.ι j = c.ι j
Tactic: rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
j : J
rw : (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = c.ι j
rw₁ : F.descColimitType c ∘ hc.down.desc F.coconeTypes ∘ c.ι j = c.ι j
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j
have rw₂ : F.descColimitType c ∘ F.coconeTypes.ι j = c.ι j
Tactic: rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
j : J
rw : (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = c.ι j
rw₁ : F.descColimitType c ∘ hc.down.desc F.coconeTypes ∘ c.ι j = c.ι j
rw₂ : F.descColimitType c ∘ F.coconeTypes.ι j = c.ι j
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j
have rw₃ : F.descColimitType c ∘ (fun (j : J) ↦ F.ιColimitType j) j = c.ι j
Tactic: rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
j : J
rw : (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = c.ι j
rw₁ : F.descColimitType c ∘ hc.down.desc F.coconeTypes ∘ c.ι j = c.ι j
rw₂ : F.descColimitType c ∘ F.coconeTypes.ι j = c.ι j
rw₃ : F.descColimitType c ∘ (fun (j : J) ↦ F.ιColimitType j) j = c.ι j
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j
have rw₄ : c.ι j = c.ι j
Tactic: rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
⊢ Function.RightInverse (hc.down.desc F.coconeTypes) (F.descColimitType c)
have this : F.descColimitType c ∘ hc.down.desc F.coconeTypes = id
Tactic: have : (F.descColimitType c).comp
              ((down.{max u w₁} hc).desc F.coconeTypes) = id :=
            (down.{max u w₀} hc).funext (fun j ↦ by
              rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
⊢ Function.Bijective (β := F.coconeTypes.pt) (F.descColimitType F.coconeTypes)
have h : Eq (α := F.ColimitType → F.coconeTypes.pt) (F.descColimitType F.coconeTypes) id
Tactic: convert! Function.bijective_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
⊢ Eq (α := F.ColimitType → F.coconeTypes.pt) (F.descColimitType F.coconeTypes) id
have h : ∀ (y : F.ColimitType), F.descColimitType F.coconeTypes y = id y
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitType (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
y : F.ColimitType
⊢ F.descColimitType F.coconeTypes y = id y
have h : ∀ (j : J) (x : F.obj j), F.descColimitType F.coconeTypes (F.ιColimitType j x) = id (F.ιColimitType j x)
Tactic: obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x y : (j : J) × F.obj j
⊢ Relation.EqvGen F.ColimitTypeRel x y ↔
    ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (x.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (y.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
have mp : Relation.EqvGen F.ColimitTypeRel x y →
  ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x y : (j : J) × F.obj j
mp :
  Relation.EqvGen F.ColimitTypeRel x y →
    ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (x.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (y.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ Relation.EqvGen F.ColimitTypeRel x y ↔
    ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (x.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (y.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
have mpr : (∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))) →
  Relation.EqvGen F.ColimitTypeRel x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x_1 y_1 x y : (j : J) × F.obj j
h : F.ColimitTypeRel x y
⊢ ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
have mp : ∀ (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ y.fst (β := fun (j : J) ↦ F.obj j))
  (h :
    y.snd (β := fun (j : J) ↦ F.obj j) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj y.fst))
        (x.snd (β := fun (j : J) ↦ F.obj j))),
  ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
Tactic: obtain ⟨f, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x y x_1 y_1 : (j : J) × F.obj j
h_1 : Relation.EqvGen F.ColimitTypeRel x_1 y_1
h :
  ∃ (k : J) (f : x_1.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y_1.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x_1.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x_1.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y_1.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y_1.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ ∃ (k : J) (f : y_1.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : x_1.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y_1.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y_1.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x_1.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x_1.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
have mp : ∀ (k : J) (f : x_1.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y_1.fst (β := fun (j : J) ↦ F.obj j) ⟶ k)
  (h :
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x_1.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x_1.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y_1.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y_1.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))),
  ∃ (k : J) (f : y_1.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : x_1.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y_1.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y_1.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x_1.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x_1.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
Tactic: obtain ⟨k, f, g, h⟩ := h
Cleared hypotheses: h