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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ M₁.X N.X Z.X).hom ≫
      M₁.X ◁ N.actRight ≫
        f.hom ▷ N.X ≫
          colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
            WalkingParallelPair.one =
    coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ▷ Z.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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷
          Z.X ≫
        TensorBimod.actRight M₂ N

Tactic:
slice_lhs 2 3 => rw [whisker_exchange]

Goal state after:
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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ M₁.X N.X Z.X).hom ≫
      (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
          WalkingParallelPair.one =
    coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ▷ Z.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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷
          Z.X ≫
        TensorBimod.actRight M₂ N
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            ((β_ B (i.obj ((reflector i).obj A))).inv ≫
              uncurry
                ((unitCompPartialBijective A ⋯)
                  (curry ((((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f) ≫ i.map g)))))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

Tactic:
curry_natural_right _ (i.map g),

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
        ((unitCompPartialBijective B ⋯)
          (curry
            ((β_ B (i.obj ((reflector i).obj A))).inv ≫
              uncurry
                ((unitCompPartialBijective A ⋯)
                  (curry (((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B)) ≫ i.map f) ≫
                    (ihom B).map (i.map g)))))) =
    prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                  ((unitCompPartialBijective A ⋯)
                    (curry ((β_ A B).inv ≫ (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = (Hom.hom (MonoidalCategoryStruct.rightUnitor A).hom) (x ⊗ₜ[R] 1)

Tactic:
MonoidalCategory.rightUnitor_hom_apply,

Goal state after:
case e'_3
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ x = 1 • x
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 G : J ⥤ C
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limit F ⊗ limit G)).map f ≫ (limit.π F j' ⊗ₘ limit.π G j') =
    (limit.π F j ⊗ₘ limit.π G j) ≫ (F ⊗ G).map f

Tactic:
dsimp
                simp only [Category.id_comp, tensorHom_comp_tensorHom, limit.w]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (((λ_ (R.X ⊗ P.X)).inv ≫ 𝟙_ C ◁ P.actLeft) ≫ η ▷ 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 2 3 => rw [whisker_exchange]

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 ≫
      (η ▷ (R.X ⊗ P.X) ≫ 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) ≫
      𝟙 (coequalizer (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
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)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
have : (f.hom ≫ u.hom) ≫ (P _).ι.app _ = (g.hom ≫ u.hom) ≫ (P _).ι.app _ := by
      simp only [Category.assoc, Functor.const_obj_obj, ← u.w, ← f.w_assoc, ← g.w_assoc]
      rw [← Functor.map_comp, hu, IsFiltered.coeq_condition f.base g.base]
      simp

Goal state after:
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)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
this :
  (f.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app
        (Total.mk P (IsFiltered.coeq f.base g.base) a').snd =
    (g.hom ≫ u.hom) ≫
      (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).ι.app (Total.mk P (IsFiltered.coeq f.base g.base) a').snd
⊢ ∃ Z h, f ≫ h = g ≫ h
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
h✝ : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
X : C
h : P.ind.ind X
⊢ P.ind X

Tactic:
choose J Jc Jf pres K Kc Kf pres' hp using h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
h : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
X : C
J : Type w
Jc : SmallCategory J
Jf : IsFiltered J
pres : ColimitPresentation J X
K : J → Type w
Kc : (i : J) → SmallCategory (K i)
Kf : ∀ (i : J), IsFiltered (K i)
pres' : (i : J) → ColimitPresentation (K i) (pres.diag.obj i)
hp : ∀ (i : J) (i_1 : K i), P ((pres' i).diag.obj i_1)
⊢ P.ind X
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : ObjectProperty D
F : C ⥤ D
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v, u_2, u, u_1} F
⊢ (P.inverseImage F).ind ≤ P.ind.inverseImage F

Tactic:
by
  intro X ⟨J, _, _, pres, h⟩
  simp only [prop_inverseImage_iff]
  use J, inferInstance, inferInstance, pres.map F, h

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z T : C
hT : P T
e : Z ≅ T
u v : Y ⟶ Z
huv : (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) v
⊢ u = v

Tactic:
rw [← cancel_mono e.hom]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z T : C
hT : P T
e : Z ≅ T
u v : Y ⟶ Z
huv : (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) v
⊢ u ≫ e.hom = v ≫ e.hom
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: case refine_1
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 : localEpi (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f))
Z : D
u v : F.obj Y ⟶ Z
huv : F.map f ≫ u = F.map f ≫ v
⊢ (fun g ↦ G.map (F.map f) ≫ g) (G.map u) = (fun g ↦ G.map (F.map f) ≫ g) (G.map v)

Tactic:
simp [← Functor.map_comp, huv]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsNoetherianObject X ↔ ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
by
  dsimp only [IsNoetherianObject]
  rw [ObjectProperty.is_iff, isNoetherianObject,
    wellFoundedGT_iff_monotone_chain_condition]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
⊢ ObjectProperty.EssentiallySmall.{w, max v_1 v_2, max (max u_1 u_2) v_3} (comma F₁ F₂ P₁ P₂)

Tactic:
by
  obtain ⟨Q₁, _, h₁, h₁'⟩ := EssentiallySmall.exists_small_le.{w} P₁
  obtain ⟨Q₂, _, h₂, h₂'⟩ := EssentiallySmall.exists_small_le.{w} P₂
  refine ⟨comma F₁ F₂ Q₁ Q₂, inferInstance, fun f hf ↦ ?_⟩
  simp only [comma_iff] at hf
  obtain ⟨X₁, hX₁, ⟨e₁⟩⟩ := h₁' _ hf.1
  obtain ⟨X₂, hX₂, ⟨e₂⟩⟩ := h₂' _ hf.2
  exact ⟨Comma.mk _ _ (F₁.map e₁.inv ≫ f.hom ≫ F₂.map e₂.hom), by tauto,
    ⟨Comma.isoMk e₁ e₂⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
⊢ ∑ j,
      { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
              π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
              ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.π
          j ≫
        { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
              π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
              ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.ι
          j =
    𝟙
      { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
          π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
          ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.pt

Tactic:
dsimp
            ext1 ⟨i, j⟩
            rintro ⟨i', j'⟩
            rw [Finset.sum_apply, Finset.sum_apply]
            dsimp
            rw [Finset.sum_eq_single i]; rotate_left
            · intro b _ hb
              apply Finset.sum_eq_zero
              intro x _
              rw [dif_neg hb.symm, zero_comp]
            · intro hi
              simp at hi
            rw [Finset.sum_eq_single j]; rotate_left
            · intro b _ hb
              rw [dif_pos rfl, dif_neg, zero_comp]
              simp only
              tauto
            · intro hj
              simp at hj
            simp only [eqToHom_refl, dite_eq_ite, ite_true, Category.id_comp,
              Sigma.mk.inj_iff, id_def]
            by_cases h : i' = i
            · subst h
              rw [dif_pos rfl]
              simp only [heq_eq_eq, true_and]
              by_cases h : j' = j
              · subst h
                simp
              · rw [dif_neg h, dif_neg (Ne.symm h)]
            · rw [dif_neg h, dif_neg]
              tauto

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
m : (cocone hc).pt ⟶ s.pt
hm : ∀ (j : J), (cocone hc).ι.app j ≫ m = s.ι.app j
j : J
x : (F ⋙ forget PartOrdEmb).obj j
⊢ (Hom.hom m) ((ConcreteCategory.hom (c.ι.app j)) x) =
    (Hom.hom (ofHom (CoconePt.desc hc s))) ((ConcreteCategory.hom (c.ι.app j)) x)

Tactic:
exact ((ConcreteCategory.congr_hom (hm j)) x).trans (CoconePt.fac_apply hc s j x).symm

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤

Tactic:
let e := equivSmallModel.{w} P.FullSubcategory

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
e : P.FullSubcategory ≌ SmallModel.{w, v, u} P.FullSubcategory := equivSmallModel P.FullSubcategory
⊢ ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∀ (j_1 : J) (hj : (Diagram.single j).IsTerminal j_1), j_1 = j

Tactic:
rintro _ ⟨⟨⟩⟩

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j X Y : J
i✝ : Unit
lift✝ : {j_1 : J} → (Diagram.single j).P j_1 → (j_1 ⟶ j)
hlift✝ : ∀ {j_1 : J} (hj : (Diagram.single j).P j_1), (Diagram.single j).W (lift✝ hj)
uniq✝ : ∀ {j_1 : J} (hj : (Diagram.single j).P j_1) {φ : j_1 ⟶ j}, (Diagram.single j).W φ → lift✝ hj = φ
comm✝ : ∀ {i j_1 : J} (f : i ⟶ j_1) (hf : (Diagram.single j).W f), f ≫ lift✝ ⋯ = lift✝ ⋯
⊢ j = j
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

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

Tactic:
rintro B₁ B₂ f S ⟨α, _, X₁, π₁, rfl, hS⟩
    obtain ⟨β, _, X₂, π₂, h, i, ι, hh⟩ := Precoherent.pullback f α X₁ π₁ hS
    refine ⟨Presieve.ofArrows X₂ π₂, ⟨β, inferInstance, X₂, π₂, rfl, h⟩, ?_⟩
    rintro _ _ ⟨b⟩
    exact ⟨(X₁ (i b)), ι _, π₁ _, ⟨_⟩, hh _⟩

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
e : Y ≅ X
h : F.IsRepresentedBy ((ConcreteCategory.hom (F.map e.hom.op)) x)
this : x = (ConcreteCategory.hom (F.map e.inv.op)) ((ConcreteCategory.hom (F.map e.hom.op)) x)
⊢ F.IsRepresentedBy x

Tactic:
exact this ▸ .of_isoObj h e.symm

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

Goal state before:
pp: case refine_1
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
he : (D₂ D hι u).IsTerminal m :=
  have H := ⋯;
  Diagram.IsTerminal.ofExistsUnique ⋯ ⋯ ⋯ ⋯
D₂' : DiagramWithUniqueTerminal J κ :=
  let __Diagram := D₂ D hι u;
  { toDiagram := __Diagram, top := m, isTerminal := he, uniq_terminal := ⋯ }
i : ι
⊢ (D i).W ≤ D₂'.W

Tactic:
exact le_trans (le_trans (le_trans (by rfl) (le_iSup _ i)) le_sup_left) le_sup_left

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
⊢ ∀ (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
α

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
⊢ ∀ [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
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) [Finite α] (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
    EffectiveEpiFamily X_1 π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X_1 π)

Tactic:
α

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
W X : C
α : Type
⊢ ∀ [Finite α] (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
    EffectiveEpiFamily X_1 π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X_1 π)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
Y : C
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
right✝ : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate (Presieve.ofArrows Y' π)).arrows (π a')

Tactic:
exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩

Goal state after:
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)
a : ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α, ∃ (_ : Finite α), ∃ Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
      choose β _ Y_n π_n H using fun a => b (h₂ a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩

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

Goal state before:
pp: case refine_2
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 : D
⊢ EffectiveEpiFamily (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B

Tactic:
· rw [← effectiveEpi_iff_effectiveEpiFamily]
    infer_instance

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

Goal state before:
pp: case mpr
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✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ (∀ ⦃X : C⦄,
      ∀ R ∈ (regularCoverage C).coverings X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))) →
    EqualizerCondition F

Tactic:
intro hF Y X f _
    exact (equalizerConditionMap_iff_nonempty_isLimit F f).2 (hF _ ⟨_, f, rfl, inferInstance⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.GlobalSections

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝³ : Category.{v₂, u₂} A
inst✝² : HasWeakSheafify J A
inst✝¹ : HasWeakSheafify J (Type w)
inst✝ : HasGlobalSectionsFunctor J (Type w)
F : Sheaf J (Type w)
⊢ (Γ J (Type w)).obj F ≃ (PUnit.{w + 1} ⟶ (Γ J (Type w)).obj F)

Tactic:
exact (Equiv.funUnique (PUnit) _).symm.trans TypeCat.homEquiv.symm

Goal state after:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ.ev i j a b * γ.ev j i b a = (γ.ev j i b a)⁻¹ * γ.ev j i b a

Tactic:
γ.ev_trans i j i a b a,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ.ev i i a a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ.ev i i a a = (γ.ev j i b a)⁻¹ * γ.ev j i b a

Tactic:
ev_refl,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ 1 = (γ.ev j i b a)⁻¹ * γ.ev j i b a