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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
refine ⟨∐ gZ, Sigma.desc gf, t.symm ≪≫ u' ≪≫ is2.symm, ?_, by simp [heq]⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ Mono (Sigma.desc gf)
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
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
A : Set (Aut F)
hA : A ∈ nhds 1
⊢ ⇑(toAut F G) ⁻¹' A ∈ nhds 1

Tactic:
obtain ⟨X, _, hX⟩ := ((nhds_one_has_basis_stabilizers F).mem_iff' A).mp hA

Goal state after:
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
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
A : Set (Aut F)
hA : A ∈ nhds 1
X : PointedGaloisObject F
left✝ : True
hX : ↑(MulAction.stabilizer (Aut F) X.pt) ⊆ A
⊢ ⇑(toAut F G) ⁻¹' A ∈ nhds 1
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d : ↑S.objs
p : c ⟶ d
⊢ ↑(inv p) = inv ↑p

Tactic:
by
  simp only [← inv_eq_inv, coe_inv_coe]

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
s t : ↑S.objs
x✝¹ x✝ : s ⟶ t
f : ↑s ⟶ ↑t
hf : f ∈ S.arrows ↑s ↑t
g : ↑s ⟶ ↑t
hg : g ∈ S.arrows ↑s ↑t
⊢ f = g → f = g

Tactic:
exact id

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

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map p✝ ≫ φ.map q✝ ∈ S.arrows (φ.obj c✝) (φ.obj e✝)

Tactic:
apply S.mul

Goal state after:
case a
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map p✝ ∈ S.arrows (φ.obj c✝) (φ.obj d✝)

case a
C : Type u
inst✝¹ : Groupoid C
S✝ : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
c✝ d✝ e✝ : C
p✝ : c✝ ⟶ d✝
a✝¹ : p✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj c✝) (φ.obj d✝)}
q✝ : d✝ ⟶ e✝
a✝ : q✝ ∈ {f | φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj e✝)}
⊢ φ.map q✝ ∈ S.arrows (φ.obj d✝) (φ.obj e✝)
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ P.complement.decompId_i ≫ P.decompId_p = 0

Tactic:
simp only [zero_def, hom_ext_iff, complement_X, comp_f,
          decompId_i_f, complement_p, decompId_p_f, sub_comp, id_comp, idem, sub_self]

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 (Arrow.mk (i.to B) □ Arrow.mk g).hom h ↔ HasLiftingProperty g ((ihom B).map h)

Tactic:
by
  dsimp
  have := HasLiftingProperty.iff_of_arrow_iso_left (isInitialIso' g i (W := B)) h
  rw [dsimp% this]
  exact Adjunction.hasLiftingProperty_iff (ihom.adjunction B) g h

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : HasPullbacks C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
A B K L X Y : C
f : A ⟶ B
g : K ⟶ L
t : IsTerminal Y
⊢ HasLiftingProperty (Arrow.mk f □ Arrow.mk g).hom (t.from X) ↔ HasLiftingProperty g ((MonoidalClosed.pre f).app X)

Tactic:
rw [hasLiftingProperty_mk_iff]
  exact HasLiftingProperty.iff_of_arrow_iso_right g (PullbackHom.isTerminalIso _ t)

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
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F : C ⥤ A
s : Cocone (Discrete.functor f ⋙ (eval C A).obj F)
i✝ : Discrete J
i : ((Discrete.functor f).obj i✝).I
⊢ (Sigma.ι (fun i ↦ F.obj (((Discrete.functor f).obj i✝).obj i)) i ≫
      (((eval C A).obj F).mapCocone (cofan J f)).ι.app i✝ ≫
        Sigma.desc fun i ↦ Sigma.ι (F.obj ∘ (f i.fst).obj) i.snd ≫ s.ι.app { as := i.fst }) =
    Sigma.ι (fun i ↦ F.obj (((Discrete.functor f).obj i✝).obj i)) i ≫ s.ι.app i✝

Tactic:
by simp [cofan, Function.comp_def]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
⊢ ∀ (a b_1 : h.LiftStruct g₁ g₂ b), a = b_1

Tactic:
rintro ⟨f, f_p₁, f_p₂, _⟩ ⟨f', f'_p₁, f'_p₂, _⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
f : Y ⟶ h.pullback
f_p₁ : f ≫ h.p₁ = g₁
f_p₂ : f ≫ h.p₂ = g₂
f_p✝¹ : f ≫ h.p = b
f' : Y ⟶ h.pullback
f'_p₁ : f' ≫ h.p₁ = g₁
f'_p₂ : f' ≫ h.p₂ = g₂
f_p✝ : f' ≫ h.p = b
⊢ { f := f, f_p₁ := f_p₁, f_p₂ := f_p₂, f_p := f_p✝¹ } = { f := f', f_p₁ := f'_p₁, f_p₂ := f'_p₂, f_p := f_p✝ }
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
j j' : J
f : j ⟶ j'
⊢ (F.map f.op).app j ≫ ι F j = (F.obj (op j')).map f ≫ ι F j'

Tactic:
ext
  apply Quot.sound
  apply coendRel.mk

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: J✝ : Type u
inst✝¹ : Category.{v, u} J✝
F✝ : J✝ᵒᵖ ⥤ J✝ ⥤ Type (max w u)
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cone (multicospanIndexEnd F).multicospan
m : s.pt ⟶ (wedge F).pt
h : ∀ (j : WalkingMulticospan (multicospanShapeEnd J)), m ≫ (wedge F).π.app j = s.π.app j
⊢ m = ↾fun x ↦ ⟨fun j ↦ (hom (Multifork.ι s j)) x, ⋯⟩

Tactic:
ext x
    apply Subtype.ext
    funext j
    exact ConcreteCategory.congr_hom (h (.left j)) x

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

Goal state before:
pp: case h_option.refine_1
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {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 : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
X₁ : C none
X₂ : (i : J) → C (some i)
⊢ ∀ ⦃Y : C none × ((i : J) → C (some i))⦄ (f : (X₁, X₂) ⟶ Y),
    (W none).prod (MorphismProperty.pi fun j ↦ W (some j)) f →
      (MorphismProperty.pi W).isoClosure.inverseImage (Pi.optionEquivalence C).symm.functor f

Tactic:
⟨Y₁, Y₂⟩

Goal state after:
case h_option.refine_1
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {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 : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
X₁ : C none
X₂ : (i : J) → C (some i)
Y₁ : C none
Y₂ : (i : J) → C (some i)
⊢ ∀ (f : (X₁, X₂) ⟶ (Y₁, Y₂)),
    (W none).prod (MorphismProperty.pi fun j ↦ W (some j)) f →
      (MorphismProperty.pi W).isoClosure.inverseImage (Pi.optionEquivalence C).symm.functor f
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
f : X ⟶ Y
⊢ 𝟙_ (Arrow C) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)
  apply (initialIsInitial.ofIso (mulZero initialIsInitial).symm).hom_ext

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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (α_ (𝟙_ C) P.X Q.X).inv ≫
      (λ_ P.X).hom ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom

Tactic:
slice_rhs 1 2 => rw [leftUnitor_naturality]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (α_ (𝟙_ C) P.X Q.X).inv ≫
      (λ_ P.X).hom ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (λ_ (P.X ⊗ Q.X)).hom ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
⊢ R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c

Tactic:
refine ⟨fun h _ a b c ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
⊢ a * (b + c) = a * b + a * c

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c
⊢ R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ ↔ ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c

Tactic:
refine ⟨fun h _ a b c ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
⊢ (a + b) * c = a * c + b * c

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ⊗ₘ (ihom (F.obj X)).map (G.map f) ≫ (pre (CategoryTheory.inv (F.map f))).app (G.obj Y)) ≫
      (ihom.ev (F.obj Y)).app (G.obj Y) =
    (ihom.ev (F.obj X)).app (G.obj X) ≫ G.map f

Tactic:
rw [tensorHom_def]

Goal state after:
D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ▷ (ihom (F.obj X)).obj (G.obj X) ≫
        F.obj Y ◁ ((ihom (F.obj X)).map (G.map f) ≫ (pre (CategoryTheory.inv (F.map f))).app (G.obj Y))) ≫
      (ihom.ev (F.obj Y)).app (G.obj Y) =
    (ihom.ev (F.obj X)).app (G.obj X) ≫ G.map 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
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫ M.X ◁ f.hom =
    (M.X ⊗ Y.X) ◁ f.hom ≫ (α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft

Tactic:
by
          simp only [Category.assoc, tensor_whiskerLeft, Iso.inv_hom_id_assoc,
            Iso.cancel_iso_hom_left]
          slice_lhs 1 2 => rw [← whiskerLeft_comp, Hom.left_act_hom]
          simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ X.X M.X N₁.X).inv ≫
      M.actLeft ▷ N₁.X ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one =
    X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫
      X.X ◁
          colimMap
            (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
              ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ≫
        TensorBimod.actLeft M N₂

Tactic:
slice_rhs 1 2 => rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one,
      whiskerLeft_comp]

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 : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ X.X M.X N₁.X).inv ≫
      M.actLeft ▷ N₁.X ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one =
    (X.X ◁ M.X ◁ f.hom ≫
        X.X ◁
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one) ≫
      TensorBimod.actLeft M N₂
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)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
rw [tensorHom_def]

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 ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫
                (α_ (A ⊗ A) A A).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
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
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
let a := IsFiltered.coeq f.base g.base

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
⊢ ∃ Z h, f ≫ h = g ≫ h
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
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

Tactic:
obtain ⟨j, p, q, hpq⟩ := IsFinitelyPresentable.exists_eq_of_isColimit (P _).isColimit _ _ this

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
j : I (Total.mk P (IsFiltered.coeq f.base g.base) a').fst
p q : (Total.mk P (IsFiltered.coeq f.base g.base) a').snd ⟶ j
hpq :
  (f.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map p =
    (g.hom ≫ u.hom) ≫ (P (Total.mk P (IsFiltered.coeq f.base g.base) a').fst).diag.map q
⊢ ∃ Z h, f ≫ h = g ≫ h