mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
⊢ ∀ (φ' : a ⟶ b') [p.IsHomLift (f ≫ g) φ'], ∃! χ, p.IsHomLift g χ ∧ φ.hom ≫ χ = φ'

Tactic:
τ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
⊢ ∀ [p.IsHomLift (f ≫ g) τ], ∃! χ, p.IsHomLift g χ ∧ φ.hom ≫ χ = τ
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : LF.IsLeftDerivedFunctor α W
G : D ⥤ H
β : L ⋙ G ⟶ F
this : LF.IsRightKanExtension α
⊢ G.IsRightKanExtension β ↔ IsIso (LF.leftDerivedLift α W G β)

Tactic:
exact isRightKanExtension_iff_isIso _ α _ (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app
        (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))

Tactic:
have : IsIso (F.map w) := by
        have := Localization.inverts L W w hw
        rw [← NatIso.naturality_2 e w]
        dsimp
        infer_instance

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
this : IsIso (F.map w)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app
        (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : PreGaloisCategory C
inst✝² : FiberFunctor F
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ PreservesColimitsOfShape (SingleObj G) F

Tactic:
choose G' hg hf he using Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.preservesColimitsOfShape_of_equiv he.some.toSingleObjEquiv.symm F

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : Nat.card (F.obj Y).obj ≤ Nat.card (F.obj X).obj
⊢ Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj

Tactic:
exact Nat.le_antisymm
    (Nat.card_le_card_of_injective (F.map f) (injective_of_mono_of_preservesPullback (F.map f))) hlt

Goal state after:
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X : C
g h : Aut X
a : (F.obj X).obj
⊢ (g * h) • a = g • h • a

Tactic:
change F.map (h.hom ≫ g.hom) a = (F.map h.hom ≫ F.map g.hom) a
    simp only [map_comp, FintypeCat.comp_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ : Aut F
⊢ ∀ ⦃a₂ : Aut F⦄, (autEmbedding F) σ = (autEmbedding F) a₂ → σ = a₂

Tactic:
τ

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
⊢ (autEmbedding F) σ = (autEmbedding F) τ → σ = τ
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case h
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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ ((gi X)⁻¹ * gs) • X.pt = X.pt

Tactic:
mul_smul,

Goal state after:
case h
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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
s : Finset (PointedGaloisObject F)
gs : G
hgs : ∀ (i : ↥s) (x : (F.obj (↑i).obj).obj), gs • x = (ConcreteCategory.hom (t.hom.app (↑i).obj)) x
X : PointedGaloisObject F
hXmem : X ∈ s
⊢ (gi X)⁻¹ • gs • X.pt = X.pt
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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
X : C
x✝ : IsGalois X
x : (F.obj X).obj
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ } • s ∈ c
⊢ (gi { obj := X, pt := x, isGalois := ⋯ } * s) • x = (ConcreteCategory.hom (t.hom.app X)) x

Tactic:
mul_smul,

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✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
X : C
x✝ : IsGalois X
x : (F.obj X).obj
s : G
hsmem : s • x = x
hg : gi { obj := X, pt := x, isGalois := ⋯ } • s ∈ c
⊢ gi { obj := X, pt := x, isGalois := ⋯ } • s • x = (ConcreteCategory.hom (t.hom.app X)) x
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
F₁ F₂ : FreeGroupoid C ⥤ G
τ : of C ⋙ F₁ ≅ of C ⋙ F₂
X : C
⊢ (liftNatIso F₁ F₂ τ).hom.app (mk X) = τ.hom.app X

Tactic:
by
  simp [liftNatIso]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
F₁ F₂ : FreeGroupoid C ⥤ G
τ : of C ⋙ F₁ ≅ of C ⋙ F₂
X : C
⊢ (liftNatIso F₁ F₂ τ).inv.app (mk X) = τ.inv.app X

Tactic:
by
  simp [liftNatIso]

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
γ₁ γ₂ : c ⟶ c
⊢ inv f ≫ (γ₁ * γ₂) ≫ f = inv f ≫ γ₁ ≫ f * inv f ≫ γ₂ ≫ f

Tactic:
by
    simp only [vertexGroup_mul, inv_eq_inv, Category.assoc, IsIso.hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g :=
  TwoSquare.StructuredArrowRightwards.mk (TwoSquare.overPost F X) g (Over.mk prod.fst)
    (Over.homMk
      (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z))
      ⋯)
    prod.snd ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ Over.Hom.left (StructuredArrow.hom Q).left ≫
      F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom) =
    Over.Hom.left (StructuredArrow.hom P).left

Tactic:
← cancel_mono (prodComparison F X _)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g :=
  TwoSquare.StructuredArrowRightwards.mk (TwoSquare.overPost F X) g (Over.mk prod.fst)
    (Over.homMk
      (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z))
      ⋯)
    prod.snd ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ (Over.Hom.left (StructuredArrow.hom Q).left ≫
        F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
      prodComparison F X Z =
    Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z
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:
change ⟦σ * τ⟧ = ⟦τ⟧

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
⊢ ⟦σ * τ⟧ = ⟦τ⟧
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C} {p : c ⟶ d}, p ∈ univ → Groupoid.inv p ∈ univ

Tactic:
by intros; trivial

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

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d e : C} {p : c ⟶ d}, p ∈ univ → ∀ {q : d ⟶ e}, q ∈ univ → p ≫ q ∈ univ

Tactic:
by intros; trivial

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Biproducts

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inr ≫ biprod.desc P.decompId_i P.complement.decompId_i ≫ biprod.lift P.decompId_p P.complement.decompId_p =
    biprod.inr ≫ 𝟙 (P ⊞ P.complement)

Tactic:
rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
        add_eq_right, ← assoc]

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (P.complement.decompId_i ≫ P.decompId_p) ≫ biprod.inl = 0
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : C
f : (left a✝).Hom y
⊢ comp (left a✝).id f = f

Tactic:
cases y

Goal state after:
case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
f : (left a✝¹).Hom (left a✝)
⊢ comp (left a✝¹).id f = f

case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : C
a✝ : D
f : (left a✝¹).Hom (right a✝)
⊢ comp (left a✝¹).id f = f
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : D
f : (right a✝).Hom y
⊢ comp (right a✝).id f = f

Tactic:
cases y

Goal state after:
case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
f : (right a✝¹).Hom (left a✝)
⊢ comp (right a✝¹).id f = f

case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
f : (right a✝¹).Hom (right a✝)
⊢ comp (right a✝¹).id f = f
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : C
f : (left a✝).Hom y
⊢ comp f y.id = f

Tactic:
cases y

Goal state after:
case left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : C
f : (left a✝¹).Hom (left a✝)
⊢ comp f (left a✝).id = f

case left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : C
a✝ : D
f : (left a✝¹).Hom (right a✝)
⊢ comp f (right a✝).id = f
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
y : C ⋆ D
a✝ : D
f : (right a✝).Hom y
⊢ comp f y.id = f

Tactic:
cases y

Goal state after:
case right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ : D
a✝ : C
f : (right a✝¹).Hom (left a✝)
⊢ comp f (left a✝).id = f

case right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝¹ a✝ : D
f : (right a✝¹).Hom (right a✝)
⊢ comp f (right a✝).id = f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 0 b.inl b.inr

Tactic:
convert! IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial

Goal state after:
case e'_7
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsInitial.to X

case e'_8
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ 0 = HasZeroObject.zeroIsInitial.to Y
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
inst✝ : Small.{w, u'} J
x✝ : Cᵒᵖ ⥤ Type w
⊢ ObjectProperty.preservesLimit F x✝ ↔ (MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal x✝

Tactic:
by_cases hF : HasLimit F

Goal state after:
case pos
C : Type u
inst✝³ : Category.{v, u} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
inst✝ : Small.{w, u'} J
x✝ : Cᵒᵖ ⥤ Type w
hF : HasLimit F
⊢ ObjectProperty.preservesLimit F x✝ ↔ (MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal x✝

case neg
C : Type u
inst✝³ : Category.{v, u} C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
inst✝ : Small.{w, u'} J
x✝ : Cᵒᵖ ⥤ Type w
hF : ¬HasLimit F
⊢ ObjectProperty.preservesLimit F x✝ ↔ (MorphismProperty.ofHoms (preservesLimitHomFamily F)).isLocal 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 : x ⟶ y
inst✝ : IsIso f
⊢ f.fst ≫ (inv f).fst = 𝟙 x.fst

Tactic:
simp [← comp_fst]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
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
⊢ (curriedAssociatorNatIso (LocalizedMonoidal L W ε)).inv ≫
      ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε) =
    ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε)

Tactic:
· apply natTrans₃_ext (L') (L') (L') W W W
    simpa using! map_hexagon_reverse _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MarkovCategory C
X : C
f : X ⟶ 𝟙_ C
⊢ f = ε

Tactic:
by
  rw [← Category.comp_id f, ← discard_unit, discard_natural]

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

Goal state before:
pp: 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))
⊢ adj.toMonad.Algebra ⥤ D

Tactic:
by
  refine
    Adjunction.leftAdjointOfEquiv (G := comparison adj)
      (F_obj := fun A => comparisonLeftAdjointObj adj A) (fun A B => ?_) ?_
  · apply comparisonLeftAdjointHomEquiv
  · intro A B B' g h
    ext1
    simp [Cofork.IsColimit.homIso, Adjunction.homEquiv_unit]

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

Goal state before:
pp: 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✝¹ : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst✝ : G.IsSplitPair f g
⊢ HasColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))

Tactic:
exact inferInstanceAs <| HasCoequalizer (G.map f) (G.map g)

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)
⊢ η ▷ (P.X ⊗ Q.X) ≫
      (α_ R.X P.X Q.X).inv ≫
        P.actLeft ▷ 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_lhs 1 2 => rw [associator_inv_naturality_left]

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 ▷ Q.X) ≫ P.actLeft ▷ 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
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)
⊢ μ ▷ (P.X ⊗ Q.X) ≫
      (α_ R.X P.X Q.X).inv ≫
        P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫
        R.X ◁ actLeft P Q ≫ actLeft P Q

Tactic:
slice_lhs 1 2 => rw [associator_inv_naturality_left]

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)
⊢ (((α_ (R.X ⊗ R.X) P.X Q.X).inv ≫ μ ▷ P.X ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫
      coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (R.X ⊗ R.X) ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom ≫
        R.X ◁ actLeft P Q ≫ actLeft P Q