awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f_1 : F.obj none ⟶ X
ι : (j : J) → F.obj (Option.some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f_1
val val_1 : J
f : Option.some val ⟶ Option.some val_1
some :
  Eq (α :=
    F.obj (Option.some val) ⟶
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (Option.some val))
    (F.map (Hom.id (Option.some val)) ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.some val with
      | none => f_1
      | Option.some j => ι j)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (Option.some val))
      (match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.some val with
      | none => f_1
      | Option.some j => ι j)
      (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.id (Option.some val))))
⊢ Eq (α :=
    F.obj (Option.some val) ⟶
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (Option.some val_1))
    (F.map f ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.some val_1 with
      | none => f_1
      | Option.some j => ι j)
    ((match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.some val with
      | none => f_1
      | Option.some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
⊢ Eq (α :=
    F.obj none ⟶
      Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X) none)
    (F.map (Hom.id none) ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        none with
      | none => f
      | some j => ι j)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X) none)
      (match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        none with
      | none => f
      | some j => ι j)
      (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.id none)))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val : J
⊢ Eq (α := F.obj none ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (some val))
    (F.map (Hom.init val) ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        some val with
      | none => f
      | some j => ι j)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X) none)
      (match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        none with
      | none => f
      | some j => ι j)
      (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.init val)))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val : J
⊢ Eq (α := F.obj (some val) ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (some val))
    (F.map (Hom.id (some val)) ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        some val with
      | none => f
      | some j => ι j)
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (some val))
      (match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        some val with
      | none => f
      | some j => ι j)
      (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.id (some val))))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J
none :
  Iso (C := WidePushoutShape J) (Functor.obj (𝟭 (WidePushoutShape J)) Option.none)
    (Functor.obj (C := WidePushoutShape J)
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.init ((h : (a : J) → J') j))
        (wideSpan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      Option.none)
some :
  (val : J) →
    Functor.obj (𝟭 (WidePushoutShape J)) (Option.some val) ≅
      Functor.obj
        (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
          (wideSpan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
            Hom.init ((h : (a : J) → J') j))
          (wideSpan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
        (Option.some val)
⊢ Functor.obj (𝟭 (WidePushoutShape J)) j ≅
    Functor.obj
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.init ((h : (a : J) → J') j))
        (wideSpan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ Eq.{w + 1} (α := WidePushoutShape J) (Functor.obj (𝟭 (WidePushoutShape J)) none)
    (Functor.obj (C := WidePushoutShape J)
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      none)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ Iso (C := WidePushoutShape J) (Functor.obj (𝟭 (WidePushoutShape J)) none)
    (Functor.obj (C := WidePushoutShape J)
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      none)

Tactic:
exact eqToIso (by simp)

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val : J
⊢ Functor.obj (𝟭 (WidePushoutShape J)) (some val) =
    Functor.obj
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      (some val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val : J
⊢ Functor.obj (𝟭 (WidePushoutShape J)) (some val) ≅
    Functor.obj
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      (some val)

Tactic:
exact eqToIso (by simp)

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J'
none :
  Iso (C := WidePushoutShape J')
    (Functor.obj (C := WidePushoutShape J')
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.init ((h : (a : J) → J') j)))
      Option.none)
    (Functor.obj (𝟭 (WidePushoutShape J')) Option.none)
some :
  (val : J') →
    Functor.obj
        (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
          (wideSpan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
          (wideSpan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
            Hom.init ((h : (a : J) → J') j)))
        (Option.some val) ≅
      Functor.obj (𝟭 (WidePushoutShape J')) (Option.some val)
⊢ Functor.obj
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.init ((h : (a : J) → J') j)))
      j ≅
    Functor.obj (𝟭 (WidePushoutShape J')) j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ Eq.{w' + 1} (α := WidePushoutShape J')
    (Functor.obj (C := WidePushoutShape J')
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j)))
      none)
    (Functor.obj (𝟭 (WidePushoutShape J')) none)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ Iso (C := WidePushoutShape J')
    (Functor.obj (C := WidePushoutShape J')
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j)))
      none)
    (Functor.obj (𝟭 (WidePushoutShape J')) none)

Tactic:
exact eqToIso (by simp)

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val : J'
⊢ Functor.obj
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j)))
      (some val) =
    Functor.obj (𝟭 (WidePushoutShape J')) (some val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val : J'
⊢ Functor.obj
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePushoutShape J)
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j))
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j)))
      (some val) ≅
    Functor.obj (𝟭 (WidePushoutShape J')) (some val)

Tactic:
exact eqToIso (by simp)

Premises used: CategoryTheory.eqToIso
-- 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
inst_1 : HasWidePullback B objs arrows
j : J
⊢ Eq (α := widePullback B objs arrows ⟶ B) (π arrows j ≫ arrows j) (base arrows)

Tactic:
apply limit.w (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.Hom.term j)

Premises used: CategoryTheory.Limits.WidePullbackShape.Hom.term, CategoryTheory.Limits.WidePullbackShape.wideCospan, CategoryTheory.Limits.limit.w
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
j : J
⊢ CategoryStruct.comp (Y := widePullback B objs arrows) (lift f fs w) (π arrows j) = fs j

Tactic:
simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]

Premises used: CategoryTheory.Limits.WidePullbackShape.mkCone_π_app, CategoryTheory.Limits.WidePullbackShape.mkCone_pt, CategoryTheory.Limits.limit.lift_π
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
⊢ CategoryStruct.comp (Y := widePullback B objs arrows) (lift f fs w) (base arrows) = f

Tactic:
simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]

Premises used: CategoryTheory.Limits.WidePullbackShape.mkCone_π_app, CategoryTheory.Limits.WidePullbackShape.mkCone_pt, CategoryTheory.Limits.limit.lift_π
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
x :
  ∀ (j : WidePullbackShape J),
    g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app j =
      NatTrans.app (Cone.π (WidePullbackShape.mkCone f fs w)) j
⊢ g = lift f fs w

Tactic:
apply
    (limit.isLimit (WidePullbackShape.wideCospan B objs arrows)).uniq
      (WidePullbackShape.mkCone f fs <| w)

Premises used: CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.WidePullbackShape.mkCone, CategoryTheory.Limits.WidePullbackShape.wideCospan
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ Eq (α :=
    Cone.pt.{w, v, w, u} (J := WidePullbackShape J) (F := WidePullbackShape.wideCospan B objs arrows)
        (WidePullbackShape.mkCone f fs w) ⟶
      (WidePullbackShape.wideCospan B objs arrows).obj none)
    (g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app none)
    (NatTrans.app (Cone.π (WidePullbackShape.mkCone f fs w)) none)

Tactic:
apply h2
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
val : J
⊢ Eq (α :=
    Cone.pt.{w, v, w, u} (J := WidePullbackShape J) (F := WidePullbackShape.wideCospan B objs arrows)
        (WidePullbackShape.mkCone f fs w) ⟶
      (WidePullbackShape.wideCospan B objs arrows).obj (some val))
    (g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app (some val))
    (NatTrans.app (Cone.π (WidePullbackShape.mkCone f fs w)) (some val))

Tactic:
apply h1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst_2 : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
⊢ ∀ (j : J), (fun (j : J) ↦ g ≫ π arrows j) j ≫ arrows j = g ≫ base arrows

Tactic:
simp
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ g = lift (g ≫ base arrows) (fun (j : J) ↦ g ≫ π arrows j) ⋯

Tactic:
aesop
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
w :
  ∀ (j : WidePullbackShape J),
    g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) j =
      g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) j
⊢ g1 = g2

Tactic:
apply limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ Eq (α := X ⟶ (WidePullbackShape.wideCospan B objs arrows).obj none)
    (g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none)
    (g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none)

Tactic:
apply h2
-- 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
inst_1 : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
val : J
⊢ Eq (α := X ⟶ (WidePullbackShape.wideCospan B objs arrows).obj (some val))
    (g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val))
    (g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val))

Tactic:
apply h1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
i : ι
⊢ s.π i ≫ f i = s.base

Tactic:
simpa using ((Cone.π s).naturality (.term i)).symm

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.WidePullbackShape.Hom.term, CategoryTheory.NatTrans.naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
W : C
b : W ⟶ X
π : (i : ι) → W ⟶ Y i
h : ∀ (i : ι), π i ≫ f i = b
⊢ (mk b π h).base = b

Tactic:
rfl

Premises used: CategoryTheory.Limits.WidePullbackCone.base, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
W : C
b : W ⟶ X
π : (i : ι) → W ⟶ Y i
h : ∀ (i : ι), π i ≫ f i = b
i : ι
⊢ (mk b π h).π i = π i

Tactic:
rfl

Premises used: CategoryTheory.Limits.WidePullbackCone.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
j : WidePullbackShape ι
none :
  Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj Option.none) (lift t ≫ s.π.app Option.none)
    (t.π.app Option.none)
some :
  ∀ (val : ι),
    Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj (Option.some val)) (lift t ≫ s.π.app (Option.some val))
      (t.π.app (Option.some val))
⊢ lift t ≫ s.π.app j = t.π.app j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
⊢ Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj none) (lift t ≫ s.π.app none) (t.π.app none)

Tactic:
facbase t

Premises used: CategoryTheory.Limits.WidePullbackCone.base
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
⊢ Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj none) (lift t ≫ s.π.app none) (t.π.app none)

Tactic:
exact facbase t
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val : ι
⊢ Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj (some val)) (lift t ≫ s.π.app (some val))
    (t.π.app (some val))

Tactic:
facπ t _

Premises used: CategoryTheory.Limits.WidePullbackCone.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val : ι
⊢ Eq (α := t.pt ⟶ (WidePullbackShape.wideCospan X Y f).obj (some val)) (lift t ≫ s.π.app (some val))
    (t.π.app (some val))

Tactic:
exact facπ t _