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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ M.X N₁.X Z.X).hom ≫
      M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫
        colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
          WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ▷ Z.X ≫
      colimMap
            (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
              ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
          Z.X ≫
        TensorBimod.actRight M N₂

Tactic:
slice_rhs 1 2 =>
      rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one, comp_whiskerRight]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ M.X N₁.X Z.X).hom ≫
      M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫
        colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
          WalkingParallelPair.one =
    ((M.X ◁ f.hom) ▷ Z.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one ▷
          Z.X) ≫
      TensorBimod.actRight M N₂
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case comm1.refine_1
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 : D
⊢ (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X

Tactic:
haveI :=
              Adjunction.rightAdjoint_preservesLimits.{0, 0} (reflectorAdjunction i)

Goal state after:
case comm1.refine_1
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 : D
this : Limits.PreservesLimitsOfSize.{0, 0, v₁, v₁, u₂, u₁} i
⊢ (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X
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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ (bijection i A B X') (f ≫ g) = (bijection i A B X) f ≫ g

Tactic:
dsimp [bijection]

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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.fullyFaithfulOfReflective.preimage
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
        ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X')).symm
            ((unitCompPartialBijective B ⋯)
              (((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X'))
                ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                  ((ihom.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X')).symm
                      ((unitCompPartialBijective A ⋯)
                        (((ihom.adjunction B).homEquiv A (i.obj X'))
                          ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X)).symm
              ((unitCompPartialBijective B ⋯)
                (((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X))
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    ((ihom.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X)).symm
                        ((unitCompPartialBijective A ⋯)
                          (((ihom.adjunction B).homEquiv A (i.obj X))
                            ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
      intro X Y f
      dsimp
      rw [leftUnitor_inv_naturality_assoc, Category.assoc, Iso.cancel_iso_inv_left]
      exact
        congr_arg (fun f => NatTrans.app f (Discrete.mk NormalMonoidalObject.unit))
          ((normalizeIso.{u} C).hom.naturality f)

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₁ y₂ : D
f : y₁ ⟶ y₂
x y : C
⊢ ((ι C V D).obj x✝).obj x ◁ ((ι C V D).map f).app y ≫ (convolutionExtensionUnit C V x✝ y₂).app (x, y) =
    (convolutionExtensionUnit C V x✝ y₁).app (x, y) ≫ ((ι C V D).map (x✝ ◁ f)).app (x ⊗ y)

Tactic:
rw [convolutionExtensionUnit_comp_ι_map_whiskerLeft_app]

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

Goal state before:
pp: case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
F : (i : E.I₀) → K.ZeroHypercover (E.X i)
hF : ∀ (i : E.I₀), S i = Presieve.ofArrows (F i).X (F i).f
U : C
g : U ⟶ X✝
x✝ : (E.bind F).presieve₀ g
j : (E.bind F).I₀
⊢ P (((F j.fst).f j.snd ≫ E.f j.fst) ≫ f)

Tactic:
rw [Category.assoc]

Goal state after:
case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
F : (i : E.I₀) → K.ZeroHypercover (E.X i)
hF : ∀ (i : E.I₀), S i = Presieve.ofArrows (F i).X (F i).f
U : C
g : U ⟶ X✝
x✝ : (E.bind F).presieve₀ g
j : (E.bind F).I₀
⊢ P ((F j.fst).f j.snd ≫ E.f j.fst ≫ f)
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isNoetherianObject 0

Tactic:
← isNoetherianObject.is_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isNoetherianObject.Is 0
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
hY : isNoetherianObject Y✝
⊢ isNoetherianObject X✝

Tactic:
← isNoetherianObject.is_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
hY : isNoetherianObject.Is Y✝
⊢ isNoetherianObject.Is X✝
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, max v_1 v_2, max (max u_1 u_2) v_3} (comma F₁ F₂ P₁ P₂)

Tactic:
refine ⟨comma F₁ F₂ Q₁ Q₂, inferInstance, fun f hf ↦ ?_⟩

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : comma F₁ F₂ P₁ P₂ f
⊢ (comma F₁ F₂ Q₁ Q₂).isoClosure f
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
⊢ F.a ≫ U.map 0 = 0 ≫ G.a

Tactic:
by simp only [Functor.map_zero, comp_zero, zero_comp]

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

Goal state before:
pp: case h₁
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
f : X ⟶ Y
⊢ biprod.lift f 0 ≫ biprod.snd = (f ≫ biprod.inl) ≫ biprod.snd

Tactic:
simp [biprod.lift_snd, Category.assoc, comp_zero]

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 Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f + g) ≫ h = f ≫ h + g ≫ h

Tactic:
simp only [add_eq_right_addition, Category.assoc]
  congr
  ext <;> simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ x_1 ∈ Finset.univ.sigma fun x ↦ Finset.univ,
      if h : x_1.fst = j then
        if h_1 : ⋯ ▸ x_1.snd = x then if h_2 : x_1.fst = j' then if h_3 : ⋯ ▸ x_1.snd = y then eqToHom ⋯ else 0 else 0
        else 0
      else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
Finset.sum_sigma

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ a,
      ∑ s,
        if h : ⟨a, s⟩.fst = j then
          if h_1 : ⋯ ▸ ⟨a, s⟩.snd = x then
            if h_2 : ⟨a, s⟩.fst = j' then if h_3 : ⋯ ▸ ⟨a, s⟩.snd = y then eqToHom ⋯ else 0 else 0
          else 0
        else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y
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.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
hy' : ∀ (x : X), (ConcreteCategory.hom (p.ι.app j')) (y' x) = SetCardinalLT.singleton κ₁ x
x✝ : SetCardinalLT κ₁ X
B : Set X
hB : HasCardinalLT (↑B) κ₁
⊢ ∃ y ∈ Set.range ⇑(ConcreteCategory.hom (p.ι.app j')), ⟨B, hB⟩ ≤ y

Tactic:
let j'' := IsCardinalFiltered.max (fun b ↦ y' b.val) hB

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
hy' : ∀ (x : X), (ConcreteCategory.hom (p.ι.app j')) (y' x) = SetCardinalLT.singleton κ₁ x
x✝ : SetCardinalLT κ₁ X
B : Set X
hB : HasCardinalLT (↑B) κ₁
j'' : ↑(p.diag.obj j').obj := IsCardinalFiltered.max (fun b ↦ y' ↑b) hB
⊢ ∃ y ∈ Set.range ⇑(ConcreteCategory.hom (p.ι.app j')), ⟨B, hB⟩ ≤ y
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
rw [Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top]
  ext Z
  simpa using! (corepresentableBy Z hW).isCorepresentable

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 ι κ
⊢ ∃ j, ∀ (k : ι), D k ≤ j

Tactic:
obtain ⟨m, u, hm₀, hm⟩ := isCardinalFiltered_aux J κ hJ D hι

Goal state after:
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₂
⊢ ∃ j, ∀ (k : ι), D k ≤ j
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Regular C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst✝¹ : HasPullback f g
inst✝ : IsRegularEpi f
⊢ IsRegularEpi (pullback.snd f g)

Tactic:
apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback (IsPullback.of_hasPullback f g)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Regular C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst✝¹ : HasPullback f g
inst✝ : IsRegularEpi f
⊢ MorphismProperty.regularEpi C f
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Regular C
X Y B : C
f : X ⟶ B
g : Y ⟶ B
inst✝¹ : HasPullback f g
inst✝ : IsRegularEpi f
⊢ IsRegularEpi (pullback.snd f g)

Tactic:
by
  apply Regular.regularEpiIsStableUnderBaseChange.of_isPullback (IsPullback.of_hasPullback f g)
  dsimp [MorphismProperty.regularEpi]
  infer_instance

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)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → ↑x ⟶ m₁
⊢ ∀ {i j : J} {f : i ⟶ j}, ((D₃ D m₁).W ⊔ MorphismProperty.ofHoms φ) f → (D₃ D m₁).P i

Tactic:
by
    rintro i j f (hf | ⟨⟨j, hj⟩⟩)
    · exact (D₃ D m₁).src hf
    · exact Or.inl hj

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

Goal state before:
pp: case 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
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₁
j : J
hj : D.P j
⊢ ∃ lift, (D₄ D φ).W lift

Tactic:
exact ⟨φ ⟨_, hj⟩, Or.inr ⟨_⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst✝ : Unique ι
X S : C
f : X ⟶ S
⊢ (F.toDescentDataAsCoalgebra fun x ↦ f).IsEquivalence ↔
    (Comonad.comparison (Adjunction.ofCat (F.map f.op.toLoc).adj)).IsEquivalence

Tactic:
by
  rw [← Functor.isEquivalence_iff_of_iso
    (F.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f)]
  exact ⟨fun _ ↦ inferInstance, fun _ ↦
    Functor.isEquivalence_of_comp_right _
      ((DescentDataAsCoalgebra.coalgebraEquivalence F ι f).functor)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case right.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map b.op

Tactic:
obtain rfl : a = b := by simpa only [← cancel_mono sq.f₃₄] using fac

Goal state after:
case right.right
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op