awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
refine : ∀ (j : κ.ord.ToType), ∃ y ∈ Set.range f, j ≤ y
⊢ Order.cof κ.ord.ToType ≤ Cardinal.mk ι

Tactic:
refine (Order.cof_le fun j ↦ ?_).trans (Cardinal.mk_le_of_surjective h)

Premises used: Cardinal.mk_le_of_surjective, Order.cof_le, LE.le.trans
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
j : κ.ord.ToType
obtain : ∀ (k : ι) (hk : j < f k), ∃ y ∈ Set.range f, j ≤ y
⊢ ∃ y ∈ Set.range f, j ≤ y

Tactic:
obtain ⟨k, hk⟩ := hs j
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
j : κ.ord.ToType
k : ι
hk : j < f k
⊢ ∃ y ∈ Set.range f, j ≤ y

Tactic:
⟨_, Set.mem_range_self k, hk.le⟩

Premises used: Set.mem_range_self, LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h :
  Function.Surjective (β := { x : κ.ord.ToType // x ∈ Set.range f }) fun (i : ι) ↦
    Subtype.mk (p := fun (x : κ.ord.ToType) ↦ x ∈ Set.range f) (f i) ⋯
hs : ∀ (j : κ.ord.ToType), ∃ (k : ι), j < f k
j : κ.ord.ToType
k : ι
hk : j < f k
⊢ ∃ y ∈ Set.range f, j ≤ y

Tactic:
exact ⟨_, Set.mem_range_self k, hk.le⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
⊢ IsFiltered.{v, u} J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
⊢ HasCardinalLT A κ

Tactic:
have hκ' : HasCardinalLT A κ := hasCardinalLT_of_hasCardinalLT_arrow hA
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a : A
⊢ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ' =
    (Functor.obj (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) a).hom

Tactic:
simpa [x] using coeq_condition x hκ' a

Premises used: CategoryTheory.IsCardinalFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a b : A
f : a ⟶ b
h :
  Eq (α :=
    (F.obj a).right ⟶ (Functor.obj (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) b).right)
    (Under.Hom.right (F.map f ≫ Under.homMk (c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯))
    (Under.Hom.right
      (Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯ ≫
        Functor.map (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) f))
⊢ Eq (α := F.obj a ⟶ Functor.obj (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) b)
    (F.map f ≫ Under.homMk (c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯)
    (Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯ ≫
      Functor.map (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a b : A
f : a ⟶ b
⊢ (F ⋙ Under.forget j₀).map f ≫ c.ι.app b = c.ι.app a

Tactic:
have := c.w f
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this_1 : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a b : A
f : a ⟶ b
this : (F ⋙ Under.forget j₀).map f ≫ c.ι.app b = c.ι.app a
h :
  Under.Hom.right (F.map f) ≫ c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ' =
    (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ≫ 𝟙 (coeq x hκ')
⊢ Eq (α :=
    (F.obj a).right ⟶ (Functor.obj (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) b).right)
    (Under.Hom.right (F.map f ≫ Under.homMk (c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯))
    (Under.Hom.right
      (Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ⋯ ≫
        Functor.map (Functor.obj (Functor.const A) (Under.mk (Y := coeq x hκ') (toCoeq x hκ'))) f))

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this_1 : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
a b : A
f : a ⟶ b
this : Under.Hom.right (F.map f) ≫ c.ι.app b = c.ι.app a
⊢ Under.Hom.right (F.map f) ≫ c.ι.app b ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ' =
    (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ') ≫ 𝟙 (coeq x hκ')

Tactic:
simp only [reassoc_of% this, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalFiltered.{w, v, u} J κ
j₀ : J
A : Type w
x_1 : SmallCategory A
F : A ⥤ Under.{v, u} j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered.{v, u} J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : (a : A) → j₀ ⟶ IsFiltered.max.{v, u} j₀ c.pt :=
  fun (a : A) ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
hκ' : HasCardinalLT A κ
⊢ Cocone F

Tactic:
exact
      { pt := Under.mk (toCoeq x hκ')
        ι :=
          { app a := Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ')
              (by simpa [x] using coeq_condition x hκ' a)
            naturality a b f := by
              ext
              have := c.w f
              dsimp at this ⊢
              simp only [reassoc_of% this, Category.comp_id] } }
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
J₂ : Type u'
inst : Category.{v, u} J₁
inst_1 : Category.{v', u'} J₂
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalFiltered.{w, v, u} J₁ κ
inst_4 : IsCardinalFiltered.{w, v', u'} J₂ κ
A : Type w
inst_5 : SmallCategory A
F : A ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := cocone (F ⋙ Prod.snd J₁ J₂) hC
i j : A
f : i ⟶ j
h₁ :
  (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).1 =
    ((c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f).1
h₂ :
  (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).2 =
    ((c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f).2
⊢ F.map f ≫ (c₁.ι.app j, c₂.ι.app j) =
    (c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
J₂ : Type u'
inst : Category.{v, u} J₁
inst_1 : Category.{v', u'} J₂
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalFiltered.{w, v, u} J₁ κ
inst_4 : IsCardinalFiltered.{w, v', u'} J₂ κ
A : Type w
inst_5 : SmallCategory A
F : A ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := cocone (F ⋙ Prod.snd J₁ J₂) hC
i j : A
f : i ⟶ j
⊢ (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).1 =
    ((c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f).1

Tactic:
simpa using c₁.w f

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
J₂ : Type u'
inst : Category.{v, u} J₁
inst_1 : Category.{v', u'} J₂
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalFiltered.{w, v, u} J₁ κ
inst_4 : IsCardinalFiltered.{w, v', u'} J₂ κ
A : Type w
inst_5 : SmallCategory A
F : A ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := cocone (F ⋙ Prod.snd J₁ J₂) hC
i j : A
f : i ⟶ j
⊢ (F.map f ≫ (c₁.ι.app j, c₂.ι.app j)).2 =
    ((c₁.ι.app i, c₂.ι.app i) ≫ Functor.map (Functor.obj (Functor.const A) (c₁.pt, c₂.pt)) f).2

Tactic:
simpa using c₂.w f

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
J₂ : Type u'
inst : Category.{v, u} J₁
inst_1 : Category.{v', u'} J₂
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalFiltered.{w, v, u} J₁ κ
inst_4 : IsCardinalFiltered.{w, v', u'} J₂ κ
A : Type w
inst_5 : SmallCategory A
F : A ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A) κ
c₁ : Cocone (F ⋙ Prod.fst J₁ J₂) := cocone (F ⋙ Prod.fst J₁ J₂) hC
c₂ : Cocone (F ⋙ Prod.snd J₁ J₂) := cocone (F ⋙ Prod.snd J₁ J₂) hC
⊢ Cocone F

Tactic:
exact
      { pt := (c₁.pt, c₂.pt)
        ι.app i := (c₁.ι.app i, c₂.ι.app i)
        ι.naturality {i j} f := by
          ext
          · simpa using c₁.w f
          · simpa using c₂.w f }
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
ι : Type u'
J : ι → Type u
inst : (i : ι) → Category.{v, u} (J i)
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : ∀ (i : ι), IsCardinalFiltered.{w, v, u} (J i) κ
A : Type w
inst_3 : SmallCategory A
F : A ⥤ ((i : ι) → J i)
hC : HasCardinalLT (Arrow A) κ
c : (i : ι) → Cocone (F ⋙ Pi.eval J i) := fun (i : ι) ↦ cocone (F ⋙ Pi.eval J i) hC
X Y : A
f : X ⟶ Y
w :
  ∀ (i : ι),
    Eq.{v + 1} (α := F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)
      ((F.map f ≫ fun (i : ι) ↦ (c i).ι.app Y) i :
        F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)
      (((fun (i : ι) ↦ (c i).ι.app X) ≫ Functor.map (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) f) i :
        F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)
⊢ Eq (α := F.obj X ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y)
    (F.map f ≫ fun (i : ι) ↦ (c i).ι.app Y)
    ((fun (i : ι) ↦ (c i).ι.app X) ≫ Functor.map (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) f)

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
ι : Type u'
J : ι → Type u
inst : (i : ι) → Category.{v, u} (J i)
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : ∀ (i : ι), IsCardinalFiltered.{w, v, u} (J i) κ
A : Type w
inst_3 : SmallCategory A
F : A ⥤ ((i : ι) → J i)
hC : HasCardinalLT (Arrow A) κ
c : (i : ι) → Cocone (F ⋙ Pi.eval J i) := fun (i : ι) ↦ cocone (F ⋙ Pi.eval J i) hC
X Y : A
f : X ⟶ Y
i : ι
⊢ Eq.{v + 1} (α := F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)
    ((F.map f ≫ fun (i : ι) ↦ (c i).ι.app Y) i :
      F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)
    (((fun (i : ι) ↦ (c i).ι.app X) ≫ Functor.map (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) f) i :
      F.obj X i ⟶ Functor.obj (Functor.obj (Functor.const A) fun (i : ι) ↦ (c i).pt) Y i)

Tactic:
simpa using (c i).ι.naturality f

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
ι : Type u'
J : ι → Type u
inst : (i : ι) → Category.{v, u} (J i)
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : ∀ (i : ι), IsCardinalFiltered.{w, v, u} (J i) κ
A : Type w
inst_3 : SmallCategory A
F : A ⥤ ((i : ι) → J i)
hC : HasCardinalLT (Arrow A) κ
c : (i : ι) → Cocone (F ⋙ Pi.eval J i) := fun (i : ι) ↦ cocone (F ⋙ Pi.eval J i) hC
⊢ Cocone F

Tactic:
exact
      { pt i := (c i).pt
        ι.app X i := (c i).ι.app X
        ι.naturality {X Y} f := by
          ext i
          simpa using (c i).ι.naturality f }
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
obtain :
  ∀ (l : J) (hl : ∀ (i : ι), Nonempty.{v + 1} (k i ⟶ l)),
    ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b
⊢ ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b

Tactic:
obtain ⟨l, hl⟩ := h₁ k hι
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
l : J
hl : ∀ (i : ι), Nonempty.{v + 1} (k i ⟶ l)
a : (i : ι) → k i ⟶ l := fun (i : ι) ↦ ⋯.some
obtain :
  ∀ (m : J) (b : l ⟶ m) (c : j ⟶ m) (hm : ∀ (i : ι), (f i ≫ a i) ≫ b = c),
    ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b
⊢ ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b

Tactic:
obtain ⟨m, b, c, hm⟩ := h₂ (fun i ↦ f i ≫ a i) hι

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
l : J
hl : ∀ (i : ι), Nonempty.{v + 1} (k i ⟶ l)
a : (i : ι) → k i ⟶ l := fun (i : ι) ↦ ⋯.some
m : J
b : l ⟶ m
c : j ⟶ m
hm : ∀ (i : ι), (f i ≫ a i) ≫ b = c
⊢ ∀ (i : ι), f i ≫ (fun (i : ι) ↦ a i ≫ b) i = c

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : J
k : ι → J
f : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
l : J
hl : ∀ (i : ι), Nonempty.{v + 1} (k i ⟶ l)
a : (i : ι) → k i ⟶ l := fun (i : ι) ↦ ⋯.some
m : J
b : l ⟶ m
c : j ⟶ m
hm : ∀ (i : ι), (f i ≫ a i) ≫ b = c
⊢ ∃ (m : J) (a : (i : ι) → k i ⟶ m) (b : j ⟶ m), ∀ (i : ι), f i ≫ a i = b

Tactic:
exact ⟨m, fun i ↦ a i ≫ b, c, by grind⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
i : ι
obtain :
  ∀ (l : J) (a : k ⟶ l) (b : j i ⟶ l)
    (hl :
      ∀ (i_1 : PUnit.{w + 1} ⊕ PUnit.{w + 1}),
        Sum.elim (fun (x : PUnit.{w + 1}) ↦ f₁ i) (fun (x : PUnit.{w + 1}) ↦ f₂ i) i_1 ≫ a = b),
    ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p
⊢ ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p

Tactic:
obtain ⟨l, a, b, hl⟩ := h₂ (Sum.elim (fun (_ : PUnit.{w + 1}) ↦ f₁ i)
      (fun (_ : PUnit.{w + 1}) ↦ f₂ i))
        (hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out))
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
i : ι
l : J
a : k ⟶ l
b : j i ⟶ l
hl :
  ∀ (i_1 : PUnit.{w + 1} ⊕ PUnit.{w + 1}),
    Sum.elim (fun (x : PUnit.{w + 1}) ↦ f₁ i) (fun (x : PUnit.{w + 1}) ↦ f₂ i) i_1 ≫ a = b
⊢ ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p

Tactic:
⟨l, a, (hl (Sum.inl .unit)).trans (hl (Sum.inr .unit)).symm⟩

Premises used: Sum.inl, Sum.inr, Exists.intro, PUnit.unit, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
i : ι
l : J
a : k ⟶ l
b : j i ⟶ l
hl :
  ∀ (i_1 : PUnit.{w + 1} ⊕ PUnit.{w + 1}),
    Sum.elim (fun (x : PUnit.{w + 1}) ↦ f₁ i) (fun (x : PUnit.{w + 1}) ↦ f₂ i) i_1 ≫ a = b
⊢ ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p

Tactic:
exact ⟨l, a, (hl (Sum.inl .unit)).trans (hl (Sum.inr .unit)).symm⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
⊢ ∀ (i : ι), ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p

Tactic:
have (i : ι) : ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p := by
    obtain ⟨l, a, b, hl⟩ := h₂ (Sum.elim (fun (_ : PUnit.{w + 1}) ↦ f₁ i)
      (fun (_ : PUnit.{w + 1}) ↦ f₂ i))
        (hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out))
    exact ⟨l, a, (hl (Sum.inl .unit)).trans (hl (Sum.inr .unit)).symm⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : ∀ (i : ι), ∃ (l : J) (p : k ⟶ l), f₁ i ≫ p = f₂ i ≫ p
choose :
  ∀ (l : (i : ι) → J) (p : (i : ι) → k ⟶ l i) (hp : ∀ (i : ι), f₁ i ≫ p i = f₂ i ≫ p i),
    ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
choose l p hp using this
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
l : (i : ι) → J
p : (i : ι) → k ⟶ l i
hp : ∀ (i : ι), f₁ i ≫ p i = f₂ i ≫ p i
obtain :
  ∀ (l_1 : J) (a : (i : ι) → l i ⟶ l_1) (b : k ⟶ l_1) (h : ∀ (i : ι), p i ≫ a i = b),
    ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
obtain ⟨l, a, b, h⟩ := isCardinalFiltered_iff_aux₁ h₁ h₂ p hι

Premises used: CategoryTheory.isCardinalFiltered_iff_aux₁
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
l_1 : (i : ι) → J
p : (i : ι) → k ⟶ l_1 i
hp : ∀ (i : ι), f₁ i ≫ p i = f₂ i ≫ p i
l : J
a : (i : ι) → l_1 i ⟶ l
b : k ⟶ l
h : ∀ (i : ι), p i ≫ a i = b
i : ι
⊢ f₁ i ≫ b = f₂ i ≫ b

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)
h₂ :
  ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
    HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
l_1 : (i : ι) → J
p : (i : ι) → k ⟶ l_1 i
hp : ∀ (i : ι), f₁ i ≫ p i = f₂ i ≫ p i
l : J
a : (i : ι) → l_1 i ⟶ l
b : k ⟶ l
h : ∀ (i : ι), p i ≫ a i = b
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
exact ⟨l, b, fun i ↦ by grind⟩