awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
J : Type u_4
inst : Zero I₂
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
i₁ : I₁
i₃ : I₃
rw : π ((i₁, 0, i₃).1, τ.p₂₃ (i₁, 0, i₃).2) = π (i₁, i₃)
⊢ r (i₁, 0, i₃) = π (i₁, i₃)
have rw₁ : π ((i₁, 0, i₃).1, i₃) = π (i₁, i₃)
Tactic: rw [← τ.hp₂₃, τ.h₃ i₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D : Type u_4
I₁ : Type u_5
I₂ : Type u_6
I₃ : Type u_7
J : Type u_8
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D
inst_4 : Zero I₂
inst_5 : DecidableEq I₂
inst_6 : HasInitial.{v_2, u_2} C₂
F₁ : C₁ ⥤ Functor.{v_2, v_1, u_2, u_1} C₂ C₁
F₂ : C₂ ⥤ Functor.{v_3, v_3, u_3, u_3} C₃ C₃
G : C₁ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst_7 : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst_8 : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst_9 : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj (Functor.obj (single₀ I₂) X₂)).HasMap τ.p₁₂
inst_10 : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂))).obj X₃).HasMap π
inst_11 : (((mapBifunctor F₂ I₂ I₃).obj (Functor.obj (single₀ I₂) X₂)).obj X₃).HasMap τ.p₂₃
inst_12 : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ (Functor.obj (single₀ I₂) X₂) X₃)).HasMap π
inst_13 : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_14 : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_15 : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj rw : π (i₁, i₃) = j
⊢ r (i₁, 0, i₃) = j
have rw₁ : j = j
Tactic: rw [τ.r_zero, hj]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D : Type u_4
I₁ : Type u_5
I₂ : Type u_6
I₃ : Type u_7
J : Type u_8
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D
inst_4 : Zero I₂
inst_5 : DecidableEq I₂
inst_6 : HasInitial.{v_2, u_2} C₂
F₁ : C₁ ⥤ Functor.{v_2, v_1, u_2, u_1} C₂ C₁
F₂ : C₂ ⥤ Functor.{v_3, v_3, u_3, u_3} C₃ C₃
G : C₁ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst_7 : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst_8 : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst_9 : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj (Functor.obj (single₀ I₂) X₂)).HasMap τ.p₁₂
inst_10 : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂))).obj X₃).HasMap π
inst_11 : (((mapBifunctor F₂ I₂ I₃).obj (Functor.obj (single₀ I₂) X₂)).obj X₃).HasMap τ.p₂₃
inst_12 : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ (Functor.obj (single₀ I₂) X₂) X₃)).HasMap π
inst_13 : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_14 : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_15 : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
⊢ Eq (α := (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single 0) X₂ 0))).obj (X₃ i₃) ⟶ mapBifunctorMapObj G π X₁ X₃ j)
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (Functor.obj (single₀ I₂) X₂ 0)) (X₃ i₃) ≫
      (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃) ≫ e₂.hom.app (X₃ i₃)) ≫
        ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j ⋯)
    (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)) ≫ e₁.hom.app (X₁ i₁))) (X₃ i₃) ≫
      ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj)
have h : Eq (α := (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single 0) X₂ 0))).obj (X₃ i₃) ⟶ mapBifunctorMapObj G π X₁ X₃ j)
  (((NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (Functor.obj (single₀ I₂) X₂ 0)) (X₃ i₃) ≫
        (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃))) ≫
      (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫
    ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j sorry)
  (((NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
        NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃)) ≫
      (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫
    ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj)
Tactic: simp only [Functor.map_comp, NatTrans.comp_app, ← triangle (X₁ i₁) (X₃ i₃), ← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D : Type u_4
I₁ : Type u_5
I₂ : Type u_6
I₃ : Type u_7
J : Type u_8
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D
inst_4 : Zero I₂
inst_5 : DecidableEq I₂
inst_6 : HasInitial.{v_2, u_2} C₂
F₁ : C₁ ⥤ Functor.{v_2, v_1, u_2, u_1} C₂ C₁
F₂ : C₂ ⥤ Functor.{v_3, v_3, u_3, u_3} C₃ C₃
G : C₁ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst_7 : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst_8 : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst_9 : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj (Functor.obj (single₀ I₂) X₂)).HasMap τ.p₁₂
inst_10 : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂))).obj X₃).HasMap π
inst_11 : (((mapBifunctor F₂ I₂ I₃).obj (Functor.obj (single₀ I₂) X₂)).obj X₃).HasMap τ.p₂₃
inst_12 : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ (Functor.obj (single₀ I₂) X₂) X₃)).HasMap π
inst_13 : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_14 : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_15 : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
⊢ Eq (α := (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single 0) X₂ 0))).obj (X₃ i₃) ⟶ mapBifunctorMapObj G π X₁ X₃ j)
    (((NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (Functor.obj (single₀ I₂) X₂ 0)) (X₃ i₃) ≫
          (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃))) ≫
        (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫
      ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j ⋯)
    (((NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
          NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃)) ≫
        (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫
      ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj)
have h : Eq (α :=
  (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single₀ I₂) X₂ 0))).obj (X₃ i₃) ⟶
    (G.obj (X₁ i₁)).obj ((F₂.obj X₂).obj (X₃ i₃)))
  (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (Functor.obj (single₀ I₂) X₂ 0)) (X₃ i₃) ≫
    (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃)))
  (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
    NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D : Type u_4
I₁ : Type u_5
I₂ : Type u_6
I₃ : Type u_7
J : Type u_8
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D
inst_4 : Zero I₂
inst_5 : DecidableEq I₂
inst_6 : HasInitial.{v_2, u_2} C₂
F₁ : C₁ ⥤ Functor.{v_2, v_1, u_2, u_1} C₂ C₁
F₂ : C₂ ⥤ Functor.{v_3, v_3, u_3, u_3} C₃ C₃
G : C₁ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst_7 : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst_8 : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst_9 : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj (Functor.obj (single₀ I₂) X₂)).HasMap τ.p₁₂
inst_10 : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂))).obj X₃).HasMap π
inst_11 : (((mapBifunctor F₂ I₂ I₃).obj (Functor.obj (single₀ I₂) X₂)).obj X₃).HasMap τ.p₂₃
inst_12 : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ (Functor.obj (single₀ I₂) X₂) X₃)).HasMap π
inst_13 : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_14 : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_15 : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
⊢ Eq (α :=
    (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single₀ I₂) X₂ 0))).obj (X₃ i₃) ⟶
      (G.obj (X₁ i₁)).obj ((F₂.obj X₂).obj (X₃ i₃)))
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (Functor.obj (single₀ I₂) X₂ 0)) (X₃ i₃) ≫
      (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃)))
    (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃))
have h : Eq (α :=
  (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single₀ I₂) X₂ 0))).obj (X₃ i₃) ⟶
    (G.obj (X₁ i₁)).obj ((F₂.obj X₂).obj (X₃ i₃)))
  (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
    NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃))
  (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (Functor.obj (single₀ I₂) X₂ 0)) (X₃ i₃) ≫
    (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃)))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
a b : J.L
⊢ Subsingleton (left a ⟶ left b)
have pos : ∀ (h : a = b), Subsingleton (left a ⟶ left b)
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
a b : J.L
pos : ∀ (h : a = b), Subsingleton (left a ⟶ left b)
⊢ Subsingleton (left a ⟶ left b)
have neg : ∀ (h : ¬a = b), Subsingleton (left a ⟶ left b)
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
a b : J.L
h : a = b
⊢ Subsingleton (left a ⟶ left b)
have pos : Subsingleton (left a ⟶ left a)
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (hypothesis)
Goal:
J : MultispanShape
a b : J.L
h : ¬a = b
⊢ Subsingleton (left a ⟶ left b)
have this : IsEmpty (left a ⟶ left b)
Tactic: have : IsEmpty (left a ⟶ left b) := ⟨by rintro ⟨⟩; simp at h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
a b : J.R
⊢ Subsingleton (right a ⟶ right b)
have pos : ∀ (h : a = b), Subsingleton (right a ⟶ right b)
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
a b : J.R
pos : ∀ (h : a = b), Subsingleton (right a ⟶ right b)
⊢ Subsingleton (right a ⟶ right b)
have neg : ∀ (h : ¬a = b), Subsingleton (right a ⟶ right b)
Tactic: by_cases h : a = b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
a b : J.R
h : a = b
⊢ Subsingleton (right a ⟶ right b)
have pos : Subsingleton (right a ⟶ right a)
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (hypothesis)
Goal:
J : MultispanShape
a b : J.R
h : ¬a = b
⊢ Subsingleton (right a ⟶ right b)
have this : IsEmpty (right a ⟶ right b)
Tactic: have : IsEmpty (right a ⟶ right b) := ⟨by rintro ⟨⟩; simp at h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u : Unit // J.fst l = r' }
T₂ : Type := { u : Unit // J.snd l = r' }
x : T₁
val : Unit
h : J.fst l = r'
⊢ left l ⟶ right r'
have subst : let T₁ := { u : Unit // J.fst l = J.fst l };
T₁ → (left l ⟶ right (J.fst l))
Tactic: subst h
Cleared hypotheses: r', T₁, T₂, x, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u : Unit // J.fst l = r' }
T₂ : Type := { u : Unit // J.snd l = r' }
x : T₂
val : Unit
h : J.snd l = r'
⊢ left l ⟶ right r'
have subst : let T₂ := { u : Unit // J.snd l = J.snd l };
T₂ → (left l ⟶ right (J.snd l))
Tactic: subst h
Cleared hypotheses: r', T₁, T₂, x, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
J : MultispanShape
l : J.L
r' : J.R
T₁ : Type := { u : Unit // J.fst l = r' }
T₂ : Type := { u : Unit // J.snd l = r' }
f : T₁ ⊕ T₂ → (left l ⟶ right r') :=
  Sum.elim
    (fun (x : T₁) ↦
      match (motive := T₁ → (left l ⟶ right r')) x with
      | ⟨val, h⟩ =>
        Eq.ndrec (motive := fun (r' : J.R) ↦
          let T₁ := { u : Unit // J.fst l = r' };
          let T₂ := { u : Unit // J.snd l = r' };
          T₁ → (left l ⟶ right r'))
          (let T₁ := { u : Unit // J.fst l = J.fst l };
          let T₂ := { u : Unit // J.snd l = J.fst l };
          fun (x : T₁) ↦ Hom.fst l)
          h x)
    fun (x : T₂) ↦
    match (motive := T₂ → (left l ⟶ right r')) x with
    | ⟨val, h⟩ =>
      Eq.ndrec (motive := fun (r' : J.R) ↦
        let T₁ := { u : Unit // J.fst l = r' };
        let T₂ := { u : Unit // J.snd l = r' };
        T₂ → (left l ⟶ right r'))
        (let T₁ := { u : Unit // J.fst l = J.snd l };
        let T₂ := { u : Unit // J.snd l = J.snd l };
        fun (x : T₂) ↦ Hom.snd l)
        h x
⊢ Small.{t, max w w'} (left l ⟶ right r')
have left : Function.Surjective f
Tactic: refine small_of_surjective (f := f) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.fst b) ≫ I.fst b
have rw : K.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) = K.ι (J.fst b) ≫ I.fst b
Tactic: rw [← K.w (WalkingMulticospan.Hom.fst b)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
K : Multifork I
b : J.R
⊢ K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b
have rw : K.π.app (WalkingMulticospan.left (J.snd b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) = K.ι (J.snd b) ≫ I.snd b
Tactic: rw [← K.w (WalkingMulticospan.Hom.snd b)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.L
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.left a) ⟶
      I.multicospan.obj (WalkingMulticospan.left a))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.left a))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) P)
        (WalkingMulticospan.Hom.id (WalkingMulticospan.left a)))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a)))
have left : 𝟙 P ≫ ι a = ι a ≫ 𝟙 (I.left a)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.left (J.fst a)) ⟶
      I.multicospan.obj (WalkingMulticospan.right a))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.right a))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.Hom.fst a))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left (J.fst a) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.fst a))
have left : 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = ι (J.fst a) ≫ I.fst a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.left (J.snd a)) ⟶
      I.multicospan.obj (WalkingMulticospan.right a))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.right a))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.Hom.snd a))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.left (J.snd a) with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.snd a))
have left : 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = ι (J.snd a) ≫ I.snd a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
⊢ Eq.{v + 1} (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.right a) ⟶
      I.multicospan.obj (WalkingMulticospan.right a))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) (WalkingMulticospan.right a))
      (Functor.map (Functor.obj (Functor.const (WalkingMulticospan J)) P)
        (WalkingMulticospan.Hom.id (WalkingMulticospan.right a)))
      (match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b))
    ((match (motive :=
        (x : WalkingMulticospan J) →
          Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) P) x ⟶ I.multicospan.obj x)
        WalkingMulticospan.right a with
      | WalkingMulticospan.left a => ι a
      | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
      I.multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right a)))
have right : 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = (ι (J.fst a) ≫ I.fst a) ≫ 𝟙 (I.right a)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : MulticospanShape
I_1 : MulticospanIndex.{w, w', v, u} J_1 C
K : Multifork I_1
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a : J.R
⊢ 𝟙 P ≫ ι (J.fst a) ≫ I.fst a = ι (J.snd a) ≫ I.snd a
have left : ι (J.fst a) ≫ I.fst a = ι (J.snd a) ≫ I.snd a
Tactic: simp only [Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
K : Multifork I
b : J.R
⊢ K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b
have rw : K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b
Tactic: rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex.{w, w', v, u} J C
K : Multifork I
b : J.R
rw : K.π.app (WalkingMulticospan.right b) = K.ι (J.snd b) ≫ I.snd b
⊢ K.ι (J.fst b) ≫ I.fst b = K.ι (J.snd b) ≫ I.snd b
have rw₁ : Eq (α := K.pt ⟶ I.right b)
  (K.π.app (WalkingMulticospan.right b) :
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan J)) K.pt) (WalkingMulticospan.right b) ⟶
      I.multicospan.obj (WalkingMulticospan.right b))
  (K.π.app (WalkingMulticospan.right b))
Tactic: rw [← app_right_eq_ι_comp_fst, ← app_right_eq_ι_comp_snd]