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

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ (ConcreteCategory.hom
        ((Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).ρ σ))
      ⟦τ⟧ =
    (ConcreteCategory.hom
        (𝟙 (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V))
      ⟦τ⟧

Tactic:
| _ τ
       => 

Goal state after:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
V : OpenSubgroup (Aut F)
I : Set C
hf : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hi : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ ↑V
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
hn : Nonempty (F.obj (∏ᶜ fun X ↦ ↑X)).obj
A : C
f : A ⟶ ∏ᶜ fun X ↦ ↑X
hgal : IsGalois A
a : (F.obj A).obj
U : OpenSubgroup (Aut F) := { toSubgroup := MulAction.stabilizer (Aut F) a, isOpen' := ⋯ }
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) :=
  fiberIsoQuotientStabilizer A a
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ (ConcreteCategory.hom
        ((Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).ρ σ))
      ⟦τ⟧ =
    (ConcreteCategory.hom
        (𝟙 (Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a))).V))
      ⟦τ⟧
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
⊢ (∃ (h : c = d), f = eqToHom h) → f ∈ discrete.arrows c d

Tactic:
by rintro ⟨rfl, rfl⟩; constructor

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsWide → S.objs = univ

Tactic:
rintro h
    ext x; constructor <;> simp only [mem_univ, imp_true_iff, forall_true_left]
    apply mem_objs_of_src S (h.wide x)

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

Goal state before:
pp: case refl.refl.refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Groupoid.inv f ≫ γ ≫ f ∈ S.arrows c' c'

Tactic:
apply Sn.conj f γS

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial A
⊢ HasLiftingProperty (pushout.desc (B ◁ g) (i.to B ▷ L) ⋯) h ↔ HasLiftingProperty g ((ihom B).map h)

Tactic:
have := HasLiftingProperty.iff_of_arrow_iso_left (isInitialIso' g i (W := B)) h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
A B K L X Y : C
g : K ⟶ L
h : X ⟶ Y
i : IsInitial A
this :
  HasLiftingProperty (ofHasPushout (curriedTensor C) (Arrow.mk (i.to B)).hom (Arrow.mk g).hom).ι h ↔
    HasLiftingProperty (B ◁ (Arrow.mk g).hom) h
⊢ HasLiftingProperty (pushout.desc (B ◁ g) (i.to B ▷ L) ⋯) h ↔ HasLiftingProperty g ((ihom B).map h)
Module: Mathlib.CategoryTheory.Limits.Final.ParallelPair

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), Zigzag (mk i) (mk j)
Z : C
this✝ : Nonempty (CostructuredArrow (parallelPair f g) Z)
this : ∀ (x : CostructuredArrow (parallelPair f g) Z), Zigzag x (mk ⋯.some)
⊢ IsConnected (CostructuredArrow (parallelPair f g) Z)

Tactic:
exact zigzag_isConnected (fun x y => (this x).trans (this y).symm)

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
i : { I := Function.Pullback f.f g.f, obj := fun i ↦ (pb i).pt }.I
⊢ ({ f := fun i ↦ (↑i).1, φ := fun i ↦ (pb i).fst } ≫ f).φ i ≫ eqToHom ⋯ =
    ({ f := fun i ↦ (↑i).2, φ := fun i ↦ (pb i).snd } ≫ g).φ i

Tactic:
simp [(pb i).condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: case neg
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
n m✝ k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  (Functor.ofOpSequence (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun m ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
h✝ : ¬k < m
⊢ (Pi.map fun m_1 ↦
        if h : m_1 < m then eqToHom ⋯ else if h_1 : m_1 < m + 1 then eqToHom ⋯ ≫ f m_1 ≫ eqToHom ⋯ else eqToHom ⋯) ≫
      Pi.π (fun i ↦ if i < m then M i else N i) k ≫ eqToHom ⋯ =
    Pi.π (fun i ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯

Tactic:
simp [dif_neg (by lia : ¬(k < m)), dif_neg hh]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits

Goal state before:
pp: J : Type u_1
C : Type u_3
K : Type u_5
inst✝² : Category.{v_1, u_5} K
inst✝¹ : Category.{v_3, u_1} J
inst✝ : Category.{v_5, u_3} C
⊢ preservesColimitsOfShape K = ⨅ F, preservesColimit F

Tactic:
ext G
  simp only [preservesColimitsOfShape_iff, iInf_apply, preservesColimit_iff, iInf_Prop_eq]
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨inferInstance⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
⊢ φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ.right.obj x) ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map (α.base.app (G.obj x)) ≫
      φ.base.map ((CatCommSq.iso G ψ'.right ψ'.base G').hom.app x) ≫
        (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ'.right.obj x)

Tactic:
rw [← Functor.map_comp_assoc, ← right_coherence_app, Functor.map_comp_assoc]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁸ : Category.{v₁, u₁} A
inst✝⁷ : Category.{v₂, u₂} B
inst✝⁶ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁵ : Category.{v₄, u₄} A'
inst✝⁴ : Category.{v₅, u₅} B'
inst✝³ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝² : Category.{v₇, u₇} A''
inst✝¹ : Category.{v₈, u₈} B''
inst✝ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
⊢ φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ.right.obj x) ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      φ.base.map (G'.map (α.right.app x)) ≫ (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ'.right.obj x)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f = g

Tactic:
apply Hom.ext <;> assumption

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
I : C
inst✝ : Closed I
A : C
⊢ uncurry (toUnit A ≫ curryRightUnitorHom I) = uncurry (curry (fst I A))

Tactic:
simp [uncurry_natural_left, curryRightUnitorHom, fst_def, toUnit]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ ((forgetAdjToOver X).homEquiv Z A).symm f = Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X

Tactic:
rw [Adjunction.homEquiv_counit, forgetAdjToOver_counit_app]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B B' : D
g : B ⟶ B'
h : comparisonLeftAdjointObj adj A ⟶ B
⊢ (comparisonLeftAdjointHomEquiv adj A B') (h ≫ g) = (comparisonLeftAdjointHomEquiv adj A B) h ≫ (comparison adj).map g

Tactic:
ext1

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B B' : D
g : B ⟶ B'
h : comparisonLeftAdjointObj adj A ⟶ B
⊢ ((comparisonLeftAdjointHomEquiv adj A B') (h ≫ g)).f =
    ((comparisonLeftAdjointHomEquiv adj A B) h ≫ (comparison adj).map g).f
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
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight

Tactic:
by
        rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ uncurry (uncurry (ihomCurry x y z)) = (α_ x y ((ihom (x ⊗ y)).obj z)).inv ≫ (ihom.ev (x ⊗ y)).app z

Tactic:
simp [uncurry_ihomCurry]

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

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ihom (F.obj j')).map (f.app (j' ⊗ c)) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
⊢ ℌ.π c j ≫ (ihom (F.obj j)).map (f.app (j ⊗ c) ≫ G'.map (φ ▷ c)) =
    (ℌ.π c j' ≫ (ihom (F.obj j')).map (f.app (j' ⊗ c))) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))

Tactic:
← f.naturality,

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ihom (F.obj j')).map (f.app (j' ⊗ c)) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
⊢ ℌ.π c j ≫ (ihom (F.obj j)).map (G.map (φ ▷ c) ≫ f.app (j' ⊗ c)) =
    (ℌ.π c j' ≫ (ihom (F.obj j')).map (f.app (j' ⊗ c))) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor

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
hasDayConvolution : ∀ (F G : C ⥤ V), (tensor C).HasPointwiseLeftKanExtension (F ⊠ G)
hasDayConvolutionUnit : (Functor.fromPUnit (𝟙_ C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (𝟙_ V))
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)
F : C ⊛⥤ V
α β : 𝟙_ (C ⊛⥤ V) ⟶ F
h : ν C V ≫ α.natTrans.app (𝟙_ C) = ν C V ≫ β.natTrans.app (𝟙_ C)
⊢ α = β

Tactic:
ext1

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
hasDayConvolution : ∀ (F G : C ⥤ V), (tensor C).HasPointwiseLeftKanExtension (F ⊠ G)
hasDayConvolutionUnit : (Functor.fromPUnit (𝟙_ C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (𝟙_ V))
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)
F : C ⊛⥤ V
α β : 𝟙_ (C ⊛⥤ V) ⟶ F
h : ν C V ≫ α.natTrans.app (𝟙_ C) = ν C V ≫ β.natTrans.app (𝟙_ C)
⊢ α.natTrans = β.natTrans
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
⊢ inv P ≫ hom P = 𝟙 P.X

Tactic:
dsimp [hom, inv]

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
⊢ ((λ_ P.X).inv ≫
        η ▷ P.X ≫
          coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft)) ≫
      coequalizer.desc P.actLeft ⋯ =
    𝟙 P.X
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
⊢ inv P ≫ hom P = 𝟙 P.X

Tactic:
dsimp [hom, inv]

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
⊢ ((ρ_ P.X).inv ≫
        P.X ◁ η ≫
          coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft)) ≫
      coequalizer.desc P.actRight ⋯ =
    𝟙 P.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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (((α_ (𝟙_ C) X.X N.X).inv ≫ η ▷ X.X ▷ N.X) ≫ μ ▷ N.X) ≫
          coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

Tactic:
slice_rhs 4 5 => rw [← comp_whiskerRight, MonObj.one_mul]

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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X ≫ coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
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
this : IsFiltered (CostructuredArrow P.ι X)
hc : P.ι.DenseAt X
⊢ P.ind X

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

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)
hc : P.ι.DenseAt X
this : EssentiallySmall.{w, v, max u v} (CostructuredArrow P.ι X)
⊢ P.ind X
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of_iso
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
U : C
v : U ⟶ X'✝
i : (Precoverage.ZeroHypercover.pushforward (Arrow.Hom.left e.hom) ⋯ E).I₀
⊢ P (E.f i ≫ f)

Tactic:
exact h _ _ ⟨i⟩

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

Goal state before:
pp: case refine_1.comp.refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
U✝ : C
g : U✝ ⟶ X✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → P (g ≫ f)
F : K.ZeroHypercover X✝
hg : Presieve.ofArrows F.X F.f g
U : C
v : U ⟶ U✝
i : (Precoverage.ZeroHypercover.pullback₁ g E).I₀
⊢ P (E.f i ≫ f)

Tactic:
exact h _ _ ⟨i⟩

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

Goal state before:
pp: case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih : ∀ (U : C) (g : U ⟶ X✝), R g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)

Tactic:
rw [K.mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      choose S hS h' using fun i : E.I₀ ↦ ih _ _ ⟨i⟩
      simp_rw [K.mem_iff_exists_zeroHypercover] at hS
      choose F hF using hS
      refine ⟨_, (E.bind F).mem₀, fun U g ⟨j⟩ ↦ ?_⟩
      dsimp
      rw [Category.assoc]
      exact h' _ _ _ (by simp [hF])

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

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

Tactic:
dsimp only [IsArtinianObject]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ isArtinianObject.Is X ↔ ∀ (f : ℕ →o (Subobject X)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictAnti f
⊢ IsArtinianObject X

Tactic:
dsimp only [IsArtinianObject]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictAnti f
⊢ isArtinianObject.Is X
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ MonoOver X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      (G ⋙ (Subobject.equivMonoOver X).inverse).toOrderHom n = (G ⋙ (Subobject.equivMonoOver X).inverse).toOrderHom m
m : ℕ
hm : n ⟶ m
⊢ IsIso (G.map hm)

Tactic:
rw [MonoOver.isIso_iff_subobjectMk_eq]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ MonoOver X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      (G ⋙ (Subobject.equivMonoOver X).inverse).toOrderHom n = (G ⋙ (Subobject.equivMonoOver X).inverse).toOrderHom m
m : ℕ
hm : n ⟶ m
⊢ Subobject.mk (G.obj n).obj.hom = Subobject.mk (G.obj m).obj.hom