awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
slice_rhs :
  Eq (α := j₁ ⟶ coeq₃ f g h)
    (g ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
    (h ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
⊢ Eq (α := j₁ ⟶ coeq₃ f g h)
    (g ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
    (h ≫
      coeqHom f g ≫
        leftToMax (coeq f g) (coeq g h) ≫
          coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))

Tactic:
slice_rhs 2 4 => rw [← Category.assoc, coeq_condition _ _]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
a : (h ≫ coeqHom g h) ≫ rightToMax (coeq f g) (coeq g h)
| g ≫ coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)

Tactic:
rw [← Category.assoc, coeq_condition _ _]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
slice_lhs :
  Eq (α := j₁ ⟶ coeq₃ f g h)
    (((h ≫ coeqHom g h) ≫ rightToMax (coeq f g) (coeq g h)) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
    (h ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
⊢ Eq (α := j₁ ⟶ coeq₃ f g h)
    (g ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
    (h ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))

Tactic:
slice_lhs 1 3 => rw [← Category.assoc, coeq_condition _ _]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ Eq (α := j₁ ⟶ coeq₃ f g h)
    (((h ≫ coeqHom g h) ≫ rightToMax (coeq f g) (coeq g h)) ≫
      coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))
    (h ≫
      (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)) ≫
        coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ Eq (α := j₁ ⟶ coeq₃ f g h) (f ≫ coeq₃Hom f g h) (h ≫ coeq₃Hom f g h)

Tactic:
Eq.trans (coeq₃_condition₁ f g h) (coeq₃_condition₂ f g h)

Premises used: CategoryTheory.IsFiltered.coeq₃_condition₁, CategoryTheory.IsFiltered.coeq₃_condition₂, Eq.trans
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
i j j' : C
f : i ⟶ j
f' : i ⟶ j'
K : C
G : j ⟶ K
G' : j' ⟶ K
h : True
k : C
e : K ⟶ k
he : (f ≫ G) ≫ e = (f' ≫ G') ≫ e
⊢ f ≫ G ≫ e = f' ≫ G' ≫ e

Tactic:
simpa only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
obtain :
  ∀ (t : C) (k₁t : k₁ ⟶ t) (k₂t : k₂ ⟶ t) (ht : f₁ ≫ k₁t = g₁ ≫ k₂t),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Tactic:
obtain ⟨t, k₁t, k₂t, ht⟩ := span f₁ g₁

Premises used: CategoryTheory.IsFiltered.span
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
obtain :
  ∀ (s : C) (ts : t ⟶ s) (hs : (f₂ ≫ k₁t) ≫ ts = (g₂ ≫ k₂t) ≫ ts),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Tactic:
obtain ⟨s, ts, hs⟩ := IsFilteredOrEmpty.cocone_maps (f₂ ≫ k₁t) (g₂ ≫ k₂t)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFilteredOrEmpty.cocone_maps
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : (f₂ ≫ k₁t) ≫ ts = (g₂ ≫ k₂t) ≫ ts
⊢ f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts

Tactic:
simp_rw [Category.assoc] at hs

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts
⊢ f₁ ≫ k₁t ≫ ts = g₁ ≫ k₂t ≫ ts

Tactic:
simp only [← Category.assoc, ht]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Tactic:
exact ⟨s, k₁t ≫ ts, k₂t ≫ ts, by simp only [← Category.assoc, ht], hs⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι : Type u_1
inst_2 : Finite ι
k₁ k₂ : C
ι₁ ι₂ : Type u_1
e : ι₁ ≃ ι₂
IH :
  ∀ (j : ι₁ → C) (f : (i : ι₁) → j i ⟶ k₁) (g : (i : ι₁) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₁), f i ≫ α = g i ≫ β
j : ι₂ → C
f : (i : ι₂) → j i ⟶ k₁
g : (i : ι₂) → j i ⟶ k₂
of_equiv :
  ∀ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s)
    (H :
      ∀ (i : ι₁),
        Eq (α := (j ∘ (⇑e : (a : ι₁) → ι₂)) i ⟶ s) (f ((e : (a : ι₁) → ι₂) i) ≫ α) (g ((e : (a : ι₁) → ι₂) i) ≫ β)),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₂), f i ≫ α = g i ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₂), f i ≫ α = g i ≫ β

Tactic:
obtain ⟨s, α, β, H⟩ := IH (j ∘ e) (f <| e ·) (g <| e ·)

Premises used: Function.comp, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι : Type u_1
inst_2 : Finite ι
k₁ k₂ : C
ι₁ ι₂ : Type u_1
e : ι₁ ≃ ι₂
IH :
  ∀ (j : ι₁ → C) (f : (i : ι₁) → j i ⟶ k₁) (g : (i : ι₁) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₁), f i ≫ α = g i ≫ β
j : ι₂ → C
f : (i : ι₂) → j i ⟶ k₁
g : (i : ι₂) → j i ⟶ k₂
s : C
α : k₁ ⟶ s
β : k₂ ⟶ s
H :
  ∀ (i : ι₁), Eq (α := (j ∘ (⇑e : (a : ι₁) → ι₂)) i ⟶ s) (f ((e : (a : ι₁) → ι₂) i) ≫ α) (g ((e : (a : ι₁) → ι₂) i) ≫ β)
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₂), f i ≫ α = g i ≫ β

Tactic:
⟨s, α, β, e.forall_congr_right.mp H⟩

Premises used: Exists.intro, Iff.mp, Equiv.forall_congr_right
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι : Type u_1
inst_2 : Finite ι
k₁ k₂ : C
ι₁ ι₂ : Type u_1
e : ι₁ ≃ ι₂
IH :
  ∀ (j : ι₁ → C) (f : (i : ι₁) → j i ⟶ k₁) (g : (i : ι₁) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₁), f i ≫ α = g i ≫ β
j : ι₂ → C
f : (i : ι₂) → j i ⟶ k₁
g : (i : ι₂) → j i ⟶ k₂
s : C
α : k₁ ⟶ s
β : k₂ ⟶ s
H :
  ∀ (i : ι₁), Eq (α := (j ∘ (⇑e : (a : ι₁) → ι₂)) i ⟶ s) (f ((e : (a : ι₁) → ι₂) i) ≫ α) (g ((e : (a : ι₁) → ι₂) i) ≫ β)
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₂), f i ≫ α = g i ≫ β

Tactic:
exact ⟨s, α, β, e.forall_congr_right.mp H⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι : Type u_1
inst_2 : Finite ι
k₁ k₂ : C
j : PEmpty.{u_1 + 1} → C
f : (i : PEmpty.{u_1 + 1}) → j i ⟶ k₁
g : (i : PEmpty.{u_1 + 1}) → j i ⟶ k₂
⊢ ∀ (i : PEmpty.{u_1 + 1}), Eq (α := j i ⟶ max.{v, u} k₁ k₂) (f i ≫ leftToMax k₁ k₂) (g i ≫ rightToMax k₁ k₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι : Type u_1
inst_2 : Finite ι
k₁ k₂ : C
j : PEmpty.{u_1 + 1} → C
f : (i : PEmpty.{u_1 + 1}) → j i ⟶ k₁
g : (i : PEmpty.{u_1 + 1}) → j i ⟶ k₂
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : PEmpty.{u_1 + 1}), f i ≫ α = g i ≫ β

Tactic:
exact ⟨max k₁ k₂, leftToMax k₁ k₂, rightToMax k₁ k₂, by simp⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι_1 : Type u_1
inst_2 : Finite ι_1
k₁ k₂ : C
ι : Type u_1
inst_3 : Fintype ι
IH :
  ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
h_option :
  ∀ (s₁ : C) (α₁ : k₁ ⟶ s₁) (β₁ : k₂ ⟶ s₁)
    (H₁ : ∀ (i : ι), Eq (α := j (some i) ⟶ s₁) (f (some i) ≫ α₁) (g (some i) ≫ β₁)),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β

Tactic:
obtain ⟨s₁, α₁, β₁, H₁⟩ := IH (j ·) (f ·) (g ·)

Premises used: Option.some
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι_1 : Type u_1
inst_2 : Finite ι_1
k₁ k₂ : C
ι : Type u_1
inst_3 : Fintype ι
IH :
  ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), Eq (α := j (some i) ⟶ s₁) (f (some i) ≫ α₁) (g (some i) ≫ β₁)
h_option :
  ∀ (s₂ : C) (α₂ : k₁ ⟶ s₂) (β₂ : k₂ ⟶ s₂) (H₂ : Eq (α := j none ⟶ s₂) (f none ≫ α₂) (g none ≫ β₂)),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β

Tactic:
obtain ⟨s₂, α₂, β₂, H₂⟩ := span (f .none) (g .none)

Premises used: Option.none, CategoryTheory.IsFiltered.span
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι_1 : Type u_1
inst_2 : Finite ι_1
k₁ k₂ : C
ι : Type u_1
inst_3 : Fintype ι
IH :
  ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), Eq (α := j (some i) ⟶ s₁) (f (some i) ≫ α₁) (g (some i) ≫ β₁)
s₂ : C
α₂ : k₁ ⟶ s₂
β₂ : k₂ ⟶ s₂
H₂ : Eq (α := j none ⟶ s₂) (f none ≫ α₂) (g none ≫ β₂)
h_option :
  ∀ (t : C) (α : s₁ ⟶ t) (β : s₂ ⟶ t) (h₁ : α₁ ≫ α = α₂ ≫ β) (h₂ : β₁ ≫ α = β₂ ≫ β),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β

Tactic:
obtain ⟨t, α, β, h₁, h₂⟩ := bowtie α₁ α₂ β₁ β₂

Premises used: CategoryTheory.IsFiltered.bowtie
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι_1 : Type u_1
inst_2 : Finite ι_1
k₁ k₂ : C
ι : Type u_1
inst_3 : Fintype ι
IH :
  ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), Eq (α := j (some i) ⟶ s₁) (f (some i) ≫ α₁) (g (some i) ≫ β₁)
s₂ : C
α₂ : k₁ ⟶ s₂
β₂ : k₂ ⟶ s₂
H₂ : Eq (α := j none ⟶ s₂) (f none ≫ α₂) (g none ≫ β₂)
t : C
α : s₁ ⟶ t
β : s₂ ⟶ t
h₁ : α₁ ≫ α = α₂ ≫ β
h₂ : β₁ ≫ α = β₂ ≫ β
⊢ Eq (α := j none ⟶ t) (f none ≫ α₁ ≫ α) (g none ≫ β₁ ≫ α)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι_1 : Type u_1
inst_2 : Finite ι_1
k₁ k₂ : C
ι : Type u_1
inst_3 : Fintype ι
IH :
  ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), Eq (α := j (some i) ⟶ s₁) (f (some i) ≫ α₁) (g (some i) ≫ β₁)
s₂ : C
α₂ : k₁ ⟶ s₂
β₂ : k₂ ⟶ s₂
H₂ : Eq (α := j none ⟶ s₂) (f none ≫ α₂) (g none ≫ β₂)
t : C
α : s₁ ⟶ t
β : s₂ ⟶ t
h₁ : α₁ ≫ α = α₂ ≫ β
h₂ : β₁ ≫ α = β₂ ≫ β
⊢ ∀ (val : ι), Eq (α := j (some val) ⟶ t) (f (some val) ≫ α₁ ≫ α) (g (some val) ≫ β₁ ≫ α)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι_1 : Type u_1
inst_2 : Finite ι_1
k₁ k₂ : C
ι : Type u_1
inst_3 : Fintype ι
IH :
  ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), Eq (α := j (some i) ⟶ s₁) (f (some i) ≫ α₁) (g (some i) ≫ β₁)
s₂ : C
α₂ : k₁ ⟶ s₂
β₂ : k₂ ⟶ s₂
H₂ : Eq (α := j none ⟶ s₂) (f none ≫ α₂) (g none ≫ β₂)
t : C
α : s₁ ⟶ t
β : s₂ ⟶ t
h₁ : α₁ ≫ α = α₂ ≫ β
h₂ : β₁ ≫ α = β₂ ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β

Tactic:
exact ⟨t, α₁ ≫ α, β₁ ≫ α, Option.rec (by grind) (by grind)⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
ι : Type u_1
inst_2 : Finite ι
j : ι → C
k₁ k₂ : C
f : (i : ι) → j i ⟶ k₁
g : (i : ι) → j i ⟶ k₂
of_equiv :
  ∀ {ι₁ ι₂ : Type u_1} (e : ι₁ ≃ ι₂)
    (IH :
      ∀ (j : ι₁ → C) (f : (i : ι₁) → j i ⟶ k₁) (g : (i : ι₁) → j i ⟶ k₂),
        ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₁), f i ≫ α = g i ≫ β)
    (j : ι₂ → C) (f : (i : ι₂) → j i ⟶ k₁) (g : (i : ι₂) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι₂), f i ≫ α = g i ≫ β
h_empty :
  ∀ (j : PEmpty.{u_1 + 1} → C) (f : (i : PEmpty.{u_1 + 1}) → j i ⟶ k₁) (g : (i : PEmpty.{u_1 + 1}) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : PEmpty.{u_1 + 1}), f i ≫ α = g i ≫ β
h_option :
  ∀ {ι : Type u_1} [Fintype ι]
    (IH :
      ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂),
        ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β)
    (j : Option ι → C) (f : (i : Option ι) → j i ⟶ k₁) (g : (i : Option ι) → j i ⟶ k₂),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β

Tactic:
induction ι using Finite.induction_empty_option with
  | @of_equiv ι₁ ι₂ e IH =>
    obtain ⟨s, α, β, H⟩ := IH (j ∘ e) (f <| e ·) (g <| e ·)
    exact ⟨s, α, β, e.forall_congr_right.mp H⟩
  | h_empty => exact ⟨max k₁ k₂, leftToMax k₁ k₂, rightToMax k₁ k₂, by simp⟩
  | @h_option ι _ IH =>
    obtain ⟨s₁, α₁, β₁, H₁⟩ := IH (j ·) (f ·) (g ·)
    obtain ⟨s₂, α₂, β₂, H₂⟩ := span (f .none) (g .none)
    obtain ⟨t, α, β, h₁, h₂⟩ := bowtie α₁ α₂ β₁ β₂
    exact ⟨t, α₁ ≫ α, β₁ ≫ α, Option.rec (by grind) (by grind)⟩

Premises used: Finite.induction_empty_option
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
obtain :
  ∀ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s)
    (H :
      ∀ (i : Fin (Nat.succ 0).succ.succ),
        Eq (α := ![j₁, j₂, j₃] i ⟶ s)
          (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ) ↦ ![j₁, j₂, j₃] i ⟶ k₁) f₁
                (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃] i.succ ⟶ k₁) f₂
                  (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃] i.succ.succ ⟶ k₁) f₃ fun (a : Fin 0) ↦ nomatch a))
                i ≫
              α :
            ![j₁, j₂, j₃] i ⟶ s)
          (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ) ↦ ![j₁, j₂, j₃] i ⟶ k₂) g₁
                (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃] i.succ ⟶ k₂) g₂
                  (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃] i.succ.succ ⟶ k₂) g₃ fun (a : Fin 0) ↦ nomatch a))
                i ≫
              β :
            ![j₁, j₂, j₃] i ⟶ s)),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β

Tactic:
obtain ⟨s, α, β, H⟩ := crown ![j₁, j₂, j₃] (Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ nofun)))
     (Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ nofun)))

Premises used: Quiver.Hom, Fin.succ, _private.0.CategoryTheory.IsFiltered.crown₃.match_1, Fin.cons, CategoryTheory.IsFiltered.crown, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
s : C
α : k₁ ⟶ s
β : k₂ ⟶ s
H :
  ∀ (i : Fin (Nat.succ 0).succ.succ),
    Eq (α := ![j₁, j₂, j₃] i ⟶ s)
      (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ) ↦ ![j₁, j₂, j₃] i ⟶ k₁) f₁
            (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃] i.succ ⟶ k₁) f₂
              (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃] i.succ.succ ⟶ k₁) f₃ fun (a : Fin 0) ↦ nomatch a))
            i ≫
          α :
        ![j₁, j₂, j₃] i ⟶ s)
      (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ) ↦ ![j₁, j₂, j₃] i ⟶ k₂) g₁
            (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃] i.succ ⟶ k₂) g₂
              (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃] i.succ.succ ⟶ k₂) g₃ fun (a : Fin 0) ↦ nomatch a))
            i ≫
          β :
        ![j₁, j₂, j₃] i ⟶ s)
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β

Tactic:
⟨s, α, β, H 0, H 1, H 2⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
s : C
α : k₁ ⟶ s
β : k₂ ⟶ s
H :
  ∀ (i : Fin (Nat.succ 0).succ.succ),
    Eq (α := ![j₁, j₂, j₃] i ⟶ s)
      (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ) ↦ ![j₁, j₂, j₃] i ⟶ k₁) f₁
            (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃] i.succ ⟶ k₁) f₂
              (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃] i.succ.succ ⟶ k₁) f₃ fun (a : Fin 0) ↦ nomatch a))
            i ≫
          α :
        ![j₁, j₂, j₃] i ⟶ s)
      (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ) ↦ ![j₁, j₂, j₃] i ⟶ k₂) g₁
            (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃] i.succ ⟶ k₂) g₂
              (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃] i.succ.succ ⟶ k₂) g₃ fun (a : Fin 0) ↦ nomatch a))
            i ≫
          β :
        ![j₁, j₂, j₃] i ⟶ s)
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β

Tactic:
exact ⟨s, α, β, H 0, H 1, H 2⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ j₄ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
f₄ : j₄ ⟶ k₁
g₄ : j₄ ⟶ k₂
obtain :
  ∀ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s)
    (H :
      ∀ (i : Fin (Nat.succ 0).succ.succ.succ),
        Eq (α := ![j₁, j₂, j₃, j₄] i ⟶ s)
          (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ.succ) ↦ ![j₁, j₂, j₃, j₄] i ⟶ k₁) f₁
                (Fin.cons (α := fun (i : Fin 3) ↦ ![j₁, j₂, j₃, j₄] i.succ ⟶ k₁) f₂
                  (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ ⟶ k₁) f₃
                    (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ.succ ⟶ k₁) f₄ fun (a : Fin 0) ↦
                      nomatch a)))
                i ≫
              α :
            ![j₁, j₂, j₃, j₄] i ⟶ s)
          (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ.succ) ↦ ![j₁, j₂, j₃, j₄] i ⟶ k₂) g₁
                (Fin.cons (α := fun (i : Fin 3) ↦ ![j₁, j₂, j₃, j₄] i.succ ⟶ k₂) g₂
                  (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ ⟶ k₂) g₃
                    (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ.succ ⟶ k₂) g₄ fun (a : Fin 0) ↦
                      nomatch a)))
                i ≫
              β :
            ![j₁, j₂, j₃, j₄] i ⟶ s)),
    ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β

Tactic:
obtain ⟨s, α, β, H⟩ := crown ![j₁, j₂, j₃, j₄]
      (Fin.cons f₁ (Fin.cons f₂ (Fin.cons f₃ (Fin.cons f₄ nofun))))
     (Fin.cons g₁ (Fin.cons g₂ (Fin.cons g₃ (Fin.cons g₄ nofun))))

Premises used: Quiver.Hom, Fin.succ, _private.0.CategoryTheory.IsFiltered.crown₃.match_1, Fin.cons, CategoryTheory.IsFiltered.crown, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ j₃ j₄ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
f₃ : j₃ ⟶ k₁
g₃ : j₃ ⟶ k₂
f₄ : j₄ ⟶ k₁
g₄ : j₄ ⟶ k₂
s : C
α : k₁ ⟶ s
β : k₂ ⟶ s
H :
  ∀ (i : Fin (Nat.succ 0).succ.succ.succ),
    Eq (α := ![j₁, j₂, j₃, j₄] i ⟶ s)
      (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ.succ) ↦ ![j₁, j₂, j₃, j₄] i ⟶ k₁) f₁
            (Fin.cons (α := fun (i : Fin 3) ↦ ![j₁, j₂, j₃, j₄] i.succ ⟶ k₁) f₂
              (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ ⟶ k₁) f₃
                (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ.succ ⟶ k₁) f₄ fun (a : Fin 0) ↦
                  nomatch a)))
            i ≫
          α :
        ![j₁, j₂, j₃, j₄] i ⟶ s)
      (Fin.cons (α := fun (i : Fin (Nat.succ 0).succ.succ.succ) ↦ ![j₁, j₂, j₃, j₄] i ⟶ k₂) g₁
            (Fin.cons (α := fun (i : Fin 3) ↦ ![j₁, j₂, j₃, j₄] i.succ ⟶ k₂) g₂
              (Fin.cons (α := fun (i : Fin 2) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ ⟶ k₂) g₃
                (Fin.cons (α := fun (i : Fin 1) ↦ ![j₁, j₂, j₃, j₄] i.succ.succ.succ ⟶ k₂) g₄ fun (a : Fin 0) ↦
                  nomatch a)))
            i ≫
          β :
        ![j₁, j₂, j₃, j₄] i ⟶ s)
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β ∧ f₃ ≫ α = g₃ ≫ β ∧ f₄ ≫ α = g₄ ≫ β

Tactic:
⟨s, α, β, H 0, H 1, H 2, H 3⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat