mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ LaxMonoidal.ofBifunctor.firstMap (curriedTensorPreIsoPost L W F G).hom =
    LaxMonoidal.ofBifunctor.secondMap (curriedTensorPreIsoPost L W F G).hom

Tactic:
refine natTrans₃_ext L L L W W W (fun X₁ X₂ X₃ ↦ ?_)
    dsimp [e]
    rw [curriedTensorPreIsoPost_hom_app_app, curriedTensorPreIsoPost_hom_app_app,
      curriedTensorPreIsoPost_hom_app_app' L W F G (μIso L _ _) (Iso.refl _),
      curriedTensorPreIsoPost_hom_app_app' L W F G (Iso.refl _) (μIso L _ _)]
    monoidal_simps
    /-
    The following `simp only` block was generated by:
    ```
    simp? [← comp_whiskerRight_assoc, -comp_whiskerRight, whisker_exchange_assoc,
      ← MonoidalCategory.whiskerLeft_comp_assoc, -MonoidalCategory.whiskerLeft_comp]
    ```
    -/
    simp only [comp_obj, μIso_hom, Iso.refl_hom, map_id, Category.id_comp, μIso_inv, Iso.refl_inv,
      MonoidalCategory.whiskerLeft_id, Category.comp_id, map_comp, Category.assoc,
      ← comp_whiskerRight_assoc, map_δ_μ_assoc, Iso.inv_hom_id_app, id_whiskerRight,
      whisker_exchange_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, whiskerRight_tensor]
    simp [← whisker_exchange_assoc, tensor_whiskerLeft_symm, -tensor_whiskerLeft,
      ← LaxMonoidal.associativity_assoc G, ← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
I : C
inst✝ : Closed I
A : C
⊢ toUnit A ≫ curryRightUnitorHom I = curry (fst I A)

Tactic:
apply uncurry_injective

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
I : C
inst✝ : Closed I
A : C
⊢ uncurry (toUnit A ≫ curryRightUnitorHom I) = uncurry (curry (fst I A))
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
c₁ c₂ c₃ : C
⊢ { app := fun x ↦ (αᵣ x c₁ c₂).inv, naturality := ⋯ } ▷ (curriedAction C D).obj c₃ ≫
      { app := fun x ↦ (αᵣ x (c₁ ⊗ c₂) c₃).inv, naturality := ⋯ } ≫ (curriedAction C D).map (α_ c₁ c₂ c₃).hom =
    (α_ ((curriedAction C D).obj c₁) ((curriedAction C D).obj c₂) ((curriedAction C D).obj c₃)).hom ≫
      (curriedAction C D).obj c₁ ◁ { app := fun x ↦ (αᵣ x c₂ c₃).inv, naturality := ⋯ } ≫
        { app := fun x ↦ (αᵣ x c₁ (c₂ ⊗ c₃)).inv, naturality := ⋯ }

Tactic:
by
    ext d
    simpa [-actionHom_associator] using
      (IsIso.inv_eq_inv.mpr <| actionHom_associator c₁ c₂ c₃ d).symm =≫
        d ⊴ᵣ (α_ c₁ c₂ c₃).hom

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)))

Tactic:
w₂,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom
        (((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
          (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
            ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom))
Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ ihomUncurry x y z ≫ ihomCurry x y z = 𝟙 ((ihom y).obj ((ihom x).obj z))

Tactic:
apply uncurry_injective

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ uncurry (ihomUncurry x y z ≫ ihomCurry x y z) = uncurry (𝟙 ((ihom y).obj ((ihom x).obj z)))
Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ uncurry (ihomUncurry x y z ≫ ihomCurry x y z) = uncurry (𝟙 ((ihom y).obj ((ihom x).obj z)))

Tactic:
apply uncurry_injective

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ uncurry (uncurry (ihomUncurry x y z ≫ ihomCurry x y z)) = uncurry (uncurry (𝟙 ((ihom y).obj ((ihom x).obj z))))
Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ ihomCurry x y z ≫ ihomUncurry x y z = 𝟙 ((ihom (x ⊗ y)).obj z)

Tactic:
apply uncurry_injective

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ uncurry (ihomCurry x y z ≫ ihomUncurry x y z) = uncurry (𝟙 ((ihom (x ⊗ y)).obj z))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case comm1.refine_2
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
l : i.EssImageSubcategory ⥤ D
φ : l ⋙ i ≅ i.essImage.ι
B X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ (tensorLeft B ⋙ i).map f ≫ (asIso (prodComparison i B Y✝)).hom =
    (asIso (prodComparison i B X✝)).hom ≫ (i ⋙ tensorLeft (i.obj B)).map f

Tactic:
· dsimp [asIso]
            rw [prodComparison_natural_whiskerLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Goal state before:
pp: V : Type u₁
inst✝⁵ : Category.{v₁, u₁} V
inst✝⁴ : MonoidalCategory V
D : Type u₂
D' : Type u₃
E : Type u₄
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} D'
inst✝¹ : Category.{v₄, u₄} E
H : D ⥤ V
L : D ⥤ D'
H' : D' ⥤ V
α : H ⟶ L ⋙ H'
K : E ⥤ V
d : D'
P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d
e : E
inst✝ : Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))
cone : Limits.Cocone (CostructuredArrow.proj ((𝟭 E).prod L) (e, d) ⋙ K ⊠ H) :=
  (Functor.LeftExtension.mk (K ⊠ H') (extensionUnitRight H' α K)).coconeAt (e, d)
equiv : CostructuredArrow (𝟭 E) e × CostructuredArrow L d ≌ CostructuredArrow ((𝟭 E).prod L) (e, d) :=
  (CostructuredArrow.prodEquivalence (𝟭 E) L e d).symm
I : CostructuredArrow L d ⥤ CostructuredArrow (𝟭 E) e × CostructuredArrow L d :=
  (prod.leftUnitorEquivalence (CostructuredArrow L d)).inverse ⋙
    (Functor.fromPUnit (CostructuredArrow.mk (𝟙 ((𝟭 E).obj e)))).prod (𝟭 (CostructuredArrow L d))
⊢ I.Final

Tactic:
let : Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.Final :=
      Functor.final_fromPUnit_of_isTerminal <| CostructuredArrow.mkIdTerminal (S := 𝟭 E) (Y := e)
    apply Iff.mp <| Functor.final_iff_final_comp
      (F := (prod.leftUnitorEquivalence <| CostructuredArrow L d).inverse)
      (G := Functor.fromPUnit.{0} (.mk (𝟙 e) : CostructuredArrow (𝟭 E) e) |>.prod <| 𝟭 _)
    infer_instance

Goal state after:
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:
ε[A].naturality,

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✝ ≫ (𝟙_ (C ⥤ D)).map f = ε.app X✝
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)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j j' : J
u : j ⟶ j'
⊢ P.diag.map u ≫ (Q j').isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j', i⟩, naturality := ⋯ } } =
    (Q j).isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j, i⟩, naturality := ⋯ } } ≫
      ((Functor.const J).obj c.pt).map u

Tactic:
refine (Q j).isColimit.hom_ext fun i ↦ ?_

Goal state after:
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)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j j' : J
u : j ⟶ j'
i : I j
⊢ { pt := P.diag.obj j, ι := (Q j).ι }.ι.app i ≫
      P.diag.map u ≫ (Q j').isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j', i⟩, naturality := ⋯ } } =
    { pt := P.diag.obj j, ι := (Q j).ι }.ι.app i ≫
      (Q j).isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j, i⟩, naturality := ⋯ } } ≫
        ((Functor.const J).obj c.pt).map u
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)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
m : { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.pt ⟶ c.pt
hm :
  ∀ (j : Total Q),
    { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.ι.app j ≫ m = c.ι.app j
j : J
⊢ P.ι.app j ≫ m = (Q j).isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j, i⟩, naturality := ⋯ } }

Tactic:
refine (Q j).isColimit.hom_ext fun i ↦ ?_

Goal state after:
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)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
m : { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.pt ⟶ c.pt
hm :
  ∀ (j : Total Q),
    { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.ι.app j ≫ m = c.ι.app j
j : J
i : I j
⊢ { pt := P.diag.obj j, ι := (Q j).ι }.ι.app i ≫ P.ι.app j ≫ m =
    { pt := P.diag.obj j, ι := (Q j).ι }.ι.app i ≫
      (Q j).isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j, i⟩, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsNoetherianObject Y
f : ℕ →o Subobject X
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
obtain ⟨n, hn⟩ := monotone_chain_condition_of_isNoetherianObject
    ⟨_, (Subobject.map i).monotone.comp f.2⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsNoetherianObject Y
f : ℕ →o Subobject X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      { toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ } n =
        { toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ } m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
⊢ ∃ c, c • 𝟙 X = f

Tactic:
have : Nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this : Nontrivial (End X)
⊢ ∃ c, c • 𝟙 X = f
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
j : J
x y : ↑(F.1 j)
⊢ { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x ≤
      { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y ↔
    x ≤ y

Tactic:
refine ⟨?_, fun h ↦ ⟨j, x, y, rfl, rfl, h⟩⟩
        rintro ⟨k, x', y', hx, hy, h⟩
        obtain ⟨l₁, a₁, b₁, hl₁⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hx
        obtain ⟨l₂, a₂, b₂, hl₂⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hy
        dsimp at hx hy hl₁ hl₂
        obtain ⟨m, d, d', h₁, h₂⟩ := bowtie a₁ a₂ b₁ b₂
        rw [← (F.map (a₁ ≫ d)).le_iff_le] at h
        rw [← (F.map (b₁ ≫ d)).le_iff_le]
        conv_rhs => rw [h₂]
        conv_rhs at h => rw [h₁]
        simpa [← hl₁, ← hl₂] using h

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

Goal state before:
pp: case refine_2
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h✝ : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
j : A
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op J)).obj j)
h :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app j)) f =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op J)).map f_1)) f =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op J)).map f_1)) g

Tactic:
choose k a hk using fun (x : J.obj) ↦
        (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (ConcreteCategory.congr_hom h x)
      dsimp at f g h k a hk ⊢
      obtain ⟨l, b, c, hl⟩ : ∃ (l : A) (c : j ⟶ l) (b : ∀ x, k x ⟶ l),
          ∀ x, a x ≫ b x = c := by
        let φ (x : J.obj) : j ⟶ IsCardinalFiltered.max k hJ :=
          a x ≫ IsCardinalFiltered.toMax k hJ x
        exact ⟨IsCardinalFiltered.coeq φ hJ,
          IsCardinalFiltered.toCoeq φ hJ,
          fun x ↦ IsCardinalFiltered.toMax k hJ x ≫ IsCardinalFiltered.coeqHom φ hJ,
          fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hJ x⟩
      refine ⟨l, b, ?_⟩
      ext x
      simpa only [← hl x, Functor.map_comp, ObjectProperty.FullSubcategory.comp_hom,
        PartOrdEmb.hom_comp, RelEmbedding.coe_trans, Function.comp_apply]
          using! congr_arg _ (hk x)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤

Tactic:
by
  let e := equivSmallModel.{w} P.FullSubcategory
  let ι := Σ (J : Type w) (_ : SmallCategory J),
    { F : J ⥤ _ // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
  let φ : ι → C := fun ⟨j, _, F, hF⟩ ↦ colimit (F ⋙ e.inverse ⋙ P.ι)
  refine ⟨ObjectProperty.ofObj φ, inferInstance, fun X _ ↦ ?_⟩
  obtain ⟨J, _, _, ⟨p⟩⟩ := hP.exists_colimitsOfShape X
  let G : J ⥤ P.FullSubcategory := P.lift p.diag p.prop_diag_obj
  let iso : (G ⋙ e.functor) ⋙ e.inverse ⋙ P.ι ≅ p.diag :=
    Functor.associator _ _ _ ≪≫
    G.isoWhiskerLeft ((Functor.associator _ _ _).symm ≪≫
    Functor.isoWhiskerRight e.unitIso.symm P.ι) ≪≫
    (Functor.associator _ _ _).symm ≪≫
    Functor.isoWhiskerRight (Functor.rightUnitor _) _
  have : HasColimit p.diag := ⟨_, p.isColimit⟩
  have := hasColimit_of_iso iso
  let i : ι := ⟨J, inferInstance, G ⋙ e.functor, inferInstance⟩
  exact ⟨_, ⟨i⟩, ⟨((IsColimit.precomposeHomEquiv iso _).2
    (p.isColimit)).coconePointUniqueUpToIso (colimit.isColimit _)⟩⟩

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

Goal state before:
pp: case refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
x✝ : IsIso (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
hZ : toSucc W Z ≫ inv (toSucc W Z) = 𝟙 Z
⊢ ∃ a, (fun g ↦ f ≫ g) a = g

Tactic:
simp only [Category.assoc] at hZ

Goal state after:
case refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
x✝ : IsIso (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
hZ : toStep W Z ≫ fromStep W Z ≫ inv (toSucc W Z) = 𝟙 Z
⊢ ∃ a, (fun g ↦ f ≫ g) a = g
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
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
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
this : (∃ a, (D a).P j) ∨ m = j
⊢ j = m

Tactic:
obtain (⟨i, hi⟩ | rfl) := this

Goal state after:
case 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
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
j : J
hj : (D₂ D hι u).IsTerminal j
i : ι
hi : (D i).P j
⊢ j = 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
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
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
hj : (D₂ D hι u).IsTerminal m
⊢ m = m