mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
inst✝⁵ : MonoidalCategory V
inst✝⁴ : BraidedCategory V
F G : C ⥤ V
η : F ⟶ G
H : C ⥤ V
inst✝³ : DayConvolution F H
inst✝² : DayConvolution H F
inst✝¹ : DayConvolution G H
inst✝ : DayConvolution H G
⊢ map η (𝟙 H) ≫ (braiding G H).hom = (braiding F H).hom ≫ map (𝟙 H) η

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ H) (unit F H)
  ext ⟨_, _⟩
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G G' : C ⥤ V
η : G ⟶ G'
c c' : C
f : c ⟶ c'
⊢ { obj := fun c ↦ (((Functor.whiskeringLeft₂ V).obj F.op).obj (tensorRight c ⋙ G)).obj MonoidalClosed.internalHom,
            map := fun {c c'} f ↦
              (((Functor.whiskeringLeft₂ V).obj F.op).map (Functor.whiskerRight ((curriedTensor C).flip.map f) G)).app
                MonoidalClosed.internalHom,
            map_id := ⋯, map_comp := ⋯ }.map
        f ≫
      (((Functor.whiskeringLeft₂ V).obj F.op).map ((tensorRight c').whiskerLeft η)).app MonoidalClosed.internalHom =
    (((Functor.whiskeringLeft₂ V).obj F.op).map ((tensorRight c).whiskerLeft η)).app MonoidalClosed.internalHom ≫
      { obj := fun c ↦ (((Functor.whiskeringLeft₂ V).obj F.op).obj (tensorRight c ⋙ G')).obj MonoidalClosed.internalHom,
            map := fun {c c'} f ↦
              (((Functor.whiskeringLeft₂ V).obj F.op).map (Functor.whiskerRight ((curriedTensor C).flip.map f) G')).app
                MonoidalClosed.internalHom,
            map_id := ⋯, map_comp := ⋯ }.map
        f

Tactic:
by
        ext j k
        dsimp
        simpa [-NatTrans.naturality] using!
          congr_arg (ihom <| F.obj <| unop j).map (η.naturality <| k ◁ f)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
| Δ ≫ A ◁ 𝒮 ≫ μ

pp: case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
| f

Tactic:
rw [antipode_right]

Goal state after:
case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
| ε ≫ η

case a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
| f
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
        ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
          P.X ◁ TensorBimod.actLeft Q L) ▷
      U.X ≫
    TensorBimod.actRight P (Q.tensorBimod L)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ P.X Q.X L.X).hom ▷ U.X

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ▷ U.X

Tactic:
erw [TensorBimod.π_tensor_id_actRight P (Q.tensorBimod L)]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ P.X (Q.tensorBimod L).X U.X).hom ≫
    P.X ◁ (Q.tensorBimod L).actRight ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
        ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ P.X Q.X L.X).hom ▷ U.X

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ▷ U.X
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (Δ ≫ A ◁ 𝒮 ≫ μ) ▷ A

pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ

Tactic:
rw [antipode_right]

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (ε ≫ η) ▷ A

case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (Δ ≫ A ◁ 𝒮 ≫ μ) ▷ A

pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮

Tactic:
rw [antipode_right]

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (ε ≫ η) ▷ A

case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (Δ ≫ A ◁ 𝒮 ≫ μ) ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ ε

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (ρ_ A).hom

Tactic:
rw [antipode_right]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (ε ≫ η) ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ ε

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (ρ_ A).hom
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y y' : C
f : x ⟶ x'
g : y ⟶ y'
⊢ (F.map f ⊗ₘ G.map g) ≫ (unit F G).app (x', y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ⊗ₘ g)

Tactic:
by
  simpa [tensorHom_def] using (unit F G).naturality (f ×ₘ g)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
c : C
v : V
f g : (F ⊛ G).obj c ⟶ v
h : ∀ {x y : C} (u : x ⊗ y ⟶ c), (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ f = (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ g
j : CostructuredArrow (tensor C) c
⊢ ((Functor.LeftExtension.mk (F ⊛ G) (unit F G)).coconeAt c).ι.app j ≫ f =
    ((Functor.LeftExtension.mk (F ⊛ G) (unit F G)).coconeAt c).ι.app j ≫ g

Tactic:
simpa using h j.hom

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 Y ⊗≫
      η_ X Y ▷ Y ⊗≫
        (𝟙 ((X ⊗ Y) ⊗ Y) ⊗≫
            X ◁ (β_ Y Y).hom ⊗≫ (β_ X Y).hom ▷ Y ⊗≫ Y ◁ (β_ Y X).inv ⊗≫ (β_ Y Y).inv ▷ X ⊗≫ 𝟙 (Y ⊗ Y ⊗ X)) ⊗≫
          Y ◁ ε_ X Y ⊗≫ 𝟙 Y =
    𝟙 Y ⊗≫ (η_ X Y ▷ Y ≫ (β_ (X ⊗ Y) Y).hom) ⊗≫ ((β_ Y (Y ⊗ X)).inv ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y

Tactic:
by
      simp [monoidalComp, braiding_tensor_left_hom, braiding_tensor_right_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : (j : J) → Category.{?u.14, u_2} (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
k l m : Total P
f : k.Hom l
g : l.Hom m
⊢ (P k.fst).ι.app k.snd ≫ D.map f.base ≫ D.map g.base = f.hom ≫ g.hom ≫ (P m.fst).ι.app m.snd

Tactic:
rw [f.w_assoc, g.w]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : (j : J) → Category.{u_3, u_2} (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : LocallySmall.{w, v_1, u_1} J
k l : Total P
f : (k ⟶ l) → (k.fst ⟶ l.fst) × ((P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd) := fun x ↦ (x.base, x.hom)
⊢ Function.Injective f

Tactic:
grind [Function.Injective, Total.Hom.ext]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝¹ : IsFiltered J
inst✝ : ∀ (j : J), IsFiltered (I j)
⊢ Nonempty (Total P)

Tactic:
by
  obtain ⟨j⟩ : Nonempty J := IsFiltered.nonempty
  obtain ⟨i⟩ : Nonempty (I j) := IsFiltered.nonempty
  exact ⟨⟨j, i⟩⟩

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') =
    (ConcreteCategory.hom (s.ι.app j)) x'
hy :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) y') =
    (ConcreteCategory.hom (s.ι.app j)) y'
⊢ x' ≤ y' ↔ (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'

Tactic:
refine ⟨fun h ↦ ⟨j, _, _, rfl, rfl, h⟩, fun ⟨k, x, y, hx', hy', h⟩ ↦ ?_⟩

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') =
    (ConcreteCategory.hom (s.ι.app j)) x'
hy :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) y') =
    (ConcreteCategory.hom (s.ι.app j)) y'
x✝ : (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'
k : J
x y : ↑(F.obj k)
hx' : (ConcreteCategory.hom (c.ι.app k)) x = (ConcreteCategory.hom (c.ι.app j)) x'
hy' : (ConcreteCategory.hom (c.ι.app k)) y = (ConcreteCategory.hom (c.ι.app j)) y'
h : x ≤ y
⊢ x' ≤ y'
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case mk
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₂ : D.IsTerminal e
prop_id✝ : D.W (𝟙 e)
lift✝ : {j : J} → D.P j → (j ⟶ e)
hlift✝ : ∀ {j : J} (hj : D.P j), D.W (lift✝ hj)
uniq✝ : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift✝ hj = φ
comm✝ : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift✝ ⋯ = lift✝ ⋯
this :
  @lift J inst✝ κ D e { prop_id := prop_id✝, lift := lift✝, hlift := hlift✝, uniq := uniq✝, comm := comm✝ } =
    @lift J inst✝ κ D e h₂
⊢ { prop_id := prop_id✝, lift := lift✝, hlift := hlift✝, uniq := uniq✝, comm := comm✝ } = h₂

Tactic:
cases h₂

Goal state after:
case mk.mk
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id✝¹ : D.W (𝟙 e)
lift✝¹ : {j : J} → D.P j → (j ⟶ e)
hlift✝¹ : ∀ {j : J} (hj : D.P j), D.W (lift✝¹ hj)
uniq✝¹ : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift✝¹ hj = φ
comm✝¹ : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift✝¹ ⋯ = lift✝¹ ⋯
prop_id✝ : D.W (𝟙 e)
lift✝ : {j : J} → D.P j → (j ⟶ e)
hlift✝ : ∀ {j : J} (hj : D.P j), D.W (lift✝ hj)
uniq✝ : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift✝ hj = φ
comm✝ : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift✝ ⋯ = lift✝ ⋯
this :
  @lift J inst✝ κ D e { prop_id := prop_id✝¹, lift := lift✝¹, hlift := hlift✝¹, uniq := uniq✝¹, comm := comm✝¹ } =
    @lift J inst✝ κ D e { prop_id := prop_id✝, lift := lift✝, hlift := hlift✝, uniq := uniq✝, comm := comm✝ }
⊢ { prop_id := prop_id✝¹, lift := lift✝¹, hlift := hlift✝¹, uniq := uniq✝¹, comm := comm✝¹ } =
    { prop_id := prop_id✝, lift := lift✝, hlift := hlift✝, uniq := uniq✝, comm := comm✝ }
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
⊢ ∃ j, ∀ (k : K), α k ≤ j

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `S)
   []
   [(Term.typeSpec ":" (Term.app `Set [`J.obj]))]
   ":="
   («term_∪_»
    (Term.paren
     (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
     (Set.«term⋃_,_»
      "⋃"
      (Batteries.ExtendedBinder.extBinders
       (Batteries.ExtendedBinder.extBinderCollection
        [(Batteries.ExtendedBinder.extBinderParenthesized
          "("
          (Batteries.ExtendedBinder.extBinder (Lean.binderIdent `k) [(group ":" `K)])
          ")")]))
      ","
      (Term.app `α [`k]))
     ")")
    "∪"
    (choice
     («term{_}» "{" [`m] "}")
     (Term.structInst
      "{"
      []
      (Term.structInstFields [(Term.structInstField (Term.structInstLVal `m []) [])])
      (Term.optEllipsis [])
      []
      "}"))))))

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
⊢ ∃ j, ∀ (k : K), α k ≤ j
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_2
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : ToType X → J
a : (x : ToType X) → j ⟶ k x
hk : ∀ (x : ToType X), (hom (F.map (a x))) (f.hom' x) = (hom (F.map (a x))) (g.hom' x)
⊢ ∃ k f_1, f ≫ F.map f_1 = g ≫ F.map f_1

Tactic:
replace hk : ∀ x, F.map (a x) (f x) = F.map (a x) (g x) := by assumption

Goal state after:
case refine_2
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : ToType X → J
a : (x : ToType X) → j ⟶ k x
hk : ∀ (x : ToType X), (hom (F.map (a x))) ((hom f) x) = (hom (F.map (a x))) ((hom g) x)
⊢ ∃ k f_1, f ≫ F.map f_1 = g ≫ F.map f_1
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X_1 π, S = Presieve.ofArrows X_1 π ∧ IsIso (Sigma.desc π)},
      ∃ T ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}, T.FactorsThruAlong S f

Tactic:
intro X Y f S ⟨α, hα, Z, π, hS, h_iso⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
⊢ ∃ T ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
m : coequalizer (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
⊢ (g₁ ≫ pullback.fst e k₁) ≫ e = g₂ ≫ pullback.fst k₂ e ≫ k₁

Tactic:
· simp [g₁, g₂, k₁, d]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
let S := Sieve.generate (Presieve.ofArrows Y π)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mpr.h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

Tactic:
exact fun _ _ hh ↦ by cases hh; exact h' _

Goal state after: