awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
⊢ IsCardinalFiltered.{w, v, u} J κ ↔
    (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)) ∧
      ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
        HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
⟨fun _ ↦ ⟨fun ι j hι ↦ ⟨_, fun i ↦ ⟨toMax j hι i⟩⟩,
    fun ι j k f hι ↦ ⟨_, _, _, coeq_condition f hι⟩⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨fun {A _} F hA ↦ ?_⟩⟩

Premises used: CategoryTheory.IsCardinalFiltered, CategoryTheory.IsCardinalFiltered.toCoeq, CategoryTheory.IsCardinalFiltered.toMax, Nonempty.intro, CategoryTheory.IsCardinalFiltered.coeqHom, CategoryTheory.IsCardinalFiltered.coeq, And.intro, Iff.intro, Exists.intro, CategoryTheory.IsCardinalFiltered.mk, _private.0.CategoryTheory.isCardinalFiltered_iff.match_1, CategoryTheory.IsCardinalFiltered.coeq_condition, CategoryTheory.IsCardinalFiltered.max
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J : Type u
inst : Category.{v, u} J
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
refine :
  ((∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)) ∧
      ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
        HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b) →
    ∀ (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)
      {A : Type w} {x : SmallCategory A} (F : Functor.{w, v, w, u} A J) (hA : HasCardinalLT (Arrow A) κ),
      Nonempty (Cocone F)
⊢ IsCardinalFiltered.{w, v, u} J κ ↔
    (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ (k : J), ∀ (i : ι), Nonempty.{v + 1} (j i ⟶ k)) ∧
      ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
        HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
refine ⟨fun _ ↦ ⟨fun ι j hι ↦ ⟨_, fun i ↦ ⟨toMax j hι i⟩⟩,
    fun ι j k f hι ↦ ⟨_, _, _, coeq_condition f hι⟩⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨fun {A _} F hA ↦ ?_⟩⟩
-- 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)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
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
A : Type w
x : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) κ
obtain : ∀ (j : J) (hj : ∀ (i : A), Nonempty.{v + 1} (F.obj i ⟶ j)), Nonempty (Cocone F)
⊢ Nonempty (Cocone F)

Tactic:
obtain ⟨j, hj⟩ := h₁ F.obj (hasCardinalLT_of_hasCardinalLT_arrow hA)

Premises used: CategoryTheory.Functor.obj, CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow
-- 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)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
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
A : Type w
x : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (i : A), Nonempty.{v + 1} (F.obj i ⟶ j)
a : (i : A) → F.obj i ⟶ j := fun (i : A) ↦ ⋯.some
obtain : ∀ (l : J) (b : j ⟶ l) (hb : ∀ (i : Arrow A), (F.map i.hom ≫ a i.right) ≫ b = a i.left ≫ b), Nonempty (Cocone F)
⊢ Nonempty (Cocone F)

Tactic:
obtain ⟨l, b, hb⟩ := isCardinalFiltered_iff_aux₂ h₁ h₂
    (fun (f : Arrow A) ↦ F.map f.hom ≫ a f.right)
    (fun (f : Arrow A) ↦ a f.left) hA

Premises used: CategoryTheory.isCardinalFiltered_iff_aux₂, CategoryTheory.Arrow.left, CategoryTheory.Arrow.hom, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Arrow.right
-- 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)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
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
A : Type w
x : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (i : A), Nonempty.{v + 1} (F.obj i ⟶ j)
a : (i : A) → F.obj i ⟶ j := fun (i : A) ↦ ⋯.some
l : J
b : j ⟶ l
hb : ∀ (i : Arrow A), (F.map i.hom ≫ a i.right) ≫ b = a i.left ≫ b
x_1 x_2 : A
f : x_1 ⟶ x_2
⊢ F.map f ≫ a x_2 ≫ b = (a x_1 ≫ b) ≫ Functor.map (Functor.obj (Functor.const A) l) f

Tactic:
simpa using hb (Arrow.mk f)

Premises used: CategoryTheory.Arrow.mk
-- 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)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
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
A : Type w
x : SmallCategory A
F : Functor.{w, v, w, u} A J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (i : A), Nonempty.{v + 1} (F.obj i ⟶ j)
a : (i : A) → F.obj i ⟶ j := fun (i : A) ↦ ⋯.some
l : J
b : j ⟶ l
hb : ∀ (i : Arrow A), (F.map i.hom ≫ a i.right) ≫ b = a i.left ≫ b
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨{
    pt := l
    ι.app i := a i ≫ b
    ι.naturality _ _ f := by simpa using hb (Arrow.mk 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 κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
⊢ 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 κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered.{v, u} J
obtain :
  ∀ (l : J) (a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l) (b : k ⟶ l)
    (h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ 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.wideSpan
    (fun i ↦ IsFiltered.coeqHom (f₁ i) (f₂ i)) hι

Premises used: CategoryTheory.IsFiltered.coeqHom, CategoryTheory.IsCardinalFiltered.wideSpan
-- 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 κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered.{v, u} J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
i : ι
rw : f₁ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i
rw₁ rw₂ : f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i
⊢ f₁ i ≫ b = f₂ i ≫ b

Tactic:
rw [← h i, IsFiltered.coeq_condition_assoc]

Premises used: CategoryTheory.IsFiltered.coeq_condition_assoc
-- 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 κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered.{v, u} J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
⊢ ∃ (l : J) (a : k ⟶ l), ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
exact ⟨l, b, fun i ↦ by rw [← h i, IsFiltered.coeq_condition_assoc]⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
⊢ IsFiltered.{v, u} J₁

Tactic:
have := isFiltered_of_isCardinalFiltered J₁ κ
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
⊢ ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)

Tactic:
obtain ⟨h₁, h₂⟩ := (Functor.final_iff_of_isFiltered F).1 inferInstance

Premises used: inferInstance, Iff.mp, CategoryTheory.Functor.final_iff_of_isFiltered
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
⊢ ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
obtain ⟨h₁, h₂⟩ := (Functor.final_iff_of_isFiltered F).1 inferInstance

Premises used: inferInstance, Iff.mp, CategoryTheory.Functor.final_iff_of_isFiltered
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
rw :
  (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
⊢ IsCardinalFiltered.{w, v', u'} J₂ κ

Tactic:
rw [isCardinalFiltered_iff]

Premises used: CategoryTheory.isCardinalFiltered_iff
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
⟨fun ι j hι ↦ ?_, fun ι j k f hι ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
refine_1 : ∀ (ι : Type w) (j : ι → J₂) (hι : HasCardinalLT ι κ), ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)
refine_2 :
  ∀ (ι : Type w) (j k : J₂) (f : ι → (j ⟶ k)) (hι : HasCardinalLT ι κ),
    ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
⊢ (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)),
      HasCardinalLT ι κ → ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
refine ⟨fun ι j hι ↦ ?_, fun ι j k f hι ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j : ι → J₂
hι : HasCardinalLT ι κ
refine_1 :
  ∀ (a : (i : ι) → J₁) (ha : ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ F.obj (a i))),
    ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)
⊢ ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)

Tactic:
choose a ha using fun i ↦ h₁ (j i)
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j : ι → J₂
hι : HasCardinalLT ι κ
a : (i : ι) → J₁
ha : ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ F.obj (a i))
⊢ ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)

Tactic:
⟨F.obj (IsCardinalFiltered.max a hι),
      fun i ↦ ⟨(ha i).some ≫ F.map (toMax a hι i)⟩⟩

Premises used: CategoryTheory.IsCardinalFiltered.toMax, Nonempty.some, Nonempty.intro, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.obj, CategoryTheory.IsCardinalFiltered.max
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j : ι → J₂
hι : HasCardinalLT ι κ
a : (i : ι) → J₁
ha : ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ F.obj (a i))
⊢ ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)

Tactic:
exact ⟨F.obj (IsCardinalFiltered.max a hι),
      fun i ↦ ⟨(ha i).some ≫ F.map (toMax a hι i)⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
pos : ∀ (h : Nonempty ι), ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
neg : ∀ (h : ¬Nonempty ι), ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
by_cases h : Nonempty ι

Premises used: Nonempty
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
pos : ∀ (l : J₁) (a : k ⟶ F.obj l), ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
obtain ⟨l, ⟨a⟩⟩ := h₁ k
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
pos :
  ∀ (m : (i : ι × ι) → J₁) (b : (i : ι × ι) → l ⟶ m i)
    (hb : ∀ (i : ι × ι), (f i.1 ≫ a) ≫ F.map (b i) = (f i.2 ≫ a) ≫ F.map (b i)),
    ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
choose m b hb using fun (i : ι × ι) ↦ h₂ (f i.1 ≫ a) (f i.2 ≫ a)

Premises used: Prod.fst, CategoryTheory.CategoryStruct.comp, Prod.snd
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : (i : ι × ι) → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (i : ι × ι), (f i.1 ≫ a) ≫ F.map (b i) = (f i.2 ≫ a) ≫ F.map (b i)
⊢ ∀ (a_1 b_1 : ι),
    Eq (α := j ⟶ F.obj (m (a_1, b_1))) (f a_1 ≫ a ≫ F.map (b (a_1, b_1))) (f b_1 ≫ a ≫ F.map (b (a_1, b_1)))

Tactic:
simp only [Category.assoc, Prod.forall] at hb

Premises used: CategoryTheory.Category.assoc, Prod.forall
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : (i : ι × ι) → J₁
b : (i : ι × ι) → l ⟶ m i
hb :
  ∀ (a_1 b_1 : ι),
    Eq (α := j ⟶ F.obj (m (a_1, b_1))) (f a_1 ≫ a ≫ F.map (b (a_1, b_1))) (f b_1 ≫ a ≫ F.map (b (a_1, b_1)))
pos :
  ∀ (n : J₁) (c : (i : ι × ι) → m i ⟶ n) (d : l ⟶ n) (hn : ∀ (i : ι × ι), b i ≫ c i = d),
    ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
obtain ⟨n, c, d, hn⟩ := wideSpan b
        (hasCardinalLT_prod (Cardinal.IsRegular.aleph0_le Fact.out) hι hι)

Premises used: hasCardinalLT_prod, Cardinal.IsRegular.aleph0_le, CategoryTheory.IsCardinalFiltered.wideSpan, Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : (i : ι × ι) → J₁
b : (i : ι × ι) → l ⟶ m i
hb :
  ∀ (a_1 b_1 : ι),
    Eq (α := j ⟶ F.obj (m (a_1, b_1))) (f a_1 ≫ a ≫ F.map (b (a_1, b_1))) (f b_1 ≫ a ≫ F.map (b (a_1, b_1)))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
i : ι
rw :
  f i ≫ a ≫ F.map (CategoryStruct.comp (Y := m (i₀, i)) (b (i₀, i)) (c (i₀, i))) =
    f i₀ ≫ a ≫ F.map (CategoryStruct.comp (Y := m (i₀, i)) (b (i₀, i)) (c (i₀, i)))
rw₁ :
  f i ≫ a ≫ CategoryStruct.comp (Y := F.obj (m (i₀, i))) (F.map (b (i₀, i))) (F.map (c (i₀, i))) =
    f i₀ ≫ a ≫ CategoryStruct.comp (Y := F.obj (m (i₀, i))) (F.map (b (i₀, i))) (F.map (c (i₀, i)))
rw₂ rw₃ :
  f i ≫ a ≫ CategoryStruct.comp (Y := F.obj (m (i₀, i))) (F.map (b (i₀, i))) (F.map (c (i₀, i))) =
    f i ≫ a ≫ CategoryStruct.comp (Y := F.obj (m (i₀, i))) (F.map (b (i₀, i))) (F.map (c (i₀, i)))
⊢ f i ≫ a ≫ F.map d = f i₀ ≫ a ≫ F.map d

Tactic:
rw [← hn (i₀, i), Functor.map_comp, reassoc_of% (hb i₀ i)]

Premises used: Prod.mk, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : (i : ι × ι) → J₁
b : (i : ι × ι) → l ⟶ m i
hb :
  ∀ (a_1 b_1 : ι),
    Eq (α := j ⟶ F.obj (m (a_1, b_1))) (f a_1 ≫ a ≫ F.map (b (a_1, b_1))) (f b_1 ≫ a ≫ F.map (b (a_1, b_1)))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b

Tactic:
exact ⟨F.obj n, a ≫ F.map d, f i₀ ≫ a ≫ F.map d,
        fun i ↦ by rw [← hn (i₀, i), Functor.map_comp, reassoc_of% (hb i₀ i)]⟩
-- Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
Goal:
J₁ : Type u
inst : Category.{v, u} J₁
J₂ : Type u'
inst_1 : Category.{v', u'} J₂
F : Functor.{v, v', u, u'} J₁ J₂
inst_2 : F.Final
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v, u} J₁ κ
this : IsFiltered.{v, u} J₁
h₁ : ∀ (d : J₂), ∃ (c : J₁), Nonempty.{v' + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ (c' : J₁) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : ¬Nonempty ι
⊢ IsEmpty ι

Tactic:
simp only [not_nonempty_iff] at h

Premises used: not_nonempty_iff