awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cotrident.{w, v, u} (C := C) (X := F.obj zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ (ofCotrident t).ι.app j = eqToHom ⋯ ≫ t.ι.app j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f : J → (X_1 ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
X : WalkingParallelFamily J
zero :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.zero
one :
  F.obj WalkingParallelFamily.one =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.one
⊢ F.obj X =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
zero zero₁ zero₂ zero₃ :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero
⊢ F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
one one₁ one₂ one₃ :
  F.obj WalkingParallelFamily.one =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.one
⊢ F.obj WalkingParallelFamily.one =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.one

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f : J → (X_1 ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
X : WalkingParallelFamily J
zero :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.zero =
    F.obj WalkingParallelFamily.zero
one :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.one =
    F.obj WalkingParallelFamily.one
⊢ Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      X =
    F.obj X

Tactic:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
zero zero₁ zero₂ zero₃ :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero =
    F.obj WalkingParallelFamily.zero
⊢ Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.zero =
    F.obj WalkingParallelFamily.zero

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
one one₁ one₂ one₃ :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.one =
    F.obj WalkingParallelFamily.one
⊢ Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦ F.map (line j))
      WalkingParallelFamily.one =
    F.obj WalkingParallelFamily.one

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
j : WalkingParallelFamily J
zero :
  F.obj WalkingParallelFamily.zero =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.zero
one :
  F.obj WalkingParallelFamily.one =
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.one
⊢ F.obj j =
    Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cone F
j : WalkingParallelFamily J
⊢ (ofCone t).π.app j = t.π.app j ≫ eqToHom ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
j : WalkingParallelFamily J
zero :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.zero =
    F.obj WalkingParallelFamily.zero
one :
  Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      WalkingParallelFamily.one =
    F.obj WalkingParallelFamily.one
⊢ Functor.obj.{w, v, w, u}
      (parallelFamily (X := F.obj WalkingParallelFamily.zero) (Y := F.obj WalkingParallelFamily.one) fun (j : J) ↦
        F.map (line j))
      j =
    F.obj j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WalkingParallelFamily J) C
t : Cocone F
j : WalkingParallelFamily J
⊢ (ofCocone t).ι.app j = eqToHom ⋯ ≫ t.ι.app j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ Eq (α := s.pt ⟶ (parallelFamily f).obj zero) (k ≫ t.π.app zero) (s.π.app zero)

Tactic:
w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ Eq (α := s.pt ⟶ (parallelFamily f).obj zero) (k ≫ t.π.app zero) (s.π.app zero)

Tactic:
exact w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ Eq (α := s.pt ⟶ (parallelFamily f).obj one) (k ≫ t.π.app one) (s.π.app one)

Tactic:
simpa using w =≫ f (Classical.arbitrary J)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s t : Trident f
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
rw : i.inv ≫ i.hom ≫ t.ι = t.ι
rw₁ rw₂ : t.ι = t.ι
⊢ i.inv ≫ s.ι = t.ι

Tactic:
rw [← w, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ Eq (α := (parallelFamily f).obj zero ⟶ t.pt) (s.ι.app zero ≫ k) (t.ι.app zero)

Tactic:
simpa using f (Classical.arbitrary J) ≫= w

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ Eq (α := (parallelFamily f).obj one ⟶ t.pt) (s.ι.app one ≫ k) (t.ι.app one)

Tactic:
w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ Eq (α := (parallelFamily f).obj one ⟶ t.pt) (s.ι.app one ≫ k) (t.ι.app one)

Tactic:
exact w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : Nonempty J
s t : Cotrident f
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
rw : t.π = s.π ≫ i.hom
rw₁ rw₂ : t.π = t.π
⊢ t.π ≫ i.inv = s.π

Tactic:
rw [Iso.comp_inv_eq, w]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideEqualizer f
⊢ (trident f).ι = ι f

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideEqualizer f
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
        (Functor.obj (Functor.const (WalkingParallelFamily J)) (trident f).pt) zero ⟶
      (parallelFamily f).obj zero)
    ((trident f).π.app zero) (ι f)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideEqualizer f
j₁ j₂ : J
⊢ Eq (α := wideEqualizer f ⟶ Y) (ι f ≫ f j₁) (ι f ≫ f j₂)

Tactic:
Trident.condition j₁ j₂ <| limit.cone <| parallelFamily f

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.Trident.condition, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.parallelFamily, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideEqualizer f
inst_2 : Nonempty J
W : C
k : W ⟶ X
h : ∀ (j₁ j₂ : J), k ≫ f j₁ = k ≫ f j₂
⊢ CategoryStruct.comp (Y := wideEqualizer f) (lift k h) (ι f) = k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideEqualizer f
inst_2 : Nonempty J
W : C
k l : W ⟶ wideEqualizer f
h : k ≫ ι f = l ≫ ι f
⊢ k = l

Tactic:
Trident.IsLimit.hom_ext (limit.isLimit _) h

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.Trident.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideCoequalizer f
⊢ (cotrident f).π = π f

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideCoequalizer f
⊢ Eq (α :=
    (parallelFamily f).obj one ⟶
      Functor.obj.{w, v, w, u} (C := WalkingParallelFamily J)
        (Functor.obj (Functor.const (WalkingParallelFamily J)) (cotrident f).pt) one)
    ((cotrident f).ι.app one) (π f)

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideCoequalizer f
j₁ j₂ : J
⊢ Eq (α := X ⟶ wideCoequalizer f) (f j₁ ≫ π f) (f j₂ ≫ π f)

Tactic:
Cotrident.condition j₁ j₂ <| colimit.cocone <| parallelFamily f

Premises used: CategoryTheory.Limits.parallelFamily, CategoryTheory.Limits.colimit, CategoryTheory.Limits.Cotrident.condition, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideCoequalizer f
inst_2 : Nonempty J
W : C
k : Y ⟶ W
h : ∀ (j₁ j₂ : J), f j₁ ≫ k = f j₂ ≫ k
⊢ CategoryStruct.comp (Y := wideCoequalizer f) (π f) (desc k h) = k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideCoequalizer f
inst_2 : Nonempty J
W : C
k l : wideCoequalizer f ⟶ W
h : π f ≫ k = π f ≫ l
⊢ k = l

Tactic:
Cotrident.IsColimit.hom_ext (colimit.isColimit _) h

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.Cotrident.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, HasColimit (parallelFamily f)
⊢ HasWideCoequalizers.{w, v, u} C

Tactic:
fun _ =>
  { has_colimit := fun F => hasColimit_of_iso (diagramIsoParallelFamily F) }

Premises used: CategoryTheory.Limits.diagramIsoParallelFamily, CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.hasColimit_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideEqualizers.{w, v, u} C
⊢ HasEqualizers.{v, u} C

Tactic:
hasLimitsOfShape_of_equivalence.{w} walkingParallelFamilyEquivWalkingParallelPair

Premises used: CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair, CategoryTheory.Limits.hasLimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst_1 : HasWideCoequalizers.{w, v, u} C
⊢ HasCoequalizers.{v, u} C

Tactic:
hasColimitsOfShape_of_equivalence.{w} walkingParallelFamilyEquivWalkingParallelPair

Premises used: CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
X Y Z : WidePullbackShape J
f : X.Hom Y
g : Y.Hom Z
id : (g : X.Hom Z) → X.Hom Z
term : (j : J) → (g : Hom none Z) → Hom (some j) Z
⊢ X.Hom Z

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
X Z : WidePullbackShape J
g : X.Hom Z
⊢ X.Hom Z

Tactic:
exact g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
Z : WidePullbackShape J
j : J
g : Hom none Z
term : Hom (some j) none
⊢ Hom (some j) Z

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
j : J
⊢ Hom (some j) none

Tactic:
apply Hom.term _

Premises used: CategoryTheory.Limits.WidePullbackShape.Hom.term
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
x x_1 : WidePullbackShape J
allEq : ∀ (a b : x ⟶ x_1), a = b
⊢ Subsingleton.{w + 1} (x ⟶ x_1)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
x x_1 : WidePullbackShape J
a b : x ⟶ x_1
allEq : Eq.{w + 1} (α := Quiver.Hom (V := WidePullbackShape J) none none) (Hom.id none) (Hom.id none)
allEq₁ : ∀ (b : J), Hom.term b = Hom.term b
allEq₂ : ∀ (x : J), Hom.id (some x) = Hom.id (some x)
⊢ a = b

Tactic:
casesm* WidePullbackShape _, (_ : WidePullbackShape _) ⟶ (_ : WidePullbackShape _)

Premises used: CategoryTheory.Limits.WidePullbackShape
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
⊢ Eq.{w + 1} (α := Quiver.Hom (V := WidePullbackShape J) none none) (Hom.id none) (Hom.id none)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
b : J
⊢ Hom.term b = Hom.term b

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
x : J
⊢ Hom.id (some x) = Hom.id (some x)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
X : WidePullbackShape J
⊢ Hom.id X = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
X Y : WidePullbackShape J
f : X ⟶ Y
id :
  Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) X B objs : C)
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) X B objs : C)
term :
  (j : J) →
    Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) (some j) B objs : C)
      (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) none B objs : C)
⊢ Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) X B objs : C)
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) Y B objs : C)

Tactic:
obtain - | j := f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
X : WidePullbackShape J
⊢ Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) X B objs : C)
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) X B objs : C)

Tactic:
apply 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
j : J
⊢ Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) (some j) B objs : C)
    (Option.casesOn (motive := fun (x : WidePullbackShape J) ↦ C) none B objs : C)

Tactic:
exact arrows j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePullbackShape J) C
X : C
f_1 : X ⟶ F.obj Option.none
π : (j : J) → X ⟶ F.obj (Option.some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f_1
j j' : WidePullbackShape J
f : j ⟶ j'
none :
  ∀ (f : Option.none ⟶ j'),
    Eq.{v + 1} (α :=
      Functor.obj.{w, v, w, u} (C := WidePullbackShape J) (Functor.obj (Functor.const (WidePullbackShape J)) X)
          Option.none ⟶
        F.obj j')
      (Functor.map (Functor.obj (Functor.const (WidePullbackShape J)) X) f ≫
        match (motive :=
          (j : WidePullbackShape J) →
            Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
          j' with
        | Option.none => f_1
        | Option.some j => π j)
      ((match (motive :=
          (j : WidePullbackShape J) →
            Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
          Option.none with
        | Option.none => f_1
        | Option.some j => π j) ≫
        F.map f)
some :
  ∀ (val : J) (f : Option.some val ⟶ j'),
    Eq.{v + 1} (α :=
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) (Option.some val) ⟶ F.obj j')
      (Functor.map (Functor.obj (Functor.const (WidePullbackShape J)) X) f ≫
        match (motive :=
          (j : WidePullbackShape J) →
            Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
          j' with
        | Option.none => f_1
        | Option.some j => π j)
      ((match (motive :=
          (j : WidePullbackShape J) →
            Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
          Option.some val with
        | Option.none => f_1
        | Option.some j => π j) ≫
        F.map f)
⊢ Eq.{v + 1} (α := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j')
    (Functor.map (Functor.obj (Functor.const (WidePullbackShape J)) X) f ≫
      match (motive :=
        (j : WidePullbackShape J) →
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
        j' with
      | Option.none => f_1
      | Option.some j => π j)
    ((match (motive :=
        (j : WidePullbackShape J) →
          Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) j ⟶ F.obj j)
        j with
      | Option.none => f_1
      | Option.some j => π j) ≫
      F.map f)

Tactic:
cases j