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

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ μ ⊵ₗ M ≫ f ⊵ₗ M ≫ γ = (f ▷ A) ⊵ₗ M ≫ ((B ◁ f) ⊵ₗ M ≫ μ ⊵ₗ M) ≫ γ

Tactic:
slice_rhs 1 2 => rw [← comp_actionHomLeft]

Goal state after:
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalLeftAction C D
M' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ μ ⊵ₗ M ≫ f ⊵ₗ M ≫ γ = ((f ▷ A ≫ B ◁ f) ⊵ₗ M ≫ μ ⊵ₗ M) ≫ γ
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
        ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
          P.X ◁ TensorBimod.actLeft Q L) ▷
      U.X ≫
    TensorBimod.actRight P (Q.tensorBimod L)

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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ P.X Q.X L.X).hom ▷ U.X

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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ▷ U.X

Tactic:
TensorBimod.π_tensor_id_actRight P (Q.tensorBimod L)

Goal state after:
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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ P.X (Q.tensorBimod L).X U.X).hom ≫
    P.X ◁ (Q.tensorBimod L).actRight ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
        ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ P.X Q.X L.X).hom ▷ U.X

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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ▷ U.X
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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (α_ P.X Q.X L.X).inv ≫
      coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
        (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫
          coequalizer.desc
            ((α_ P.X Q.X L.X).hom ≫
              P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
                coequalizer.π (P.actRight ▷ TensorBimod.X Q L)
                  ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L))
            ⋯ =
    P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
          ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫
        𝟙 (TensorBimod.X P (Q.tensorBimod L))

Tactic:
slice_lhs 2 4 => rw [π_tensor_id_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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (α_ P.X Q.X L.X).inv ≫
      (α_ P.X Q.X L.X).hom ≫
        P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
          coequalizer.π (P.actRight ▷ TensorBimod.X Q L)
            ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L) =
    P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
          ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫
        𝟙 (TensorBimod.X P (Q.tensorBimod L))
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
D : Type u₃
inst✝² : Category.{v₃, u₃} D
inst✝¹ : MonoidalCategoryStruct D
inst✝ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d₁ d₂ d₁' d₂' : D
f : d₁ ⟶ d₂
f' : 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 ⊗ₘ f')).app (x ⊗ y) =
    (((ι C V D).map f).app x ⊗ₘ ((ι C V D).map f').app y) ≫
      (DayConvolution.unit ((ι C V D).obj d₂) ((ι C V D).obj d₂')).app (x, y)

Tactic:
exact convolutionExtensionUnit_comp_ι_map_tensorHom_app C V _ _ _ _

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H✝ : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
incl : P.FullSubcategory ⥤ (isFinitelyPresentable C).FullSubcategory := ιOfLE H✝
H :
  ∀ (d : CostructuredArrow (isFinitelyPresentable C).ι X),
    ∃ c, Nonempty (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable C).ι X).obj c)
this : (CostructuredArrow.pre incl (isFinitelyPresentable C).ι X).Final
⊢ P.ind X

Tactic:
have : IsFiltered (CostructuredArrow P.ι X) :=
      .of_exists_of_isFiltered_of_fullyFaithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X) H

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H✝ : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
incl : P.FullSubcategory ⥤ (isFinitelyPresentable C).FullSubcategory := ιOfLE H✝
H :
  ∀ (d : CostructuredArrow (isFinitelyPresentable C).ι X),
    ∃ c, Nonempty (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable C).ι X).obj c)
this✝ : (CostructuredArrow.pre incl (isFinitelyPresentable C).ι X).Final
this : IsFiltered (CostructuredArrow P.ι X)
⊢ P.ind X
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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
⊢ (ι C V D).map (λ_ d).hom = (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom

Tactic:
apply corepresentableByLeft
    (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.obj d) |>.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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
⊢ (corepresentableByLeft ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).homEquiv ((ι C V D).map (λ_ d).hom) =
    (corepresentableByLeft ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).homEquiv
      (DayConvolutionUnit.leftUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
⊢ P.limitsClosure J ≤ (P.limitsClosure J).shift a

Tactic:
intro X hX
    induction hX with
    | of_mem X hX => exact limitsClosure.of_mem _ (IsStableUnderShiftBy.le_shift X hX)
    | of_isoClosure e hX hX' => exact limitsClosure.of_isoClosure ((shiftFunctor C a).mapIso e) hX'
    | of_limitPresentation pres h h' =>
      exact limitsClosure.of_limitPresentation (pres.map (shiftFunctor C a)) h'

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)

Tactic:
{

Goal state after:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)
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'
⊢ (ConcreteCategory.hom (s.ι.app j)) x' ≤ (ConcreteCategory.hom (s.ι.app j)) y' ↔
    (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'

Tactic:
OrderEmbedding.le_iff_le

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' ≤ y' ↔ (ConcreteCategory.hom (c.ι.app j)) x' ≤ (ConcreteCategory.hom (c.ι.app j)) y'
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'
⊢ x' ≤ y'

Tactic:
obtain ⟨l', f', g', hl'⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hy'

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 ⋙ 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'
⊢ x' ≤ y'
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : DiagramWithUniqueTerminal J κ
⊢ functorMap ⋯ = 𝟙 D.top

Tactic:
simp [functorMap]

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

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∀ {i j_1 : J} {f : i ⟶ j_1}, MorphismProperty.ofHoms (fun x ↦ 𝟙 j) f → ObjectProperty.ofObj (fun x ↦ j) i

Tactic:
rintro _ _ _ ⟨⟩

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j X Y : J
i✝ : Unit
⊢ ObjectProperty.ofObj (fun x ↦ j) j
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∀ {i j_1 : J} {f : i ⟶ j_1}, MorphismProperty.ofHoms (fun x ↦ 𝟙 j) f → ObjectProperty.ofObj (fun x ↦ j) j_1

Tactic:
rintro _ _ _ ⟨⟩

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j X Y : J
i✝ : Unit
⊢ ObjectProperty.ofObj (fun x ↦ j) j
Module: Mathlib.CategoryTheory.Profunctor.Basic

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
P : ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D
X : C
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ P.map (𝟙 X) (g ≫ g') = P.map (𝟙 X) g' ≫ P.map (𝟙 X) g

Tactic:
nth_rw 1 [← Category.id_comp (𝟙 X)]
  simp only [P.map_comp]

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
⊢ Presieve.singleton h = Presieve.ofArrows (fun x ↦ W) fun x ↦ h

Tactic:
{

Goal state after:
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 = Presieve.ofArrows (fun x ↦ W) fun x ↦ h
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X_1 π, S = Presieve.ofArrows X_1 π ∧ IsIso (Sigma.desc π)},
      ∃ T ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}, T.FactorsThruAlong S f

Tactic:
by
    intro X Y f S ⟨α, hα, Z, π, hS, h_iso⟩
    let Z' : α → C := fun a ↦ pullback f (π a)
    let π' : (a : α) → Z' a ⟶ Y := fun a ↦ pullback.fst _ _
    refine ⟨@Presieve.ofArrows C _ _ α Z' π', ⟨?_, ?_⟩⟩
    · constructor
      exact ⟨hα, Z', π', ⟨by simp only,
        FinitaryPreExtensive.isIso_sigmaDesc_fst (fun x => π x) f h_iso⟩⟩
    · intro W g hg
      rcases hg with ⟨a⟩
      refine ⟨Z a, pullback.snd _ _, π a, ?_, by rw [CategoryTheory.Limits.pullback.condition]⟩
      rw [hS]
      exact Presieve.ofArrows.mk a

Goal state after:
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
⊢ (∀ {Y : C}, Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    ∀ (X_1 : Cᵒᵖ), IsIso ((uliftYonedaEquiv.symm { down := x }).app X_1)

Tactic:
Opposite.op_surjective.forall

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
⊢ (∀ {Y : C}, Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    ∀ (x_1 : C), IsIso ((uliftYonedaEquiv.symm { down := x }).app (op x_1))
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α, ∃ (_ : Finite α), ∃ Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
choose β _ Y_n π_n H using fun a => b (h₂ a)

Goal state after:
case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α, ∃ (_ : Finite α), ∃ Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : α → Type
x✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
inst✝ : HasFiniteCoproducts C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
x✝ : EffectiveEpi g
hp : EffectiveEpi g → ∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ ι, ∀ (b : β), ι b ≫ g = π₂ b ≫ f
β : Type
w✝ : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ X
h : EffectiveEpiFamily X₂ π₂
ι : (b : β) → X₂ b ⟶ Z
hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f
b : β
⊢ Sigma.ι X₂ b ≫ Sigma.desc ι ≫ g = Sigma.ι X₂ b ≫ Sigma.desc π₂ ≫ f

Tactic:
simpa using hι b

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B
⊢ S ∈ (coherentTopology C) B

pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (coherentTopology C) B
⊢ S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B

Tactic:
· induction h with
    | of Y T hT =>
      apply Coverage.Saturate.of
      simp only [Coverage.sup_covering, Set.mem_union] at hT
      exact Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
h : S ∈ (coherentTopology C) B
⊢ S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B
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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ ∃ Y π, EffectiveEpi π ∧ (Sieve.functorPushforward F S).arrows π

Tactic:
refine ⟨F.obj Y, F.map π, ⟨?_, Sieve.image_mem_functorPushforward F S H₂⟩⟩

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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ EffectiveEpi (F.map π)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
inst✝ : ∀ (X : C), Projective X
⊢ IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F

Tactic:
by
  rw [isSheaf_coherent_iff_regular_and_extensive, and_iff_left (isSheaf_of_projective F),
    isSheaf_iff_preservesFiniteProducts]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
inst✝ : ∀ (X : C), Projective X
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective, isSheaf_iff_preservesFiniteProducts]

Goal state after: