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

Goal state before:
pp: case max
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j j✝ j'✝ : C
hj₁ : filteredClosure f j✝
hj₂ : filteredClosure f j'✝
ih : ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := j✝, property := hj₁ }.obj
ih' : ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := j'✝, property := hj₂ }.obj
⊢ ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := max j✝ j'✝, property := ⋯ }.obj

Tactic:
| max hj₁ hj₂ ih ih' =>

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_2
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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
⊢ ∃ W h, h ≫ u = h ≫ v

Tactic:
obtain ⟨Q⟩ : Nonempty (CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))) :=
        IsCofiltered.nonempty
      obtain ⟨ia, va₁, va₂, heqa⟩ := exists_eq_of_isCofiltered_costructuredArrow L
        (Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right)) j₁.hom
      obtain ⟨i₀, α, β, hα, hβ⟩ := IsCofiltered.bowtie u.left (va₂ ≫ v.left) (𝟙 _) va₂
      have := IsCofiltered.eq_condition u.right v.right
      exact ⟨⟨i₀, IsCofiltered.eq u.right v.right, L.map (β ≫ va₁) ≫ Q.hom⟩,
        ⟨β ≫ va₂, IsCofiltered.eqHom u.right v.right, by cat_disch⟩, by cat_disch⟩

Goal state after:
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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
⊢ (fst L R).Initial

Tactic:
have := isCofiltered_of_isCofiltered_costructuredArrow L R

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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
this : IsCofiltered (Comma L R)
⊢ (fst L R).Initial
Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x✝¹ x✝ : K f g P₁ P₂
h : x✝¹ ⟶ x✝
⊢ (F₁ f g P₁ P₂).map h ≫ x✝.hom.1.left = x✝¹.hom.1.left ≫ (F₂ f g P₁ P₂).map h

Tactic:
have := h.w

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x✝¹ x✝ : K f g P₁ P₂
h : x✝¹ ⟶ x✝
this :
  ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod' (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g)).map
        h.left ≫
      x✝.hom =
    x✝¹.hom ≫ (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow).map h.right
⊢ (F₁ f g P₁ P₂).map h ≫ x✝.hom.1.left = x✝¹.hom.1.left ≫ (F₂ f g P₁ P₂).map h
Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x✝¹ x✝ : K f g P₁ P₂
h : x✝¹ ⟶ x✝
⊢ (F₁ f g P₁ P₂).map h ≫ x✝.hom.2.left = x✝¹.hom.2.left ≫ (F₂ f g P₁ P₂).map h

Tactic:
have := h.w

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x✝¹ x✝ : K f g P₁ P₂
h : x✝¹ ⟶ x✝
this :
  ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod' (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g)).map
        h.left ≫
      x✝.hom =
    x✝¹.hom ≫ (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow).map h.right
⊢ (F₁ f g P₁ P₂).map h ≫ x✝.hom.2.left = x✝¹.hom.2.left ≫ (F₂ f g P₁ P₂).map h
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type v
inst✝² : SmallCategory J
inst✝¹ : IsFiltered J
F : J ⥤ Cᵒᵖ ⥤ Type v
inst✝ : HasColimit F
hF : ∀ (j : J), IsIndObject (F.obj j)
⊢ IsIndObject (colimit F)

Tactic:
exact isIndObject_colimit _ _ hF

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Indization

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (ObjectProperty.ofObj Ind.yoneda.obj).IsSeparating

Tactic:
by
  refine fun X Y f g h => (cancel_epi (Ind.colimitPresentationCompYoneda X).hom).1 ?_
  exact colimit.hom_ext (fun i => by simp [← Category.assoc, h])

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex)

Tactic:
apply descHomotopy (𝟙 X)

Goal state after:
case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ I.ι ≫ desc (𝟙 X) I I = (CochainComplex.single₀ C).map (𝟙 X) ≫ I.ι

case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ I.ι ≫ 𝟙 I.cocomplex = (CochainComplex.single₀ C).map (𝟙 X) ≫ I.ι
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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk (Cocycle.fromSingleMk ((f - g) ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))

Tactic:
simp only [Preadditive.sub_comp]

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 g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) -
      R.extEquivCohomologyClass.symm
        (CohomologyClass.mk (Cocycle.fromSingleMk (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)) =
    R.extEquivCohomologyClass.symm
      (CohomologyClass.mk
        (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv - g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯
          ⋯))
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
hf : f.hom = 0
⊢ biprod.fst ≫ f.hom = biprod.snd ≫ (Over.mk 0).hom

Tactic:
by
      rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
this : P.monoModSerre f
⊢ P.isoModSerre f ↔ P.epiModSerre f

Tactic:
rw [isoModSerre_iff]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Mono f
this : P.monoModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.epiModSerre f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Epi f
this : P.epiModSerre f
⊢ P.isoModSerre f ↔ P.monoModSerre f

Tactic:
rw [isoModSerre_iff]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
X Y : C
f : X ⟶ Y
inst✝ : Epi f
this : P.epiModSerre f
⊢ P.monoModSerre f ∧ P.epiModSerre f ↔ P.monoModSerre f
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (P.ι.f 0) ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).d 0 1 = 0

Tactic:
by
    dsimp
    rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d,
      zero_comp, F.map_zero]

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

Goal state before:
pp: case refine_2
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
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f₁ = s ≫ f₂
⊢ f₁ ≫ cokernel.π (f₁ - f₂) = f₂ ≫ cokernel.π (f₁ - f₂)

Tactic:
· simpa only [Preadditive.sub_comp, sub_eq_zero] using cokernel.condition (f₁ - f₂)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ { X₁ := F.obj X, X₂ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 0,
        X₃ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 1, f := F.map (P.ι.f 0),
        g := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).d 0 1, zero := ⋯ }.Exact ∧
    Mono (F.map (P.ι.f 0))

Tactic:
ShortComplex.exact_and_mono_f_iff_f_is_kernel

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteLimits F
X : C
P : InjectiveResolution X
⊢ Nonempty
    (IsLimit
      (KernelFork.ofι
        { X₁ := F.obj X, X₂ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 0,
            X₃ := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).X 1, f := F.map (P.ι.f 0),
            g := ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).d 0 1, zero := ⋯ }.f
        ⋯))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
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 : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
⊢ MorphismProperty.epimorphisms D (L.map f')

Tactic:
simpa using inferInstanceAs (Epi (L.map f'))

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
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
this : PreservesLimit K F'
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor

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

Goal state before:
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝ : Abelian D := abelian L P
this : PreservesFiniteColimits L
x✝ : PreservesFiniteColimits (L ⋙ G)
⊢ (L ⋙ G).Additive

Tactic:
by
    have := preservesBinaryBiproducts_of_preservesBinaryCoproducts (L ⋙ G)
    exact Functor.additive_of_preservesBinaryBiproducts _

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

Goal state before:
pp: case refine_1
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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ (h X).left ≫ s.π = (h X).right ≫ s.π

Tactic:
← cancel_epi (adj₁.counit.app (h X).W)

Goal state after:
case refine_1
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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ adj₁.counit.app (h X).W ≫ (h X).left ≫ s.π = adj₁.counit.app (h X).W ≫ (h X).right ≫ s.π
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π
⊢ m = ↑((h X).desc' s.π ⋯)

Tactic:
← cancel_epi (adj₁.counit.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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π
⊢ adj₁.counit.app X ≫ m = adj₁.counit.app X ≫ ↑((h X).desc' s.π ⋯)
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

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 : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫ F'.map (U.map (adj₁.counit.app X)) = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))

Tactic:
by
      rw [← F'.map_comp, adj₁.right_triangle_components]
      apply F'.map_id

Goal state after:
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✝¹ : G.Full
inst✝ : G.Faithful
x✝ : Cᵒᵖ
⊢ t.op.rightToLeft.app x✝ = (NatTrans.op t.rightToLeft).app x✝

Tactic:
rw [rightToLeft_eq_units, rightToLeft_eq_counits]

Goal state after:
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✝¹ : G.Full
inst✝ : G.Faithful
x✝ : Cᵒᵖ
⊢ (F.op.leftUnitor.inv ≫
          whiskerRight t.op.adj₁.unit F.op ≫
            (H.op.associator G.op F.op).hom ≫ inv (H.op.whiskerLeft t.op.adj₂.unit) ≫ H.op.rightUnitor.hom).app
      x✝ =
    (NatTrans.op
          (H.rightUnitor.inv ≫
            inv (H.whiskerLeft t.adj₁.counit) ≫
              (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom)).app
      x✝
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
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map (G.map ((whiskerRight t.adj₁.unit H).app X)) ≫ t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)

Tactic:
rw [whiskerRight_app _ H, (asIso (t.adj₂.counit.app (G.obj _))).eq_comp_inv.2
      (t.adj₂.counit_naturality (t.adj₁.unit.app X)),
    ← (asIso _).comp_hom_eq_id.1 <| t.adj₂.left_triangle_components (F.obj X)]

Goal state after:
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
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map ((t.adj₂.counit.app ((𝟭 C).obj X) ≫ t.adj₁.unit.app X) ≫ G.map (t.adj₂.unit.app (F.obj X))) ≫
      t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵒᵖᴸ C
η θ : F ⟶ G
Γ : η ⟶ θ
ι : G ⟶ H
a b : B
f : a ⟶ b
⊢ Γ.as.app a ▷ ι.app a ▷ H.map f ≫ (θ ≫ ι).naturality f = (η ≫ ι).naturality f ≫ F.map f ◁ Γ.as.app b ▷ ι.app b

Tactic:
dsimp only [comp_app, comp_naturality]
      calc
        _ = 𝟙 _ ⊗≫ (Γ.as.app a ▷ (ι.app a ≫ H.map f) ≫ θ.app a ◁ ι.naturality f) ⊗≫
              θ.naturality f ▷ ι.app b ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.app a ◁ ι.naturality f ⊗≫ (Γ.as.app a ▷ G.map f ≫
              θ.naturality f) ▷ ι.app b ⊗≫ 𝟙 _ := by
          rw [← whisker_exchange]
          bicategory
        _ = _ := by
          rw [Γ.as.naturality]
          bicategory

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
G H : B ⥤ᵒᵖᴸ C
θ : StrongTrans G H
a b : B
a' : C
f : a' ⟶ G.obj a
g h : a ⟶ b
β : g ⟶ h
⊢ f ◁ G.map₂ β ▷ θ.app b ≫ f ◁ (θ.naturality h).hom = f ◁ (θ.naturality g).hom ≫ f ◁ θ.app a ◁ H.map₂ β

Tactic:
by
  apply θ.toOplax.whiskerLeft_naturality_naturality

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ f ≫ 𝟙 b = f

Tactic:
ext
    · simp
    · simp [F.mapComp_id_left_inv_app, Strict.leftUnitor_eqToIso, ← Functor.map_comp_assoc,
        ← Cat.Hom₂.comp_app]

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

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a b c : ∫ᶜ F
f : a ⟶ b
g : b ⟶ c
⊢ (α.app { as := op a.base }).toFunctor.map f.fiber ≫
      (((α.app { as := op a.base }).toFunctor.map ((F.map f.base.op.toLoc).toFunctor.map g.fiber) ≫
            (α.naturality f.base.op.toLoc).hom.toNatTrans.app ((F.map g.base.op.toLoc).toFunctor.obj c.fiber)) ≫
          (G.map f.base.op.toLoc).toFunctor.map ((α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber)) ≫
        (G.mapComp g.base.op.toLoc f.base.op.toLoc).inv.toNatTrans.app
          ((α.app { as := op c.base }).toFunctor.obj c.fiber) =
    (α.app { as := op a.base }).toFunctor.map f.fiber ≫
      (α.naturality f.base.op.toLoc).hom.toNatTrans.app b.fiber ≫
        (G.map f.base.op.toLoc).toFunctor.map ((α.app { as := op b.base }).toFunctor.map g.fiber) ≫
          (G.map f.base.op.toLoc).toFunctor.map ((α.naturality g.base.op.toLoc).hom.toNatTrans.app c.fiber) ≫
            (G.mapComp g.base.op.toLoc f.base.op.toLoc).inv.toNatTrans.app
              ((α.app { as := op c.base }).toFunctor.obj c.fiber)

Tactic:
simp only [assoc, ← reassoc_of% Cat.Hom.comp_map,
        Cat.Hom.comp_toFunctor, Functor.comp_obj, NatTrans.naturality_assoc]

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
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ leftZigzag adj.unit adj.counit ⊗≫ τ ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift

Tactic:
leftZigzag

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
τ : h ≫ f ⟶ s.lift := StructuredArrow.Hom.right τ₀
hτ : h ◁ adj.unit ⊗≫ τ ▷ u = s.unit
⊢ 𝟙 (h ≫ f) ⊗≫ h ◁ (adj.unit ▷ f ⊗≫ f ◁ adj.counit) ⊗≫ τ ⊗≫ 𝟙 s.lift =
    𝟙 (h ≫ f) ⊗≫ h ◁ adj.unit ▷ f ⊗≫ ((h ≫ f) ◁ adj.counit ≫ τ ▷ 𝟙 b) ⊗≫ 𝟙 s.lift
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)

Tactic:
leftZigzag

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := H'.desc (LeftLift.mk (𝟙 b) ((ρ_ u).hom ≫ (λ_ u).inv))
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ 𝟙 (𝟙 a) ⊗≫ t.unit ⊗≫ (t.unit ▷ t.lift ⊗≫ t.lift ◁ ε) ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u) =
    𝟙 (𝟙 a) ⊗≫ (𝟙 a ◁ t.unit ≫ t.unit ▷ (t.lift ≫ u)) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 ((t.lift ≫ 𝟙 b) ≫ u)
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝¹ : Cat
x : ConnectedComponents ↑x✝¹
x✝ : ↑x✝¹
h : ⟦x✝⟧ = x
⊢ (𝟭 ↑x✝¹).mapConnectedComponents x = x

Tactic:
by subst h; rfl

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

Goal state before:
pp: X : Type u
C : Cat
X✝ Y✝ Z✝ : Cat
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x : ConnectedComponents ↑X✝
x✝ : ↑X✝
h : ⟦x✝⟧ = x
⊢ (x✝².toFunctor ⋙ x✝¹.toFunctor).mapConnectedComponents x =
    x✝¹.toFunctor.mapConnectedComponents (x✝².toFunctor.mapConnectedComponents x)

Tactic:
by subst h; rfl

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih ↦
      Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
        (fun b' e ↦
          have e := ⋯;
          hbase a' ⋯)
        (fun a'' e ↦
          have e := ⋯;
          hind a' a'' ⋯ e (ih a'' e))
        ⋯) =
    hbase a fa

Tactic:
rw [fixInduction_spec]

Goal state after:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x ↦ (f a).get ⋯ = x → C a) ((f a).get ⋯)
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hbase a fa