mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this✝ : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
this : (fst R.op L.op).Initial
⊢ (snd L R).Final

Tactic:
have : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Initial :=
    initial_equivalence_comp (opEquiv L R).functor.leftOp _

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
this✝¹ : ∀ (a : Aᵒᵖ), IsCofiltered (CostructuredArrow R.op (L.op.obj a))
this✝ : (fst R.op L.op).Initial
this : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Initial
⊢ (snd L R).Final
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this✝ : IsFiltered (CostructuredArrow yoneda (colimit F))
this :
  ∀ (i : I),
    ∃ s, ∃ (_ : Small.{v, max u v} ↑s), ∀ (i_1 : CostructuredArrow yoneda (F.obj i)), ∃ j ∈ s, Nonempty (i_1 ⟶ j)
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))

Tactic:
choose s hs j hjs hj using this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type u_1
I : α → Type u_2
inst✝¹ : (i : α) → Category.{v_1, u_2} (I i)
inst✝ : HasProductsOfShape α C
F : (i : α) → I i ⥤ C
c c' : (i : α) → Cocone (F i)
e : (i : α) → c i ≅ c' i
i : (i : α) → I i
⊢ (coconePointwiseProduct c).ι.app i ≫ (Pi.mapIso fun i ↦ (Cocone.forget (F i)).mapIso (e i)).hom =
    (coconePointwiseProduct c').ι.app i

Tactic:
by
    dsimp
    ext
    simp [Functor.pi]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
ι✝ : Type u_2
inst✝⁵ : HasProductsOfShape ι✝ C
inst✝⁴ : HasProducts C
inst✝³ : HasFilteredColimitsOfSize.{w, w, v_1, u_1} C
inst✝² : IsIPC C
ι : Type u_3
inst✝¹ : Small.{w, u_3} ι
inst✝ : HasProductsOfShape ι C
⊢ IsIPCOfShape.{w, w, v_1, u_1} (Shrink.{w, u_3} ι) C

Tactic:
apply IsIPC.isIPCOfShape

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
⊢ ∑ j ∈ F.attach,
      (h ≫
          pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
            Sigma.π (fun a ↦ G) j ≫ Sigma.ι (fun x ↦ G) (↑j).as) ≫
        d f =
    0

Tactic:
simp only [Category.assoc, ι_d]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
⊢ ∑ x ∈ F.attach,
      h ≫
        pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
          Sigma.π (fun a ↦ G) x ≫ (ModuleCat.Hom.hom f) (↑x).as =
    0
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) 0

pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) (n✝ + 1)

Tactic:
· rw [CochainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros]
      · refine (ShortComplex.exact_and_mono_f_iff_of_iso ?_).2
          ⟨exact_f_d (Injective.ι Z), by dsimp; infer_instance⟩
        exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp)
          (by simp [ofCocomplex])
      all_goals rfl

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n✝ : ℕ
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) (n✝ + 1)
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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ R.cochainComplex.d ↑n ↑m = 0

Tactic:
by simp [R.cochainComplex_d _ _ _ _ rfl rfl, reassoc_of% hf]

Goal state after:
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 : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯
              (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
            ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯) ≫
              (shiftFunctor (CochainComplex C ℤ) ↑n).map φ.hom')
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯

Tactic:
← ShiftedHom.comp_mk₀ _ 0 rfl,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯
              (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
            ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      (((ShiftedHom.comp
                (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
                (ShiftedHom.mk₀ 0 ⋯ φ.hom') ⋯).map
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯
          (inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'))
        ⋯)
      ⋯
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 : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯) ≫
              (shiftFunctor (CochainComplex C ℤ) ↑n).map ((singleFunctor C 0).map g))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y')) ⋯)
      ⋯

Tactic:
← ShiftedHom.comp_mk₀ _ 0 rfl,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
          ((ShiftedHom.map
                (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
                DerivedCategory.Q).comp
            (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
          ⋯).comp
      (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)) ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
      (((ShiftedHom.comp
                (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
                (ShiftedHom.mk₀ 0 ⋯ ((singleFunctor C 0).map g)) ⋯).map
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y')) ⋯)
      ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q P' : ObjectProperty C
h : P ≤ P'
⊢ ofObjectProperty P Q ≤ ofObjectProperty P' Q

Tactic:
intro _ _ _ ⟨hX, hY⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q P' : ObjectProperty C
h : P ≤ P'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hX : P X✝
hY : Q Y✝
⊢ ofObjectProperty P' Q f✝
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
⊢ ofObjectProperty P Q ≤ ofObjectProperty P Q'

Tactic:
intro _ _ _ ⟨hX, hY⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hX : P X✝
hY : Q Y✝
⊢ ofObjectProperty P Q' f✝
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), f ≫ s = 0

Tactic:
· exact ⟨_, cokernel.π f, hf, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case inr
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w

pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
hw' : ∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w

Tactic:
· obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.isoModSerre
      ((L.objObjPreimageIso W).hom ≫ w)
    rw [← cancel_epi (L.map φ.s),
      MorphismProperty.RightFraction.map_s_comp_map] at hφ
    obtain ⟨l, hl⟩ := this _ (L.map φ.f) (by
      rw [← hφ, Category.assoc, Category.assoc, hw, comp_zero, comp_zero]) ⟨_, rfl, by simp⟩
    exact ⟨(L.objObjPreimageIso W).inv ≫ inv (L.map φ.s) ≫ l, by simp [hl, ← hφ]⟩

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
hw' : ∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
⊢ ∃ l, l ≫ L.map (kernel.ι f) = w
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ t.leftToRight.app (G.obj X) = t.adj₁.counit.app X ≫ t.adj₂.unit.app X

Tactic:
refine (((t.adj₂.homEquiv _ _).apply_symm_apply _).symm.trans ?_).symm
  rw [homEquiv_symm_apply, map_comp, Category.assoc, left_triangle_components,
    homEquiv_apply, leftToRight_app, ← H.map_inv]
  congr
  simpa using IsIso.eq_inv_of_hom_inv_id (t.adj₁.right_triangle_components _)

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

Goal state before:
pp: case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ f✝ ◁ η✝.mk ≫
      (α_ ((preinclusion B).map { as := p }) f✝ h✝).inv ≫
        (normalizeIso p f✝).hom ▷ h✝ ≫ (normalizeIso (normalizeAux p f✝) h✝).hom =
    ((α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      eqToHom ⋯

Tactic:
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]

Goal state after:
case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
      (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    ((α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      eqToHom ⋯
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✝
⊢ eqToHom ⋯ ≫ ((f ≫ g) ≫ h).fiber = (f ≫ g ≫ h).fiber

Tactic:
· simp [mapComp_assoc_right_hom_app_assoc, Strict.associator_eqToIso]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ g ◁ η' ⊗≫ (t.unit ▷ h ⊗≫ f ◁ τ') ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = t.unit ≫ f ◁ H.desc σs'

Tactic:
rw [Hτ', IsKan.fac]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
σs' : LeftExtension f g := mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))
⊢ 𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u) = σs'.unit
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X✝ Y✝ Z✝ : PartialFun
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
o : { X := Option X✝, point := none }.X
a : X✝
⊢ { toFun := Option.elim' none fun a ↦ ((f ≫ g) a).toOption, map_point := ⋯ }.toFun (some a) =
    ({ toFun := Option.elim' none fun a ↦ (f a).toOption, map_point := ⋯ } ≫
          { toFun := Option.elim' none fun a ↦ (g a).toOption, map_point := ⋯ }).toFun
      (some a)

Tactic:
dsimp [CategoryStruct.comp]
        rw [Part.bind_toOption g (f a), Option.elim'_eq_elim]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = (s.π.app j').toFunctor
⊢ eqToHom ⋯ ≫ ((s.π.app j).toFunctor ⋙ (F.map h).toFunctor).map f ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯

Tactic:
Functor.congr_hom this f

Goal state after:
case h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
j j' : J
h : j ⟶ j'
this : (s.π.app j).toFunctor ⋙ (F.map h).toFunctor = (s.π.app j').toFunctor
⊢ eqToHom ⋯ ≫ (eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (s.π.app j').toFunctor.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [eq, ← Subobject.pullback_comp]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
⊢ φ₁ = φ₂

Tactic:
let φ₂' : U ⟶ (pullback g).obj (Over.mk f) := Over.homMk φ₂ (by simpa using! h₂.symm)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
⊢ φ₁ = φ₂
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
adj : map g ⊣ pullback g := mapPullbackAdj g
a' : (map g).obj (Over.mk b) ⟶ Over.mk f := homMk a h
⊢ (map g).map ((adj.homEquiv (Over.mk b) (Over.mk f)) (homMk a ⋯)) ≫ fst' f g = a'

Tactic:
simp only [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply, adj, a']

Goal state after: