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

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

Tactic:
by
      dsimp
      simp only [id_tensorHom, limit.lift_map, Category.assoc, limit.lift_π]
      dsimp
      simp only [tensorHom_def, ← whisker_exchange, whiskerRight_id, Category.assoc, Iso.inv_hom_id,
        Category.comp_id, ← whiskerLeft_comp_assoc]
      erw [limit.lift_π]
      rw [whiskerLeft_id, Category.id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X ≫
      ((PreservesCoequalizer.iso (tensorRight S.X) (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
          colimMap
            (parallelPairHom (μ ▷ P.X ▷ S.X) (((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X) (μ ▷ P.X)
              ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
              ((α_ (R.X ⊗ R.X) P.X S.X).hom ≫
                (α_ R.X R.X (P.X ⊗ S.X)).hom ≫ R.X ◁ R.X ◁ P.actRight ≫ (α_ R.X R.X P.X).inv)
              ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ⋯ ⋯)) ≫
        coequalizer.desc P.actLeft ⋯ =
    coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X ≫
      coequalizer.desc P.actLeft ⋯ ▷ S.X ≫ P.actRight

Tactic:
slice_lhs 1 4 => rw [π_tensor_id_preserves_coequalizer_inv_colimMap_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ≫ P.actLeft =
    coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X ≫
      coequalizer.desc P.actLeft ⋯ ▷ S.X ≫ P.actRight
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X ≫
      ((PreservesCoequalizer.iso (tensorRight S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)).inv ≫
          colimMap
            (parallelPairHom (P.actRight ▷ S.X ▷ S.X) (((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X) (P.actRight ▷ S.X)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
              ((α_ (P.X ⊗ S.X) S.X S.X).hom ≫ (α_ P.X S.X (S.X ⊗ S.X)).hom ≫ P.X ◁ S.X ◁ μ ≫ (α_ P.X S.X S.X).inv)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ⋯ ⋯)) ≫
        coequalizer.desc P.actRight ⋯ =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X ≫
      coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight

Tactic:
slice_lhs 1 4 => rw [π_tensor_id_preserves_coequalizer_inv_colimMap_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫ P.actRight =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X ≫
      coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 Y ⊗≫
      η_ X Y ▷ Y ⊗≫
        (𝟙 ((X ⊗ Y) ⊗ Y) ⊗≫
            X ◁ (β_ Y Y).hom ⊗≫ (β_ X Y).hom ▷ Y ⊗≫ Y ◁ (β_ Y X).inv ⊗≫ (β_ Y Y).inv ▷ X ⊗≫ 𝟙 (Y ⊗ Y ⊗ X)) ⊗≫
          Y ◁ ε_ X Y ⊗≫ 𝟙 Y =
    𝟙 Y ⊗≫ (η_ X Y ▷ Y ≫ (β_ (X ⊗ Y) Y).hom) ⊗≫ ((β_ Y (Y ⊗ X)).inv ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y

Tactic:
simp [monoidalComp, braiding_tensor_left_hom, braiding_tensor_right_inv]

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

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
x y₁ : D
y₂ : x ⟶ y₁
f : D
⊢ y₂ ⊗ₘ 𝟙 f = y₂ ▷ f

Tactic:
apply Functor.Faithful.map_injective (F := ι C V D)
      simp only [ι_map_tensorHom_hom_eq_tensorHom]
      apply (corepresentableBy (ι C V D |>.obj _) (ι C V D |>.obj _)).homEquiv.injective
      dsimp
      ext ⟨x, y⟩
      dsimp
      simp only [Functor.map_id, DayConvolution.unit_app_map_app, Functor.comp_obj,
        tensor_obj, NatTrans.id_app, tensorHom_id]
      dsimp [DayConvolution.unit]
      rw [convolutionExtensionUnit_comp_ι_map_whiskerRight_app]

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✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore 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) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
d₁✝ d₁'✝ : D
f₁✝ : d₁✝ ⟶ d₁'✝
d₂✝ : D
x✝ y✝ : C
⊢ (DayConvolution.unit ((ι C V D).obj d₁✝) ((ι C V D).obj d₂✝)).app (x✝, y✝) ≫
      ((ι C V D).map (f₁✝ ▷ d₂✝)).app (x✝ ⊗ y✝) =
    ((ι C V D).map f₁✝).app x✝ ▷ ((ι C V D).obj d₂✝).obj y✝ ≫
      (DayConvolution.unit ((ι C V D).obj d₁'✝) ((ι C V D).obj d₂✝)).app (x✝, y✝)

Tactic:
simp [← tensorHom_id, ι_map_tensorHom_eq C V D]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y : C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsArtinianObject X
h : ¬IsZero X
⊢ Mono (simpleSubobjectArrow h)

Tactic:
dsimp only [simpleSubobjectArrow]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsNoetherianObject X ↔ ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F

Tactic:
by
  rw [isNoetherianObject_iff_monotone_chain_condition]
  refine ⟨fun h G ↦ ?_, fun h F ↦ ?_⟩
  · obtain ⟨n, hn⟩ := h (G ⋙ (Subobject.equivMonoOver _).inverse).toOrderHom
    refine ⟨n, fun m hm ↦ ?_⟩
    rw [MonoOver.isIso_iff_subobjectMk_eq]
    exact hn m (leOfHom hm)
  · obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ Subobject.representative)
    refine ⟨n, fun m hm ↦ ?_⟩
    simpa [← MonoOver.isIso_iff_isIso_hom_left, isIso_iff_of_reflects_iso,
      PartialOrder.isIso_iff_eq] using hn (homOfLE hm)

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

Goal state before:
pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0

Tactic:
convert! comp_zero

Goal state after:
case e'_2.e'_7
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
⊢ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case w'
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a ↦ s (f a)) a ≫
        z ≫ biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c =
    0

Tactic:
convert! comp_zero

Goal state after:
case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ biproduct.ι (fun a ↦ s (f a)) a ≫
      z ≫ biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c =
    0
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ biproduct.ι (fun a ↦ s (f a)) a ≫
      z ≫ biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c =
    0

Tactic:
convert! comp_zero

Goal state after:
case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ z ≫ biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c = 0
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ z ≫ biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c = 0

Tactic:
convert! comp_zero

Goal state after:
case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c = 0
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ biproduct.π (fun b ↦ s (g b)) b ≫ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c = 0

Tactic:
convert! comp_zero

Goal state after:
case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ biproduct.ι (fun b ↦ s (g b)) b ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c = 0
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 = (algebraMap 𝕜 (End X)) c
⊢ c • 𝟙 X = f

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
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
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₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
l₂ : J
a' : j ⟶ l₂
b' : k ⟶ l₂
h₄ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a')) y₁ =
    (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b')) y₂
l : J
d : l₁ ⟶ l
d' : l₂ ⟶ l
h₅ : a ≫ d = a' ≫ d'
h₆ : b ≫ d = b' ≫ d'
⊢ ∃ l a b x₃ y₃,
    x₃ = (ConcreteCategory.hom (F.map a)) x₁ ∧
      x₃ = (ConcreteCategory.hom (F.map b)) x₂ ∧
        y₃ = (ConcreteCategory.hom (F.map a)) y₁ ∧ y₃ = (ConcreteCategory.hom (F.map b)) y₂

Tactic:
exact ⟨l, a ≫ d, b ≫ d, F.map (a ≫ d) x₁, F.map (a' ≫ d') y₁, rfl,
        by simpa, by rw [h₅], by simpa [h₆]⟩

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
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') =
    (ConcreteCategory.hom (s.ι.app j)) x'
hy :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) y') =
    (ConcreteCategory.hom (s.ι.app j)) y'
x✝ : (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'
k : J
x y : ↑(F.obj k)
hx' : (ConcreteCategory.hom (c.ι.app k)) x = (ConcreteCategory.hom (c.ι.app j)) x'
hy' : (ConcreteCategory.hom (c.ι.app k)) y = (ConcreteCategory.hom (c.ι.app j)) y'
h : x ≤ y
l : J
f : k ⟶ l
g : j ⟶ l
hl :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map f)) x = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map g)) x'
l' : J
f' : k ⟶ l'
g' : j ⟶ l'
hl' :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map f')) y = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map g')) y'
m : J
a : l ⟶ m
b : l' ⟶ m
h₁ : f ≫ a = f' ≫ b
h₂ : g ≫ a = g' ≫ b
⊢ x' ≤ y'

Tactic:
dsimp at hl hl'

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
j : J
x' y' : (F ⋙ forget PartOrdEmb).obj j
hx :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) x') =
    (ConcreteCategory.hom (s.ι.app j)) x'
hy :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) ((ConcreteCategory.hom (c.ι.app j)) y') =
    (ConcreteCategory.hom (s.ι.app j)) y'
x✝ : (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'
k : J
x y : ↑(F.obj k)
hx' : (ConcreteCategory.hom (c.ι.app k)) x = (ConcreteCategory.hom (c.ι.app j)) x'
hy' : (ConcreteCategory.hom (c.ι.app k)) y = (ConcreteCategory.hom (c.ι.app j)) y'
h : x ≤ y
l : J
f : k ⟶ l
g : j ⟶ l
hl : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
l' : J
f' : k ⟶ l'
g' : j ⟶ l'
hl' : (ConcreteCategory.hom (F.map f')) y = (ConcreteCategory.hom (F.map g')) y'
m : J
a : l ⟶ m
b : l' ⟶ m
h₁ : f ≫ a = f' ≫ b
h₂ : g ≫ a = g' ≫ b
⊢ x' ≤ y'
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : 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
hc : IsColimit c
⊢ IsColimit ((coyoneda.obj (Opposite.op J)).mapCocone c)

Tactic:
· have := isFiltered_of_isCardinalFiltered A κ'
    have := IsCardinalFiltered.of_le A h
    replace hc := isColimitOfPreserves (forget _) hc
    refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_)
    · dsimp at f
      choose j g hg using fun (x : J.obj) ↦ Types.jointly_surjective_of_isColimit hc (f x)
      let m := IsCardinalFiltered.max j hJ
      let φ (x : J.obj) : (F.obj m).obj := F.map (IsCardinalFiltered.toMax j hJ x) (g x)
      have hφ (x : J.obj) : f x = c.ι.app _ (φ x) := by
        dsimp [φ]
        rw [← hg, ← ConcreteCategory.comp_apply, c.w]
        rfl
      refine ⟨m,
        ObjectProperty.homMk (PartOrdEmb.ofHom
          { toFun := φ
            inj' x y h := Hom.injective f (by simpa [hφ])
            map_rel_iff' {x y} := ?_ }), ?_⟩
      · simp [← Hom.le_iff_le f, hφ]
      · dsimp
        ext x
        trans c.ι.app (j x) (g x)
        · exact (hg x).symm
        · exact (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x))
    · 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.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
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).2.1 }
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT shape.L κ

Tactic:
have : HasCardinalLT (ι × (Σ (i : ι), Subtype (D i).P)) κ :=
      hasCardinalLT_prod hκ hι (hasCardinalLT_sigma _ _ hι (fun i ↦ (D i).hP))

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
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).2.1 }
hκ : Cardinal.aleph0 ≤ κ
this : HasCardinalLT (ι × (i : ι) × Subtype (D i).P) κ
⊢ HasCardinalLT shape.L κ