mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case eq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f
      ⟨(max n m).succ, ⋯.mpr (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')⟩ =
    { obj := eq g g', property := ⋯ }.obj

Tactic:
simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]

Goal state after:
case eq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure f (max n m).succ).snd
      (⋯.mpr (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')) =
    eq g g'
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i ≫
                    K.whiskerLeft (colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda) i)).app
                j ≫
              (K.isoWhiskerLeft
                      ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                        (Presheaf.isColimitTautologicalCocone A))).hom.app
                j

Tactic:
isoWhiskerLeft_hom,

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                (limit.π K j)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i ≫
                    K.whiskerLeft (colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda) i)).app
                j ≫
              (K.whiskerLeft
                    ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                        (Presheaf.isColimitTautologicalCocone A)).hom).app
                j
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
A B : Ind C
f : A ⟶ B
P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map f)
⊢ (Arrow.mk f).left ≅ (Arrow.mk ((Ind.lim P.I).map P.φ)).left

Tactic:
exact P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.zero

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s))
      yk =
    (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) yk
hy₂ :
  (hom (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s))
      yk' =
    (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) yk'
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')

Tactic:
dsimp at hy₁ hy₂ hy

Goal state after:
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
hy₂ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
α : Ext X Y n
m : ℕ
hm : n + 1 = m
⊢ ∃ f, ∃ (hf : f ≫ R.cocomplex.d n m = 0), R.extMk f m hm hf = α

Tactic:
by
  obtain ⟨x, rfl⟩ := R.extEquivCohomologyClass.symm.surjective α
  obtain ⟨x, rfl⟩ := x.mk_surjective
  obtain ⟨f, hf, rfl⟩ := Cocycle.fromSingleMk_surjective x n (by simp) m (by lia)
  exact ⟨f ≫ (R.cochainComplexXIso n n rfl).hom,
    by simpa [R.cochainComplex_d _ _ _ _ rfl rfl,
      ← cancel_mono (R.cochainComplexXIso m m rfl).inv] using hf, by simp [extMk]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ (SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q)
      ((SmallShiftedHom.mk₀Inv 0 ⋯ R.π' ⋯).comp (CohomologyClass.mk x).toSmallShiftedHom ⋯) =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯

Tactic:
simp only [SmallShiftedHom.equiv_comp, SmallShiftedHom.equiv_mk₀Inv, isoOfHom, asIso_inv,
    CohomologyClass.equiv_toSmallShiftedHom_mk,
    DerivedCategory.singleFunctorIsoCompQ, Iso.refl_hom, NatTrans.id_app, Category.id_comp,
    Iso.refl_inv]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.π'))).comp
      (ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (𝟙 ((DerivedCategory.singleFunctor C 0).obj Y))) ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: case left
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
b : X
⊢ ⟨fun b ↦ F.map (homOfPair b 1), 1⟩.left b = left 1 b

Tactic:
exact F_map_eq.symm.trans (F.map_id b)

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v a b : G
h : a ≈ b
⊢ a * v⁻¹ ≈ b * v⁻¹

Tactic:
by
      apply (QuotientGroup.leftRel_apply).mpr
      -- We avoid `group` here to minimize imports while low in the hierarchy;
      -- typically it would be better to invoke the tactic.
      simpa [mul_assoc] using Subgroup.Normal.conj_mem ‹_› _ (QuotientGroup.leftRel_apply.mp h) _

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape J (F ⋙ forget V G)

Tactic:
exact PreservesLimitsOfSize.preservesLimitsOfShape

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: case refine_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt
hm : m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
⊢ m = ↑((h X).lift' s.ι ⋯)

Tactic:
rw [← cancel_mono (adj₁.unit.app X)]

Goal state after:
case refine_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt
hm : m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι
⊢ m ≫ adj₁.unit.app X = ↑((h X).lift' s.ι ⋯) ≫ adj₁.unit.app X
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C) (Z : D), Function.Injective fun g ↦ L.map (q.adj₂.counit.app X) ≫ g) ↔
    ∀ (X : D), Mono (q.adj₃.unit.app (F.obj X))

Tactic:
mono_iff_forall_injective

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C) (Z : D), Function.Injective fun g ↦ L.map (q.adj₂.counit.app X) ≫ g) ↔
    ∀ (X : D) (Z : C), Function.Injective fun g ↦ g ≫ q.adj₃.unit.app (F.obj X)
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝³ : L.Full
inst✝² : L.Faithful
inst✝¹ : G.Full
inst✝ : G.Faithful
h :
  (∀ (X : Dᵒᵖ), Epi (q.op.leftTriple.rightToLeft.app X)) ↔
    ∀ (a : C), Mono (q.op.rightTriple.leftToRight.app (Opposite.equivToOpposite a))
⊢ (∀ (X : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)

Tactic:
rw [← (Opposite.equivToOpposite (α := D)).forall_congr_right] at h

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝³ : L.Full
inst✝² : L.Faithful
inst✝¹ : G.Full
inst✝ : G.Faithful
h :
  (∀ (a : D), Epi (q.op.leftTriple.rightToLeft.app (Opposite.equivToOpposite a))) ↔
    ∀ (a : C), Mono (q.op.rightTriple.leftToRight.app (Opposite.equivToOpposite a))
⊢ (∀ (X : C), Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.rightToLeft.app X)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

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
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
⊢ B ⥤ C

Tactic:
refine Adjunction.rightAdjointOfEquiv
    (fun X Y => (constructRightAdjointEquiv L _ adj₁ adj₂ h X Y).symm) ?_
  intro X Y Y' g h
  rw [constructRightAdjointEquiv_symm_apply, constructRightAdjointEquiv_symm_apply,
    Equiv.symm_apply_eq, Subtype.ext_iff]
  dsimp
  simp only [Adjunction.homEquiv_counit]
  erw [Fork.IsLimit.homIso_natural, Fork.IsLimit.homIso_natural]
  simp only [Fork.ofι_pt, Functor.map_comp, assoc, limit.cone_x]
  erw [adj₂.homEquiv_naturality_left, Equiv.rightInverse_symm]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ ((α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
        η.naturality (f ≫ g) ▷ θ.app c ≫
          (α_ (η.app a) (G.map (f ≫ g)) (θ.app c)).hom ≫
            η.app a ◁ θ.naturality (f ≫ g) ≫ (α_ (η.app a) (θ.app a) (H.map (f ≫ g))).inv) ≫
      (η.app a ≫ θ.app a) ◁ H.mapComp f g =
    (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      F.mapComp f g ▷ η.app c ▷ θ.app c ≫
        (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
          (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                  (F.map f ≫ η.app b) ◁ θ.naturality g ≫
                    η.naturality f ▷ (θ.app b ≫ H.map g) ≫
                      (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                        η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                          η.app a ◁ θ.naturality f ▷ H.map g ≫
                            η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                              (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv

Tactic:
rw [whisker_exchange_assoc]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
W✝ X✝ Y✝ Z✝ : ∫ᶜ F
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber ≫ eqToHom ⋯

Tactic:
simp [← NatTrans.naturality_assoc, F.mapComp_assoc_right_inv_app, Strict.associator_eqToIso]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₁ ≫ f₁₃ = f
⊢ (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom =
    (F.mapComp' f₀₂ f₂₃ f ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
subst h₀₂ h₁₃ hf
  simp [mapComp_assoc_right_hom, Strict.associator_eqToIso, mapComp']

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y ↦ Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf ↦
      match e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p ↦
            WellFounded.fixF
              (fun a IH ↦
                Part.assert (f a).Dom fun hf ↦
                  match e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯)
              y ⋯)
          a' ⋯
⊢ (f a).Dom

Tactic:
exact h₂.fst.fst

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case mpr
X Y : RelCat
f : X ≅ Y
⊢ IsIso (graphFunctor.map f.hom)

Tactic:
apply graphFunctor.map_isIso

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : SymmetricCategory C
inst✝ : P.IsStableUnderBraiding
c c' : WideSubcategory P
⊢ ((β_ c c').hom ≫ (β_ c' c).hom).hom = (𝟙 (c ⊗ c')).hom

Tactic:
exact SymmetricCategory.symmetry _ _

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F)).obj ((Subobject.pullback π(π₁, F.F)).obj X.rel)

Tactic:
simp [← Subobject.pullback_comp]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F)).obj
      ((Subobject.pullback (prod.map F.f (𝟙 Y.tgt))).obj Y.rel) ≤
    (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).obj ((Subobject.pullback π(π₁, G.F)).obj Y.rel)

Tactic:
simp [← Subobject.pullback_comp]

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

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).obj ((Subobject.pullback (prod.map G.f (𝟙 Z.tgt))).obj Z.rel) ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel

Tactic:
simp [← Subobject.pullback_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a : α
⊢ (pullback.snd g₁ (Sigma.ι X a) ≫ Sigma.ι X a) ≫ Sigma.desc e = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e

Tactic:
simp only [Category.assoc, colimit.ι_desc, Cofan.mk_ι_app]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a : α
⊢ pullback.snd g₁ (Sigma.ι X a) ≫ e a = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a b : α
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a =
    (pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ Sigma.ι X b) ≫ Sigma.desc e

Tactic:
simp only [Category.assoc, colimit.ι_desc, Cofan.mk_ι_app]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a b : α
⊢ pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a) ≫ e a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ e b
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : F ⟶ G
x✝ : IsIso ((forgetful 𝒳 𝒴).map α)
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) ((inv ((forgetful 𝒳 𝒴).map α)).app a)

Tactic:
simp [lift_id_inv_isIso]

Goal state after: