mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
j : J
⊢ ι (F ⋙ G) j ≫ post F G = G.map (ι F j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: 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✝
⊢ Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
j : WidePullbackShape J
⊢ F.obj j = (wideCospan (F.obj none) (fun j ↦ F.obj (some j)) fun j ↦ F.map (Hom.term j)).obj j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
⊢ post F G ≫ G.map (desc F c) = desc (F ⋙ G) (G.mapCocone c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
⊢ post (F ⋙ G) H ≫ H.map (post F G) = post F (G ⋙ H)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
⊢ post (E ⋙ F) G ≫ G.map (pre F E) = pre (F ⋙ G) E ≫ post F G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasColimit (e.functor ⋙ F)
⊢ HasColimit F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
j j' : WidePullbackShape J
f : j ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match j with
      | none => f✝
      | some j => π j) ≫
      F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
j : J
⊢ ι F j ≫ colim.map α = α.app j ≫ ι G j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePullbackShape J)).obj none =
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      none

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePullbackShape J)).obj (some val✝) =
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePullbackShape J
⊢ (𝟭 (WidePullbackShape J)).obj j ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      none =
    (𝟭 (WidePullbackShape J')).obj none

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      (some val✝) =
    (𝟭 (WidePullbackShape J')).obj (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePullbackShape J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      j ≅
    (𝟭 (WidePullbackShape J')).obj j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
⊢ pre F E ≫ colim.map α = colim.map (E.whiskerLeft α) ≫ pre G E

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₁ = colim.map (whiskerRight α F) ≫ pre F E₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J C
F : J ⥤ C
⊢ pre F (𝟭 J) = colim.map F.leftUnitor.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
X✝ Y✝ : WidePullbackShape ι
f : X✝ ⟶ Y✝
⊢ F.map f ≫
      (match Y✝ with
        | none => base
        | some i => comp i).hom =
    (match X✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePushoutShape J
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Y✝ : WidePushoutShape J
f : X✝ ⟶ Y✝
⊢ Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
⊢ post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ post G H

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
f : J ⥤ C
c : C
⊢ Function.LeftInverse (fun g ↦ colimit.desc f { pt := c, ι := g }) fun g ↦
    { app := fun x ↦ colimit.ι f x ≫ g, naturality := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
f : J ⥤ C
c : C
⊢ Function.RightInverse (fun g ↦ colimit.desc f { pt := c, ι := g }) fun g ↦
    { app := fun x ↦ colimit.ι f x ≫ g, naturality := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F✝ F G : J ⥤ C
inst✝² : HasColimit F
inst✝¹ : HasColimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Epi (α.app j)
Z : C
u v : colimit G ⟶ Z
h : colimMap α ≫ u = colimMap α ≫ v
j : J
⊢ α.app j ≫ colimit.ι G j ≫ u = α.app j ≫ colimit.ι G j ≫ v

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J' C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasColimitsOfShape J C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : EssentiallySmall.{u₁, v₂, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasColimitsOfShape J C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ m = (P.lift s.unop).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.casesOn (motive := fun a a_1 x ↦
      X✝ = a → Z✝ = a_1 → f ≫ g ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs)) (f ≫ g)
      (fun X h ↦
        Eq.ndrec (motive := fun X ↦ Z✝ = X → f ≫ g ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs))
          (fun h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ (f ≫ g))
          h)
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ B objs))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ arrows j) ⋯ f)
          ⋯ (f ≫ g))
      ⋯ ⋯ ⋯ =
    Hom.casesOn (motive := fun a a_1 x ↦
        X✝ = a → Y✝ = a_1 → f ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) f
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦ Y✝ = X → f ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ f)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Y✝) → Y✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Y✝ B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ f)
        ⋯ ⋯ ⋯ ≫
      Hom.casesOn (motive := fun a a_1 x ↦
        Y✝ = a → Z✝ = a_1 → g ≍ x → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Z✝ B objs)) g
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦ Z✝ = X → g ≍ Hom.id X → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Z✝ B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : Y✝ ⟶ Y) → f ≍ Hom.id Y✝ → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn Y✝ B objs)) ⋯ g)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ g)
        ⋯ ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
j : WidePushoutShape J
⊢ F.obj j = (wideSpan (F.obj none) (fun j ↦ F.obj (some j)) fun j ↦ F.map (Hom.init j)).obj j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ m = (P.desc s.unop).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : 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✝
j j' : WidePushoutShape J
f : j ⟶ j'
⊢ (F.map f ≫
      match j' with
      | none => f✝
      | some j => ι j) =
    (match j with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePushoutShape J)).obj none =
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      none

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePushoutShape J)).obj (some val✝) =
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J
⊢ (𝟭 (WidePushoutShape J)).obj j ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      none =
    (𝟭 (WidePushoutShape J')).obj none

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      (some val✝) =
    (𝟭 (WidePushoutShape J')).obj (some val✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
⊢ m = (P.lift s.op).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      j ≅
    (𝟭 (WidePushoutShape J')).obj j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
j : J
⊢ π arrows j ≫ arrows j = base arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : 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
⊢ lift f fs w ≫ π arrows j = fs j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
⊢ lift f fs w ≫ base arrows = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : 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), g ≫ π arrows j = fs j) → g ≫ base arrows = f → g = lift f fs w

Tactic:
intro h1 h2

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : 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
⊢ g = lift f fs w
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : 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), g ≫ π arrows j = fs j) → g ≫ base arrows = f → g = lift f fs w

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : 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), (g ≫ π arrows j) ≫ arrows j = g ≫ base arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g : X ⟶ widePullback B objs arrows
⊢ g = lift (g ≫ base arrows) (fun j ↦ g ≫ π arrows j) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
⊢ m = (P.desc s.op).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
⊢ (∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j) → g1 ≫ base arrows = g2 ≫ base arrows → g1 = g2

Tactic:
intro h1 h2

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : 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
⊢ g1 = g2
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
⊢ (∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j) → g1 ≫ base arrows = g2 ≫ base arrows → g1 = g2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: 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 ι
⊢ lift t ≫ s.π.app j = t.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ k = l

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
⊢ ∀ (j : WidePullbackShape ι), s.π.app j = e.hom ≫ t.π.app j

Tactic:
by

Goal state after: