awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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 ι κ
⊢ ∃ (k : J₂), ∀ (i : ι), Nonempty.{v' + 1} (j i ⟶ k)
have 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)
Tactic: choose a ha using fun i ↦ h₁ (j i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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 ι κ
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have pos : ∀ (h : Nonempty ι), ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
Tactic: by_cases h : Nonempty ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have neg : ∀ (h : ¬Nonempty ι), ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
Tactic: by_cases h : Nonempty ι
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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 ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have pos : ∀ (l : J₁) (a : k ⟶ F.obj l), ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
Tactic: obtain ⟨l, ⟨a⟩⟩ := h₁ k
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have 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
Tactic: choose m b hb using fun (i : ι × ι) ↦ h₂ (f i.1 ≫ a) (f i.2 ≫ a)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
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)
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have 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)))
Tactic: simp only [Category.assoc, Prod.forall] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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)))
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have 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
Tactic: obtain ⟨n, c, d, hn⟩ := wideSpan b
        (hasCardinalLT_prod (Cardinal.IsRegular.aleph0_le Fact.out) hι hι)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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 : ι
⊢ f i ≫ a ≫ F.map d = f i₀ ≫ a ≫ F.map d
have 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)))
Tactic: rw [← hn (i₀, i), Functor.map_comp, reassoc_of% (hb i₀ i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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)))
⊢ f i ≫ a ≫ F.map d = f i₀ ≫ a ≫ F.map d
have 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)))
Tactic: rw [← hn (i₀, i), Functor.map_comp, reassoc_of% (hb i₀ i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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)))
⊢ f i ≫ a ≫ F.map d = f i₀ ≫ a ≫ F.map d
have 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)))
Tactic: rw [← hn (i₀, i), Functor.map_comp, reassoc_of% (hb i₀ i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (hypothesis)
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 ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have h₃ : IsEmpty ι
Tactic: simp only [not_nonempty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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 : IsEmpty ι
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have neg : ∀ (j' : J₁) (a : j ⟶ F.obj j'), ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
Tactic: obtain ⟨j', ⟨a⟩⟩ := h₁ j
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.IsCardinalFiltered (goal)
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 : IsEmpty ι
j' : J₁
a : j ⟶ F.obj j'
⊢ ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
have neg : ∀ (k' : J₁) (b : k ⟶ F.obj k'), ∃ (l : J₂) (a : k ⟶ l) (b : j ⟶ l), ∀ (i : ι), f i ≫ a = b
Tactic: obtain ⟨k', ⟨b⟩⟩ := h₁ k
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
⊢ ∃ (j : J) (x' : c.pt.obj (X.obj j)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app j) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj j)) →
            (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj j))
        x'
have this : IsFiltered J
Tactic: have := isFiltered_of_isCardinalFiltered J κ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
⊢ ∃ (j : J) (x' : c.pt.obj (X.obj j)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app j) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj j)) →
            (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj j))
        x'
have obtain : ∀ (y : (↑(F ⋙ obj (evaluation C (Type w')) cX.pt).sections : Type (max w' u')))
  (hy :
    (Equiv.symm (Types.isLimitEquivSections (hc cX.pt)) :
          (a : (↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections : Type (max w' u'))) →
            (((evaluation C (Type w')).obj cX.pt).mapCone c).pt)
        y =
      x),
  ∃ (j : J) (x' : c.pt.obj (X.obj j)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app j) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj j)) →
            (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj j))
        x'
Tactic: obtain ⟨y, hy⟩ := (Types.isLimitEquivSections (hc cX.pt)).symm.surjective x
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : (↑(F ⋙ obj (evaluation C (Type w')) cX.pt).sections : Type (max w' u'))
hy :
  (Equiv.symm (Types.isLimitEquivSections (hc cX.pt)) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj cX.pt).mapCone c).pt)
      y =
    x
⊢ ∃ (j₀ : J) (z : (k : K) → (F.obj k).obj (X.obj j₀)),
    ∀ (k : K),
      (↑y : (j : K) → (F ⋙ (evaluation C (Type w')).obj cX.pt).obj j) k =
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k).map (cX.ι.app j₀)) :
            (a : (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj j₀))) →
              (fun (X : Type w') ↦ X) ((F.obj k).obj (((const J).obj cX.pt).obj j₀)))
          (z k)
have H : ∀ (k : K),
  ∃ (j : J) (y_1 : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (((F.obj k).mapCocone cX).ι.app j) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k).obj j)) →
            (fun (X : Type w') ↦ X) (((const J).obj ((F.obj k).mapCocone cX).pt).obj j))
        y_1 =
      (↑y : (j : K) → (F ⋙ (evaluation C (Type w')).obj cX.pt).obj j) k
Tactic: have H (k : K) := Types.jointly_surjective_of_isColimit (hF k) (y.1 k)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : (↑(F ⋙ obj (evaluation C (Type w')) cX.pt).sections : Type (max w' u'))
hy :
  (Equiv.symm (Types.isLimitEquivSections (hc cX.pt)) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj cX.pt).mapCone c).pt)
      y =
    x
⊢ ∃ (j : J) (x' : c.pt.obj (X.obj j)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app j) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj j)) →
            (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj j))
        x'
have obtain : ∀ (j₀ : J) (z : (k : K) → (F.obj k).obj (X.obj j₀))
  (hz :
    ∀ (k : K),
      (↑y : (j : K) → (F ⋙ (evaluation C (Type w')).obj cX.pt).obj j) k =
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k).map (cX.ι.app j₀)) :
            (a : (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj j₀))) →
              (fun (X : Type w') ↦ X) ((F.obj k).obj (((const J).obj cX.pt).obj j₀)))
          (z k)),
  ∃ (j : J) (x' : c.pt.obj (X.obj j)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((c.pt.mapCocone cX).ι.app j) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ c.pt).obj j)) →
            (fun (X : Type w') ↦ X) (((const J).obj (c.pt.mapCocone cX).pt).obj j))
        x'
Tactic: obtain ⟨j₀, z, hz⟩ : ∃ (j₀ : J) (z : (k : K) → (F.obj k).obj (X.obj j₀)),
      ∀ (k : K), y.1 k = (F.obj k).map (cX.ι.app j₀) (z k) := by
    have H (k : K) := Types.jointly_surjective_of_isColimit (hF k) (y.1 k)
    let j (k : K) : J := (H k).choose
    let z (k : K) : (F.obj k).obj (X.obj (j k)) := (H k).choose_spec.choose
    have hz (k : K) : (F.obj k).map (cX.ι.app (j k)) (z k) = y.1 k :=
      (H k).choose_spec.choose_spec
    exact ⟨IsCardinalFiltered.max j (hasCardinalLT_of_hasCardinalLT_arrow hK),
      fun k ↦ (F.obj k).map (X.map (IsCardinalFiltered.toMax j _ k)) (z k),
        fun k ↦ by rw [← hz, ← comp_apply, ← Functor.map_comp, cX.w]; rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type u'
inst_1 : Category.{v', u'} K
F : K ⥤ Functor.{v, w', u, w' + 1} C (Type w')
c : Cone F
hc : (Y : C) → IsLimit (F := F ⋙ obj (evaluation C (Type w')) Y) (mapCone (obj (evaluation C (Type w')) Y) c)
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
X : Functor.{w, v, w, u} J C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : (↑(F ⋙ obj (evaluation C (Type w')) cX.pt).sections : Type (max w' u'))
hy :
  (Equiv.symm (Types.isLimitEquivSections (hc cX.pt)) :
        (a : (↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections : Type (max w' u'))) →
          (((evaluation C (Type w')).obj cX.pt).mapCone c).pt)
      y =
    x
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz :
  ∀ (k : K),
    (↑y : (j : K) → (F ⋙ (evaluation C (Type w')).obj cX.pt).obj j) k =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k).map (cX.ι.app j₀)) :
          (a : (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj j₀))) →
            (fun (X : Type w') ↦ X) ((F.obj k).obj (((const J).obj cX.pt).obj j₀)))
        (z k)
k k' : K
φ : k ⟶ k'
⊢ Eq (α := (fun (X : Type w') ↦ X) (obj (obj (const J) ((F.obj k').mapCocone cX).pt) j₀))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F.obj k').mapCocone cX).ι.app j₀) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j₀)) →
            (fun (X : Type w') ↦ X) (((const J).obj ((F.obj k').mapCocone cX).pt).obj j₀))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
              (a : (fun (X : Type w') ↦ X) ((F.obj k).obj (X.obj j₀))) →
                (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀)))
            (z k) :
          (fun (X : Type w') ↦ X) ((F.obj k').obj (X.obj j₀))) :
      (fun (X : Type w') ↦ X) (obj (obj (const J) ((F.obj k').mapCocone cX).pt) j₀))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F.obj k').mapCocone cX).ι.app j₀) :
          (a : (fun (X : Type w') ↦ X) ((X ⋙ F.obj k').obj j₀)) →
            (fun (X : Type w') ↦ X) (((const J).obj ((F.obj k').mapCocone cX).pt).obj j₀))
        (z k') :
      (fun (X : Type w') ↦ X) (obj (obj (const J) ((F.obj k').mapCocone cX).pt) j₀))
have dsimp : Eq (α := (F.obj k').obj cX.pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k').map (cX.ι.app j₀)) :
        (a : (F.obj k').obj (X.obj j₀)) → (F.obj k').obj cX.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map φ).app (X.obj j₀)) :
            (a : (F.obj k).obj (X.obj j₀)) → (F.obj k').obj (X.obj j₀))
          (z k) :
        (F.obj k').obj (X.obj j₀)) :
    (F.obj k').obj cX.pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.obj k').map (cX.ι.app j₀)) :
        (a : (F.obj k').obj (X.obj j₀)) → (F.obj k').obj cX.pt)
      (z k') :
    (F.obj k').obj cX.pt)
Tactic: dsimp at hz ⊢