mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯ ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))

Tactic:
Wedge.IsLimit.lift_ι

Goal state after:
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✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
⊢ G.map f ≫ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
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 H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c j : C
⊢ Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c))

Tactic:
Wedge.IsLimit.lift_ι

Goal state after:
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 H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c j : C
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c))
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| { pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } }.π.app j ▷ limit H ≫
    (α_ (F.obj j) (G.obj j) (limit H)).hom ≫
      F.obj j ◁ G.obj j ◁ limit.π H j ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).inv ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| { pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } }.π.app j ▷ limit H ≫
    (α_ (F.obj j) (G.obj j) (limit H)).hom ≫ F.obj j ◁ G.obj j ◁ limit.π H j ≫ 𝟙 (F.obj j ⊗ G.obj j ⊗ H.obj j)
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (limit F)).hom ≫ limit.π F j =
    (limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } } ≫
          limit.π (𝟙_ (J ⥤ C)) j) ▷
        limit F ≫
      (λ_ (limit F)).hom ≫ limit.π F j

Tactic:
limit.lift_π

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (limit F)).hom ≫ limit.π F j =
    { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ▷ limit F ≫
      (λ_ (limit F)).hom ≫ limit.π F j
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁
        (limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } } ≫
          limit.π (𝟙_ (J ⥤ C)) j) ≫
      (ρ_ (limit F)).hom ≫ limit.π F j

Tactic:
limit.lift_π

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁ { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ≫
      (ρ_ (limit F)).hom ≫ limit.π F j
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
⊢ 𝟙 X ⊗≫
      X ◁ η_ X Y ⊗≫
        (𝟙 (X ⊗ X ⊗ Y) ⊗≫
            (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)) ⊗≫
          ε_ X Y ▷ X ⊗≫ 𝟙 X =
    𝟙 X ⊗≫ (X ◁ η_ X Y ≫ (β_ X (X ⊗ Y)).hom) ⊗≫ ((β_ (Y ⊗ X) X).inv ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X

Tactic:
by
      simp [monoidalComp, braiding_tensor_right_hom, braiding_tensor_left_inv]

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
⊢ (η_ X Y ≫ (β_ Y X).inv) ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ ((β_ X Y).hom ≫ ε_ X Y) = (λ_ Y).hom ≫ (ρ_ Y).inv

Tactic:
rw [Iso.eq_comp_inv, ← Iso.inv_comp_eq_id]
  calc
    _ = 𝟙 Y ⊗≫ η_ X Y ▷ Y ⊗≫ ((β_ Y X).inv ▷ Y ⊗≫ Y ◁ (β_ X Y).hom) ≫ Y ◁ ε_ X Y ⊗≫ 𝟙 Y := by
      monoidal
    _ = 𝟙 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 := by
      congr 3
      on_goal 2 => simp [monoidalComp]
      simp only [monoidalComp, MonoidalCoherence.assoc_iso, MonoidalCoherence.whiskerRight_iso,
        MonoidalCoherence.refl_iso, whiskerRightIso_refl, Iso.trans_refl,
        MonoidalCoherence.assoc'_iso, Iso.refl_trans, Iso.symm_hom, comp_id, id_comp]
      iterate 2 rw [← IsIso.eq_inv_comp]
      repeat rw [← assoc]
      iterate 4 rw [← IsIso.comp_inv_eq]
      simpa using (yang_baxter Y X Y).symm
    _ = 𝟙 Y ⊗≫ (η_ X Y ▷ Y ≫ (β_ (X ⊗ Y) Y).hom) ⊗≫ ((β_ Y (Y ⊗ X)).inv ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y := by
      simp [monoidalComp, braiding_tensor_left_hom, braiding_tensor_right_inv]
    _ = _ := by
      rw [braiding_naturality_left, ← braiding_inv_naturality_left]
      simp [monoidalComp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f✝ : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow C
hf✝ : f ∈ (ofHoms f✝).toSet
hf : ∃ i, Arrow.mk f.hom = Arrow.mk (f✝ i)
⊢ ∃ a, (fun i ↦ ⟨Arrow.mk (f✝ i), ⋯⟩) a = ⟨f, hf✝⟩

Tactic:
obtain ⟨i, hf⟩ := hf

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f✝ : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow C
hf✝ : f ∈ (ofHoms f✝).toSet
i : ι
hf : Arrow.mk f.hom = Arrow.mk (f✝ i)
⊢ ∃ a, (fun i ↦ ⟨Arrow.mk (f✝ i), ⋯⟩) a = ⟨f, hf✝⟩
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ A.map f ≫ ε.app Y✝ = ε.app X✝

Tactic:
rw [ε[A].naturality, tensorUnit_map]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ε.app X✝ ≫ 𝟙 (𝟙_ D) = ε.app X✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ A.map f ≫ Δ = Δ ≫ (A.map f ⊗ₘ A.map f)

Tactic:
by dsimp; rw [Δ[A].naturality, tensorObj_map]

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✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ map ((ι C V D).map f) (𝟙 ((ι C V D).obj (𝟙_ D))) ≫
      (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj Y✝)).hom =
    (ι C V D).map (ρ_ X✝).hom ≫ (ι C V D).map f

Tactic:
ι_map_rightUnitor_hom_eq_rightUnitor_hom

Goal state after:
C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ map ((ι C V D).map f) (𝟙 ((ι C V D).obj (𝟙_ D))) ≫
      (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj Y✝)).hom =
    (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj X✝)).hom ≫ (ι C V D).map f
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✝
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
inst✝ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
d d' : D
⊢ ∀ ⦃X Y : C × C⦄ (f : X ⟶ Y),
    ((ι C V D).obj d ⊠ (ι C V D).obj d').map f ≫ convolutionUnitApp V d d' Y.1 Y.2 =
      convolutionUnitApp V d d' X.1 X.2 ≫ (tensor C ⋙ (ι C V D).obj (tensorObj C V d d')).map f

Tactic:
intros
        simp only [convolutionUnitApp_eq, Category.assoc, NatTrans.naturality_assoc]
        simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ localEpi (fun x ↦ x ∈ Set.range G.obj) (f ≫ adj.unit.app Y) ↔ Epi (F.map f)

Tactic:
dsimp% adj.unit.naturality f,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ localEpi (fun x ↦ x ∈ Set.range G.obj) (adj.unit.app X ≫ G.map (F.map f)) ↔ Epi (F.map f)
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝¹ g : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f✝ : u ⟶ v
X✝ Y✝ : RightFreyd V
f : X✝.as ⟶ Y✝.as
⊢ Nonempty (ColimitCocone (parallelPair ((quotient V).map f) 0))

Tactic:
exact ⟨_, Candidate.isColimitCokernelCofork f⟩

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₂ a b = m₂ b a

Tactic:
simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib e₂ a b e₂

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ Projective P → (MorphismProperty.epimorphisms C).llp 0

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ (MorphismProperty.epimorphisms C).llp 0 → Projective P

Tactic:
· intro _ X Y p (_ : Epi p)
    exact Projective.hasLiftingProperty_of_isZero 0 p hZ

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ (MorphismProperty.epimorphisms C).llp 0 → Projective P
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
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : ↑(F.obj l)
h₃ : x₃ = (ConcreteCategory.hom (F.map a)) x₁
h₄ : x₃ = (ConcreteCategory.hom (F.map b)) x₂
h₅ : y₃ = (ConcreteCategory.hom (F.map a)) y₁
h₆ : y₃ = (ConcreteCategory.hom (F.map b)) y₂
⊢ x = y

Tactic:
have h₇ : x₃ = y₃ :=
      le_antisymm
        (by simpa only [h₃, h₅] using (F.map a).hom.monotone h₁)
        (by simpa only [h₄, h₆] using (F.map b).hom.monotone h₂)

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l : J
a : j ⟶ l
b : k ⟶ l
x₃ y₃ : ↑(F.obj l)
h₃ : x₃ = (ConcreteCategory.hom (F.map a)) x₁
h₄ : x₃ = (ConcreteCategory.hom (F.map b)) x₂
h₅ : y₃ = (ConcreteCategory.hom (F.map a)) y₁
h₆ : y₃ = (ConcreteCategory.hom (F.map b)) y₂
h₇ : x₃ = y₃
⊢ x = y
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
hf : ∃ i, (D i).W f✝
⊢ (∃ a, (D a).P i✝) ∨ m = i✝

Tactic:
obtain ⟨i, hf⟩ := hf

Goal state after:
case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
i : ι
hf : (D i).W f✝
⊢ (∃ a, (D a).P i✝) ∨ m = i✝
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
hf : ∃ i, (D i).W f✝
⊢ (∃ a, (D a).P j✝) ∨ m = j✝

Tactic:
obtain ⟨i, hf⟩ := hf

Goal state after:
case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
i : ι
hf : (D i).W f✝
⊢ (∃ a, (D a).P j✝) ∨ m = j✝
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
this : ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ π = h ≫ f
⊢ ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f

Tactic:
obtain ⟨W, h, _, i, this⟩ := this

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf : ∃ i, (D i).W f
⊢ f = φ ⟨i, ⟨j, hj⟩⟩

Tactic:
obtain ⟨i, hf⟩ := hf

Goal state after:
case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
i✝ : ι
j : J
hj : (D i✝).P j
f : j ⟶ m
i : ι
hf : (D i).W f
⊢ f = φ ⟨i✝, ⟨j, hj⟩⟩
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_4.inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j k : J
f : j ⟶ k
hf : ∃ i, (D i).W f
⊢ ∃ li lj, (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li

Tactic:
obtain ⟨i, hf⟩ := hf

Goal state after:
case refine_4.inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j k : J
f : j ⟶ k
i : ι
hf : (D i).W f
⊢ ∃ li lj, (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ IsSheaf (extensiveTopology C) F

Tactic:
rw [extensiveTopology, Presieve.isSheaf_coverage]
    intro X R ⟨Y, α, Z, π, hR, hi⟩
    have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi
    have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩
    exact isSheafFor_extensive_of_preservesFiniteProducts R F

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
⊢ S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B ↔ S ∈ (coherentTopology C) B

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B
⊢ S ∈ (coherentTopology C) B

case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (coherentTopology C) B
⊢ S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
this : IsIso (coproductUniqueIso fun x ↦ X).hom
⊢ IsIso (Sigma.desc (Cofan.mk X fun x ↦ 𝟙 X).inj)

Tactic:
exact this

Goal state after: