mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor.map (ρ.map f)
⊢ (W₂.inverseImage Φ.functor).inverseImage ρ f

Tactic:
simp only [MorphismProperty.inverseImage_iff]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor.map (ρ.map f)
⊢ W₂ (Φ.functor.map (ρ.map f))
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case refine_2
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
⊢ (W.functorCategory (Discrete J)).IsInvertedBy L₂

Tactic:
· intro X Y f hf
    have : ∀ (j : Discrete J), IsIso ((L₂.map f).app j) :=
      fun j => Localization.inverts L W _ (hf j)
    apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case h.ρ_hom
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
X : F C
⊢ motive ⟦Hom.ρ_hom X⟧

Tactic:
| ρ_hom X =>

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
⊢ (comparison adj).IsEquivalence

Tactic:
by
    have : ∀ (X : Algebra adj.toMonad), IsIso ((comparisonAdjunction adj).unit.app X) := by
      intro X
      apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _
      · change IsIso ((comparisonAdjunction adj).unit.app X).f
        rw [comparisonAdjunction_unit_f]
        exact (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X)
          (unitColimitOfPreservesCoequalizer X)).isIso_hom
    have : ∀ (Y : D), IsIso ((comparisonAdjunction adj).counit.app Y) := by
      intro Y
      rw [comparisonAdjunction_counit_app]
      -- Porting note: passing instances through
      change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
      · infer_instance
      -- Porting note: passing instances through
      apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ _ ?_
      apply reflectsColimit_of_reflectsIsomorphisms
    exact (comparisonAdjunction adj).toEquivalence.isEquivalence_inverse

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:
change
    (unit G F).app (x, y) ≫ (braiding F G).inv.app ((tensor C).obj (x, y)) = _

Goal state after:
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 ((tensor C).obj (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
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
r : R
a : ↑A
h₁ :
  (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ)) (r ⊗ₜ[R] a) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor A).hom) (r ⊗ₜ[R] a)
⊢ (Hom.hom η) r * a = a * (Hom.hom η) r

Tactic:
have h₂ := LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_one A)) (a ⊗ₜ r)

Goal state after:
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
r : R
a : ↑A
h₁ :
  (Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ)) (r ⊗ₜ[R] a) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor A).hom) (r ⊗ₜ[R] a)
h₂ :
  (Hom.hom (MonoidalCategoryStruct.whiskerLeft A η ≫ μ)) (a ⊗ₜ[R] r) =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor A).hom) (a ⊗ₜ[R] r)
⊢ (Hom.hom η) r * a = a * (Hom.hom η) r
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
⊢ (λ_ (limit F)).hom ≫ limit.π F j =
    (limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } } ≫
          limit.π (𝟙_ (J ⥤ C)) j) ▷
        limit F ≫
      (λ_ (limit F)).hom ≫ limit.π F j

Tactic:
erw [limit.lift_π]

Goal state after:
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
⊢ (λ_ (limit F)).hom ≫ limit.π F j =
    { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ▷ limit F ≫
      (λ_ (limit F)).hom ≫ limit.π F j
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
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁
        (limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } } ≫
          limit.π (𝟙_ (J ⥤ C)) j) ≫
      (ρ_ (limit F)).hom ≫ limit.π F j

Tactic:
erw [limit.lift_π]

Goal state after:
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
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁ { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ≫
      (ρ_ (limit F)).hom ≫ limit.π F j
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
⊢ map (𝟙 ((ι C V D).obj x)) (𝟙 ((ι C V D).obj y)) = 𝟙 ((ι C V D).obj (x ⊗ y))

Tactic:
apply (DayConvolution.corepresentableBy
        (ι C V D |>.obj _) (ι C V D |>.obj _)).homEquiv.injective

Goal state after:
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
⊢ (corepresentableBy ((ι C V D).obj x) ((ι C V D).obj y)).homEquiv (map (𝟙 ((ι C V D).obj x)) (𝟙 ((ι C V D).obj y))) =
    (corepresentableBy ((ι C V D).obj x) ((ι C V D).obj y)).homEquiv (𝟙 ((ι C V D).obj (x ⊗ y)))
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 := ⋯ }
x✝ : Total Q
j : J
i : I j
⊢ { pt := X, ι := { app := fun k ↦ (Q k.fst).ι.app k.snd ≫ P.ι.app k.fst, naturality := ⋯ } }.ι.app ⟨j, i⟩ ≫
      P.isColimit.desc
        { pt := c.pt,
          ι :=
            {
              app := fun j ↦
                (Q j).isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j, i⟩, naturality := ⋯ } },
              naturality := ⋯ } } =
    c.ι.app ⟨j, i⟩

Tactic:
by simp [P.isColimit.fac, (Q j).isColimit.fac]

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      ((M.X ◁ N.X ◁ f.hom ≫
            M.X ◁
              colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))
                WalkingParallelPair.one) ≫
          (PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P'.X)
              ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)).inv) ≫
        coequalizer.desc
          ((α_ M.X N.X P'.X).inv ≫
            coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X ≫
              coequalizer.π (TensorBimod.actRight M N ▷ P'.X)
                ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft))
          ⋯

Tactic:
slice_rhs 3 5 => rw [id_tensor_π_preserves_coequalizer_inv_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
W X Y Z : Mon C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫
      coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫
        colimit.ι
          (parallelPair (TensorBimod.actRight M N ▷ P'.X)
            ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫
              coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁ N.X ◁ f.hom ≫
        (α_ M.X N.X P'.X).inv ≫
          coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X ≫
            coequalizer.π (TensorBimod.actRight M N ▷ P'.X)
              ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft)
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

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

Tactic:
obtain ⟨n, hn⟩ := h (G ⋙ (Subobject.equivMonoOver _).inverse).toOrderHom

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ MonoOver X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      (G ⋙ (Subobject.equivMonoOver X).inverse).toOrderHom n = (G ⋙ (Subobject.equivMonoOver X).inverse).toOrderHom m
⊢ IsFiltered.IsEventuallyConstant G
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)
⊢ finrank 𝕜 (X ⟶ X) = 1

Tactic:
have id_nonzero := (isIso_iff_nonzero (𝟙 X)).mp (by infer_instance)

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
⊢ finrank 𝕜 (X ⟶ X) = 1
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case mp
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 → Nonempty (X ≅ Y)

Tactic:
intro h
    rw [finrank_eq_one_iff'] at h
    obtain ⟨f, nz, -⟩ := h
    rw [← isIso_iff_nonzero] at nz
    exact ⟨asIso f⟩

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft))
            WalkingParallelPair.one) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      ((M.X ◁ f.hom ▷ P.X ≫
            M.X ◁
              colimit.ι (parallelPair (N'.actRight ▷ P.X) ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft))
                WalkingParallelPair.one) ≫
          (PreservesCoequalizer.iso (tensorLeft M.X) (N'.actRight ▷ P.X)
              ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft)).inv) ≫
        coequalizer.desc
          ((α_ M.X N'.X P.X).inv ≫
            coequalizer.π (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ▷ P.X ≫
              coequalizer.π (TensorBimod.actRight M N' ▷ P.X)
                ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
          ⋯

Tactic:
slice_rhs 3 5 => rw [id_tensor_π_preserves_coequalizer_inv_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft))
            WalkingParallelPair.one) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    (α_ M.X N.X P.X).hom ≫
      M.X ◁ f.hom ▷ P.X ≫
        (α_ M.X N'.X P.X).inv ≫
          coequalizer.π (M.actRight ▷ N'.X) ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ▷ P.X ≫
            coequalizer.π (TensorBimod.actRight M N' ▷ P.X)
              ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft)
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : Cardinal.mk K < κ
⊢ ∃ j, ∀ (k : K), α k ≤ j

Tactic:
by
    rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK
    let t (k : K) : (α k).val := ⊤_ _
    let m := IsCardinalFiltered.max (fun k ↦ (t k).val) hK
    let S : Set J.obj := (⋃ (k : K), α k) ∪ {m}
    let : OrderTop S :=
      { top := ⟨m, by simp [S]⟩
        le_top := by
          rintro ⟨s, hs⟩
          simp only [Set.union_singleton, Set.mem_insert_iff, Set.mem_iUnion, S] at hs
          obtain rfl | ⟨k, hs⟩ := hs
          · simp
          · simp only [Subtype.mk_le_mk]
            exact leOfHom ((by exact terminal.from (C := (α k).val) ⟨_, hs⟩) ≫
              IsCardinalFiltered.toMax _ hK k) }
    refine ⟨⟨S, ?_, isTerminalTop.hasTerminal⟩, fun k ↦ ?_⟩
    · have hκ : Cardinal.aleph0 ≤ κ :=  Cardinal.IsRegular.aleph0_le Fact.out
      exact hasCardinalLT_union hκ (hasCardinalLT_iUnion _ hK (fun k ↦ (α k).2.1))
        (hasCardinalLT_of_finite _ _ hκ)
    · simp only [← Subtype.coe_le_coe]
      exact subset_trans (Set.subset_iUnion_of_subset k (subset_refl _)) Set.subset_union_left

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) κ₂
⊢ ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y

Tactic:
choose j y hy using fun x ↦ Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (forget (CardinalDirectedPoset κ₁)) p.isColimit)
    (SetCardinalLT.singleton κ₁ x)

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) → (fun X ↦ X) ((p.diag ⋙ forget (CardinalDirectedPoset κ₁)).obj (j x))
hy :
  ∀ (x : X),
    (ConcreteCategory.hom
          (((forget (CardinalDirectedPoset κ₁)).mapCocone { pt := setCardinalLT κ₁ X, ι := p.ι }).ι.app (j x)))
        (y x) =
      SetCardinalLT.singleton κ₁ x
⊢ ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
hf : (⨆ i, (D i).W) f✝
⊢ (∃ a, (D a).P i✝) ∨ m = i✝

Tactic:
simp only [MorphismProperty.iSup_iff] at hf

Goal state after:
case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
hf : ∃ i, (D i).W f✝
⊢ (∃ a, (D a).P i✝) ∨ m = i✝
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
hf : (⨆ i, (D i).W) f✝
⊢ (∃ a, (D a).P j✝) ∨ m = j✝

Tactic:
simp only [MorphismProperty.iSup_iff] at hf

Goal state after:
case inl.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
hf : ∃ i, (D i).W f✝
⊢ (∃ a, (D a).P j✝) ∨ m = j✝
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inl.inl
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf : (⨆ i, (D i).W) f
⊢ f = 𝟙 m

Tactic:
simp only [MorphismProperty.iSup_iff] at hf

Goal state after:
case inl.inl
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf : ∃ i, (D i).W f
⊢ f = 𝟙 m