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.tensorBimod N₁).actLeft ≫
      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) ⋯ ⋯) =
    X.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) ⋯ ⋯) ≫
      (M.tensorBimod N₂).actLeft

Tactic:
by
    refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
    dsimp
    slice_lhs 1 2 => rw [TensorBimod.whiskerLeft_π_actLeft]
    slice_lhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
    slice_rhs 1 2 => rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one,
      whiskerLeft_comp]
    slice_rhs 2 3 => rw [TensorBimod.whiskerLeft_π_actLeft]
    slice_rhs 1 2 => rw [associator_inv_naturality_right]
    slice_rhs 2 3 => rw [whisker_exchange]
    simp

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

Goal state before:
pp: C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
⊢ ((tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom).app { as := n } =
    ((normalizeIsoAux C X).hom ≫ (normalize' C).map f).app { as := n }

Tactic:
convert! normalize_naturality n f using 1

Goal state after:
case e'_2
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ ((tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom).app { as := n } = inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom

case e'_3
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ ((normalizeIsoAux C X).hom ≫ (normalize' C).map f).app { as := n } =
    (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (Δ ⊗ₘ Δ) ≫
    (α_ A A (A ⊗ A)).hom ≫
      A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv ≫ (μ ⊗ₘ μ)

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| 𝒮 ▷ A

Tactic:
rw [Bimon.compatibility]

Goal state after:
case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ≫ Δ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| 𝒮 ▷ A
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
⊢ (λ_ (R.X ⊗ P.X)).inv ≫
      (((α_ (𝟙_ C) R.X P.X).inv ≫ η ▷ R.X ▷ P.X) ≫ μ ▷ P.X) ≫
        coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) =
    coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      𝟙 (coequalizer (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))

Tactic:
slice_lhs 3 4 => rw [← comp_whiskerRight, MonObj.one_mul]

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
⊢ (λ_ (R.X ⊗ P.X)).inv ≫
      (α_ (𝟙_ C) R.X P.X).inv ≫ (λ_ R.X).hom ▷ P.X ≫ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) =
    coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      𝟙 (coequalizer (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
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
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (unit F G).app x✝.1 ▷ H.obj x✝.2 ≫
      ((map f g).app (x✝.1.1 ⊗ x✝.1.2) ⊗ₘ h.app x✝.2) ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (unit F G).app x✝.1 ▷ H.obj x✝.2 ≫
      (unit (F ⊛ G) H).app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫
        (associator F G H).hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) ≫ (map f (map g h)).app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2)

Tactic:
rw [associator_hom_unit_unit_assoc]

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
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (unit F G).app x✝.1 ▷ H.obj x✝.2 ≫
      ((map f g).app (x✝.1.1 ⊗ x✝.1.2) ⊗ₘ h.app x✝.2) ≫
        (unit (F' ⊛ G') H').app (x✝.1.1 ⊗ x✝.1.2, x✝.2) ≫ (associator F' G' H').hom.app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2) =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      F.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
        (unit F (G ⊛ H)).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
          (F ⊛ G ⊛ H).map (α_ x✝.1.1 x✝.1.2 x✝.2).inv ≫ (map f (map g h)).app ((x✝.1.1 ⊗ x✝.1.2) ⊗ x✝.2)
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (𝟙_ (C ⥤ D)).map f ≫ η.app Y✝ = η.app Y✝

Tactic:
tensorUnit_map

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ 𝟙 (𝟙_ D) ≫ η.app Y✝ = η.app Y✝
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ε.app X✝ ≫ (𝟙_ (C ⥤ D)).map f = ε.app X✝

Tactic:
tensorUnit_map

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ε.app X✝ ≫ 𝟙 (𝟙_ D) = ε.app X✝
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: case refine_1
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
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
⊢ ∃ c, Nonempty (f ⟶ p.toCostructuredArrow.obj c)

Tactic:
obtain ⟨j, g, hg⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit f.hom

Goal state after:
case refine_1
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
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
j : J
g : (isCardinalPresentable C κ).ι.obj f.left ⟶ p.diag.obj j
hg : g ≫ { pt := X, ι := p.ι }.ι.app j = f.hom
⊢ ∃ c, Nonempty (f ⟶ p.toCostructuredArrow.obj c)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ P.ind f ↔ ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

Tactic:
rw [ind_iff_ind_underMk, ObjectProperty.ind_iff_exists]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ (∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W) ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
h : Epi (F.map f)
Z : D
u v : F.obj Y ⟶ Z
huv : u = v
⊢ G.map u = G.map v

Tactic:
rw [huv]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v : Arrow V
f g : u✝ ⟶ v
inst✝ : HasZeroObject V
X✝ Y✝ : V
u : (rightFunctor V).obj X✝ ⟶ (rightFunctor V).obj Y✝
⊢ ∃ a, (functor V).map a = (quotient V).map u

Tactic:
exact ⟨u.right, (quotient V).congr_map (by cat_disch)⟩

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ ((M + N).map fun i j ↦ ⇑f) = (M.map fun i j ↦ ⇑f) + N.map fun i j ↦ ⇑f

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ ((M - N).map fun i j ↦ ⇑f) = (M.map fun i j ↦ ⇑f) - N.map fun i j ↦ ⇑f

Tactic:
by
  ext; simp

Goal state after:
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
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
f g : End X
⊢ f * g = g * f

Tactic:
obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f

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
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
g : End X
c : 𝕜
⊢ c • 𝟙 X * g = g * c • 𝟙 X
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ ∑ x, (∑ j, f i✝ j ≫ g j x) ≫ h x j✝ = ∑ x, f i✝ x ≫ ∑ j, g x j ≫ h j j✝

Tactic:
sum_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ ∑ x, ∑ j, (f i✝ j ≫ g j x) ≫ h x j✝ = ∑ x, f i✝ x ≫ ∑ j, g x j ≫ h j j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat R
⊢ (equivalenceSingleObjInverse R).obj { ι := X.obj, fintype := FintypeCat.fintype, X := fun x ↦ PUnit.unit } = X

Tactic:
by cases X; congr

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
g₁ g₂ : Y ⟶ Z
h : (fun g ↦ f ≫ g) g₁ = (fun g ↦ f ≫ g) g₂
⊢ g₁ = g₂

Tactic:
obtain ⟨j₁, g₁, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₁

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
g₂ : Y ⟶ Z
j₁ : J
g₁ : Y ⟶ p.diag.obj j₁
h : (fun g ↦ f ≫ g) (g₁ ≫ { pt := Z, ι := p.ι }.ι.app j₁) = (fun g ↦ f ≫ g) g₂
⊢ g₁ ≫ { pt := Z, ι := p.ι }.ι.app j₁ = g₂
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

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

Tactic:
rw [transfiniteIterate_succ _ _ _ hj, φ_eq _ _ _ hj']

Goal state after:
case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
⊢ HasCardinalLT (↑(φ₀ Y m (transfiniteIterate (φ Y m) j A) hj')) κ₂
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_2
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)
h : (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1, (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) f = (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) g

Tactic:
· choose k a hk using fun x ↦
          (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (congr_hom h x)
        dsimp at f g h k a hk ⊢
        replace hk : ∀ x, F.map (a x) (f x) = F.map (a x) (g x) := by assumption
        obtain ⟨l, b, c, hl⟩ : ∃ (l : J) (c : j ⟶ l) (b : ∀ x, k x ⟶ l),
            ∀ x, a x ≫ b x = c := by
          let φ (x : X) : j ⟶ IsCardinalFiltered.max k hX :=
            a x ≫ IsCardinalFiltered.toMax k hX x
          exact ⟨IsCardinalFiltered.coeq φ hX,
            IsCardinalFiltered.toCoeq φ hX,
            fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX,
            fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x⟩
        refine ⟨l, b, by ext x; simp [← hl x, hk]⟩

Goal state after:
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 κ
Z : C
⊢ W.isLocal.ι.leftAdjointObjIsDefined Z ↔ ⊤ Z

Tactic:
simpa using! (corepresentableBy Z hW).isCorepresentable

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f

Tactic:
refine ⟨Presieve.singleton h, ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.singleton h ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ (Presieve.singleton h).FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_4.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
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₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j k : J
f : j ⟶ k
hf : (Diagram.iSup (fun i ↦ (D i).toDiagram) hι).W f
⊢ ∃ li lj, (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li

Tactic:
simp only [Diagram.iSup_W, MorphismProperty.iSup_iff] at hf

Goal state after:
case refine_4.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
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₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j k : J
f : j ⟶ k
hf : ∃ i, (D i).W f
⊢ ∃ li lj, (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ f ≫ lj = li
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generateFamily Y π).arrows.cocone
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)

Tactic:
← Sieve.generateFamily_eq

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
⊢ Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
⊢ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck (∐ fun i ↦ X i)

Tactic:
have : generate (Presieve.ofArrows X fun (i : I) ↦ Sigma.ι X i) ≤
            (generate (Presieve.ofArrows X f)).pullback (Sigma.desc f) := by
          rintro Q q ⟨E, e, r, ⟨hq, rfl⟩⟩
          exact ⟨E, e, r ≫ (Sigma.desc f), by cases hq; simpa using Presieve.ofArrows.mk _, by simp⟩

Goal state after:
case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y✝ : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y✝
hT : EffectiveEpiFamily X f
R Y : C
i✝ : Unit
ψ : R ⟶ ∐ fun i ↦ X i
this :
  generate (Presieve.ofArrows X fun i ↦ Sigma.ι X i) ≤ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))
⊢ Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck (∐ fun i ↦ X i)