awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitEpi f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
rw : (f ≫ section_ f) ≫ s.π = s.π
⊢ f ≫ section_ f ≫ s.π = s.π
have rw₁ : 𝟙 X ≫ s.π = s.π
Tactic: rw [← Category.assoc, ← s.condition, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitEpi f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
rw : (f ≫ section_ f) ≫ s.π = s.π
rw₁ : 𝟙 X ≫ s.π = s.π
⊢ f ≫ section_ f ≫ s.π = s.π
have rw₂ : s.π = s.π
Tactic: rw [← Category.assoc, ← s.condition, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
⊢ (h ≫ f) ≫ c.π = (h ≫ g) ≫ c.π
have simp : h ≫ f ≫ c.π = h ≫ g ≫ c.π
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
s : Cofork (h ≫ f) (h ≫ g)
⊢ f ≫ s.π = g ≫ s.π
have a : h ≫ f ≫ s.π = h ≫ g ≫ s.π
Tactic: apply hm.left_cancellation
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
s : Cofork (h ≫ f) (h ≫ g)
⊢ h ≫ f ≫ s.π = h ≫ g ≫ s.π
have a : (h ≫ f) ≫ s.π = (h ≫ g) ≫ s.π
Tactic: simp_rw [← Category.assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm_1 : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ c.π ⋯).π ≫ m = s.π
⊢ m = (↑l : c.pt ⟶ s'.pt)
have apply : c.π ≫ m = c.π ≫ (↑l : c.pt ⟶ s'.pt)
Tactic: apply Cofork.IsColimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm_1 : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ c.π ⋯).π ≫ m = s.π
⊢ c.π ≫ m = c.π ≫ (↑l : c.pt ⟶ s'.pt)
have hm₁ : c.π ≫ m = s.π
Tactic: rw [Cofork.π_ofπ] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm_1 : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : c.π ≫ m = s.π
⊢ c.π ≫ m = c.π ≫ (↑l : c.pt ⟶ s'.pt)
have rw : s.π = c.π ≫ (↑l : c.pt ⟶ s'.pt)
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f_1 g : X_1 ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
this : Epi c.π := ⋯
⊢ i.desc (Cofork.ofπ f ⋯) ≫ c.π = 𝟙 c.pt
have rw : 𝟙 X ≫ c.π = c.π
Tactic: rw [← cancel_epi_id c.π, ← Category.assoc, Cofork.IsColimit.π_desc, Cofork.π_ofπ, ←
      c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteLimits.{v, u} C
J : Type w
inst_2 : SmallCategory J
inst_3 : FinCategory J
⊢ HasLimitsOfShape.{w, w, v, u} J C
have apply : HasLimitsOfShape.{0, 0, v, u} (FinCategory.AsType J) C
Tactic: apply @hasLimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape.{w, w, v, u} J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasLimitsOfShape.{0, 0, v, u} J C
have this : HasLimitsOfShape.{w, w, v, u} (ULiftHom (ULift.{w, 0} J)) C
Tactic: haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape.{w, w, v, u} J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape.{w, w, v, u} (ULiftHom (ULift.{w, 0} J)) C
⊢ HasLimitsOfShape.{0, 0, v, u} J C
have have : ∀ (l : J ≌ ULiftHom (ULift.{w, 0} J)), HasLimitsOfShape.{0, 0, v, u} J C
Tactic: have l : @Equivalence J (ULiftHom (ULift J)) hJ
                          (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
      @ULiftHomULiftCategory.equiv J hJ
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
J : Type w
inst_2 : SmallCategory J
inst_3 : FinCategory J
⊢ HasColimitsOfShape.{w, w, v, u} J C
have refine : HasColimitsOfShape.{0, 0, v, u} (FinCategory.AsType J) C
Tactic: refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape.{w, w, v, u} J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasColimitsOfShape.{0, 0, v, u} J C
have this : HasColimitsOfShape.{w, w, v, u} (ULiftHom (ULift.{w, 0} J)) C
Tactic: haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape.{w, w, v, u} J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape.{w, w, v, u} (ULiftHom (ULift.{w, 0} J)) C
⊢ HasColimitsOfShape.{0, 0, v, u} J C
have have : ∀ (l : J ≌ ULiftHom (ULift.{w, 0} J)), HasColimitsOfShape.{0, 0, v, u} J C
Tactic: have l : @Equivalence J (ULiftHom (ULift J)) hJ
                           (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
      @ULiftHomULiftCategory.equiv J hJ
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : WalkingParallelPair
⊢ x ∈ [zero, one].toFinset
have zero : zero ∈ [zero, one].toFinset
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
x : WalkingParallelPair
zero : WalkingParallelPair.zero ∈ [WalkingParallelPair.zero, one].toFinset
⊢ x ∈ [WalkingParallelPair.zero, one].toFinset
have one : one ∈ [WalkingParallelPair.zero, one].toFinset
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ Finset (j ⟶ j')
have none : Finset (j ⟶ none)
Tactic: obtain - | j' := j'
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
none : Finset (j ⟶ Option.none)
⊢ Finset (j ⟶ j')
have some : (j' : J) → Finset (j ⟶ some j')
Tactic: obtain - | j' := j'
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Finset (j ⟶ none)
have none : Finset (Quiver.Hom (V := WidePullbackShape J) none none)
Tactic: obtain - | j := j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
none : Finset (Quiver.Hom (V := WidePullbackShape J) Option.none Option.none)
⊢ Finset (j ⟶ Option.none)
have none₁ : (j : J) → Finset (some j ⟶ Option.none)
Tactic: obtain - | j := j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')
have pos : (h : some j' = j) → Finset (j ⟶ some j')
Tactic: by_cases h : some j' = j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
pos : (h : some j' = j) → Finset (j ⟶ some j')
⊢ Finset (j ⟶ some j')
have neg : (h : ¬some j' = j) → Finset (j ⟶ some j')
Tactic: by_cases h : some j' = j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ some j')
have pos : Finset (j ⟶ j)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Membership.mem (γ := Finset (j ⟶ j))
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (j ⟶ x)) j
        (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (x ⟶ none)) j {Hom.id none} fun (j : J) ↦
          {Hom.term j})
        fun (j' : J) ↦ if h : some j' = j then Eq.mpr (β := Finset (j ⟶ j)) ⋯ {Hom.id j} else ∅ :
      Finset (j ⟶ j))
    (Hom.id j)
have id : Membership.mem (γ := Finset (Quiver.Hom (V := WidePullbackShape J) none none))
  (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (none ⟶ x)) none
      (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (x ⟶ none)) none {Hom.id none} fun (j : J) ↦
        {Hom.term j})
      fun (j' : J) ↦
      if h : some j' = none then Eq.mpr (β := Finset (Quiver.Hom (V := WidePullbackShape J) none none)) sorry {Hom.id none}
      else ∅ :
    Finset (Quiver.Hom (V := WidePullbackShape J) none none))
  (Hom.id none)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
id :
  Membership.mem (γ := Finset (Quiver.Hom (V := WidePullbackShape J) none none))
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (none ⟶ x)) none
        (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (x ⟶ none)) none {Hom.id none} fun (j : J) ↦
          {Hom.term j})
        fun (j' : J) ↦
        if h : some j' = none then
          Eq.mpr (β := Finset (Quiver.Hom (V := WidePullbackShape J) none none)) ⋯ {Hom.id none}
        else ∅ :
      Finset (Quiver.Hom (V := WidePullbackShape J) none none))
    (Hom.id none)
⊢ Membership.mem (γ := Finset (j ⟶ j))
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (j ⟶ x)) j
        (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (x ⟶ none)) j {Hom.id none} fun (j : J) ↦
          {Hom.term j})
        fun (j' : J) ↦ if h : some j' = j then Eq.mpr (β := Finset (j ⟶ j)) ⋯ {Hom.id j} else ∅ :
      Finset (j ⟶ j))
    (Hom.id j)
have id₁ : ∀ (val : J),
  Membership.mem (γ := Finset (some val ⟶ some val))
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (some val ⟶ x)) (some val)
        (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (x ⟶ none)) (some val) {Hom.id none}
          fun (j : J) ↦ {Hom.term j})
        fun (j' : J) ↦
        if h : some j' = some val then Eq.mpr (β := Finset (some val ⟶ some val)) sorry {Hom.id (some val)} else ∅ :
      Finset (some val ⟶ some val))
    (Hom.id (some val))
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ Finset (j ⟶ j')
have none : Finset (none ⟶ j')
Tactic: obtain - | j := j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
none : Finset (Option.none ⟶ j')
⊢ Finset (j ⟶ j')
have some : (j : J) → Finset (some j ⟶ j')
Tactic: obtain - | j := j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
⊢ Finset (none ⟶ j')
have none : Finset (Quiver.Hom (V := WidePushoutShape J) none none)
Tactic: obtain - | j' := j'
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
none : Finset (Quiver.Hom (V := WidePushoutShape J) Option.none Option.none)
⊢ Finset (Option.none ⟶ j')
have none₁ : (j' : J) → Finset (Option.none ⟶ some j')
Tactic: obtain - | j' := j'
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')
have pos : (h : some j = j') → Finset (some j ⟶ j')
Tactic: by_cases h : some j = j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
pos : (h : some j = j') → Finset (some j ⟶ j')
⊢ Finset (some j ⟶ j')
have neg : (h : ¬some j = j') → Finset (some j ⟶ j')
Tactic: by_cases h : some j = j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (some j ⟶ j')
have pos : Finset (j' ⟶ j')
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePushoutShape J
⊢ Membership.mem (γ := Finset (j ⟶ j))
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (x ⟶ j)) j
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (none ⟶ x)) j {Hom.id none} fun (j' : J) ↦
          {Hom.init j'})
        fun (j_1 : J) ↦ if h : some j_1 = j then Eq.mpr (β := Finset (j ⟶ j)) ⋯ {Hom.id j} else ∅ :
      Finset (j ⟶ j))
    (Hom.id j)
have id : Membership.mem (γ := Finset (Quiver.Hom (V := WidePushoutShape J) none none))
  (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (x ⟶ none)) none
      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (none ⟶ x)) none {Hom.id none} fun (j' : J) ↦
        {Hom.init j'})
      fun (j : J) ↦
      if h : some j = none then Eq.mpr (β := Finset (Quiver.Hom (V := WidePushoutShape J) none none)) sorry {Hom.id none}
      else ∅ :
    Finset (Quiver.Hom (V := WidePushoutShape J) none none))
  (Hom.id none)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePushoutShape J
id :
  Membership.mem (γ := Finset (Quiver.Hom (V := WidePushoutShape J) none none))
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (x ⟶ none)) none
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (none ⟶ x)) none {Hom.id none} fun (j' : J) ↦
          {Hom.init j'})
        fun (j : J) ↦
        if h : some j = none then Eq.mpr (β := Finset (Quiver.Hom (V := WidePushoutShape J) none none)) ⋯ {Hom.id none}
        else ∅ :
      Finset (Quiver.Hom (V := WidePushoutShape J) none none))
    (Hom.id none)
⊢ Membership.mem (γ := Finset (j ⟶ j))
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (x ⟶ j)) j
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (none ⟶ x)) j {Hom.id none} fun (j' : J) ↦
          {Hom.init j'})
        fun (j_1 : J) ↦ if h : some j_1 = j then Eq.mpr (β := Finset (j ⟶ j)) ⋯ {Hom.id j} else ∅ :
      Finset (j ⟶ j))
    (Hom.id j)
have id₁ : ∀ (val : J),
  Membership.mem (γ := Finset (some val ⟶ some val))
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (x ⟶ some val)) (some val)
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (none ⟶ x)) (some val) {Hom.id none}
          fun (j' : J) ↦ {Hom.init j'})
        fun (j : J) ↦
        if h : some j = some val then Eq.mpr (β := Finset (some val ⟶ some val)) sorry {Hom.id (some val)} else ∅ :
      Finset (some val ⟶ some val))
    (Hom.id (some val))
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
J : Type
inst_1 : Finite J
inst_2 : HasFiniteWidePullbacks.{v, u} C
⊢ HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C
have this : ∀ [Finite J], HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C
Tactic: haveI := @HasFiniteWidePullbacks.out C _ _ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
J : Type
inst_1 : Finite J
inst_2 : HasFiniteWidePushouts.{v, u} C
⊢ HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C
have this : ∀ [Finite J], HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C
Tactic: haveI := @HasFiniteWidePushouts.out C _ _ J
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
inst_1 : HasFiniteLimits.{v, u} C
J : Type
h : Finite J
⊢ HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C
have intro : ∀ (val : Fintype J), HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C
Tactic: cases nonempty_fintype J
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
inst_1 : HasFiniteColimits.{v, u} C
J : Type
h : Finite J
⊢ HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C
have intro : ∀ (val : Fintype J), HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C
Tactic: cases nonempty_fintype J
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
x : WalkingPair
⊢ Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} x
have left : Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} WalkingPair.left
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
x : WalkingPair
left : Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} WalkingPair.left
⊢ Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} x
have right : Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} WalkingPair.right
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) (if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0)
      (if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0)).Nodup
have pos : ∀ (h₁ : J.fst b = a) (h₂ : J.snd b = a),
  (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom sorry ≫ Hom.fst b} {eqToHom sorry ≫ Hom.snd b}).Nodup
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
pos :
  ∀ (h₁ : J.fst b = a) (h₂ : J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} {eqToHom ⋯ ≫ Hom.snd b}).Nodup
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) (if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0)
      (if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0)).Nodup
have neg : ∀ (h₁ : J.fst b = a) (h₂ : ¬J.snd b = a), (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom sorry ≫ Hom.fst b} 0).Nodup
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
pos :
  ∀ (h₁ : J.fst b = a) (h₂ : J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} {eqToHom ⋯ ≫ Hom.snd b}).Nodup
neg :
  ∀ (h₁ : J.fst b = a) (h₂ : ¬J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} 0).Nodup
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) (if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0)
      (if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0)).Nodup
have pos₁ : ∀ (h₁ : ¬J.fst b = a) (h : J.snd b = a), (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 {eqToHom sorry ≫ Hom.snd b}).Nodup
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
pos :
  ∀ (h₁ : J.fst b = a) (h₂ : J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} {eqToHom ⋯ ≫ Hom.snd b}).Nodup
neg :
  ∀ (h₁ : J.fst b = a) (h₂ : ¬J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} 0).Nodup
pos₁ :
  ∀ (h₁ : ¬J.fst b = a) (h : J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 {eqToHom ⋯ ≫ Hom.snd b}).Nodup
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) (if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0)
      (if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0)).Nodup
have neg₁ : ∀ (h₁ : ¬J.fst b = a), ¬J.snd b = a → (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 0).Nodup
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} {eqToHom ⋯ ≫ Hom.snd b}).Nodup
have pos : ¬Eq (α := left a ⟶ right b) (eqToHom sorry ≫ Hom.fst b) (eqToHom sorry ≫ Hom.snd b)
Tactic: simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
⊢ ¬Eq (α := left a ⟶ right b) (eqToHom ⋯ ≫ Hom.fst b) (eqToHom ⋯ ≫ Hom.snd b)
have pos : f (eqToHom sorry ≫ Hom.fst b) ≠ f (eqToHom sorry ≫ Hom.snd b)
Tactic: apply ne_of_apply_ne f