mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑n
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∫ (x : ℝ) in Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)

Tactic:
rw [← summable_nat_add_iff N] at summable

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∫ (x : ℝ) in Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ (J : ι → Type w) [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [inst_2 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct F)), IsIso (colimitPointwiseProductToProductColimit F)
⊢ IsIPCOfShape.{w, u_2, v_1, u_1} ι C

Tactic:
refine .of_forall_exists fun J _ _ F _ ↦ ?_
  refine ⟨fun i ↦ colimit.cocone _, fun i ↦ colimit.isColimit _, ?_⟩
  obtain ⟨_, h⟩ := H J F
  rwa [IsColimit.nonempty_isColimit_iff_isIso_desc (colimit.isColimit _)]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
h :
  ∃ l,
    d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
      d (ModuleCat.ofHom g)
⊢ ∃ g', ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M), g' x = g ⟨x, mem⟩

Tactic:
obtain ⟨l, hl⟩ := h

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
l : G ⟶ B
hl :
  d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
    d (ModuleCat.ofHom g)
⊢ ∃ g', ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M), g' x = g ⟨x, mem⟩
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
X' : C
R' : ProjectiveResolution X'
f : X ⟶ X'
φ : R.Hom R' f
⊢ (φ.hom' ≫ R'.π').f 0 = (R.π' ≫ (CochainComplex.singleFunctor C 0).map f).f 0

Tactic:
by
    simp [hom'_f _ 0 0 rfl, π'_f_zero, CochainComplex.singleFunctor,
      CochainComplex.singleFunctors,
      HomologicalComplex.single, HomologicalComplex.singleObjXSelf,
      HomologicalComplex.singleObjXIsoOfEq]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ : Preradical C
X : C
⊢ Φ.ι.app X ≫ Φ.π.app X = 0

Tactic:
by
  simp [← NatTrans.comp_app]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f 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.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯

Tactic:
by
  simp only [extMk, Preadditive.add_comp]
  rw [Cocycle.fromSingleMk_add _ _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hg])]
  simp

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 g : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
hg : R.complex.d m n ≫ g = 0
⊢ R.extMk f m hm hf - R.extMk g m hm hg = R.extMk (f - g) m hm ⋯

Tactic:
by
  simp only [extMk, Preadditive.comp_sub]
  rw [Cocycle.toSingleMk_sub _ _ _ _ _
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])
    (by simpa [cochainComplex_d _ _ _ m n rfl rfl])]
  simp

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
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.rightDerivedToHomotopyCategory.map f ≫ (J.isoRightDerivedToHomotopyCategoryObj F).hom =
    (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ

Tactic:
dsimp [Functor.rightDerivedToHomotopyCategory, isoRightDerivedToHomotopyCategoryObj]
  rw [← Functor.map_comp_assoc, iso_hom_naturality f I J φ comm, Functor.map_comp,
    assoc, assoc]
  erw [(F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.naturality]
  rfl

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.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.f
⊢ L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w ≫ L.map f = 0

Tactic:
hw,

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

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
this : Continuous v
u : H × ↑((forget₂ (ContAction V H) TopCat).obj X) → ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.obj.ρ p.1))) p.2
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
have : Continuous u := X.2.1

Goal state after:
V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
this✝ : Continuous v
u : H × ↑((forget₂ (ContAction V H) TopCat).obj X) → ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.obj.ρ p.1))) p.2
this : Continuous u
⊢ Continuous fun p ↦ p.1 • p.2
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b), ⋯.hom ≫ ⋯.hom = s.inl

Tactic:
intros; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b), ⋯.hom ≫ ⋯.hom = s.inr

Tactic:
intros; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
⊢ ∀ (s : BinaryCofan a b) (m : Subobject.mk (pushout.desc a.arrow b.arrow ⋯) ⟶ s.pt),
    ⋯.hom ≫ m = s.inl → ⋯.hom ≫ m = s.inr → m = ⋯.hom

Tactic:
intros; rfl

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
⊢ IsIso t.adj₁.unit ↔ IsIso t.adj₂.counit

Tactic:
let adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
  constructor
  · intro h
    let idAdj : 𝟭 C ⊣ H ⋙ G := adj.ofNatIsoLeft (asIso t.adj₁.unit).symm
    exact t.adj₂.isIso_counit_of_iso (idAdj.rightAdjointUniq id)
  · intro h
    let adjId : F ⋙ G ⊣ 𝟭 C := adj.ofNatIsoRight (asIso t.adj₂.counit)
    exact t.adj₁.isIso_unit_of_iso (adjId.leftAdjointUniq id)

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

Tactic:
by
          rw [whisker_exchange]
          bicategory

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

Tactic:
by
          rw [whisker_exchange]
          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
F G : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
a : B
a' : C
f : G.obj a ⟶ a'
⊢ η.naturality (𝟙 a) ▷ f ≫ (α_ (η.app a) (G.map (𝟙 a)) f).hom ≫ η.app a ◁ G.mapId a ▷ f =
    F.mapId a ▷ η.app a ▷ f ≫ (λ_ (η.app a)).hom ▷ f ≫ (ρ_ (η.app a)).inv ▷ f ≫ (α_ (η.app a) (𝟙 (G.obj a)) f).hom

Tactic:
by
  rw [← associator_naturality_middle, ← comp_whiskerRight_assoc, naturality_id]; simp

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

Tactic:
by
          rw [whisker_exchange]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ : B
f : b₀ ⟶ b₁
⊢ F.mapComp' (𝟙 b₀) f f ⋯ = (λ_ (F.map f)).symm ≪≫ (F.mapId b₀).symm ▷ᵢ F.map f

Tactic:
by
  ext
  rw [mapComp']
  dsimp
  rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
    ← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
    Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
⊢ (F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯).hom =
    (F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯).hom ≫
      (F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯).hom ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
simp [mapComp_assoc_right_hom, Strict.associator_eqToIso, mapComp']

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
⊢ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ ≫ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯

Tactic:
have := F.map₂_associator f₀₁ f₁₂ f₂₃

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
this :
  F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.map₂ (α_ f₀₁ f₁₂ f₂₃).hom =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃)
⊢ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ ≫ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
⊢ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ =
    F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom

Tactic:
have := F.map₂_associator f₀₁ f₁₂ f₂₃

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
this :
  F.map₂ (α_ f₀₁ f₁₂ f₂₃).hom ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃) ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ =
    F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
⊢ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ ≫ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ =
    F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
⊢ f.preimage Set.univ = f.Dom

Tactic:
by ext; simp [mem_preimage, mem_dom]

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y : limit (F ⋙ objects)
X : J
f : (hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y
this : Category.{v, v} (objects.obj (F.obj X)) := inferInstance
⊢ (hom (↾fun g ↦ eqToHom ⋯ ≫ (F.map (𝟙 X)).toFunctor.map g ≫ eqToHom ⋯)).toFun f =
    (hom (𝟙 ((hom (limit.π (F ⋙ objects) X)) X✝ ⟶ (hom (limit.π (F ⋙ objects) X)) Y))).toFun f

Tactic:
simp [Functor.congr_hom congr($(F.map_id X).toFunctor) f]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.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✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
⊢ L.Final

Tactic:
let R' := sB.inverse ⋙ R ⋙ sT.functor

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✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
⊢ L.Final
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 (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y

Tactic:
obtain ⟨X', ⟨e₁⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ X) := ⟨_, ⟨(L').objObjPreimageIso 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
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' : C
e₁ : L'.obj X' ≅ X
⊢ (α_ X (𝟙_ (LocalizedMonoidal L W ε)) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁶ : Category.{v₂, u₂} H
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
F : C ⥤ Cat
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
⊢ PreservesLimitsOfShape J colim

Tactic:
constructor
  intro K
  let i₂ := calc colimit (limit K)
    _ ≅ colimit (fiberwiseColimit (limit K)) := (colimitFiberwiseColimitIso _).symm
    _ ≅ colimit (limit (K ⋙ fiberwiseColim _ _)) :=
          HasColimit.isoOfNatIso (fiberwiseColimitLimitIso _)
    _ ≅ limit ((K ⋙ fiberwiseColim _ _) ⋙ colim) :=
          preservesLimitIso colim (K ⋙ fiberwiseColim _ _)
    _ ≅ limit (K ⋙ colim) :=
      HasLimit.isoOfNatIso
       (associator _ _ _ ≪≫ isoWhiskerLeft _ fiberwiseColimCompColimIso)
  have : IsIso (limit.post K colim) := by
    convert! Iso.isIso_hom i₂
    ext
    simp only [colim_obj, Functor.comp_obj, limit.post_π, colim_map, Iso.trans_def,
      Iso.trans_assoc, Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π,
      fiberwiseColim_obj, isoWhiskerLeft_hom, NatTrans.comp_app, Functor.associator_hom_app,
      whiskerLeft_app, fiberwiseColimCompColimIso_hom_app, Category.id_comp,
      preservesLimitIso_hom_π_assoc, i₂]
    ext
    simp only [ι_colimMap, Trans.trans, Iso.symm_hom, ι_colimitFiberwiseColimitIso_inv_assoc,
      HasColimit.isoOfNatIso_ι_hom_assoc, fiberwiseColimit_obj, fiberwiseColimitLimitIso_hom_app,
      ι_colimMap_assoc, Category.assoc, limitObjIsoLimitCompEvaluation_inv_π_app_assoc,
      Functor.comp_obj, fiberwiseColim_obj, HasLimit.isoOfNatIso_hom_π_assoc,
      whiskeringLeft_obj_obj, colim_obj, evaluation_obj_obj, Iso.trans_hom, isoWhiskerLeft_hom,
      NatTrans.comp_app, Functor.associator_hom_app, whiskerLeft_app,
      fiberwiseColimCompEvaluationIso_inv_app, Functor.associator_inv_app, Category.comp_id,
      Category.id_comp, preservesLimitIso_hom_π_assoc, colim_map, Grothendieck.ι_obj,
      ι_colimitFiberwiseColimitIso_hom]
    simp [← Category.assoc, ← NatTrans.comp_app]
  apply preservesLimit_of_isIso_post

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
a : (F.obj A).obj
f g : A ⟶ X
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) a
⊢ ∀ (a : IsInitial (equalizer f g)), False

Tactic:
exact not_initial_of_inhabited F ((fiberEqualizerEquiv F f g).symm ⟨a, h⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
A : PointedGaloisObject F
⊢ (ConcreteCategory.hom
        (F.map ((evaluationEquivOfIsGalois F A.obj A.pt).symm ((ConcreteCategory.hom (f.app A.obj)) A.pt)).hom))
      A.pt =
    (ConcreteCategory.hom (f.app A.obj)) A.pt

Tactic:
erw [evaluationEquivOfIsGalois_symm_fiber]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f →
    ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

pp: case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ (∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb) →
    Arrows φ hφ S c d f

Tactic:
· rintro ⟨g, hg⟩; exact ⟨_, _, g, rfl, rfl, hg, eq_conj_eqToHom _⟩

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ (∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb) →
    Arrows φ hφ S c d f
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
f : d ⟶ d
hf : f ∈ {x | Map.Arrows φ hφ S d d x}
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Tactic:
change Map.Arrows φ hφ S d d f at hf

Goal state after:
case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
f : d ⟶ d
hf : Map.Arrows φ hφ S d d f
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasPullbacks C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty X.hom (Opposite.op Y ⋔ Z).hom

Tactic:
← hasLiftingProperty_iff

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasPullbacks C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty (Y □ X).hom Z.hom