mathlib-initiative/mathlib-tactics huggingface dataset:
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
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
⊢ ∀ (R : D) (g : L.obj Y ⟶ R), L.map f ≫ g = 0 → g = 0

Tactic:
intro W

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.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
⊢ ∀ (g : L.obj Y ⟶ W), L.map f ≫ g = 0 → g = 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 Y : C
f : X ⟶ Y
this✝ : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
this : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s
⊢ 0 ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = 0

Tactic:
zero_comp

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.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
W : D
z : L.obj Y ⟶ W
hz : L.map f ≫ z = 0
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : z ≫ (L.objObjPreimageIso W).inv = φ.map L ⋯
this : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s
⊢ 0 = 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 Y : C
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.EssSurj
⊢ ∀ (W : D) (z : W ⟶ L.obj X), z ≫ L.map f = 0 → ∃ l, l ≫ L.map (kernel.ι f) = z

Tactic:
intro W

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
⊢ ∀ (z : W ⟶ L.obj X), z ≫ L.map f = 0 → ∃ l, l ≫ L.map (kernel.ι f) = z
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.PreservesEpimorphisms
this : L.EssSurj
⊢ ∀ (W : D) (z : L.obj Y ⟶ W), L.map f ≫ z = 0 → ∃ l, L.map (cokernel.π f) ≫ l = z

Tactic:
intro W

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.PreservesEpimorphisms
this : L.EssSurj
W : D
⊢ ∀ (z : L.obj Y ⟶ W), L.map f ≫ z = 0 → ∃ l, L.map (cokernel.π f) ≫ l = z
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.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
⊢ 0 ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = 0

Tactic:
zero_comp

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.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
⊢ 0 = 0
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
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (b : X ⟶ Y), 1 • b = b

Tactic:
intros; ext; exact one_smul _ _

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
⊢ PreservesFiniteColimits (L ⋙ G) ↔ PreservesFiniteColimits G

Tactic:
let := abelian L P
  have := preservesFiniteColimits L P
  refine ⟨fun _ ↦ ?_, fun _ ↦ comp_preservesFiniteColimits _ _⟩
  have := (Localization.functor_additive_iff L P.isoModSerre G).mpr (by
    have := preservesBinaryBiproducts_of_preservesBinaryCoproducts (L ⋙ G)
    exact Functor.additive_of_preservesBinaryBiproducts _)
  refine ((Functor.preservesFiniteColimits_tfae G).out 2 3).mp (fun _ _ f ↦ ?_)
  obtain ⟨f', ⟨iso⟩⟩ :=
    (Localization.essSurj_mapArrow L P.isoModSerre).mem_essImage (Arrow.mk f)
  have : PreservesColimit (parallelPair (L.map f'.hom) 0) G :=
    preservesColimit_of_preserves_colimit_cocone
      (CokernelCofork.isColimitMapCoconeEquiv _ _
        (isColimitOfPreserves L (cokernelIsCokernel f'.hom)))
          ((CokernelCofork.isColimitMapCoconeEquiv _ G).symm
            (CokernelCofork.isColimitMapCoconeEquiv _ (L ⋙ G)
              (isColimitOfPreserves (L ⋙ G) (cokernelIsCokernel f'.hom))))
  exact preservesColimit_of_iso_diagram G
    (show parallelPair (L.map f'.hom) 0 ≅ parallelPair f 0 from
      parallelPair.ext (Arrow.leftFunc.mapIso iso) (Arrow.rightFunc.mapIso iso))

Goal state after:
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
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint :=
  Adjunction.isLeftAdjoint
    ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft
      (L.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction F)).symm))
X : (comonadicAdjunction F).toComonad.Coalgebra
⊢ RegularMono ((comonadicAdjunction F).toComonad.adj.unit.app X)

Tactic:
simp only [Comonad.adj_unit]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint :=
  Adjunction.isLeftAdjoint
    ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft
      (L.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction F)).symm))
X : (comonadicAdjunction F).toComonad.Coalgebra
⊢ RegularMono { f := X.a, h := ⋯ }
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 : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (t.adj₂.unit.app (F.obj X))

Tactic:
rw [← leftToRight_app_map_adj₁_unit_app, mono_comp_iff_of_mono]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ≅ t
x : B
h : c ⟶ x
⊢ StructuredArrow.Hom.right (i.inv ≫ i.hom) ▷ h = 𝟙 (StructuredArrow.right t ≫ h)

Tactic:
by simp [Iso.inv_hom_id]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ h ◁ StructuredArrow.Hom.right (i.inv ≫ i.hom) = 𝟙 (h ≫ StructuredArrow.right t)

Tactic:
by simp [Iso.inv_hom_id]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ h ◁ (i.inv ≫ i.hom).left = 𝟙 (h ≫ t.left)

Tactic:
by simp [Iso.inv_hom_id]

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      η.app a ◁ (θ.app a ◁ H.mapId a ≫ θ.naturality (𝟙 a)) ⊗≫
        η.naturality (𝟙 a) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a)

Tactic:
by
      rw [naturality_id]
      bicategory

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : LaxTrans F G
θ : LaxTrans G H
a : B
⊢ 𝟙 (η.vCompApp θ a ≫ 𝟙 (H.obj a)) ⊗≫
      (η.app a ◁ G.mapId a ≫ η.naturality (𝟙 a)) ▷ θ.app a ⊗≫ 𝟙 (F.map (𝟙 a) ≫ η.app a ≫ θ.app a) =
    (ρ_ (η.vCompApp θ a)).hom ≫ (λ_ (η.vCompApp θ a)).inv ≫ F.mapId a ▷ η.vCompApp θ a

Tactic:
by
      rw [naturality_id]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

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
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫
      (α_ (F.map f) (η.app b) (ι.app b)).inv ≫
        η.naturality f ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫ η.app a ◁ ι.naturality f ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        η.naturality f ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫ η.app a ◁ θ.naturality f ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f

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

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

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮 ⥤ᵖ Cat
a b : ∫ F
f : a ⟶ b
⊢ eqToHom ⋯ ≫ (𝟙 a ≫ f).fiber = f.fiber

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

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

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

Tactic:
simp [mapIdIso]

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
⊢ 𝟙 a ≫ f = f

Tactic:
by
    ext
    · simp
    · simp [F.mapComp_id_right_inv_app, Strict.rightUnitor_eqToIso, ← NatTrans.naturality_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 : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ (f ≫ 𝟙 b).fiber = f.fiber ≫ eqToHom ⋯

Tactic:
· 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: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
x : ∫ᶜ F
⊢ (mapIdIso F).hom.app x = eqToHom ⋯

Tactic:
simp [mapIdIso]

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 : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
⊢ adj.unit ▷ h ⊗≫ f ◁ τ = s.unit

Tactic:
simpa [bicategoricalComp] using LeftExtension.w τ₀

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.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ rightZigzag t.unit ε) =
    t.unit ≫ f ◁ ((ρ_ t.extension).inv ≫ (ρ_ t.extension).hom ≫ (λ_ t.extension).inv)

Tactic:
calc _
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ f ◁ rightZigzag t.unit ε ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ (t.unit ▷ _ ≫ _ ◁ t.unit) ⊗≫ f ◁ ε ▷ t.extension ⊗≫ 𝟙 _ := by
          rw [rightZigzag]; bicategory
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ (t.unit ▷ f ⊗≫ f ◁ ε) ▷ t.extension ⊗≫ 𝟙 _ := by
          rw [← whisker_exchange]; bicategory
        _ = _ := by
          rw [← leftZigzag, Hε]; bicategory

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

Goal state before:
pp: case refine_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (𝟙 X✝ ≫ f✝) x✝ = f✝ x✝

Tactic:
simp +unfoldPartialApp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]

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

Goal state before:
pp: case refine_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x✝ : X✝
⊢ (f✝ ≫ 𝟙 Y✝) x✝ = f✝ x✝

Tactic:
simp +unfoldPartialApp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]

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

Goal state before:
pp: case refine_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
x✝ : W✝
⊢ ((f✝ ≫ g✝) ≫ h✝) x✝ = (f✝ ≫ g✝ ≫ h✝) x✝

Tactic:
simp +unfoldPartialApp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]

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

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ (∃ a_1 ∈ (PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val) ⟨a, ha⟩,
      ⟨c, hc⟩ ∈ (PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val) a_1) →
    ↑⟨c, hc⟩ = (f ≫ g).toFun ↑⟨a, ha⟩

Tactic:
by simp; grind

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
⊢ C a'

Tactic:
rcases e : (f a').get (dom_of_mem_fix h) with b' | a''

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
b' : β
e : (f a').get ⋯ = Sum.inl b'
⊢ C a'

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : (f a').get ⋯ = Sum.inr a''
⊢ C a'
Module: Mathlib.CategoryTheory.Limits.Shapes.End

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
C : Type u'
inst✝² : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝¹ : HasEnd F
X : C
f✝ : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f✝ i ≫ (F.obj (op i)).map g = f✝ j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
⊢ (π F j ≫ (f.app (op j)).app j) ≫ (F'.obj (op j)).map φ = (π F j' ≫ (f.app (op j')).app j') ≫ (F'.map φ.op).app j'

Tactic:
by
    have e := (f.app (op j)).naturality φ
    simp only [Category.assoc]
    rw [← e, reassoc_of% end_.condition F φ]
    simp

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ (λ_ Y).hom =
    L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y

Tactic:
simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, comp_id, id_comp,
    ← tensor_comp_assoc, id_comp]

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ (λ_ Y).hom =
    e₁.hom ⊗ₘ ((ε' L W ε).hom ≫ 𝟙 (𝟙_ (LocalizedMonoidal L W ε)) ⊗ₘ e₂.hom) ≫ (λ_ Y).hom
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X : Type w
φ : X → X → Prop
Y : Type w
f g : Y ⟶ ROfRel φ
h₁ : f ≫ p₁OfRel φ = g ≫ p₁OfRel φ
h₂ : f ≫ p₂OfRel φ = g ≫ p₂OfRel φ
⊢ f = g

Tactic:
by
    ext y
    · exact congr($h₁ y)
    · exact congr($h₂ y)

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
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₂ F₃) i ≫
      (ρ_ (F₂.obj i ⟶[V] F₃.obj i)).inv ≫
        (F₂.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₂.obj i) (F₃.obj i) (F₃.obj j) =
    end_.π (diagram V F₂ F₃) j ≫
      (λ_ (F₂.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₂.map f) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₂.obj i) (F₂.obj j) (F₃.obj j)
⊢ end_.π (diagram V F₁ F₂) i ▷ enrichedHom V F₂ F₃ ≫
      (F₁.obj i ⟶[V] F₂.obj i) ◁ end_.π (diagram V F₂ F₃) i ≫
        eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i) ≫
          (ρ_ (F₁.obj i ⟶[V] F₃.obj i)).inv ≫
            (F₁.obj i ⟶[V] F₃.obj i) ◁ (eHomEquiv V) (F₃.map f) ≫ eComp V (F₁.obj i) (F₃.obj i) (F₃.obj j) =
    (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      ((ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
        (((F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f)) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
          (eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) ▷ F₂.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₂.obj j) (F₃.obj j)

Tactic:
conv_rhs =>
        rw [tensorHom_def_assoc, whisker_assoc_assoc, e_assoc,
          triangle_assoc_comp_right_inv_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          ← MonoidalCategory.whiskerLeft_comp_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
          assoc, assoc, ← this, MonoidalCategory.whiskerLeft_comp_assoc,
          MonoidalCategory.whiskerLeft_comp_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
          ← e_assoc, whiskerLeft_rightUnitor_inv_assoc, associator_inv_naturality_right_assoc,
          Iso.hom_inv_id_assoc, whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc,
          Iso.inv_hom_id_assoc]

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

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

Tactic:
let ψ := pullbackMap (domain_eq p f φ) g
    -- Let `τ` be the map induced by the universal property of `ψ ≫ φ`.
    let τ := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
    use τ ≫ ψ
    -- It is easily verified that `τ ≫ ψ` lifts `g` and `τ ≫ ψ ≫ φ = φ'`
    refine ⟨⟨inferInstance, by simp only [assoc, IsCartesian.fac, τ]⟩, ?_⟩
    -- It remains to check that `τ ≫ ψ` is unique.
    -- So fix another lift `π` of `g` satisfying `π ≫ φ = φ'`.
    intro π ⟨hπ, hπ_comp⟩
    -- Write `π` as `π = τ' ≫ ψ` for some `τ'` induced by the universal property of `ψ`.
    rw [← fac p g ψ π]
    -- It remains to show that `τ' = τ`. This follows again from the universal property of `ψ`.
    congr 1
    apply map_uniq
    rwa [← assoc, IsCartesian.fac]

Goal state after: