awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ s ≫ i = t ≫ i

Tactic:
apply coequalizer.condition

Premises used: CategoryTheory.Limits.coequalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ IsColimit.{w, v₂, w, u₂} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (F :=
    Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
    (Cofan.mk (G.obj Q) fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦
      G.map
        (Sigma.ι.{w, v, u} (C := C)
          (fun (j : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj j.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) j))

Tactic:
apply isColimitOfHasCoproductOfPreservesColimit

Premises used: CategoryTheory.Limits.isColimitOfHasCoproductOfPreservesColimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ IsColimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
    (Cofan.mk (G.obj (sigmaObj.{w, v, u} K.obj)) fun (f : J) ↦ G.map (Sigma.ι K.obj f))

Tactic:
apply isColimitOfHasCoproductOfPreservesColimit

Premises used: CategoryTheory.Limits.isColimitOfHasCoproductOfPreservesColimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
l : IsColimit (Cofork.ofπ i ⋯)
w : s ≫ i = t ≫ i
⊢ IsColimit (F := parallelPair (G.map s) (G.map t)) (Cofork.ofπ (G.map i) ⋯ : Cofork (G.map s) (G.map t))

Tactic:
apply isColimitCoforkMapOfIsColimit

Premises used: CategoryTheory.Limits.isColimitCoforkMapOfIsColimit
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ ∀ (j : J),
    (G.map (Sigma.ι K.obj j) ≫ G.map (coequalizer.π s t)) ≫ 𝟙 (G.obj I) =
      G.map (colimit.ι (Discrete.functor K.obj) { as := j } ≫ coequalizer.π s t)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasCoequalizers.{v, u} C
inst_3 : HasFiniteCoproducts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape WalkingParallelPair G
inst_5 : PreservesFiniteCoproducts G
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J G

Tactic:
apply preservesColimit_of_preservesCoequalizers_and_coproduct

Premises used: CategoryTheory.Limits.preservesColimit_of_preservesCoequalizers_and_coproduct
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasPushouts.{v, u} C
⊢ HasFiniteColimits.{v, u} C

Tactic:
@hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts C _
    (@hasFiniteCoproducts_of_has_binary_and_initial C _
      (hasBinaryCoproducts_of_hasInitial_and_pushouts C) inferInstance)
    (@hasCoequalizers_of_hasPushouts_and_binary_coproducts C _
      (hasBinaryCoproducts_of_hasInitial_and_pushouts C) inferInstance)

Premises used: CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
⊢ HasFiniteColimits.{v, u} C

Tactic:
haveI : HasFiniteColimits C := hasFiniteColimits_of_hasInitial_and_pushouts
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this : HasFiniteColimits.{v, u} C
⊢ PreservesColimitsOfShape (Discrete WalkingPair) G

Tactic:
haveI : PreservesColimitsOfShape (Discrete WalkingPair) G :=
    preservesBinaryCoproducts_of_preservesInitial_and_pushouts G
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this : PreservesColimitsOfShape (Discrete WalkingPair) G
⊢ PreservesColimitsOfShape WalkingParallelPair G

Tactic:
haveI : PreservesColimitsOfShape (WalkingParallelPair) G :=
      (preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts G)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this_2 : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteColimits G

Tactic:
@preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts _ _ _ _ _ _ G _ ?_

Premises used: CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this_2 : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
_ : PreservesFiniteCoproducts G
⊢ PreservesFiniteColimits G

Tactic:
refine
    @preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts _ _ _ _ _ _ G _ ?_

Premises used: CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this_2 : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteCoproducts G

Tactic:
⟨fun _ ↦ ?_⟩

Premises used: CategoryTheory.Limits.PreservesFiniteCoproducts.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this_2 : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
refine : ∀ (x : ℕ), PreservesColimitsOfShape (Discrete (Fin x)) G
⊢ PreservesFiniteCoproducts G

Tactic:
refine ⟨fun _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this_2 : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x)) G

Tactic:
apply PreservesFiniteCoproducts.of_preserves_binary_and_initial G

Premises used: CategoryTheory.PreservesFiniteCoproducts.of_preserves_binary_and_initial
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasPullbacks.{v, u} C
⊢ HasPullbacks (Over.{v, u} B)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasEqualizers.{v, u} C
⊢ HasEqualizers (Over.{v, u} B)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePullbacks.{v, u} C
⊢ HasFiniteProducts (Over.{v, u} B)

Tactic:
have := ConstructProducts.over_finiteProducts_of_finiteWidePullbacks (B := B)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePullbacks.{v, u} C
this : HasFiniteProducts (Over.{v, u} B)
⊢ HasEqualizers (Over.{v, u} B)

Tactic:
have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePullbacks.{v, u} C
this_1 : HasFiniteProducts (Over.{v, u} B)
this : HasEqualizers (Over.{v, u} B)
⊢ HasFiniteLimits (Over.{v, u} B)

Tactic:
apply hasFiniteLimits_of_hasEqualizers_and_finite_products

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePullbacks.{w, v, u} C
⊢ HasBinaryProducts (Over.{v, u} B)

Tactic:
have := ConstructProducts.over_binaryProduct_of_pullback (B := B)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePullbacks.{w, v, u} C
this : HasBinaryProducts (Over.{v, u} B)
⊢ HasEqualizers (Over.{v, u} B)

Tactic:
have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePullbacks.{w, v, u} C
this_1 : HasBinaryProducts (Over.{v, u} B)
this : HasEqualizers (Over.{v, u} B)
⊢ HasProducts (Over.{v, u} B)

Tactic:
have := ConstructProducts.over_products_of_widePullbacks (B := B)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePullbacks.{w, v, u} C
this_1 : HasBinaryProducts (Over.{v, u} B)
this_2 : HasEqualizers (Over.{v, u} B)
this : HasProducts (Over.{v, u} B)
⊢ HasLimitsOfSize.{w, w, v, max u v} (Over.{v, u} B)

Tactic:
apply has_limits_of_hasEqualizers_and_products

Premises used: CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePushouts.{v, u} C
rw : HasFiniteLimits (Under.{v, u} B)ᵒᵖ
⊢ HasFiniteColimits (Under.{v, u} B)

Tactic:
rw [← hasFiniteLimits_opposite_iff]

Premises used: CategoryTheory.Limits.hasFiniteLimits_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePushouts.{v, u} C
⊢ HasFiniteLimits (Under.{v, u} B)ᵒᵖ

Tactic:
hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Over.opEquivOpUnder _).inverse

Premises used: CategoryTheory.Over.opEquivOpUnder, CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePushouts.{v, u} C
⊢ HasFiniteLimits (Under.{v, u} B)ᵒᵖ

Tactic:
exact hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Over.opEquivOpUnder _).inverse

Premises used: CategoryTheory.Over.opEquivOpUnder, CategoryTheory.Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePushouts.{w, v, u} C
rw : HasLimitsOfSize.{w, w, v, max u v} (Under.{v, u} B)ᵒᵖ
⊢ HasColimitsOfSize.{w, w, v, max u v} (Under.{v, u} B)

Tactic:
rw [← hasLimitsOfSize_opposite_iff]

Premises used: CategoryTheory.Limits.hasLimitsOfSize_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePushouts.{w, v, u} C
⊢ HasLimitsOfSize.{w, w, v, max u v} (Under.{v, u} B)ᵒᵖ

Tactic:
hasLimits_of_hasLimits_createsLimits (Over.opEquivOpUnder _).inverse

Premises used: CategoryTheory.Over.opEquivOpUnder, CategoryTheory.hasLimits_of_hasLimits_createsLimits, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePushouts.{w, v, u} C
⊢ HasLimitsOfSize.{w, w, v, max u v} (Under.{v, u} B)ᵒᵖ

Tactic:
exact hasLimits_of_hasLimits_createsLimits (Over.opEquivOpUnder _).inverse

Premises used: CategoryTheory.Over.opEquivOpUnder, CategoryTheory.hasLimits_of_hasLimits_createsLimits, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : Quiver.Hom (V := Functor.{v', v_1, u', u_1} J D) (Functor.obj (Functor.const J) (K.obj c.pt))
  (Functor.obj (Functor.const J) B) :=
  Iso.inv (Functor.constComp J c.pt K) ≫ Functor.whiskerRight c.π K ≫ natTransInCostructuredArrow F
⊢ z.app j = z.app (Classical.arbitrary J)

Tactic:
(nat_trans_from_is_connected z j (Classical.arbitrary J))

Premises used: Classical.arbitrary, CategoryTheory.nat_trans_from_is_connected
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : Quiver.Hom (V := Functor.{v', v_1, u', u_1} J D) (Functor.obj (Functor.const J) (K.obj c.pt))
  (Functor.obj (Functor.const J) B) :=
  Iso.inv (Functor.constComp J c.pt K) ≫ Functor.whiskerRight c.π K ≫ natTransInCostructuredArrow F
h :
  (K.obj
          (Functor.obj
              (Functor.obj (Functor.const J)
                (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
              j).left ⟶
        B) =
      (Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) (K.obj c.pt)) j ⟶
        Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) B) j) →
    K.map (c.π.app j) ≫ (F.obj j).hom = z.app j
h₁ :
  (K.obj
          (Functor.obj
              (Functor.obj (Functor.const J)
                (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
              j).left ⟶
        B) =
      (Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) (K.obj c.pt)) j ⟶
        Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) B) j) →
    (Functor.obj
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          j).hom =
      z.app (Classical.arbitrary J)
⊢ K.map (c.π.app j) ≫ (F.obj j).hom =
    (Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        j).hom

Tactic:
convert! (nat_trans_from_is_connected z j (Classical.arbitrary J))

Premises used: Classical.arbitrary, CategoryTheory.nat_trans_from_is_connected
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : Quiver.Hom (V := Functor.{v', v_1, u', u_1} J D) (Functor.obj (Functor.const J) (K.obj c.pt))
  (Functor.obj (Functor.const J) B) :=
  Iso.inv (Functor.constComp J c.pt K) ≫ Functor.whiskerRight c.π K ≫ natTransInCostructuredArrow F
e_1 :
  (K.obj
        (Functor.obj
            (Functor.obj (Functor.const J)
              (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
            j).left ⟶
      B) =
    (Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) (K.obj c.pt)) j ⟶
      Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) B) j)
⊢ K.map (c.π.app j) ≫ (F.obj j).hom = z.app j

Tactic:
simp [z]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : Quiver.Hom (V := Functor.{v', v_1, u', u_1} J D) (Functor.obj (Functor.const J) (K.obj c.pt))
  (Functor.obj (Functor.const J) B) :=
  Iso.inv (Functor.constComp J c.pt K) ≫ Functor.whiskerRight c.π K ≫ natTransInCostructuredArrow F
e_1 :
  (K.obj
        (Functor.obj
            (Functor.obj (Functor.const J)
              (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
            j).left ⟶
      B) =
    (Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) (K.obj c.pt)) j ⟶
      Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) B) j)
⊢ (Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        j).hom =
    z.app (Classical.arbitrary J)

Tactic:
simp [z]