mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : IsNaturalSMul F G
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i ↦ F.obj (X i)).obj ≃ ((i : ι) → (F.obj (X i)).obj) := FintypeCat.productEquiv fun i ↦ F.obj (X i)
px : (F.obj P).obj := (ConcreteCategory.hom is₁.inv) (is₂.symm x)
hpx : ∀ (i : ι), (ConcreteCategory.hom (F.map (Pi.π X i))) px = x i
A : C
f : A ⟶ P
a : (F.obj A).obj
left✝ : IsGalois A
hfa : (ConcreteCategory.hom (F.map f)) a = px
g : G
hg : ∀ (x : (F.obj A).obj), g • x = (ConcreteCategory.hom (t.hom.app A)) x
i : ι
y : (F.obj (X i)).obj
⊢ g • x i = (ConcreteCategory.hom (t.hom.app (X i))) (x i)

Tactic:
rw [← hpx i, ← IsNaturalSMul.naturality, FunctorToFintypeCat.naturality,
    ← hfa, FunctorToFintypeCat.naturality, ← IsNaturalSMul.naturality, hg]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
⊢ Φ.toPrefunctor.map ((Quotient.functor redStep).toPrefunctor.map (reverse f).toPath) =
    reverse (Φ.toPrefunctor.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))

Tactic:
change Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
      Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))

Goal state after:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
⊢ Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))

Tactic:
convert! this

Goal state after:
case e'_2
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath) =
    inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)

case e'_3
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
X Y : Symmetrify V
f : X ⟶ Y
this :
  Φ.map (inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
⊢ Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
    inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ IsColimit (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone)

Tactic:
by
    refine IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_ (BinaryBiproduct.isColimit (F.obj d) (G.obj d))
    · exact (pairComp F G ((evaluation D C).obj d)).symm
    · exact Cocone.ext (Iso.refl _) <| by rintro (_ | _ | _) <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
m : T ⟶ (pullbackCone f g pb).pt
i : T.I
⊢ ((fun s ↦
              { f := fun i ↦ ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩,
                φ := fun i ↦ (hpb ⟨((↑s).1.f i, (↑s).2.f i), ⋯⟩).lift (PullbackCone.mk ((↑s).1.φ i) ((↑s).2.φ i) ⋯) })
            ((fun m ↦ ⟨(m ≫ (pullbackCone f g pb).fst, m ≫ (pullbackCone f g pb).snd), ⋯⟩) m)).φ
        i ≫
      eqToHom ⋯ =
    m.φ i

Tactic:
simp only [eqToHom_refl, Category.comp_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
m : T ⟶ (pullbackCone f g pb).pt
i : T.I
⊢ (hpb ⟨((m ≫ (pullbackCone f g pb).fst).f i, (m ≫ (pullbackCone f g pb).snd).f i), ⋯⟩).lift
      (PullbackCone.mk ((m ≫ (pullbackCone f g pb).fst).φ i) ((m ≫ (pullbackCone f g pb).snd).φ i) ⋯) =
    m.φ i
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ (b ≫ h₂₃.p₁) ≫ f₂ = (a ≫ h₁₃.p₁) ≫ f₁

Tactic:
by simpa using w.symm =≫ f₃

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝ : C
a : x✝ ⟶ h₁₃.pullback
b : x✝ ⟶ h₂₃.pullback
w : a ≫ h₁₃.p₂ = b ≫ h₂₃.p₂
⊢ ∃ l, l ≫ h.p₁₃ = a ∧ l ≫ h.p₂₃ = b

Tactic:
obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ :=
        h.exists_lift (a ≫ h₁₃.p₁) (b ≫ h₂₃.p₁) (a ≫ h₁₃.p₂) _ rfl
          (by simpa using w.symm =≫ f₃) (by simp)
      exact ⟨φ, by cat_disch, by cat_disch⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case of_equiv
J₁ J₂ : Type w
⊢ ∀ (a : J₁ ≃ J₂),
    (∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
        [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
        (Functor.pi L).IsLocalization (MorphismProperty.pi W)) →
      ∀ {C : J₂ → Type u₁} {D : J₂ → Type u₂} [inst : (j : J₂) → Category.{v₁, u₁} (C j)]
        [inst_1 : (j : J₂) → Category.{v₂, u₂} (D j)] (L : (j : J₂) → C j ⥤ D j) (W : (j : J₂) → MorphismProperty (C j))
        [∀ (j : J₂), (W j).ContainsIdentities] [∀ (j : J₂), (L j).IsLocalization (W j)],
        (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
e

Goal state after:
case of_equiv
J₁ J₂ : Type w
e : J₁ ≃ J₂
⊢ (∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
      [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
      [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
      (Functor.pi L).IsLocalization (MorphismProperty.pi W)) →
    ∀ {C : J₂ → Type u₁} {D : J₂ → Type u₂} [inst : (j : J₂) → Category.{v₁, u₁} (C j)]
      [inst_1 : (j : J₂) → Category.{v₂, u₂} (D j)] (L : (j : J₂) → C j ⥤ D j) (W : (j : J₂) → MorphismProperty (C j))
      [∀ (j : J₂), (W j).ContainsIdentities] [∀ (j : J₂), (L j).IsLocalization (W j)],
      (Functor.pi L).IsLocalization (MorphismProperty.pi W)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X A A' : C
f : A ⟶ A'
⊢ (toOver X).map f = Over.homMk (f ▷ X) ⋯

Tactic:
simp [toOver]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
c₁ c₂ c₃ : Cᴹᵒᵖ
d : D
⊢ (α_ c₁ c₂ c₃).hom.unmop ⊵ₗ d ≫ (αₗ (c₂ ⊗ c₃).unmop c₁.unmop d).hom ≫ (αₗ c₃.unmop c₂.unmop (c₁.unmop ⊙ₗ d)).hom =
    (αₗ c₃.unmop (c₁ ⊗ c₂).unmop d).hom ≫ c₃.unmop ⊴ₗ (αₗ c₂.unmop c₁.unmop d).hom

Tactic:
by
    simpa only [mop_tensorObj, mop_hom_associator,
      MonoidalLeftAction.inv_hom_actionHomLeft_assoc] using!
      (α_ (unmop c₃) (unmop c₂) (unmop c₁)).inv ⊵ₗ d ≫=
        MonoidalLeftAction.associator_actionHom
          (unmop c₃) (unmop c₂) (unmop c₁) d |>.symm

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      F.map (prodComparison L (F.obj A) (F.obj B)) ≫
        F.map (h.counit.app A ▷ L.obj (F.obj B)) ≫
          prodComparison F A (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (F.obj A ⊗ F.obj B)

Tactic:
prodComparison_natural_whiskerRight_assoc

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      F.map (prodComparison L (F.obj A) (F.obj B)) ≫
        prodComparison F (L.obj (F.obj A)) (L.obj (F.obj B)) ≫
          F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (F.obj A ⊗ F.obj B)
Module: Mathlib.CategoryTheory.Monoidal.Conv

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
M N : C
inst✝¹ : ComonObj M
inst✝ : MonObj N
f g h : Conv M N
⊢ f * g * h = f * (g * h)

Tactic:
simp only [mul_eq]
    simp only [comp_whiskerRight, whisker_assoc, Category.assoc,
      MonoidalCategory.whiskerLeft_comp]
    slice_lhs 7 8 =>
      rw [← whisker_exchange]
    slice_rhs 2 3 =>
      rw [← whisker_exchange]
    simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫ (A ◁ 𝒮) ▷ A ≫ (A ⊗ A) ◁ ε ≫ μ ▷ 𝟙_ C ≫ (ρ_ A).hom = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
slice_lhs 3 4 =>
    rw [whisker_exchange]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫ (A ◁ 𝒮) ▷ A ≫ (μ ▷ A ≫ A ◁ ε) ≫ (ρ_ A).hom = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
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
R S : Mon C
P : Bimod R S
⊢ (regular R).actRight ▷ P.X ≫ P.actLeft = ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) ≫ P.actLeft

Tactic:
dsimp; rw [Category.assoc, left_assoc]

Goal state after:
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✝
⊢ A.map f ≫ Δ = Δ ≫ (A.map f ⊗ₘ A.map f)

Tactic:
dsimp; rw [Δ[A].naturality, tensorObj_map]

Goal state after:
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).map f) (𝟙 ((ι C V D).obj (𝟙_ D))) ≫ (ι C V D).map (ρ_ Y✝).hom =
    (ι C V D).map (ρ_ X✝).hom ≫ (ι C V D).map f

Tactic:
ι_map_rightUnitor_hom_eq_rightUnitor_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).map f) (𝟙 ((ι C V D).obj (𝟙_ D))) ≫
      (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj Y✝)).hom =
    (ι C V D).map (ρ_ X✝).hom ≫ (ι C V D).map f
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:
← 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.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Coalgebra F
α β : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (α.f + β.f) = (α.f + β.f) ≫ A₂.str

Tactic:
simp only [Functor.map_add, comp_add, Endofunctor.Coalgebra.Hom.h, add_comp]

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
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ j,
        (fun x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
          if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0)
      ⟨i, j⟩ ⟨i', j'⟩ =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩

Tactic:
rw [Finset.sum_apply, Finset.sum_apply]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∑ c,
      ((fun x y ↦ if h : x.fst = c then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
          if h : y.fst = c then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0)
        ⟨i, j⟩ ⟨i', j'⟩ =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case pos
κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
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
B : Set X
hB : HasCardinalLT (↑B) κ₂
⊢ B ⊆ φ₀ Y m B hB

Tactic:
intro b hb

Goal state after:
case pos
κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
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
B : Set X
hB : HasCardinalLT (↑B) κ₂
b : X
hb : b ∈ B
⊢ b ∈ φ₀ Y m B hB
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
i✝ : Unit
⊢ ∃ e, S.arrows e ∧ 𝟙 Y ≫ e = π

Tactic:
exact ⟨π, ⟨h.2, Category.id_comp π⟩⟩

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

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ PreservesColimit G (sheafToPresheaf (extensiveTopology C) A)

Tactic:
suffices CreatesColimit G (sheafToPresheaf (extensiveTopology C) A) from inferInstance
    refine createsColimitOfIsSheaf _ (fun c hc ↦ ?_)
    let i : c.pt ≅ (G ⋙ sheafToPresheaf _ _).flip ⋙ colim :=
      hc.coconePointUniqueUpToIso (pointwiseIsColimit _)
    rw [Presheaf.isSheaf_of_iso_iff i]
    exact isSheaf_pointwiseColimit _

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
⊢ ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y

Tactic:
intro b hb

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
⊢ ∃! x, (ConcreteCategory.hom (P.map π.op)) x = b
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀
    (b :
      (fun X ↦ X)
        ↑{x |
            (ConcreteCategory.hom (P.map (pullback.fst π π).op)) x =
              (ConcreteCategory.hom (P.map (pullback.snd π π).op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = b
⊢ ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y

Tactic:
intro b hb

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀
    (b :
      (fun X ↦ X)
        ↑{x |
            (ConcreteCategory.hom (P.map (pullback.fst π π).op)) x =
              (ConcreteCategory.hom (P.map (pullback.snd π π).op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = b
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
⊢ ∃! x, (ConcreteCategory.hom (P.map π.op)) x = b
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
h : Presheaf.IsLocallySurjective (coherentTopology C) f
U✝ : C
y : ToType (G.obj (op U✝))
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝

Tactic:
replace h := h.1 y

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
h : Presheaf.imageSieve f y ∈ (coherentTopology C) U✝
⊢ Presheaf.imageSieve f y ∈ (regularTopology C) U✝