awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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.π
rw : s.π = c.π ≫ (↑l : c.pt ⟶ s'.pt)
⊢ c.π ≫ m = c.π ≫ (↑l : c.pt ⟶ s'.pt)

Tactic:
rw [hm]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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.π
⊢ s.π = c.π ≫ (↑l : c.pt ⟶ s'.pt)

Tactic:
l.2.symm

Premises used: CategoryTheory.Limits.Cofork.ofπ, Eq.symm, CategoryTheory.Limits.parallelPair, Subtype.property, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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.π
⊢ s.π = c.π ≫ (↑l : c.pt ⟶ s'.pt)

Tactic:
exact l.2.symm

Premises used: Eq.symm, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
W : C
h : W ⟶ X
inst_2 : Epi h
⊢ HasCoequalizer (h ≫ f) (h ≫ g)

Tactic:
⟨⟨{   cocone := _
        isColimit := isCoequalizerEpiComp (colimit.isColimit _) h }⟩⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, Nonempty.intro, CategoryTheory.Limits.isCoequalizerEpiComp, CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.Cofork.π, CategoryTheory.Limits.isCoequalizerEpiComp._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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
⊢ 𝟙 X ≫ f = f ≫ f

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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.π := ⋯
rw : 𝟙 X ≫ c.π = c.π
⊢ i.desc (Cofork.ofπ f ⋯) ≫ c.π = 𝟙 c.pt

Tactic:
rw [← cancel_epi_id c.π, ← Category.assoc, Cofork.IsColimit.π_desc, Cofork.π_ofπ, ←
      c.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cofork.condition, CategoryTheory.cancel_epi_id, CategoryTheory.Limits.Cofork.IsColimit.π_desc, CategoryTheory.Limits.Cofork.π_ofπ, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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.π := ⋯
⊢ 𝟙 X ≫ c.π = c.π

Tactic:
Category.id_comp _

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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.π := ⋯
⊢ 𝟙 X ≫ c.π = c.π

Tactic:
exact Category.id_comp _

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : e.IsEquivalence
inst_3 : HasInitial.{v₁, u₁} C
⊢ HasInitial.{v₂, u₂} D

Tactic:
Adjunction.hasColimitsOfShape_of_equivalence e

Premises used: CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ HasInitial.{v₁, u₁} C ↔ HasInitial.{v₂, u₂} D

Tactic:
⟨fun (_ : HasInitial C) => hasInitial_of_equivalence e.inverse,
    fun (_ : HasInitial D) => hasInitial_of_equivalence e.functor⟩

Premises used: CategoryTheory.hasInitial_of_equivalence, CategoryTheory.Equivalence.functor, Iff.intro, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : e.IsEquivalence
inst_3 : HasTerminal.{v₁, u₁} C
⊢ HasTerminal.{v₂, u₂} D

Tactic:
Adjunction.hasLimitsOfShape_of_equivalence e

Premises used: CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equivalence
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ HasTerminal.{v₁, u₁} C ↔ HasTerminal.{v₂, u₂} D

Tactic:
⟨fun (_ : HasTerminal C) => hasTerminal_of_equivalence e.inverse,
    fun (_ : HasTerminal D) => hasTerminal_of_equivalence e.functor⟩

Premises used: CategoryTheory.Equivalence.functor, Iff.intro, CategoryTheory.hasTerminal_of_equivalence, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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
apply : HasLimitsOfShape.{0, 0, v, u} (FinCategory.AsType J) C
⊢ HasLimitsOfShape.{w, w, v, u} J C

Tactic:
apply @hasLimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_

Premises used: CategoryTheory.FinCategory.equivAsType, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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.{0, 0, v, u} (FinCategory.AsType J) C

Tactic:
apply HasFiniteLimits.out

Premises used: CategoryTheory.Limits.HasFiniteLimits.out
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
⊢ HasFiniteLimits.{v, u} C

Tactic:
hasFiniteLimits_of_hasLimitsOfSize C

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{0, 0, v, u} C
⊢ HasFiniteLimits.{v, u} C

Tactic:
hasFiniteLimits_of_hasLimitsOfSize C

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsOfSize
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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.{w, w, v, u} (ULiftHom (ULift.{w, 0} J)) C

Tactic:
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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
have : ∀ (l : J ≌ ULiftHom (ULift.{w, 0} J)), HasLimitsOfShape.{0, 0, v, u} J C
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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
l : J ≌ ULiftHom (ULift.{w, 0} J)
⊢ HasLimitsOfShape.{0, 0, v, u} J C

Tactic:
apply @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ l.symm _

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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

Tactic:
@hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_

Premises used: CategoryTheory.FinCategory.equivAsType, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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
refine : HasColimitsOfShape.{0, 0, v, u} (FinCategory.AsType J) C
⊢ HasColimitsOfShape.{w, w, v, u} J C

Tactic:
refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_

Premises used: CategoryTheory.FinCategory.equivAsType, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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.{0, 0, v, u} (FinCategory.AsType J) C

Tactic:
apply HasFiniteColimits.out

Premises used: CategoryTheory.Limits.HasFiniteColimits.out
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
⊢ HasFiniteColimits.{v, u} C

Tactic:
hasFiniteColimits_of_hasColimitsOfSize C

Premises used: CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfSize.{0, 0, v, u} C
⊢ HasFiniteColimits.{v, u} C

Tactic:
hasFiniteColimits_of_hasColimitsOfSize C

Premises used: CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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.{w, w, v, u} (ULiftHom (ULift.{w, 0} J)) C

Tactic:
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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
have : ∀ (l : J ≌ ULiftHom (ULift.{w, 0} J)), HasColimitsOfShape.{0, 0, v, u} J C
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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
l : J ≌ ULiftHom (ULift.{w, 0} J)
⊢ HasColimitsOfShape.{0, 0, v, u} J C

Tactic:
apply @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
      (@Equivalence.symm J hJ (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
x : WalkingParallelPair
zero : WalkingParallelPair.zero ∈ [WalkingParallelPair.zero, WalkingParallelPair.one].toFinset
one : WalkingParallelPair.one ∈ [WalkingParallelPair.zero, WalkingParallelPair.one].toFinset
⊢ x ∈ [WalkingParallelPair.zero, WalkingParallelPair.one].toFinset

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
⊢ zero ∈ [zero, one].toFinset

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
⊢ one ∈ [zero, one].toFinset

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
j j' : WalkingParallelPair
⊢ ∀ (x : WalkingParallelPairHom j j'),
    Membership.mem (γ := Finset (WalkingParallelPairHom j j'))
      (WalkingParallelPair.recOn (motive := fun (x : WalkingParallelPair) ↦ Finset (WalkingParallelPairHom x j')) j
          (WalkingParallelPair.recOn (motive := fun (x : WalkingParallelPair) ↦ Finset (WalkingParallelPairHom zero x))
            j' [WalkingParallelPairHom.id zero].toFinset [left, right].toFinset)
          (WalkingParallelPair.recOn (motive := fun (x : WalkingParallelPair) ↦ Finset (WalkingParallelPairHom one x))
            j' ∅ [WalkingParallelPairHom.id one].toFinset) :
        Finset (WalkingParallelPairHom j j'))
      x

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteLimits.{v, u} C
⊢ HasEqualizers.{v, u} C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteColimits.{v, u} C
⊢ HasCoequalizers.{v, u} C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
none : Finset (j ⟶ Option.none)
some : (j' : J) → Finset (j ⟶ Option.some j')
⊢ Finset (j ⟶ j')

Tactic:
obtain - | j' := j'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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)
none₁ : (j : J) → Finset (some j ⟶ Option.none)
⊢ Finset (j ⟶ Option.none)

Tactic:
obtain - | j := j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
⊢ Finset (Quiver.Hom (V := WidePullbackShape J) none none)

Tactic:
exact {Hom.id none}

Premises used: Option.none, CategoryTheory.Limits.WidePullbackShape.Hom.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : J
⊢ Finset (some j ⟶ none)

Tactic:
exact {Hom.term j}

Premises used: CategoryTheory.Limits.WidePullbackShape.Hom.term
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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')
neg : (h : ¬some j' = j) → Finset (j ⟶ some j')
⊢ Finset (j ⟶ some j')

Tactic:
by_cases h : some j' = j

Premises used: Option.some
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
pos : Finset (j ⟶ j)
⊢ Finset (j ⟶ some j')

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ j)

Tactic:
exact {Hom.id j}

Premises used: CategoryTheory.Limits.WidePullbackShape.Hom.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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')

Tactic:
exact ∅
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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)
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)) ⋯ {Hom.id (some val)} else ∅ :
        Finset (some val ⟶ some val))
      (Hom.id (some val))
⊢ 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)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
⊢ 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)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
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)) ⋯ {Hom.id (some val)} else ∅ :
      Finset (some val ⟶ some val))
    (Hom.id (some val))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : J
⊢ Membership.mem (γ := Finset (some j ⟶ none))
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (some j ⟶ x)) none
        (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ Finset (x ⟶ none)) (some j) {Hom.id none}
          fun (j : J) ↦ {Hom.term j})
        fun (j' : J) ↦ if h : some j' = some j then Eq.mpr (β := Finset (some j ⟶ some j)) ⋯ {Hom.id (some j)} else ∅ :
      Finset (some j ⟶ none))
    (Hom.term j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
none : Finset (Option.none ⟶ j')
some : (j : J) → Finset (Option.some j ⟶ j')
⊢ Finset (j ⟶ j')

Tactic:
obtain - | j := j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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)
none₁ : (j' : J) → Finset (Option.none ⟶ some j')
⊢ Finset (Option.none ⟶ j')

Tactic:
obtain - | j' := j'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
⊢ Finset (Quiver.Hom (V := WidePushoutShape J) none none)

Tactic:
exact {Hom.id none}

Premises used: CategoryTheory.Limits.WidePushoutShape.Hom.id, Option.none
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j' : J
⊢ Finset (none ⟶ some j')

Tactic:
exact {Hom.init j'}

Premises used: CategoryTheory.Limits.WidePushoutShape.Hom.init
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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')
neg : (h : ¬some j = j') → Finset (some j ⟶ j')
⊢ Finset (some j ⟶ j')

Tactic:
by_cases h : some j = j'

Premises used: Option.some
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
pos : Finset (j' ⟶ j')
⊢ Finset (some j ⟶ j')

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (j' ⟶ j')

Tactic:
exact {Hom.id j'}

Premises used: CategoryTheory.Limits.WidePushoutShape.Hom.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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')

Tactic:
exact ∅
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
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)
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)) ⋯ {Hom.id (some val)} else ∅ :
        Finset (some val ⟶ some val))
      (Hom.id (some val))
⊢ 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)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
⊢ 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)

Tactic:
simp