mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ ((Functor.const J).obj Z).map g ≫ f ⋯ = f ⋯ ≫ F.map g

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j j' : J
g : j ⟶ j'
⊢ 𝟙 Z ≫ f ⋯ = f ⋯ ≫ F.map g
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
x : t.pt
⊢ (hom m).toFun x = (hom (↾fun x ↦ (hom (s.ι.app (α x))) (f x))).toFun x

Tactic:
dsimp

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
x : t.pt
⊢ (hom m) x = (hom (s.ι.app (α x))) (f x)
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝² : Category.{w, v} J
F : J ⥤ Type u
inst✝¹ : IsFilteredOrEmpty J
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ (hom ((colimitCocone F).ι.app i)) xi = (hom ((colimitCocone F).ι.app j)) xj ↔ FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩

Tactic:
dsimp

Goal state after:
J : Type v
inst✝² : Category.{w, v} J
F : J ⥤ Type u
inst✝¹ : IsFilteredOrEmpty J
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ (equivShrink F.ColimitType) (F.ιColimitType i xi) = (equivShrink F.ColimitType) (F.ιColimitType j xj) ↔
    FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, 0⟩.fst))) ⟨j, 0⟩.snd *
          (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, 0⟩.fst))) ⟨j, x⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
dsimp

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat) ⟨j, 0 * x⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
x y : M F
⊢ ∀ (a₁ a₂ b : (j : J) × ↑(F.obj j)),
    (F ⋙ forget MonCat).ColimitTypeRel a₁ a₂ → colimitMulAux F a₁ b = colimitMulAux F a₂ b

Tactic:
· intro x x' y h
      apply colimitMulAux_eq_of_rel_left
      apply Types.FilteredColimit.rel_of_colimitTypeRel
      exact h

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ (ConcreteCategory.hom (F.map α))
      ⟨IsFiltered.max ⟨⟨j₁, x⟩.fst, ⟨j₁, x⟩.snd⟩.fst ⟨⟨j₂, y⟩.fst, ⟨j₂, y⟩.snd⟩.fst,
          (ConcreteCategory.hom
                (F.map (IsFiltered.leftToMax ⟨⟨j₁, x⟩.fst, ⟨j₁, x⟩.snd⟩.fst ⟨⟨j₂, y⟩.fst, ⟨j₂, y⟩.snd⟩.fst)))
              ⟨⟨j₁, x⟩.fst, ⟨j₁, x⟩.snd⟩.snd *
            (ConcreteCategory.hom
                (F.map (IsFiltered.rightToMax ⟨⟨j₁, x⟩.fst, ⟨j₁, x⟩.snd⟩.fst ⟨⟨j₂, y⟩.fst, ⟨j₂, y⟩.snd⟩.fst)))
              ⟨⟨j₂, y⟩.fst, ⟨j₂, y⟩.snd⟩.snd⟩.snd =
    (ConcreteCategory.hom (F.map β))
      ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩.snd

Tactic:
dsimp

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ (ConcreteCategory.hom (F.map α))
      ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax j₁ j₂))) x *
        (ConcreteCategory.hom (F.map (IsFiltered.rightToMax j₁ j₂))) y) =
    (ConcreteCategory.hom (F.map β)) ((ConcreteCategory.hom (F.map f)) x * (ConcreteCategory.hom (F.map g)) y)
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, x⟩.fst))) ⟨j, x⟩.snd *
          (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, x⟩.fst))) ⟨j, 0⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
dsimp

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat) ⟨j, x * 0⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
      (M.mk F
        ⟨IsFiltered.max i j,
          (ConcreteCategory.hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd *
            (ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩) =
    (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨i, x⟩) *
      (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨j, y⟩)

Tactic:
dsimp

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (ConcreteCategory.hom (t.ι.app (IsFiltered.max i j)))
      ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax i j))) x *
        (ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) y) =
    (ConcreteCategory.hom (t.ι.app i)) x * (ConcreteCategory.hom (t.ι.app j)) y
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
i : J
x : ↑((F ⋙ forget₂ CommMonCat MonCat).obj i)
j : J
y : ↑((F ⋙ forget₂ CommMonCat MonCat).obj j)
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      ⟨k,
        (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map f)) ⟨i, x⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map g)) ⟨j, y⟩.snd⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat)
      ⟨k,
        (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map g)) ⟨j, y⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ CommMonCat MonCat).map f)) ⟨i, x⟩.snd⟩

Tactic:
dsimp

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
i : J
x : ↑((F ⋙ forget₂ CommMonCat MonCat).obj i)
j : J
y : ↑((F ⋙ forget₂ CommMonCat MonCat).obj j)
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨k, (Hom.hom (F.map f)) x * (Hom.hom (F.map g)) y⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨k, (Hom.hom (F.map g)) y * (Hom.hom (F.map f)) x⟩
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m : ℕ
⊢ ∀ (f : Opposite.op n ⟶ Opposite.op m),
    (ConcreteCategory.hom (F.map f))
        ((fun x ↦
            match x with
            | Opposite.op n => preimage hF a n)
          (Opposite.op n)) =
      (fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op m)

Tactic:
⟨⟨⟨(h : m ≤ n)⟩⟩⟩

Goal state after:
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m : ℕ
h : m ≤ n
⊢ (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op n)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
h' : m ≤ p
⊢ (ConcreteCategory.hom (F.map (Opposite.op { down := { down := ⋯ } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p.succ)) =
    (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p))

Tactic:
erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
      comp_apply, (hF p _).choose_spec]

Goal state after:
case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
h' : m ≤ p
⊢ (ConcreteCategory.hom (F.map (homOfLE h').op)) (preimage hF a p) =
    (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p))
Module: Mathlib.CategoryTheory.Limits.Preserves.Limits

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesLimit F G
inst✝³ : HasLimit F
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ ((lim ⋙ G).map f ≫ (preservesLimitIso G Y✝).hom) ≫ limit.π (((Functor.whiskeringRight J C D).obj G).obj Y✝) j =
    ((preservesLimitIso G X✝).hom ≫ ((Functor.whiskeringRight J C D).obj G ⋙ lim).map f) ≫
      limit.π (((Functor.whiskeringRight J C D).obj G).obj Y✝) j

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesLimit F G
inst✝³ : HasLimit F
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ (G.map (limMap f) ≫ (preservesLimitIso G Y✝).hom) ≫ limit.π (Y✝ ⋙ G) j =
    ((preservesLimitIso G X✝).hom ≫ limMap (Functor.whiskerRight f G)) ≫ limit.π (Y✝ ⋙ G) j
Module: Mathlib.CategoryTheory.Limits.Preserves.Limits

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (((Functor.whiskeringRight J C D).obj G).obj X✝) j ≫ (preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f =
    colimit.ι (((Functor.whiskeringRight J C D).obj G).obj X✝) j ≫
      ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f ≫ (preservesColimitIso G Y✝).inv

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    colimit.ι (X✝ ⋙ G) j ≫ colimMap (Functor.whiskerRight f G) ≫ (preservesColimitIso G Y✝).inv
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B × C ⥤ D
x✝² x✝¹ : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (uncurry.obj (curry.obj F)).map (f₁, f₂) = eqToHom ⋯ ≫ F.map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B × C ⥤ D
x✝² x✝¹ : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ F.map (f₁ ×ₘ 𝟙 x₂) ≫ F.map (𝟙 y₁ ×ₘ f₂) = 𝟙 (F.obj (x₁, x₂)) ≫ F.map (f₁, f₂) ≫ 𝟙 (F.obj (y₁, y₂))
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip).map (f₁, f₂) = eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ G.map (F₁.map f₁ ×ₘ 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁) ×ₘ F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁ ×ₘ F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip)).map (f₁, f₂) =
    eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp

Goal state after:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ G.map (F₁.map f₁ ×ₘ 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁) ×ₘ F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁ ×ₘ F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
X : C
s : ↑(F ⋙ coyoneda.obj (op X)).sections
j j' : J
f : j ⟶ j'
⊢ ((const J).obj X).map f ≫ ↑s j' = ↑s j ≫ F.map f

Tactic:
dsimp

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
X : C
s : ↑(F ⋙ coyoneda.obj (op X)).sections
j j' : J
f : j ⟶ j'
⊢ 𝟙 X ≫ ↑s j' = ↑s j ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
X : C
s : ↑(F.op ⋙ yoneda.obj X).sections
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ↑s (op j') = ↑s (op j) ≫ ((const J).obj X).map f

Tactic:
dsimp

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
X : C
s : ↑(F.op ⋙ yoneda.obj X).sections
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ↑s (op j') = ↑s (op j) ≫ 𝟙 X
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ Cᵒᵖ
X : C
s : ↑(F ⋙ yoneda.obj X).sections
j j' : J
f : j ⟶ j'
⊢ ((const J).obj (op X)).map f ≫ Quiver.Hom.op (↑s j') = Quiver.Hom.op (↑s j) ≫ F.map f

Tactic:
dsimp

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ Cᵒᵖ
X : C
s : ↑(F ⋙ yoneda.obj X).sections
j j' : J
f : j ⟶ j'
⊢ 𝟙 (op X) ≫ (↑s j').op = (↑s j).op ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  (IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ ((Cone.postcompose (isoWhiskerRight h F).hom).obj ((Cone.postcompose (isoWhiskerRight h F).inv).obj c)).π.app j =
    (Iso.refl
          ((Cone.postcompose (isoWhiskerRight h F).hom).obj
              ((Cone.postcompose (isoWhiskerRight h F).inv).obj c)).pt).hom ≫
      c.π.app j

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  (IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (c.π.app j ≫ F.map (h.inv.app j)) ≫ F.map (h.hom.app j) = 𝟙 c.pt ≫ c.π.app j
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  (IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ ((Cocone.precompose (isoWhiskerRight h F).inv).obj ((Cocone.precompose (isoWhiskerRight h F).hom).obj c)).ι.app j ≫
      (Iso.refl
          ((Cocone.precompose (isoWhiskerRight h F).inv).obj
              ((Cocone.precompose (isoWhiskerRight h F).hom).obj c)).pt).hom =
    c.ι.app j

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  (IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (F.map (h.inv.app j) ≫ F.map (h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
x✝ : Cᵒᵖ
⊢ Small.{w, v} ((yoneda.obj X).obj x✝)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
x✝ : Cᵒᵖ
⊢ Small.{w, v} (unop x✝ ⟶ X)
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P Q : Cᵒᵖ ⥤ Type w
α : shrinkYoneda.{w, v, u}.obj X ⟶ P
β : P ⟶ Q
⊢ shrinkYonedaEquiv (α ≫ β) = (ConcreteCategory.hom (β.app (op X))) (shrinkYonedaEquiv α)

Tactic:
simp [shrinkYonedaEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
x✝ : C
⊢ Small.{w, v} ((coyoneda.obj X).obj x✝)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
x✝ : C
⊢ Small.{w, v} (unop X ⟶ x✝)
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j k : J
⊢ F.obj k ⟶ ((Functor.const J).obj (of R ↑c.pt)).obj k

Tactic:
letI : Algebra R c.pt := algebraOfIsFiltered hc j
    refine AlgCat.ofHom { __ := (c.ι.app k).hom, commutes' r := ?_ }
    simp [RingHom.algebraMap_toAlgebra', ← c.w (IsFiltered.leftToMax j k),
      ← c.w (IsFiltered.rightToMax j k)]

Goal state after: