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

Goal state before:
pp: 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
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ f.inverse ⋙ f.functor = 𝟭 E

Tactic:
exact f.counit_eq

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ ({ pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
              inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.fst ≫
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
              inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.inl +
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
              inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.snd ≫
          { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
              inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
              inr_snd := ⋯ }.inr).f =
    (𝟙
        { pt := { X := P.X, p := 𝟙 P.X, idem := ⋯ }, fst := P.decompId_p, snd := P.complement.decompId_p,
            inl := P.decompId_i, inr := P.complement.decompId_i, inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯,
            inr_snd := ⋯ }.pt).f

Tactic:
simp only [complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, add_def, idem,
        comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel, id_f]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
i j : X ⟶ Z
⊢ Zigzag (mk i) (mk j)

Tactic:
obtain ⟨a, rfl, rfl⟩ := h₂ i j
    let f₁ : (mk (Y := zero) (f ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a :=
      homMk left
    let f₂ : (mk (Y := zero) (g ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a :=
      homMk right
    exact Zigzag.of_hom_inv f₁ f₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : r • (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Tactic:
rw [← map_smul (colimit.ι F j).hom] at hx

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.edge
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
d✝ : D
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      ((inclLeft C D).map f✝ ≫ edge y✝ d✝) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclLeft C D).map f✝) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (edge y✝ d✝)

Tactic:
case left.edge f d => simpa using! (α.naturality <| (Prod.sectL _ d).map f).symm

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F F' : C ⋆ D ⥤ E
α : F ⟶ F'
⊢ mkNatTrans ((inclLeft C D).whiskerLeft α) ((inclRight C D).whiskerLeft α) ⋯ = α

Tactic:
apply natTrans_ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f ≫ ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i ↦ Y ↑i) (∏ᶜ fun i ↦ Y ↑i))).hom =
    ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i))).hom ≫
      prod.map (map fun i ↦ f ↑i) (map fun i ↦ f ↑i)

Tactic:
dsimp only [IsLimit.conePointUniqueUpToIso, binaryFanOfProp, prodIsProd]

Goal state after:
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f ≫
      ((Cone.forget (pair (∏ᶜ fun i ↦ Y ↑i) (∏ᶜ fun i ↦ Y ↑i))).mapIso
          ((binaryFanOfPropIsLimit Y P).uniqueUpToIso
            ((limit.isLimit (pair (∏ᶜ fun i ↦ Y ↑i) (∏ᶜ fun i ↦ Y ↑i))).ofIsoLimit
              (Cone.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i ↦ Y ↑i) (∏ᶜ fun i ↦ Y ↑i))).pt) ⋯)))).hom =
    ((Cone.forget (pair (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i))).mapIso
          ((binaryFanOfPropIsLimit X P).uniqueUpToIso
            ((limit.isLimit (pair (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i))).ofIsoLimit
              (Cone.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i))).pt) ⋯)))).hom ≫
      prod.map (map fun i ↦ f ↑i) (map fun i ↦ f ↑i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
⊢ h.p₂ ≫ f₂ = h.p

Tactic:
← h.condition,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
⊢ h.p₁ ≫ f₁ = h.p
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_ F
i : J
⊢ ∀ ⦃j : J⦄ (f_1 : i ⟶ j),
    (Hom.hom ((G.obj (op i)).map f_1)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) i) =
      (Hom.hom ((G.map f_1.op).app j)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) j)

Tactic:
j

Goal state after:
J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F G : Jᵒᵖ ⥤ J ⥤ Type (max w u)
f : F ⟶ G
x : Types.end_ F
i j : J
⊢ ∀ (f_1 : i ⟶ j),
    (Hom.hom ((G.obj (op i)).map f_1)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) i) =
      (Hom.hom ((G.map f_1.op).app j)) ((fun j ↦ (hom ((f.app (op j)).app j)) (↑x j)) j)
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_1.isMin
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : IsMin j
⊢ hf.incl.app j ≫ g₁ = hf.incl.app j ≫ g₂

Tactic:
| isMin j hj =>

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
I : C
inst✝ : ChosenPullbacksAlong (𝟙 I)
⊢ pushforward (𝟙 I) = 𝟭 (Over I)

Tactic:
dsimp +instances only [id]

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
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
⊢ ∀ (f : (toOver I).obj A ⟶ X') (g : X' ⟶ X),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g

Tactic:
u

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
⊢ ∀ (g : X' ⟶ X),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (u ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } u ≫ (sections I).map g
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: case refine_1
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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
⊢ R ⋙ tensorLeft (R.obj c) ⋙ L ≅ tensorLeft c ⋙ 𝟭 C

pp: case refine_2
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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
⊢ 𝟭 C ⋙ R ⋙ ihom (R.obj c) ≅ (R ⋙ ihom (R.obj c) ⋙ L) ⋙ R

Tactic:
· refine NatIso.ofComponents (fun _ ↦ (μIso L _ _).symm ≪≫
        asIso ((adj.counit.app _) ⊗ₘ (adj.counit.app _))) (fun _ ↦ ?_)
      dsimp
      rw [Category.assoc, ← δ_natural_right_assoc,
        tensorHom_def', ← MonoidalCategory.whiskerLeft_comp_assoc,
        Adjunction.counit_naturality, whisker_exchange,
        tensorHom_def_assoc, MonoidalCategory.whiskerLeft_comp]

Goal state after:
case refine_2
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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c : C
⊢ 𝟭 C ⋙ R ⋙ ihom (R.obj c) ≅ (R ⋙ ihom (R.obj c) ⋙ L) ⋙ R
Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (ρ_ ((ihom X).obj Y₁)).inv ≫ (ihom X).obj Y₁ ◁ curry' g ≫ comp X Y₁ Y₂ = (ihom X).map g

Tactic:
rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]

Goal state after:
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
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
x y : C
⊢ (unit G F).app (x, y) ≫ (braiding F G).inv.app (x ⊗ y) =
    (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)).inv ≫
      (unit F G).app (y, x) ≫ (F ⊛ G).map (β_ (y, x).2 (y, x).1).inv

Tactic:
by
  change
    (unit G F).app (x, y) ≫ (braiding F G).inv.app ((tensor C).obj (x, y)) = _
  simp [braiding, braidingHomCorepresenting, -tensor_obj]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (((((α_ (A ⊗ A) A A).hom ≫ μ ▷ (A ⊗ A)) ≫ A ◁ (β_ A A).hom) ≫ A ◁ (𝒮 ⊗ₘ 𝒮)) ≫ A ◁ μ) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 8 9 =>
    rw [← whisker_exchange]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫ ((((A ⊗ A) ◁ (β_ A A).hom ≫ μ ▷ (A ⊗ A)) ≫ A ◁ (𝒮 ⊗ₘ 𝒮)) ≫ A ◁ μ) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
N : C
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ MonObj.mul ≫ f.mop = (f.mop ⊗ₘ f.mop) ≫ MonObj.mul

Tactic:
apply mopEquiv C |>.fullyFaithfulInverse.map_injective
    simpa [-IsMonHom.mul_hom] using! IsMonHom.mul_hom f

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

Goal state before:
pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y✝ : C
f : X ⟶ Y✝
inst✝ : IsFinitelyAccessibleCategory (Under X)
Y : Under X
⊢ P.underObj Y ≤ ObjectProperty.isFinitelyPresentable (Under X) Y

Tactic:
hY

Goal state after:
case H
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y✝ : C
f : X ⟶ Y✝
inst✝ : IsFinitelyAccessibleCategory (Under X)
Y : Under X
hY : P.underObj Y
⊢ ObjectProperty.isFinitelyPresentable (Under X) Y
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.ind f
hg : P.ind g
T : C
p : X ⟶ T
⊢ ∀ (g_1 : T ⟶ Z), isFinitelyPresentable C p → p ≫ g_1 = f ≫ g → ∃ W u v, u ≫ v = g_1 ∧ P (p ≫ u)

Tactic:
u

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.ind f
hg : P.ind g
T : C
p : X ⟶ T
u : T ⟶ Z
⊢ isFinitelyPresentable C p → p ≫ u = f ≫ g → ∃ W u_1 v, u_1 ≫ v = u ∧ P (p ≫ u_1)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
Z : C
hZ : P Z
⊢ Function.Injective fun g ↦ f ≫ g

Tactic:
u

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
Z : C
hZ : P Z
u : Y ⟶ Z
⊢ ∀ ⦃a₂ : Y ⟶ Z⦄, (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) a₂ → u = a₂
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z T : C
hT : P T
e : Z ≅ T
⊢ Function.Injective fun g ↦ f ≫ g

Tactic:
u

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z T : C
hT : P T
e : Z ≅ T
u : Y ⟶ Z
⊢ ∀ ⦃a₂ : Y ⟶ Z⦄, (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) a₂ → u = a₂
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F
F : ℕ →o (Subobject X)ᵒᵈ
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m

Tactic:
· obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ (orderDualEquivalence _).functor ⋙
      Subobject.representative.op)
    refine ⟨n, fun m hm ↦ Eq.symm ?_⟩
    simpa [isIso_op_iff, isIso_iff_of_reflects_iso, PartialOrder.isIso_iff_eq]
      using hn (homOfLE hm)

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

Goal state before:
pp: case h
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)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : End.of f = c • 1
⊢ c • 𝟙 X = f

Tactic:
exact nu.symm

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝² : Category.{v, u} C
inst✝¹ : Category.{v', u'} D
e : C ≌ D
inst✝ : IsLocallyPresentable.{w, v, u} C
⊢ IsLocallyPresentable.{w, v', u'} D

Tactic:
by
  obtain ⟨κ, _, _⟩ := IsLocallyPresentable.exists_cardinal.{w} C
  exact ⟨κ, inferInstance, e.isCardinalLocallyPresentable κ⟩

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this✝ : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this✝ a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
f : ↑J.obj ↪ X
e : ↑J.obj ≃ ↑(Set.range ⇑f) := Equiv.ofInjective ⇑f ⋯
this : PartialOrder ↑(Set.range ⇑f) := PartialOrder.lift ⇑e.symm ⋯
e' : ↑(Set.range ⇑f) ≃o ↑J.obj :=
  let __Equiv := e.symm;
  { toEquiv := __Equiv, map_rel_iff' := ⋯ }
⊢ (ObjectProperty.ofObj ι).isoClosure J

Tactic:
exact ⟨_, ⟨⟨Set.range f, inferInstance,
      ⟨⟨IsCardinalFiltered.of_equivalence κ e'.symm.equivalence⟩⟩⟩⟩,
        ⟨CardinalDirectedPoset.ι.preimageIso (PartOrdEmb.Iso.mk (by exact e'.symm))⟩⟩

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
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:
by simpa only [h₃, h₅] using (F.map a).hom.monotone h₁

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ L.map f ≫
      (additiveObjIsoBiproduct L Y✝ ≪≫
          (biproduct.mapIso fun i ↦ α.app (Y✝.X i)) ≪≫
            (biproduct.mapIso fun i ↦ (embeddingLiftIso F).symm.app (Y✝.X i)) ≪≫
              (additiveObjIsoBiproduct (lift F) Y✝).symm).hom =
    (additiveObjIsoBiproduct L X✝ ≪≫
          (biproduct.mapIso fun i ↦ α.app (X✝.X i)) ≪≫
            (biproduct.mapIso fun i ↦ (embeddingLiftIso F).symm.app (X✝.X i)) ≪≫
              (additiveObjIsoBiproduct (lift F) X✝).symm).hom ≫
      (lift F).map f

Tactic:
dsimp only [Iso.trans_hom, Iso.symm_hom, biproduct.mapIso_hom]

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ L.map f ≫
      (additiveObjIsoBiproduct L Y✝).hom ≫
        (biproduct.map fun b ↦ (α.app (Y✝.X b)).hom) ≫
          (biproduct.map fun b ↦ ((embeddingLiftIso F).symm.app (Y✝.X b)).hom) ≫
            (additiveObjIsoBiproduct (lift F) Y✝).inv =
    ((additiveObjIsoBiproduct L X✝).hom ≫
        (biproduct.map fun b ↦ (α.app (X✝.X b)).hom) ≫
          (biproduct.map fun b ↦ ((embeddingLiftIso F).symm.app (X✝.X b)).hom) ≫
            (additiveObjIsoBiproduct (lift F) X✝).inv) ≫
      (lift F).map f
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 κ
e : P.FullSubcategory ≌ SmallModel.{w, v, u} P.FullSubcategory := equivSmallModel P.FullSubcategory
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤

Tactic:
let ι := Σ (J : Type w) (_ : SmallCategory J),
    { F : J ⥤ _ // HasColimit (F ⋙ e.inverse ⋙ P.ι) }

Goal state after:
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 κ
e : P.FullSubcategory ≌ SmallModel.{w, v, u} P.FullSubcategory := equivSmallModel P.FullSubcategory
ι : Type (w + 1) := (J : Type w) × (x : SmallCategory J) × { F // HasColimit (F ⋙ e.inverse ⋙ P.ι) }
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: 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 Y : C
f : X ⟶ Y
hf : W f
g₁ g₂ : Y ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
⊢ f ≫ g₁ ≫ toStep W Z = f ≫ g₂ ≫ toStep W Z

Tactic:
simp [reassoc_of% hg]

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

Goal state before:
pp: 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 Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
⊢ f ≫ D₁.ιRight f hf g ≫ pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ fromStep W Z = g ≫ toSucc W Z

Tactic:
simp [← D₁.ιLeft_comp_t_assoc, pushout.condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case isMin
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : IsMin j
⊢ HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂

Tactic:
| isMin j hj =>

Goal state after: