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
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'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this✝¹ : (R ⋙ H).Final
this✝ :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙ StructuredArrow.map₂ u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom (inv iR.inv)))

Tactic:
rw [IsIso.Iso.inv_inv]

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
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'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this✝¹ : (R ⋙ H).Final
this✝ :
  StructuredArrow.map₂ u₂ iR.hom ≅
    StructuredArrow.post j₂ G R' ⋙ StructuredArrow.map₂ u₂ iR.hom ⋙ StructuredArrow.pre (L'.obj i₂) R H
this : (StructuredArrow.map₂ u₂ iR.hom).Final
⊢ IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ }.hom iR.hom))
Module: Mathlib.CategoryTheory.Limits.Indization.Equalizers

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v
inst✝ : HasLimit F
h : ∀ (j : WalkingParallelPair), IsIndObject (F.obj j)
⊢ IsIndObject (limit F)

Tactic:
obtain ⟨P⟩ := nonempty_indParallelPairPresentation (h WalkingParallelPair.zero)
      (h WalkingParallelPair.one) (F.map WalkingParallelPairHom.left)
      (F.map WalkingParallelPairHom.right)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
F : WalkingParallelPair ⥤ Cᵒᵖ ⥤ Type v
inst✝ : HasLimit F
h : ∀ (j : WalkingParallelPair), IsIndObject (F.obj j)
P : IndParallelPairPresentation (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)
⊢ IsIndObject (limit F)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = 0
this : f ≫ g = f ≫ 0
⊢ f ≫ g = 0

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
this : g ≫ f = 0 ≫ f
⊢ g ≫ f = 0

Tactic:
by simpa

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
X' : C
R' : InjectiveResolution X'
f : X ⟶ X'
φ : R.Hom R' f
n : ℤ
m : ℕ
h : ↑m = n
⊢ ComplexShape.embeddingUpNat.f m = n

Tactic:
by simpa

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ (J.ι.f 0 ≫ factorThru (f ≫ I.ι.f 0) (J.ι.f 0)) ≫ I.cocomplex.d 0 1 = 0

Tactic:
simp [assoc]

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 : ℕ
x y : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y

Tactic:
by
  have := HasDerivedCategory.standard C
  obtain ⟨x, rfl⟩ := x.mk_surjective
  obtain ⟨y, rfl⟩ := y.mk_surjective
  ext
  simp [← CohomologyClass.mk_add, extEquivCohomologyClass_symm_mk_hom, ShiftedHom.map]

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 : ℕ
x y : CohomologyClass R.cochainComplex ((singleFunctor C 0).obj Y) ↑n
⊢ R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y

Tactic:
by
  have := HasDerivedCategory.standard C
  obtain ⟨x, rfl⟩ := x.mk_surjective
  obtain ⟨y, rfl⟩ := y.mk_surjective
  ext
  simp [← CohomologyClass.mk_add, extEquivCohomologyClass_symm_mk_hom, ShiftedHom.map]

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 : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
x✝ : ∃ g, R.complex.d n p ≫ g = f
g : R.complex.X p ⟶ Y
hg : R.complex.d n p ≫ g = f
⊢ ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ R.complex.d n p ≫ (R.cochainComplexXIso (-↑p) p ⋯).inv) ≫
      (R.cochainComplexXIso (-↑p) p ⋯).hom ≫ g =
    (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f

Tactic:
by simpa

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 m : ℕ
hm : n + 1 = m
f : R.cochainComplex.X (-↑n) ⟶ Y
hf : R.cochainComplex.d (-↑m) (-↑n) ≫ f = 0
⊢ ∃ f_1,
    ∃ (hf_1 : R.complex.d m n ≫ f_1 = 0),
      R.extMk f_1 m hm hf_1 = R.extEquivCohomologyClass.symm (CohomologyClass.mk (Cocycle.toSingleMk f ⋯ (-↑m) ⋯ hf))

Tactic:
refine ⟨(R.cochainComplexXIso (-n) n rfl).inv ≫ f, ?_, by simp [extMk]⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n m : ℕ
hm : n + 1 = m
f : R.cochainComplex.X (-↑n) ⟶ Y
hf : R.cochainComplex.d (-↑m) (-↑n) ≫ f = 0
⊢ R.complex.d m n ≫ (R.cochainComplexXIso (-↑n) n ⋯).inv ≫ f = 0
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 : C
x✝ : P X
⊢ P.isoModSerre 0

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : HasKernels C
inst✝ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) P.ι

Tactic:
by
  have := P.createsKernels f
  have := P.hasLimit_parallelPair_comp_ι f
  exact preservesLimit_of_createsLimit_and_hasLimit _ _

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
W : C
s : W ⟶ X
hs : P.epiModSerre s
eq : s ≫ f ≫ z = 0
⊢ (s ≫ f) ≫ z = 0

Tactic:
by simpa

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

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
σ τ x : G
⊢ ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧

Tactic:
mul_inv_rev,

Goal state after:
case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
σ τ x : G
⊢ ⟦x * (τ⁻¹ * σ⁻¹)⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
n : G
hn : n ∈ N
a✝ : G
⊢ (a✝ * n⁻¹)⁻¹ * a✝ ∈ N

Tactic:
by simpa

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ ⟨n, g⟩ = inl n * inr g

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ inl x.left * inr x.right = x

Tactic:
by ext <;> simp

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

Goal state before:
pp: case refine_1
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✝ : Epi f✝
X Y : C
f : X ⟶ Y
hf : Epi (L.map f)
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))

Tactic:
epi_map_iff L P

Goal state after:
case refine_1
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✝ : Epi f✝
X Y : C
f : X ⟶ Y
hf : P.epiModSerre f
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
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✝ : Epi f
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Epi (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Epi f'),
          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
        let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
        obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.epimorphisms D).arrow_iso_iff e).2 (.infer_property f))
        exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩
    intro X Y f hf
    rw [epi_map_iff L P] at hf
    refine ⟨_, _, Abelian.factorThruImage f, inferInstance, ⟨?_⟩⟩
    have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_image_ι
    refine Arrow.isoMk (Iso.refl _) (asIso (L.map (Abelian.image.ι f))) (by simp [← L.map_comp])

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
⊢ (map fn fg h).comp inl = inl.comp fn

Tactic:
by ext <;> 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 : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a b : B
a' : C
f g : a ⟶ b
β : f ⟶ g
h : G.obj b ⟶ a'
⊢ F.map₂ β ▷ η.app b ▷ h ≫ η.naturality g ▷ h =
    η.naturality f ▷ h ≫ (α_ (η.app a) (G.map f) h).hom ≫ η.app a ◁ G.map₂ β ▷ h ≫ (α_ (η.app a) (G.map g) h).inv

Tactic:
rw [← comp_whiskerRight, naturality_naturality, comp_whiskerRight, whisker_assoc]

Goal state after:
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
⊢ (η.app a ◁ Γ.as.app a) ▷ H.map f ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ F.map f ◁ η.app b ◁ Γ.as.app b

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

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮 ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x✝ : ∫ F
⊢ (mapCompIso α β).hom.app x✝ = eqToHom ⋯

Tactic:
simp [mapCompIso]

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
β : G ⟶ H
x✝ : ∫ᶜ F
⊢ (mapCompIso α β).hom.app x✝ = eqToHom ⋯

Tactic:
simp [mapCompIso]

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
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := ⋯
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (ρ_ t.extension).inv ≫ rightZigzag t.unit ε = (ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv

Tactic:
apply H.hom_ext

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
t : LeftExtension f (𝟙 a)
H : t.IsKan
H' : (t.whisker f).IsKan
ε : t.extension ≫ f ⟶ 𝟙 b := ⋯
Hε : leftZigzag t.unit ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ rightZigzag t.unit ε) =
    t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)
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:
rw [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ε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ (λ_ t.lift).inv ≫ leftZigzag t.unit ε = (λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv

Tactic:
apply H.hom_ext

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ε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u
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:
rw [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.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 := ⋯
H' : (LeftLift.mk h η').IsAbsKan := ⋯
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := ⋯
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
⊢ (ρ_ t.extension).inv ≫ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
    (ρ_ t.extension).inv ≫
      (LeftLift.mk s'.extension
          ((ρ_ t.extension).hom ≫
            H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))).unit

Tactic:
apply H.hom_ext

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 := ⋯
H' : (LeftLift.mk h η').IsAbsKan := ⋯
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := ⋯
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
⊢ t.unit ≫
      f ◁ ((ρ_ t.extension).inv ≫ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u) =
    t.unit ≫
      f ◁
        ((ρ_ t.extension).inv ≫
          (LeftLift.mk s'.extension
              ((ρ_ t.extension).hom ≫
                H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))).unit)
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y Z : RelCat
⊢ opFunctor.IsEquivalence

Tactic:
change opEquivalence.functor.IsEquivalence

Goal state after:
X Y Z : RelCat
⊢ opEquivalence.functor.IsEquivalence
Module: Mathlib.CategoryTheory.Dialectica.Monoidal

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [tensorObjImpl, Subobject.inf_pullback]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ X₂ Y₁ Y₂ : Dial C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ≫ (∂R X Y Z).hom = coprod.inl ▷ X

Tactic:
rightDistrib_hom,

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inl ≫ coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X) = coprod.inl ▷ X
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inr ≫ (∂R X Y Z).hom = coprod.inr ▷ X

Tactic:
rightDistrib_hom,

Goal state after:
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : IsMonoidalRightDistrib C
X Y Z : C
⊢ coprod.inr ≫ coprod.desc (coprod.inl ▷ X) (coprod.inr ▷ X) = coprod.inr ▷ X
Module: Mathlib.CategoryTheory.Distributive.Monoidal

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : HasBinaryCoproducts C
inst✝ : MonoidalClosed C
X Y Z : C
⊢ (∂L X Y Z).inv = uncurry (coprod.desc (curry coprod.inl) (curry coprod.inr))

Tactic:
by
  rw [← curry_eq_iff]
  ext <;> simp [← curry_natural_left]

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
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
h : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ (g₁ ≫ c.ι.app { as := a₁ }) ≫ hc.desc (Cofan.mk B π) = (g₂ ≫ c.ι.app { as := a₂ }) ≫ hc.desc (Cofan.mk B π)

Tactic:
by simpa

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✝ : EffectiveEpiFamily X π
⊢ EffectiveEpi (Sigma.desc π)

Tactic:
by
  let e := effectiveEpiStructIsColimitDescOfEffectiveEpiFamily X _ (coproductIsCoproduct _) π
  simp only [Cofan.mk_pt, coproductIsCoproduct, colimit.cocone_x, IsColimit.ofIsoColimit_desc,
    Cocone.ext_inv_hom, Iso.refl_inv, colimit.isColimit_desc, Category.id_comp] at e
  exact ⟨⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X R : Type w
p₁ p₂ : R ⟶ X
e : SymmetricRelation p₁ p₂
x₁ x₂ : X
x✝ : Rel.ofPair p₁ p₂ x₁ x₂
r : R
hr₁ : (ConcreteCategory.hom p₁) r = x₁
hr₂ : (ConcreteCategory.hom p₂) r = x₂
⊢ (ConcreteCategory.hom p₁) ((ConcreteCategory.hom e.s) r) = x₂

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X R : Type w
p₁ p₂ : R ⟶ X
e : SymmetricRelation p₁ p₂
x₁ x₂ : X
x✝ : Rel.ofPair p₁ p₂ x₁ x₂
r : R
hr₁ : (ConcreteCategory.hom p₁) r = x₁
hr₂ : (ConcreteCategory.hom p₂) r = x₂
⊢ (ConcreteCategory.hom p₂) ((ConcreteCategory.hom e.s) r) = x₁

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
S : 𝒮
ha : 𝒳.p.obj a = S
⊢ 𝒴.p.IsHomLift (𝟙 S) (α.app a)

Tactic:
by
  subst ha; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₂
inst✝ : HasEnrichedHom V F₂ F₂
⊢ (ρ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedHom V F₁ F₂ ◁ enrichedId V F₂ ≫ enrichedComp V F₁ F₂ F₂ =
    𝟙 (enrichedHom V F₁ F₂)

Tactic:
by
  ext j
  rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def', assoc,
    ← MonoidalCategory.whiskerLeft_comp_assoc, enrichedId_π,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id, assoc, assoc,
    Iso.inv_hom_id_assoc]
  dsimp
  rw [e_comp_id, comp_id]

Goal state after: