awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ G.hom.app i = (Over.Hom.left (α.app k)).app i ≫ (c.obj k).hom.app i

Tactic:
simp [← comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
refine_2 : l ≫ (Over.Hom.left (α.app k)).app i ≫ (c.obj k).hom.app i = s.snd
⊢ l ≫ G.hom.app i = s.snd

Tactic:
rw [show G.hom.app i = (α.app k).left.app i ≫ (c.obj k).hom.app i by simp [← comp_app]]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ app
        (Cone.π
          { pt := s.1,
            π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } })
        k ≫
      (c.obj k).hom.app i =
    s.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ l ≫ (Over.Hom.left (α.app k)).app i ≫ (c.obj k).hom.app i = s.snd

Tactic:
exact (hcᵢ.fac_assoc ..).trans (by simp)

Premises used: CategoryTheory.Limits.IsLimit.fac_assoc, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst
hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
k : J
refine_3 :
  (m ≫ (Over.Hom.left (α.app k)).app i) ≫ (c.obj k).left.map f =
    ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯ ≫ (c.obj k).left.map f
⊢ (m ≫ ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }).π.app k) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).left.map f =
    app
        (Cone.π
          { pt := s.1,
            π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } })
        k ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).left.map f

Tactic:
dsimp at *
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ G.left.map f = s.fst
hm₂ : m ≫ G.hom.app i = s.snd
k : J
⊢ (m ≫ (Over.Hom.left (α.app k)).app i) ≫ (c.obj k).left.map f =
    ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯ ≫ (c.obj k).left.map f

Tactic:
simp [← NatTrans.naturality, reassoc_of% hm₁]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst
hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
k : J
⊢ (m ≫ ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }).π.app k) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).hom.app i =
    app
        (Cone.π
          { pt := s.1,
            π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } })
        k ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).hom.app i

Tactic:
simpa [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
X Y : Under F
e : X ≅ Y
rw : Coequifibered X.hom → Coequifibered X.hom
⊢ Coequifibered X.hom → Coequifibered Y.hom

Tactic:
rw [← Under.w e.hom, Coequifibered.cancel_right_of_respectsIso]

Premises used: CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso, CategoryTheory.Under.w, CategoryTheory.NatTrans.Coequifibered
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
X Y : Under F
e : X ≅ Y
⊢ Coequifibered X.hom → Coequifibered X.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
⊢ IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom

Tactic:
have : IsClosedUnderIsomorphisms fun f : Under F ↦ f.hom.Coequifibered :=
    ⟨fun {X Y} e ↦ by rw [← Under.w e.hom, Coequifibered.cancel_right_of_respectsIso]; simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
⊢ ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ

Tactic:
have (a b : Cᵒᵖ) : HasCoproductsOfShape (a ⟶ b) Dᵒᵖ :=
    hasColimitsOfShape_of_equivalence (Discrete.equivalence Quiver.Hom.opEquiv)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this_1 : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
rw : (inverseImage (ObjectProperty.op fun (f : Under F) ↦ Coequifibered f.hom) e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ
⊢ IsClosedUnderColimitsOfShape (C := Under F) (fun (f : Under F) ↦ Coequifibered f.hom) J

Tactic:
rw [isClosedUnderColimitsOfShape_iff_op, ← isClosedUnderLimitsOfShape_inverseImage_iff _ _ e]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_op, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this_1 : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ IsClosedUnderLimitsOfShape (C := Over F.op) (fun (f : Over F.op) ↦ Equifibered f.hom) Jᵒᵖ

Tactic:
(inferInstance : IsClosedUnderLimitsOfShape (fun f : Over F.op ↦ f.hom.Equifibered) Jᵒᵖ)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this_1 : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
h :
  ∀ (f : Over F.op),
    inverseImage (ObjectProperty.op fun (f : Under F) ↦ Coequifibered f.hom) e.functor f ↔ Equifibered f.hom
⊢ (inverseImage (ObjectProperty.op fun (f : Under F) ↦ Coequifibered f.hom) e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ

Tactic:
convert!
    (inferInstance : IsClosedUnderLimitsOfShape (fun f : Over F.op ↦ f.hom.Equifibered) Jᵒᵖ) with f

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this_1 : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
f : Over F.op
h :
  Coequifibered.{v_2, u_3, v_4, u_4} (J := C) (C := D) (X := F.op.unop) (Y := f.left.unop)
      { app := fun (X : C) ↦ Quiver.Hom.unop (f.hom.app (Opposite.op X)), naturality := ⋯ } ↔
    Coequifibered (NatTrans.unop f.hom)
⊢ inverseImage (ObjectProperty.op fun (f : Under F) ↦ Coequifibered f.hom) e.functor f ↔ Equifibered f.hom

Tactic:
simp [e, MorphismProperty.cancel_left_of_respectsIso, ← coequifibered_unop_iff]

Premises used: CategoryTheory.NatTrans.coequifibered_unop_iff, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this_1 : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
f : Over F.op
⊢ Coequifibered.{v_2, u_3, v_4, u_4} (J := C) (C := D) (X := F.op.unop) (Y := f.left.unop)
      { app := fun (X : C) ↦ Quiver.Hom.unop (f.hom.app (Opposite.op X)), naturality := ⋯ } ↔
    Coequifibered (NatTrans.unop f.hom)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ CategoryStruct.comp (Y := pullback f g) (lift h k ⋯) (fst f g) = h ∧
    CategoryStruct.comp (Y := pullback f g) (lift h k ⋯) (snd f g) = k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ CategoryStruct.comp (Y := pushout f g) (inl f g) (desc h k ⋯) = h ∧
    CategoryStruct.comp (Y := pushout f g) (inr f g) (desc h k ⋯) = k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasLimit (cospan f g)
⊢ fst (limit.cone (cospan f g)) = pullback.fst f g

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasLimit (cospan f g)
⊢ snd (limit.cone (cospan f g)) = pullback.snd f g

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inst_1 : HasColimit (span f g)
⊢ inl (colimit.cocone (span f g)) = pushout.inl f g

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
inst_1 : HasColimit (span f g)
⊢ inr (colimit.cocone (span f g)) = pushout.inr f g

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ CategoryStruct.comp (Y := pullback f g) (lift h k w) (fst f g) = h

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ CategoryStruct.comp (Y := pullback f g) (lift h k w) (snd f g) = k

Tactic:
limit.lift_π _ _

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ CategoryStruct.comp (Y := pushout f g) (inl f g) (desc h k w) = h

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ CategoryStruct.comp (Y := pushout f g) (inr f g) (desc h k w) = k

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ Eq (α := pullback f g ⟶ Z) (fst f g ≫ f) (snd f g ≫ g)

Tactic:
PullbackCone.condition _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ Eq (α := X ⟶ pushout f g) (f ≫ inl f g) (g ≫ inr f g)

Tactic:
PushoutCocone.condition _

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
W : C
k l : W ⟶ pullback f g
h₀ : k ≫ fst f g = l ≫ fst f g
h₁ : k ≫ snd f g = l ≫ snd f g
⊢ k = l

Tactic:
limit.hom_ext <| PullbackCone.equalizer_ext _ h₀ h₁

Premises used: CategoryTheory.Limits.limit.hom_ext, CategoryTheory.Limits.PullbackCone.equalizer_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
W : C
k l : pushout f g ⟶ W
h₀ : inl f g ≫ k = inl f g ≫ l
h₁ : inr f g ≫ k = inr f g ≫ l
⊢ k = l

Tactic:
colimit.hom_ext <| PushoutCocone.coequalizer_ext _ h₀ h₁

Premises used: CategoryTheory.Limits.PushoutCocone.coequalizer_ext, CategoryTheory.Limits.colimit.hom_ext