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

Goal state before:
pp: case a.a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| 𝟙_ C ◁ N.actLeft ≫ η ▷ N.X

pp: case a.a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

pp: case a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| X.X ◁ f.hom

pp: case a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| (λ_ (X.X ⊗ N.X)).inv

Tactic:
rw [whisker_exchange]

Goal state after:
case a.a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| η ▷ (X.X ⊗ N.X) ≫ X.X ◁ N.actLeft

case a.a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

case a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| X.X ◁ f.hom

case a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| (λ_ (X.X ⊗ N.X)).inv
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
⊢ p.toCostructuredArrow.Final

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
  rw [Functor.final_iff_of_isFiltered]
  refine ⟨fun f ↦ ?_, fun {f j} g₁ g₂ ↦ ?_⟩
  · obtain ⟨j, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit f.hom
    exact ⟨j, ⟨CostructuredArrow.homMk (ObjectProperty.homMk g)⟩⟩
  · obtain ⟨k, a, h⟩ := IsCardinalPresentable.exists_eq_of_isColimit' κ p.isColimit
      g₁.left.hom g₂.left.hom ((CostructuredArrow.w g₁).trans (CostructuredArrow.w g₂).symm)
    exact ⟨k, a, by cat_disch⟩

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
x✝ : P.ind.strictLimitsOfShape (Discrete ι) X
Y : Discrete ι ⥤ C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : ι ≃ Shrink.{w, u_1} ι := equivShrink ι
this✝¹ : HasProductsOfShape (Shrink.{w, u_1} ι) C
this✝ : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅ ∏ᶜ fun i ↦ Y.obj { as := e.symm i } :=
  (Pi.isoLimit Y).symm ≪≫ (Pi.reindex e.symm fun j ↦ Y.obj { as := j }).symm
⊢ P.ind (limit Y)

Tactic:
(ind.{w} P).prop_iff_of_iso iso

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
x✝ : P.ind.strictLimitsOfShape (Discrete ι) X
Y : Discrete ι ⥤ C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : ι ≃ Shrink.{w, u_1} ι := equivShrink ι
this✝¹ : HasProductsOfShape (Shrink.{w, u_1} ι) C
this✝ : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅ ∏ᶜ fun i ↦ Y.obj { as := e.symm i } :=
  (Pi.isoLimit Y).symm ≪≫ (Pi.reindex e.symm fun j ↦ Y.obj { as := j }).symm
⊢ P.ind (∏ᶜ fun i ↦ Y.obj { as := e.symm i })
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
f : X✝ ⟶ Y✝
⊢ map (𝟙 ((ι C V D).obj (𝟙_ D))) ((ι C V D).map f) ≫ (ι C V D).map (λ_ Y✝).hom =
    (ι C V D).map (λ_ X✝).hom ≫ (ι C V D).map f

Tactic:
rw [ι_map_leftUnitor_hom_eq_leftUnitor_hom,
        ι_map_leftUnitor_hom_eq_leftUnitor_hom]

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
f : X✝ ⟶ Y✝
⊢ map (𝟙 ((ι C V D).obj (𝟙_ D))) ((ι C V D).map f) ≫
      (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj Y✝)).hom =
    (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj X✝)).hom ≫ (ι C V D).map f
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
⊢ P.ind f

Tactic:
· refine ⟨J, ‹_›, ‹_›, pres.diag ⋙ CategoryTheory.Under.forget _, ?_, ?_, ?_, fun j ↦ ⟨?_, ?_⟩⟩
    · exact { app j := (pres.diag.obj j).hom }
    · exact Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)
    · exact isColimitOfPreserves (CategoryTheory.Under.forget _) pres.isColimit
    · exact hpres j
    · simp

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

Goal state before:
pp: case refine_1.comp.refine_1
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✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ K.morphismProperty (pullback.snd g (E.f i))

Tactic:
obtain ⟨j⟩ := hg

Goal state after:
case refine_1.comp.refine_1
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✝
hf : sourceLocalClosure K P f
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
U Y : C
j : F.I₀
v : U ⟶ F.X j
i : (Precoverage.ZeroHypercover.pullback₁ (F.f j) E).I₀
⊢ K.morphismProperty (pullback.snd (F.f j) (E.f i))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
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 M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
    f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)

pp: case a
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 M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| colimit.ι
    (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))
      ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫
        M'.X ◁ TensorBimod.actLeft N P))
    WalkingParallelPair.one

Tactic:
rw [whisker_exchange]

Goal state after:
case a
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 M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| f.hom ▷ (N.X ⊗ P.X) ≫ M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)

case a
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 M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| colimit.ι
    (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))
      ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫
        M'.X ◁ TensorBimod.actLeft N P))
    WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
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)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| M.X ◁ g.hom ≫ f.hom ▷ Q.X

pp: case a
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)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one

Tactic:
rw [whisker_exchange]

Goal state after:
case a
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)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| f.hom ▷ P.X ≫ N.X ◁ g.hom

case a
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)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
⊢ ∀ {W X Y Z : Mat R} (f : Matrix W.obj X.obj R) (g : Matrix X.obj Y.obj R) (h : Matrix Y.obj Z.obj R),
    ((have this :=
          (have this := f;
            this) *
            have this := g;
            this;
        this) *
        have this := h;
        this) =
      (have this := f;
        this) *
        have this :=
          (have this := g;
            this) *
            have this := h;
            this;
        this

Tactic:
by intros; simp [Matrix.mul_assoc]

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
s : ↑J.obj
hs✝ : s ∈ S
hs : s = m ∨ ∃ i, s ∈ ↑(α i)
⊢ ⟨s, hs✝⟩ ≤ ⟨m, ⋯⟩

Tactic:
obtain rfl | ⟨k, hs⟩ := hs

Goal state after:
case inl
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
hs : m ∈ S
⊢ ⟨m, hs⟩ ≤ ⟨m, ⋯⟩

case inr
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
s : ↑J.obj
hs✝ : s ∈ S
k : K
hs : s ∈ ↑(α k)
⊢ ⟨s, hs✝⟩ ≤ ⟨m, ⋯⟩
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
⊢ A ⊆ ⋃ j, transfiniteIterate (φ Y m) j A

Tactic:
by
  have := Cardinal.nonempty_ord_toType (c := κ₁) (IsRegular.ne_zero Fact.out)
  let := WellFoundedLT.toOrderBot κ₁.ord.ToType
  exact subset_trans (by simp) (Set.subset_iUnion _ ⊥)

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

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝³ : Fact κ₁.IsRegular
inst✝² : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
X : Type w
inst✝¹ : PartialOrder X
inst✝ : IsCardinalFiltered X κ₁
A : Set X
hA : HasCardinalLT (↑A) κ₂
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
⊢ ∃ B, A ⊆ B ∧ IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂

Tactic:
exact ⟨⋃ j, transfiniteIterate (φ Y m) j A, subset_iUnion Y m A,
    isCardinalFiltered_iUnion h₀ Y hY hY' m hm A hA,
    hasCardinalLT_iUnion _ (by simpa [hasCardinalLT_iff_cardinal_mk_lt])
      (hasCardinalLT_transfiniteIterate_φ h₀ Y hY m A hA)⟩

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ HasCardinalLT PUnit.{u + 1} κ

Tactic:
exact hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out)

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)
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₁
hm₁ : (D₄ D φ).IsTerminal m₁ := Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
lift_eq : ∀ (j : J) (hj : D.P j), hm₁.lift ⋯ = φ ⟨j, hj⟩
D₄' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₄ D φ;
  { toDiagram := __Diagram, top := m₁, isTerminal := hm₁, uniq_terminal := ⋯ }
⊢ ∃ c' t, f₁ ≫ (functor J κ).map t = f₂ ≫ (functor J κ).map t

Tactic:
exact ⟨D₄', homOfLE ⟨le_sup_left.trans le_sup_left, le_sup_left⟩,
    by simpa [functorMap, D₄', lift_eq _ D.isTerminal.prop, φ]⟩

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ ∃ α x, ∃ (_ : IsDirected α fun x1 x2 ↦ x1 ≤ x2) (_ : Nonempty α), ∃ F, F.Final

Tactic:
by
  have := (isCardinalFiltered_aleph0_iff.{w} J).2 inferInstance
  obtain ⟨α, _, _, F, _⟩ := IsCardinalFiltered.exists_cardinal_directed J .aleph0
  have : IsFiltered α := by rwa [← isCardinalFiltered_aleph0_iff.{w}]
  exact ⟨α, _, IsFiltered.isDirectedOrder _, nonempty, F, inferInstance⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
x✝¹ : C
x✝ : x✝¹ ⟶ X
hh : Presieve.ofArrows Y π x✝
⊢ S.arrows x✝

Tactic:
cases hh; exact h' _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

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
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B x✝¹ : D
x✝ : x✝¹ ⟶ B
⊢ Presieve.singleton (F.effectiveEpiOver B) x✝ ↔
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) (fun x ↦ F.effectiveEpiOver B) x✝

Tactic:
refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩

Goal state after:
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
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B x✝¹ : D
x✝ : x✝¹ ⟶ B
⊢ Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) (fun x ↦ F.effectiveEpiOver B) x✝ →
    Presieve.singleton (F.effectiveEpiOver B) x✝
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : HasFunctorialSurjectiveInjectiveFactorization A
inst✝¹ : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
⊢ (Arrow.leftFunc.whiskerLeft (inv (sheafificationAdjunction J A).counit) ≫
        (sheafToPresheaf J A).mapArrow.whiskerLeft
          (whiskerRight (MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i
            (presheafToSheaf J A))) ≫
      (sheafToPresheaf J A).mapArrow.whiskerLeft
          (whiskerRight (MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).p
            (presheafToSheaf J A)) ≫
        Arrow.rightFunc.whiskerLeft (sheafificationAdjunction J A).counit =
    Arrow.leftToRight

Tactic:
ext f : 2
    dsimp
    simp only [assoc, ← Functor.map_comp_assoc,
      MorphismProperty.FunctorialFactorizationData.fac_app,
      NatIso.isIso_inv_app, IsIso.inv_comp_eq]
    exact (sheafificationAdjunction J A).counit.naturality f.hom

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
B x✝¹ : D
x✝ : x✝¹ ⟶ B
⊢ Presieve.singleton (F.effectiveEpiOver B) x✝ ↔
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) (fun x ↦ F.effectiveEpiOver B) x✝

Tactic:
refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
B x✝¹ : D
x✝ : x✝¹ ⟶ B
⊢ Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) (fun x ↦ F.effectiveEpiOver B) x✝ →
    Presieve.singleton (F.effectiveEpiOver B) x✝