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
⊢ NatIso.ofComponents (isoOnObj F 1) ⋯ = 1

Tactic:
by
    ext
    dsimp [isoOnObj]
    cat_disch

Goal state after:
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
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
σ : ↥↑V
μ : Aut F
⊢ ⟦μ * ↑σ⁻¹⟧ = ⟦μ⟧

Tactic:
apply Quotient.sound

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
σ : ↥↑V
μ : Aut F
⊢ μ * ↑σ⁻¹ ≈ μ
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
⊢ ⟦σ * τ⟧ = ⟦τ⟧

Tactic:
apply Quotient.sound

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) := ⋯
u : (functorToAction F).obj A ≅
  Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (Aut F) a)) := ⋯
hUnormal : (↑U).Normal
σ : Aut F
σinU : σ ∈ U
τ : Aut F
⊢ σ * τ ≈ τ
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : j = j'
⊢ { f := biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p, comm := ⋯ } ≫
      { f := (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j', comm := ⋯ } =
    eqToHom ⋯

Tactic:
subst h

Goal state after:
case pos
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ { f := biproduct.ι (fun j ↦ (F j).X) j ≫ biproduct.map fun j ↦ (F j).p, comm := ⋯ } ≫
      { f := (biproduct.map fun j ↦ (F j).p) ≫ (biproduct.bicone fun j ↦ (F j).X).π j, comm := ⋯ } =
    eqToHom ⋯
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ 𝟭 C = e.functor ⋙ (f.functor ⋙ f.inverse) ⋙ e.inverse

Tactic:
← f.unit_eq,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ 𝟭 C = e.functor ⋙ 𝟭 D ⋙ e.inverse
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ (f.inverse ⋙ e.inverse) ⋙ e.functor ⋙ f.functor = 𝟭 E

Tactic:
by
    rw [Functor.assoc, ← Functor.assoc e.inverse, e.counit_eq, Functor.id_comp]
    exact f.counit_eq

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

Goal state before:
pp: case 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
g : φ.obj c ⟶ φ.obj c'
this : ∃ a b g_1, ∃ (ha : φ.obj a = φ.obj c) (hb : φ.obj b = φ.obj c'), g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows (φ.obj c') (φ.obj c')

Tactic:
obtain ⟨b, b', f, hb, hb', _, hf⟩ := this

Goal state after:
case 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' b b' : C
f : b ⟶ b'
hb : φ.obj b = φ.obj c
hb' : φ.obj b' = φ.obj c'
⊢ Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb' ∈
    (map φ hφ S).arrows (φ.obj c') (φ.obj c')
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → c = d

Tactic:
by
  constructor
  · rintro h c d ⟨f, fS⟩
    exact congr_arg Subtype.val <| h ⟨c, mem_objs_of_src S fS⟩ ⟨d, mem_objs_of_tgt S fS⟩ ⟨f, fS⟩
  · rintro h ⟨c, hc⟩ ⟨d, hd⟩ ⟨f, fS⟩
    simp only [Subtype.mk_eq_mk]
    exact h c d ⟨f, fS⟩

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
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty X.hom (Opposite.op Y ⋔ Z).hom

Tactic:
rw [← hasLiftingProperty_iff]
  exact HasLiftingProperty.iff_of_arrow_iso_left (braiding _ _) _

Goal state after:
Module: Mathlib.CategoryTheory.Join.Pseudofunctor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {a b : Cat} (f : a ⟶ b),
    NatTrans.toCatHom₂ (mapWhiskerLeft (𝟭 C) (ρ_ f).hom.toNatTrans) =
      (Cat.Hom.isoMk (mapCompRight C f.toFunctor (𝟙 b).toFunctor)).hom ≫
        (mapPair (𝟭 C) f.toFunctor).toCatHom ◁ (Cat.Hom.isoMk mapPairId).hom ≫
          (ρ_ (mapPair (𝟭 C) f.toFunctor).toCatHom).hom

Tactic:
by intros; exact congr($(mapWhiskerLeft_rightUnitor_hom C _).toCatHom₂)

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
hm : ∀ (j : α), { f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
⊢ { f := fun i a ↦ (s.proj a).f i, φ := φ }.f i =
    { f := fun i a ↦ (s.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (s.proj a).φ i }.f i

pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
hm : ∀ (j : α), { f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
⊢ { f := fun i a ↦ (s.proj a).f i, φ := φ }.φ i ≫ eqToHom ⋯ =
    { f := fun i a ↦ (s.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (s.proj a).φ i }.φ i

Tactic:
· rfl

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
hm : ∀ (j : α), { f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
⊢ { f := fun i a ↦ (s.proj a).f i, φ := φ }.φ i ≫ eqToHom ⋯ =
    { f := fun i a ↦ (s.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (s.proj a).φ i }.φ i
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''
⊢ (CatCommSq.iso G (ψ.comp φ).right (ψ.comp φ).base G'').hom ≫
      Functor.whiskerRight (Functor.whiskerRight α.right φ.right) G'' =
    G.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫ (CatCommSq.iso G (ψ'.comp φ).right (ψ'.comp φ).base G'').hom

Tactic:
ext x
    dsimp
    simp only [CatCommSq.vComp_iso_hom_app, Category.assoc]
    rw [← Functor.map_comp_assoc, ← right_coherence_app, Functor.map_comp_assoc]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
X : C₂
⊢ ∀ ⦃Y : C₂⦄ (f : X ⟶ Y), W₂ f → (W₂.inverseImage Φ.functor).inverseImage ρ f

Tactic:
Y

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
X Y : C₂
⊢ ∀ (f : X ⟶ Y), W₂ f → (W₂.inverseImage Φ.functor).inverseImage ρ f
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case refine_1
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X : J → C
⊢ ∀ ⦃Y : J → C⦄ (f : X ⟶ Y),
    MorphismProperty.pi (fun x ↦ W) f → (W.functorCategory (Discrete J)).isoClosure.inverseImage E.functor f

Tactic:
Y

Goal state after:
case refine_1
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X Y : J → C
⊢ ∀ (f : X ⟶ Y),
    MorphismProperty.pi (fun x ↦ W) f → (W.functorCategory (Discrete J)).isoClosure.inverseImage E.functor f
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case refine_2
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X : Discrete J ⥤ C
⊢ ∀ ⦃Y : Discrete J ⥤ C⦄ (f : X ⟶ Y), W.functorCategory (Discrete J) f → IsIso (L₂.map f)

Tactic:
Y

Goal state after:
case refine_2
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
this : CatCommSq E.functor L₁ L₂ E'.functor
X Y : Discrete J ⥤ C
⊢ ∀ (f : X ⟶ Y), W.functorCategory (Discrete J) f → IsIso (L₂.map f)
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y : C
⊢ ((braidingNatIso L W ε).hom.app (L'.obj X)).app (L'.obj Y) =
    LaxMonoidal.μ L' X Y ≫ L'.map (β_ X Y).hom ≫ OplaxMonoidal.δ L' Y X

Tactic:
by
  simp [braidingNatIso, lift₂NatIso]
  rfl

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]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ (Over.forget X).map f ≫ SemiCartesianMonoidalCategory.fst A X =
    Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ ((α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (R.X ◁ P.actRight) ▷ Q.X) ≫ P.actLeft ▷ Q.X =
    (α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (α_ R.X P.X S.X).inv ▷ Q.X ≫ P.actLeft ▷ S.X ▷ Q.X ≫ P.actRight ▷ Q.X

Tactic:
slice_rhs 3 4 => rw [← comp_whiskerRight, middle_assoc, comp_whiskerRight]

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
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)
⊢ ((α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (R.X ◁ P.actRight) ▷ Q.X) ≫ P.actLeft ▷ Q.X =
    (α_ R.X (P.X ⊗ S.X) Q.X).inv ≫
      (α_ R.X P.X S.X).inv ▷ Q.X ≫ (α_ R.X P.X S.X).hom ▷ Q.X ≫ (R.X ◁ P.actRight ≫ P.actLeft) ▷ Q.X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
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)
| μ ▷ P.X ▷ Q.X ≫ P.actLeft ▷ Q.X

pp: case a.a
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)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
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)
| (α_ (R.X ⊗ R.X) P.X Q.X).inv

Tactic:
rw [← comp_whiskerRight, left_assoc, comp_whiskerRight, comp_whiskerRight]

Goal state after:
case a.a
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)
| (α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X

case a.a
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)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
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)
| (α_ (R.X ⊗ R.X) P.X Q.X).inv
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 : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y),
    ((𝟭 (D ⥤ C)).obj G).map f ≫ (ihom.coev (F.obj Y)).app (G.obj Y) =
      (ihom.coev (F.obj X)).app (G.obj X) ≫ ((tensorLeft F ⋙ F.closedIhom).obj G).map f

Tactic:
Y

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),
    ((𝟭 (D ⥤ C)).obj G).map f ≫ (ihom.coev (F.obj Y)).app (G.obj Y) =
      (ihom.coev (F.obj X)).app (G.obj X) ≫ ((tensorLeft F ⋙ F.closedIhom).obj G).map f
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 : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y),
    ((F.closedIhom ⋙ tensorLeft F).obj G).map f ≫ (ihom.ev (F.obj Y)).app (G.obj Y) =
      (ihom.ev (F.obj X)).app (G.obj X) ≫ ((𝟭 (D ⥤ C)).obj G).map f

Tactic:
Y

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.closedIhom ⋙ tensorLeft F).obj G).map f ≫ (ihom.ev (F.obj Y)).app (G.obj Y) =
      (ihom.ev (F.obj X)).app (G.obj X) ≫ ((𝟭 (D ⥤ C)).obj G).map f
Module: Mathlib.CategoryTheory.Monoidal.Closed.Zero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ ⊥_ C ≅ 𝟙_ C

Tactic:
refine ⟨default, (default : 𝟙_ C ⟶ 0) ≫ default, ?_, ?_⟩ <;> simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.mk
C : Type u
Z : F C
as✝¹ as✝ : NormalMonoidalObject C
h : as✝¹ = as✝
⊢ ((tensorFunc C).obj Z).map { down := { down := h } } = inclusion.map { down := { down := h } } ▷ Z

Tactic:
subst h

Goal state after:
case mk.mk
C : Type u
Z : F C
as✝ : NormalMonoidalObject C
⊢ ((tensorFunc C).obj Z).map { down := { down := ⋯ } } = inclusion.map { down := { down := ⋯ } } ▷ Z
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Y

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f : X ⟶ Y), (tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom = (normalizeIsoAux C X).hom ≫ (normalize' C).map f
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Y

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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]
  slice_lhs 3 4 => rw [coequalizer.π_desc]
  rw [one_actLeft, Iso.inv_hom_id]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P f → P.ind f

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
⊢ ∀ (f : X ⟶ Y), P f → P.ind f
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), sourceLocalClosure K P f → Q f

Tactic:
Y

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
⊢ ∀ (f : X ⟶ Y), sourceLocalClosure K P f → Q f
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✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore 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) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
⊢ ∀ {d₁ d₁' : D} (f₁ : d₁ ⟶ d₁') (d₂ : D) (x y : C),
    (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₂)).app (x, y) ≫ ((ι C V D).map (f₁ ▷ d₂)).app (x ⊗ y) =
      ((ι C V D).map f₁).app x ▷ ((ι C V D).obj d₂).obj y ≫
        (DayConvolution.unit ((ι C V D).obj d₁') ((ι C V D).obj d₂)).app (x, y)

Tactic:
by
      intros
      simp [← tensorHom_id, ι_map_tensorHom_eq C V D]

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 : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), P.localEpi f → P.isoClosure.localEpi f

Tactic:
Y

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
⊢ ∀ (f : X ⟶ Y), P.localEpi f → P.isoClosure.localEpi f
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
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
RelEmbedding.wellFounded_iff_isEmpty

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictAnti f
⊢ IsEmpty ((fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2)