mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ ∀ (j : J),
    (hc.lift { pt := 𝟙_ C, π := { app := fun X ↦ η, naturality := ⋯ } } ▷ c.pt ≫
          hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } }) ≫
        c.π.app j =
      (λ_ c.pt).hom ≫ c.π.app j

Tactic:
by simp [whiskerRight_comp_tensorHom_assoc]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
⊢ ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((tensoringLeft D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((tensoringLeft C).map f))

Tactic:
have vcomp1 := mateEquiv_conjugateEquiv_vcomp
    (ihom.adjunction A) (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))
    ((prodComparisonNatIso F A).inv) (((curriedTensor D).map (F.map f)))

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
⊢ ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((tensoringLeft D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((tensoringLeft C).map f))
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry (F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ (ihom (F₁.obj k₁.right)).map (F₃.map (Under.Hom.right φ)) =
    curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right) ≫ (pre (F₁.map (Under.Hom.right φ))).app (F₃.obj k₂.right)

Tactic:
← curry_natural_right,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ curry ((F₁.obj k₁.right ◁ F₂.map k₁.hom ≫ f.app k₁.right) ≫ F₃.map (Under.Hom.right φ)) =
    curry (F₁.obj k₂.right ◁ F₂.map k₂.hom ≫ f.app k₂.right) ≫ (pre (F₁.map (Under.Hom.right φ))).app (F₃.obj k₂.right)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        B ◁ (reflectorAdjunction i).unit.app A ≫
          uncurry
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                uncurry
                  ((reflectorAdjunction i).unit.app B ≫
                    curry (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)))) =
    prodComparison (reflector i) A B

Tactic:
uncurry_curry,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        B ◁ (reflectorAdjunction i).unit.app A ≫
          (β_ B (i.obj ((reflector i).obj A))).hom ≫
            uncurry
              ((reflectorAdjunction i).unit.app B ≫
                curry (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)) =
    prodComparison (reflector i) A B
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        B ◁ (reflectorAdjunction i).unit.app A ≫
          (β_ B (i.obj ((reflector i).obj A))).hom ≫
            i.obj ((reflector i).obj A) ◁ (reflectorAdjunction i).unit.app B ≫
              uncurry (curry (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)) =
    prodComparison (reflector i) A B

Tactic:
uncurry_curry,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        B ◁ (reflectorAdjunction i).unit.app A ≫
          (β_ B (i.obj ((reflector i).obj A))).hom ≫
            i.obj ((reflector i).obj A) ◁ (reflectorAdjunction i).unit.app B ≫
              (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B
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:
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.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 : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C
this :
  ∀ (β : F ⊠ H ⟶ tensor C ⋙ G) (X : C × C),
    (DayConvolution.unit F H).app X ≫ ((F ⊛ H).descOfIsLeftKanExtension (DayConvolution.unit F H) G β).app (X.1 ⊗ X.2) =
      β.app X
⊢ (DayConvolution.unit F H).app (x, y) ≫ ℌ.ev_app.app (x ⊗ y) = MonoidalClosed.uncurry (ℌ.π y x)

Tactic:
simp [this, ev_app]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
⊢ EckmannHilton.IsUnital (fun x1 x2 ↦ leftAdd X Y x1 x2) 0

Tactic:
have hl : ∀ f : X ⟶ Y, biprod.lift f (0 : X ⟶ Y) = f ≫ biprod.inl := by
    intro f
    ext
    · simp
    · simp [biprod.lift_snd, Category.assoc, comp_zero]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
⊢ EckmannHilton.IsUnital (fun x1 x2 ↦ leftAdd X Y x1 x2) 0
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
⊢ f ≠ 0

Tactic:
by
    intro h
    apply id_nonzero X
    simp only [← IsIso.hom_inv_id f, h, zero_comp]

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

Goal state before:
pp: α β : PartOrdEmb
f : α ⟶ β
hf : IsIso ((forget PartOrdEmb).map f)
⊢ IsIso f

Tactic:
by
    rw [CategoryTheory.isIso_iff_bijective] at hf
    let e : α ≃o β :=
      { toEquiv := Equiv.ofBijective _ hf
        map_rel_iff' := by simp }
    exact (Iso.mk e).isIso_hom

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

Goal state before:
pp: 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, (D i).W) ⊔ MorphismProperty.ofHoms fun x ↦ 𝟙 m) ⊔
          MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst)
        f →
      (∃ a, (D a).P i) ∨ m = i

Tactic:
rintro _ _ _ ((hf | ⟨⟨⟩⟩) | ⟨i, j, hj⟩)

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✝
hf : (⨆ i, (D i).W) f✝
⊢ (∃ a, (D a).P i✝) ∨ m = i✝

case inl.inr
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
X Y : J
i✝ : Unit
⊢ (∃ a, (D a).P m) ∨ m = m

case inr
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
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ a, (D a).P ↑⟨i, ⟨j, hj⟩⟩.snd) ∨ m = ↑⟨i, ⟨j, hj⟩⟩.snd
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_1
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
f : X ⟶ c.pt
j : X → J
g : (x : X) → (fun X ↦ X) (F.obj (j x))
hg : ∀ (x : X), (hom (c.ι.app (j x))) (g x) = (hom f) x
x : X
⊢ (hom f).toFun x =
    (hom
          ((↾fun x ↦ (hom (F.map (IsCardinalFiltered.toMax j hX x))) (g x)) ≫
            c.ι.app (IsCardinalFiltered.max j hX))).toFun
      x

Tactic:
dsimp at j g hg x ⊢

Goal state after:
case refine_1
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
f : X ⟶ c.pt
j : X → J
g : (x : X) → F.obj (j x)
hg : ∀ (x : X), (hom (c.ι.app (j x))) (g x) = (hom f) x
x : X
⊢ (hom f) x = (hom (c.ι.app (IsCardinalFiltered.max j hX))) ((hom (F.map (IsCardinalFiltered.toMax j hX x))) (g x))
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: 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, (D i).W) ⊔ MorphismProperty.ofHoms fun x ↦ 𝟙 m) ⊔
          MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst)
        f →
      (∃ a, (D a).P j) ∨ m = j

Tactic:
rintro _ _ _ ((hf | ⟨⟨⟩⟩) | ⟨i, j, hj⟩)

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✝
hf : (⨆ i, (D i).W) f✝
⊢ (∃ a, (D a).P j✝) ∨ m = j✝

case inl.inr
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
X Y : J
i✝ : Unit
⊢ (∃ a, (D a).P m) ∨ m = m

case inr
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
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ (∃ a, (D a).P m) ∨ m = m
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsSmall.{w, v, u} W
inst✝¹ : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
inst✝ : HasColimitsOfSize.{w, w, v, u} C
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
by
  have : Nonempty κ.ord.ToType := by simpa using Cardinal.IsRegular.ne_zero Fact.out
  have := WellFoundedLT.toOrderBot κ.ord.ToType
  have := D₁.hasCoproductsOfShape.{w} W
  have := D₂.hasColimitsOfShape.{w} W
  exact isRightAdjoint_ι W κ hW

Goal state after:
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)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
j : J
hj : D.P j
f : j ⟶ m₁
hf : D.W f
⊢ f = φ ⟨j, hj⟩

pp: case inl.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
X Y : J
i✝ : Unit
hj : D.P m₁
⊢ 𝟙 m₁ = φ ⟨m₁, hj⟩

pp: case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
X Y : J
i✝ : Subtype D.P
hj : D.P ↑i✝
⊢ φ i✝ = φ ⟨↑i✝, hj⟩

Tactic:
· exact (h₁ (D.tgt hf)).elim

Goal state after:
case inl.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
X Y : J
i✝ : Unit
hj : D.P m₁
⊢ 𝟙 m₁ = φ ⟨m₁, hj⟩

case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
X Y : J
i✝ : Subtype D.P
hj : D.P ↑i✝
⊢ φ i✝ = φ ⟨↑i✝, hj⟩
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j✝ : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j✝ ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ ⟨j, hj⟩
j : J
hj : (D₄ D φ).IsTerminal j
⊢ j = m₁

Tactic:
obtain (hj' | ⟨⟨⟩⟩) := hj.prop
        · exact hm₀.elim (u ≫ hj.lift (Or.inr ⟨⟨⟩⟩) ≫ D.isTerminal.lift hj')
        · rfl

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

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
⊢ (functor J κ).Final

Tactic:
by
  have := isCardinalFiltered J κ hJ
  have := isFiltered_of_isCardinalFiltered J κ
  have := isFiltered_of_isCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
  rw [Functor.final_iff_of_isFiltered]
  refine ⟨fun j ↦ ⟨.single j, ⟨𝟙 _⟩⟩, fun {j D} (f₁ f₂ : j ⟶ D.top) ↦ ?_⟩
  obtain ⟨m₀, t, hm₀⟩ := hJ D.top
  obtain ⟨m₁, u, hu⟩ : ∃ (m₁ : J) (u : m₀ ⟶ m₁), f₁ ≫ t ≫ u = f₂ ≫ t ≫ u :=
    ⟨_, IsFiltered.coeqHom (f₁ ≫ t) (f₂ ≫ t),
      by simpa using IsFiltered.coeq_condition (f₁ ≫ t) (f₂ ≫ t)⟩
  have h₁ : ¬ (D.P m₁) := fun h₁ ↦ hm₀.false (u ≫ D.isTerminal.lift h₁)
  let φ (x : Subtype D.P) : x.1 ⟶ m₁ := D.isTerminal.lift x.2 ≫ t ≫ u
  have h₂ {j : J} (hj : D.P j) {f : j ⟶ m₁} (hf : (D₄ D φ).W f) :
      f = φ ⟨_, hj⟩ := by
    obtain ((hf | ⟨⟨⟩⟩) | ⟨⟨⟩⟩) := hf
    · exact (h₁ (D.tgt hf)).elim
    · exact (h₁ hj).elim
    · rfl
  have h₃ {f : m₁ ⟶ m₁} (hf : (D₄ D φ).W f) : f = 𝟙 _ := by
    obtain ((hf | ⟨⟨⟩⟩) | hf) := hf
    · exact (h₁ (D.src hf)).elim
    · rfl
    · rw [MorphismProperty.ofHoms_iff] at hf
      obtain ⟨⟨j, hj⟩, hf⟩ := hf
      obtain rfl : m₁ = j := congr_arg Arrow.leftFunc.obj hf
      exact (h₁ hj).elim
  let hm₁ : (D₄ D φ).IsTerminal m₁ :=
    .ofExistsUnique (Or.inl (Or.inr ⟨⟨⟩⟩)) (by
        rintro j (hj | ⟨⟨⟨⟩⟩⟩)
        · exact ⟨φ ⟨_, hj⟩, Or.inr ⟨_⟩⟩
        · exact ⟨𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩)⟩) (by
        rintro j (hj | ⟨⟨⟨⟩⟩⟩) l₁ l₂ hl₁ hl₂
        · obtain rfl := h₂ hj hl₁
          obtain rfl := h₂ hj hl₂
          rfl
        · rw [h₃ hl₁, h₃ hl₂]) (by
      rintro j k f ((hf | ⟨⟨⟩⟩) | ⟨⟨j, hj⟩⟩)
      · exact ⟨φ ⟨_, D.src hf⟩, φ ⟨_, D.tgt hf⟩,
          Or.inr ⟨_⟩, Or.inr ⟨_⟩, D.isTerminal.comm_assoc _ hf _⟩
      · exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩
      · exact ⟨φ ⟨_, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩)
  have lift_eq (j : J) (hj : D.P j) : hm₁.lift (Or.inl hj) = φ ⟨_, hj⟩ :=
    hm₁.uniq _ (Or.inr ⟨_⟩)
  let D₄' : DiagramWithUniqueTerminal J κ :=
    { toDiagram := D₄ D φ
      top := m₁
      isTerminal := hm₁
      uniq_terminal j hj := by
        obtain (hj' | ⟨⟨⟩⟩) := hj.prop
        · exact hm₀.elim (u ≫ hj.lift (Or.inr ⟨⟨⟩⟩) ≫ D.isTerminal.lift hj')
        · rfl }
  exact ⟨D₄', homOfLE ⟨le_sup_left.trans le_sup_left, le_sup_left⟩,
    by simpa [functorMap, D₄', lift_eq _ D.isTerminal.prop, φ]⟩

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

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π)).arrows f →
      (regularCoverage C).Saturate Y_1
        (Sieve.pullback f (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)))

Tactic:
· intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩
    rw [← hf, Sieve.pullback_comp]
    apply (regularTopology C).pullback_stable'
    apply regularTopology.mem_sieves_of_hasEffectiveEpi
    cases hY
    exact ⟨Y', π', inferInstance, Y', (𝟙 _), π' ≫ π, Presieve.ofArrows.mk (), (by simp)⟩

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

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))

Tactic:
Presieve.isSheaf_iff_preservesFiniteProducts

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : PreservesFiniteProducts (F ⋙ coyoneda.obj (op E))
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))