awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
J : Type w
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{w, v, w, u} J C
let let₁ let₂ let₃ : Nonempty (Cocone F)
⊢ Nonempty (Cocone F)
have let₄ : let O := Finset.image F.obj Finset.univ;
let H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.biUnion Finset.univ fun (X : J) ↦
    Finset.biUnion Finset.univ fun (Y : J) ↦
      Finset.image
        (fun (f : X ⟶ Y) ↦
          PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) (F.obj X)
            (PSigma.mk (β := fun (Y : C) ↦ (_ : F.obj X ∈ O) ×' (_ : Y ∈ O) ×' (F.obj X ⟶ Y)) (F.obj Y)
              (PSigma.mk (β := fun (x : F.obj X ∈ O) ↦ (_ : F.obj Y ∈ O) ×' (F.obj X ⟶ F.obj Y)) sorry
                (PSigma.mk (β := fun (x : F.obj Y ∈ O) ↦ F.obj X ⟶ F.obj Y) sorry (F.map f)))))
        Finset.univ;
∀ (Z : C) (f : {X : C} → X ∈ O → (X ⟶ Z))
  (w :
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y},
      PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
              (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f_1))) ∈
          H →
        f_1 ≫ f mY = f mX),
  Nonempty (Cocone F)
Tactic: classical
  let O := Finset.univ.image F.obj
  let H : Finset (Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
    Finset.univ.biUnion fun X : J => Finset.univ.biUnion fun Y : J =>
      Finset.univ.image fun f : X ⟶ Y => ⟨F.obj X, F.obj Y, by simp [O], by simp [O], F.map f⟩
  obtain ⟨Z, f, w⟩ := sup_exists O H
  refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩
  intro j j' g
  dsimp
  simp only [Category.comp_id]
  apply w
  simp only [O, H, Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq,
    true_and, exists_and_left]
  exact ⟨j, rfl, j', g, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
⊢ Nonempty C
have obtain : ∀ (c : Cocone.{w, v, w, u} (Functor.empty C)), Nonempty C
Tactic: obtain ⟨c⟩ := h (Functor.empty _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
⊢ IsFiltered.{v, u} C
have this : Nonempty C
Tactic: have : Nonempty C := by
    obtain ⟨c⟩ := h (Functor.empty _)
    exact ⟨c.pt⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
this : Nonempty C
⊢ IsFilteredOrEmpty.{v, u} C
have refine_1 : ∀ (X Y : C), ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
this : Nonempty C
refine_1 : ∀ (X Y : C), ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True
⊢ IsFilteredOrEmpty.{v, u} C
have refine_2 : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
⊢ ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True
have refine_1 : ∀ (c : Cocone.{w, v, w, u} (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)), ∃ (Z : C) (x : X ⟶ Z) (x : Y ⟶ Z), True
Tactic: obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
⊢ ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h
have refine_2 : ∀ (c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)), ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h
Tactic: obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ (Z : C) (h : Y ⟶ Z), f ≫ h = g ≫ h
have refine_2 : Eq (α := X ⟶ c.pt) (f ≫ c.ι.app { down := WalkingParallelPair.one }) (g ≫ c.ι.app { down := WalkingParallelPair.one })
Tactic: refine ⟨c.pt, c.ι.app ⟨WalkingParallelPair.one⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ Eq (α := X ⟶ c.pt) (f ≫ c.ι.app { down := WalkingParallelPair.one }) (g ≫ c.ι.app { down := WalkingParallelPair.one })
have h₁ : (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
      { down := WalkingParallelPairHom.left :
        ULift.{w, 0}
          (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
            ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) } ≫
    c.ι.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
  c.ι.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
    Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
      { down := WalkingParallelPairHom.left }
Tactic: have h₁ := c.ι.naturality ⟨WalkingParallelPairHom.left⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
        { down := WalkingParallelPairHom.left :
          ULift.{w, 0}
            (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
              ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) } ≫
      c.ι.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.ι.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.left }
⊢ Eq (α := X ⟶ c.pt) (f ≫ c.ι.app { down := WalkingParallelPair.one }) (g ≫ c.ι.app { down := WalkingParallelPair.one })
have h₂ : (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
      { down := WalkingParallelPairHom.right :
        ULift.{w, 0}
          (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
            ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) } ≫
    c.ι.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
  c.ι.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
    Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
      { down := WalkingParallelPairHom.right }
Tactic: have h₂ := c.ι.naturality ⟨WalkingParallelPairHom.right⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cocone F)
this : Nonempty C
⊢ IsFiltered.{v, u} C
have this₁ : IsFilteredOrEmpty.{v, u} C
Tactic: have : IsFilteredOrEmpty C := by
    refine ⟨?_, ?_⟩
    · intro X Y
      obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
      exact ⟨c.pt, c.ι.app ⟨⟨WalkingPair.left⟩⟩, c.ι.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩
    · intro X Y f g
      obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
      refine ⟨c.pt, c.ι.app ⟨WalkingParallelPair.one⟩, ?_⟩
      have h₁ := c.ι.naturality ⟨WalkingParallelPairHom.left⟩
      have h₂ := c.ι.naturality ⟨WalkingParallelPairHom.right⟩
      simp_all
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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) (g ≫ coeq₃Hom f g h) (h ≫ coeq₃Hom f g h)
have dsimp : Eq (α := j₁ ⟶ coeq₃ f g h)
  (g ≫
    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)))
  (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: dsimp [coeq₃Hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| 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))
have a : (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: rw [← Category.assoc, coeq_condition _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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)
    (g ≫
      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)))
    (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)))
have slice_lhs : 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_lhs 2 4 => rw [← Category.assoc, coeq_condition _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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)
    (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)))
have 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)))
Tactic: slice_rhs 2 4 => rw [← Category.assoc, coeq_condition _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| g ≫ coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)
have a : (h ≫ coeqHom g h) ≫ rightToMax (coeq f g) (coeq g h)
Tactic: rw [← Category.assoc, coeq_condition _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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)
    (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)))
have 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)))
Tactic: slice_lhs 1 3 => rw [← Category.assoc, coeq_condition _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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₂
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
have 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₂ ≫ β
Tactic: obtain ⟨t, k₁t, k₂t, ht⟩ := span f₁ g₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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) (α : k₁ ⟶ s) (β : k₂ ⟶ s), f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
have 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₂ ≫ β
Tactic: obtain ⟨s, ts, hs⟩ := IsFilteredOrEmpty.cocone_maps (f₂ ≫ k₁t) (g₂ ≫ k₂t)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
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₂ ≫ β
have hs₁ : f₂ ≫ k₁t ≫ ts = g₂ ≫ k₂t ≫ ts
Tactic: simp_rw [Category.assoc] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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), ∀ (i : ι₂), f i ≫ α = g i ≫ β
have 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 ≫ β
Tactic: obtain ⟨s, α, β, H⟩ := IH (j ∘ e) (f <| e ·) (g <| e ·)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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), ∀ (i : Option ι), f i ≫ α = g i ≫ β
have 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 ≫ β
Tactic: obtain ⟨s₁, α₁, β₁, H₁⟩ := IH (j ·) (f ·) (g ·)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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), ∀ (i : Option ι), f i ≫ α = g i ≫ β
have 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 ≫ β
Tactic: obtain ⟨s₂, α₂, β₂, H₂⟩ := span (f .none) (g .none)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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 ≫ β₂)
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β
have h_option : ∀ (t : C) (α : s₁ ⟶ t) (β : s₂ ⟶ t) (h₁ : α₁ ≫ α = α₂ ≫ β) (h₂ : β₁ ≫ α = β₂ ≫ β),
  ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : Option ι), f i ≫ α = g i ≫ β
Tactic: obtain ⟨t, α, β, h₁, h₂⟩ := bowtie α₁ α₂ β₁ β₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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₂
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
have 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 ≫ β
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)⟩
Cleared hypotheses: j, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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 ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
have 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 ≫ β
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)⟩
Cleared hypotheses: j, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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 ≫ β
⊢ ∃ (s : C) (α : k₁ ⟶ s) (β : k₂ ⟶ s), ∀ (i : ι), f i ≫ α = g i ≫ β
have 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 ≫ β
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)⟩
Cleared hypotheses: j, f, g