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

Goal state before:
pp: case base
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ ∃ a, FilteredClosureSmall.abstractFilteredClosureRealization f a = { obj := f x, property := ⋯ }.obj

Tactic:
refine ⟨⟨0, ?_⟩, ?_⟩

Goal state after:
case base.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ (FilteredClosureSmall.bundledAbstractFilteredClosure f 0).fst

case base.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
x : α
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f ⟨0, ?base.refine_1⟩ = { obj := f x, property := ⋯ }.obj
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case e'_3.e'_6
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ ↑M + ↑N = ↑(N + M)

Tactic:
grind [anti.mono]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case convert_4
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ N ≤ N + M

Tactic:
grind [anti.mono]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case convert_5
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
M : ℕ
⊢ AntitoneOn f (Icc ↑N ↑(N + M))

Tactic:
grind [anti.mono]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda ⋙ (evaluation Cᵒᵖ (Type u)).obj (limit K)) i ≫
        (HasColimit.isoOfNatIso (isoAux A K)).hom ≫
          (HasColimit.isoOfNatIso
                (preservesLimitIso
                  (coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                  K)).hom ≫
            (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom ≫
              (colimitLimitIso (functorToInterchange A K)).hom ≫
                limit.π (colimit (functorToInterchange A K).flip) j ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j

Tactic:
HasColimit.isoOfNatIso_ι_hom_assoc,

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (isoAux A K).hom.app i ≫
        colimit.ι (CostructuredArrow.proj yoneda A ⋙ coyoneda.obj (limit K)) i ≫
          (HasColimit.isoOfNatIso
                (preservesLimitIso
                  (coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                  K)).hom ≫
            (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom ≫
              (colimitLimitIso (functorToInterchange A K)).hom ≫
                limit.π (colimit (functorToInterchange A K).flip) j ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (isoAux A K).hom.app i ≫
        colimit.ι (CostructuredArrow.proj yoneda A ⋙ coyoneda.obj (limit K)) i ≫
          (HasColimit.isoOfNatIso
                (preservesLimitIso
                  (coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                  K)).hom ≫
            (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom ≫
              (colimitLimitIso (functorToInterchange A K)).hom ≫
                limit.π (colimit (functorToInterchange A K).flip) j ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j

Tactic:
HasColimit.isoOfNatIso_ι_hom_assoc,

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (isoAux A K).hom.app i ≫
        (preservesLimitIso
                  (coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                  K).hom.app
            i ≫
          colimit.ι
              (limit
                (K ⋙
                  coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)))
              i ≫
            (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom ≫
              (colimitLimitIso (functorToInterchange A K)).hom ≫
                limit.π (colimit (functorToInterchange A K).flip) j ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (isoAux A K).hom.app i ≫
        (preservesLimitIso
                  (coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                  K).hom.app
            i ≫
          colimit.ι
              (limit
                (K ⋙
                  coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)))
              i ≫
            (HasColimit.isoOfNatIso (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm)).hom ≫
              (colimitLimitIso (functorToInterchange A K)).hom ≫
                limit.π (colimit (functorToInterchange A K).flip) j ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j

Tactic:
HasColimit.isoOfNatIso_ι_hom_assoc,

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (isoAux A K).hom.app i ≫
        (preservesLimitIso
                  (coyoneda ⋙
                    (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A))
                  K).hom.app
            i ≫
          (HasLimit.isoOfNatIso (functorToInterchangeIso A K).symm).hom.app i ≫
            colimit.ι (limit (functorToInterchange A K)) i ≫
              (colimitLimitIso (functorToInterchange A K)).hom ≫
                limit.π (colimit (functorToInterchange A K).flip) j ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom.app j ≫
                    (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
                      (K.isoWhiskerLeft
                              ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                                (Presheaf.isColimitTautologicalCocone A))).hom.app
                        j
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)
⊢ IsZero (Ψ.r.obj (Φ.quotient.obj X))

Tactic:
exact IsZero.of_epi_eq_zero ((colonπ Φ Ψ).app X)
      (zero_of_epi_comp ((toColon Φ Ψ).hom.left.app X) (by simp))

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✝ : P.IsClosedUnderSubobjects
i✝ X₁✝ X₂✝ : C
f✝ : X₁✝ ⟶ X₂✝
k : KernelFork f✝
hk : IsLimit k
hf : MorphismProperty.ofObjectProperty P P f✝
⊢ P k.pt

Tactic:
let := Fork.IsLimit.mono hk

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderSubobjects
i✝ X₁✝ X₂✝ : C
f✝ : X₁✝ ⟶ X₂✝
k : KernelFork f✝
hk : IsLimit k
hf : MorphismProperty.ofObjectProperty P P f✝
this : Mono (Fork.ι k) := Fork.IsLimit.mono hk
⊢ P k.pt
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
⊢ [Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0].TFAE

Tactic:
by
  have := Localization.essSurj L P.isoModSerre
  tfae_have 1 → 2 := fun _ ↦ by
    have hf : L.map (cokernel.π f) = 0 := by
      rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]
    simpa [hf] using! map_comp_eq_zero_iff_of_epi_mono L P (cokernel.π f) (𝟙 _)
  tfae_have 2 → 3 := fun hf ↦ by
    intro Z z hz
    rw [← L.map_comp] at hz
    rw [map_eq_zero_iff L P, ← exists_epiModSerre_comp_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    refine ⟨_, s ≫ f, MorphismProperty.comp_mem _ _ _ hs hf, by simpa⟩
  tfae_have 3 → 1 := fun hf ↦ by
    rw [Preadditive.epi_iff_cancel_zero]
    intro W z hz
    obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.isoModSerre
      (z ≫ (L.objObjPreimageIso W).inv)
    rw [← cancel_mono (L.objObjPreimageIso W).inv, zero_comp, hφ,
      ← cancel_mono (L.map φ.s), zero_comp,
      MorphismProperty.LeftFraction.map_comp_map_s]
    apply hf φ.f
    have : L.map φ.f = z ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s := by
      simp [reassoc_of% hφ]
    rw [this, reassoc_of% hz, zero_comp]
  tfae_finish

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
F : N ⋊[φ] G →* H
x✝ : G
⊢ (F.comp inl).comp (MulEquiv.toMonoidHom (φ x✝)) =
    (MulEquiv.toMonoidHom (MulAut.conj ((F.comp inr) x✝))).comp (F.comp inl)

Tactic:
ext; simp [inl_aut]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)

Tactic:
ext
    dsimp
    rw [← Functor.map_comp, X.unit, Functor.map_id]

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

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.Monoidal
⊢ ε (F.mapAction G) ≫ η (F.mapAction G) = 𝟙 (𝟙_ (Action W G))

Tactic:
by ext; dsimp; rw [ε_η]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

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

Tactic:
rw [← ((q.adj₂.homEquiv _ _).trans (q.adj₃.homEquiv _ _)).comp_injective _]

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

Goal state before:
pp: case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
η' : Hom₂ f g
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
clear η

Goal state after:
case mk
B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η' : Hom₂ f g
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    Quot.map (Hom₂.whisker_right (g ≫ h)) ⋯ η =
      { hom := Quot.mk Rel (Hom₂.associator f g h), inv := Quot.mk Rel (Hom₂.associator_inv f g h), hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.inv ≫
        Quot.map (Hom₂.whisker_right h) ⋯ (Quot.map (Hom₂.whisker_right g) ⋯ η) ≫
          { hom := Quot.mk Rel (Hom₂.associator f' g h), inv := Quot.mk Rel (Hom₂.associator_inv f' g h),
              hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom

Tactic:
rintro a b c d f f' ⟨η⟩ g h
    exact Quot.sound (Rel.whisker_right_comp g h η)

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : B
f : Discrete (Path a b)
⊢ (inclusionPath a b ⋙ (normalize B).mapFunctor a b).obj f = (𝟭 (Discrete (Path a b))).obj f

Tactic:
obtain ⟨f⟩ := f

Goal state after:
B : Type u
inst✝ : Quiver B
a b : B
f : Path a b
⊢ (inclusionPath a b ⋙ (normalize B).mapFunctor a b).obj { as := f } = (𝟭 (Discrete (Path a b))).obj { as := f }
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 c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        (η.app a ◁ G.mapComp f g ≫ η.naturality (f ≫ g)) ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)

Tactic:
rw [naturality_comp η]

Goal state after:
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 c : B
f : a ⟶ b
g : b ⟶ c
⊢ 𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ (θ.naturality f ▷ H.map g ⊗≫ G.map f ◁ θ.naturality g) ⊗≫
        ((α_ (η.app a) (G.map f) (G.map g)).inv ≫
              η.naturality f ▷ G.map g ≫
                (α_ (F.map f) (η.app b) (G.map g)).hom ≫
                  F.map f ◁ η.naturality g ≫ (α_ (F.map f) (F.map g) (η.app c)).inv ≫ F.mapComp f g ▷ η.app c) ▷
            θ.app c ⊗≫
          𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c) =
    𝟙 (η.vCompApp θ a ≫ H.map f ≫ H.map g) ⊗≫
      η.app a ◁ θ.naturality f ▷ H.map g ⊗≫
        ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
          F.map f ◁ η.naturality g ▷ θ.app c ⊗≫
            F.mapComp f g ▷ η.app c ▷ θ.app c ⊗≫ 𝟙 (F.map (f ≫ g) ≫ η.app c ≫ θ.app c)
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 : ∫ᶜ F
⊢ { base := (𝟙 a).base,
        fiber :=
          (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
            (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber }.fiber =
    (𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }).fiber ≫ eqToHom ⋯

Tactic:
simp [Cat.Hom.comp_toFunctor, naturality_id_hom_app, Cat.Hom.id_toFunctor, ← Category.assoc,
        ← Functor.map_comp, ← Cat.Hom₂.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str

Tactic:
simp only [Iso.hom_inv_id, Functor.map_id, Category.comp_id]

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 : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ p.IsHomLift g (τ' ≫ Φ.hom)

Tactic:
by simp only [Φ]; infer_instance

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

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ' ≫ φ = 𝟙 b

Tactic:
have h₁ : IsHomLift p (𝟙 (p.obj b)) (φ' ≫ φ) := by
    rw [← IsIso.inv_hom_id (p.map φ)]
    apply IsHomLift.comp

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCocartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ' ≫ φ = 𝟙 b
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: C : Type u_1
C' : Type ?u.4
D : Type u_2
D' : Type ?u.8
H : Type u_3
H' : Type ?u.12
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, ?u.4} C'
inst✝⁵ : Category.{v_3, u_2} D
inst✝⁴ : Category.{v_4, ?u.8} D'
inst✝³ : Category.{v_5, u_3} H
inst✝² : Category.{v_6, ?u.12} H'
LF'' LF' LF : D ⥤ H
F F' F'' : C ⥤ H
e : F ≅ F'
L : C ⥤ D
α'' : L ⋙ LF'' ⟶ F''
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
α'₂ : L ⋙ LF' ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : F.HasLeftDerivedFunctor W
⊢ (F.totalLeftDerived L W).IsRightKanExtension (F.totalLeftDerivedCounit L W)

Tactic:
dsimp [totalLeftDerived, totalLeftDerivedCounit]

Goal state after:
C : Type u_1
C' : Type ?u.4
D : Type u_2
D' : Type ?u.8
H : Type u_3
H' : Type ?u.12
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, ?u.4} C'
inst✝⁵ : Category.{v_3, u_2} D
inst✝⁴ : Category.{v_4, ?u.8} D'
inst✝³ : Category.{v_5, u_3} H
inst✝² : Category.{v_6, ?u.12} H'
LF'' LF' LF : D ⥤ H
F F' F'' : C ⥤ H
e : F ≅ F'
L : C ⥤ D
α'' : L ⋙ LF'' ⟶ F''
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
α'₂ : L ⋙ LF' ⟶ F
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : F.HasLeftDerivedFunctor W
⊢ (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)
Module: Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan f₁
c₂ : Fan f₂
bc : BinaryFan c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
w : ι₁ ⊕ ι₂
⊢ (IsLimit.lift h fun i ↦
        WalkingPair.casesOn (motive := fun t ↦ i = t → (s.pt ⟶ WalkingPair.casesOn i c₁.pt c₂.pt)) i
          (fun h ↦ ⋯ ▸ IsLimit.lift h₁ fun a ↦ s.proj (Sum.inl a))
          (fun h ↦ ⋯ ▸ IsLimit.lift h₂ fun a ↦ s.proj (Sum.inr a)) ⋯) ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj w =
    s.proj w

Tactic:
by
      cases w <;>
      · simp only [fan_mk_proj, combPairHoms]
        erw [← Category.assoc, h.fac]
        simp only [pair_obj_left, mk_π_app, IsLimit.fac]

Goal state after: