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

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∑ i ∈ Finset.Ico a b, ∫ (x : ℝ) in ↑i..↑(i + 1), g x = ∫ (x : ℝ) in ↑a..↑b, g x

Tactic:
rw [sum_integral_adjacent_intervals_Ico (a := (↑·)) hab]

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
A : ∀ i ∈ Finset.Ico a b, IntervalIntegrable g volume ↑i ↑(i + 1)
⊢ ∀ k ∈ Ico a b, IntervalIntegrable g volume ↑k ↑(k + 1)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case hg
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
⊢ IntegrableOn (fun x ↦ f x * g (x - 1)) (Ico ↑a ↑b) volume

Tactic:
· apply Integrable.mono_measure _ (volume.restrict_mono_set Ico_subset_Icc_self)
    apply (hf.integrableOn_isCompact isCompact_Icc).mul_of_top_left
    apply AntitoneOn.memLp_isCompact isCompact_Icc
    intro _ _ _ _ _
    apply hg <;> grind

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

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Function.Surjective φ.map

Tactic:
exact fun f => ⟨f (𝟙 G), by cat_disch⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (largeCurriedYonedaLemma.hom.app (op X)).app (F.obj j) ≫
      (↾fun x ↦ { down := (ConcreteCategory.hom (colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)) j)) x.down }) ≫
        (↾fun x ↦ { down := (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    ↾fun g ↦ g ≫ colimit.ι F j

Tactic:
ext η Y f

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
η : yoneda.obj X ⟶ F.obj j
Y : Cᵒᵖ
f : (yoneda.obj X).obj Y
⊢ (ConcreteCategory.hom
          (((ConcreteCategory.hom
                    ((largeCurriedYonedaLemma.hom.app (op X)).app (F.obj j) ≫
                      (↾fun x ↦
                          {
                            down :=
                              (ConcreteCategory.hom (colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)) j))
                                x.down }) ≫
                        (↾fun x ↦
                            {
                              down :=
                                (ConcreteCategory.hom (colimitObjIsoColimitCompEvaluation F (op X)).inv) x.down }) ≫
                          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X))).toFun
                η).app
            Y)).toFun
      f =
    (ConcreteCategory.hom (((ConcreteCategory.hom (↾fun g ↦ g ≫ colimit.ι F j)).toFun η).app Y)).toFun f
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)
⊢ (iso A K).hom = limit.post K A

Tactic:
dsimp [iso, -Iso.app_hom]
  simp only [Category.assoc]
  rw [Eq.comm, ← Iso.inv_comp_eq, ← Iso.inv_comp_eq]
  refine limit.hom_ext (fun j => colimit.hom_ext (fun i => ?_))
  simp only [Category.assoc]
  -- `simp` is not too helpful here because we will need to apply `NatTrans.comp_app_assoc`
  -- backwards at certain points, so we rewrite the term manually.
  rw [HasLimit.isoOfNatIso_hom_π, HasLimit.isoOfNatIso_hom_π_assoc, limit.post_π,
    colimitObjIsoColimitCompEvaluation_ι_inv_assoc (CostructuredArrow.proj yoneda A ⋙ yoneda),
    Iso.app_inv, ← NatTrans.comp_app_assoc, colimit.comp_coconePointUniqueUpToIso_inv,
    Presheaf.tautologicalCocone_ι_app, HasColimit.isoOfNatIso_ι_hom_assoc,
    HasLimit.isoOfNatIso_hom_π_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
    HasColimit.isoOfNatIso_ι_hom_assoc, HasColimit.isoOfNatIso_ι_hom_assoc,
    ι_colimitLimitIso_limit_π_assoc, isoAux_hom_app, ← NatTrans.comp_app_assoc,
    ← NatTrans.comp_app_assoc, Category.assoc, HasLimit.isoOfNatIso_hom_π,
    preservesLimitIso_hom_π_assoc, Iso.symm_hom,
    ← NatTrans.comp_app_assoc, HasColimit.isoOfNatIso_ι_hom,
    ← NatTrans.comp_app_assoc, Category.assoc,
    ι_colimitCompWhiskeringLeftIsoCompColimit_hom,
    NatTrans.comp_app, Category.assoc, isoWhiskerLeft_hom, NatTrans.comp_app, Category.assoc,
    ← NatTrans.comp_app, ← whiskerLeft_comp, colimit.comp_coconePointUniqueUpToIso_hom]
  have := i.hom.naturality (limit.π K j)
  dsimp only [yoneda_obj_obj, Functor.const_obj_obj] at this
  rw [← this]
  ext
  simp [flipFunctorToInterchange, functorToInterchangeIso, functorToInterchange]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasLimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ (piObjIso f d).hom ≫ Pi.π (fun s ↦ (f s).obj d) s = (Pi.π f s).app d

Tactic:
simp [piObjIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
α : Type w
inst✝ : HasLimitsOfShape (Discrete α) C
f : α → D ⥤ C
d : D
s : α
⊢ (piObjIso f d).inv ≫ (Pi.π f s).app d = Pi.π (fun s ↦ (f s).obj d) s

Tactic:
simp [piObjIso]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (F C ⋙ G C ⋙ H C).Faithful

Tactic:
have : (F C).Faithful := by rw [F]; infer_instance

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (F C).Faithful
⊢ (F C ⋙ G C ⋙ H C).Faithful
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✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : C
f : c.pt ⟶ X
hpush :
  IsPushout (limMap c.π) (limMap ((Functor.const J).map f)) (limMap (pushout.inl c.π ((Functor.const J).map f)))
    (limMap (pushout.inr c.π ((Functor.const J).map f)))
⊢ IsIso (limMap (pushout.inr c.π ((Functor.const J).map f)))

Tactic:
have := hc.isIso_limMap_π

Goal state after:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : C
f : c.pt ⟶ X
hpush :
  IsPushout (limMap c.π) (limMap ((Functor.const J).map f)) (limMap (pushout.inl c.π ((Functor.const J).map f)))
    (limMap (pushout.inr c.π ((Functor.const J).map f)))
this : IsIso (limMap c.π)
⊢ IsIso (limMap (pushout.inr c.π ((Functor.const J).map f)))
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v b : ↥S
hb : b ∈ S.attach
hb₁ : b ≠ v
⊢ Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) b ≫ Sigma.ι f (↑b).as = 0

Tactic:
Sigma.ι_π_of_ne_assoc _ (Ne.symm hb₁),

Goal state after:
case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v b : ↥S
hb : b ∈ S.attach
hb₁ : b ≠ v
⊢ 0 ≫ Sigma.ι f (↑b).as = 0
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
⊢ R.cochainComplex.IsGE 0

Tactic:
simp only [HomologicalComplex.isSupported_iff_of_quasiIso R.π']
  infer_instance

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

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) 0

Tactic:
CochainComplex.quasiIsoAt₀_iff,

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ShortComplex.QuasiIso
    ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
      (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩))
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ pseudoApply f ⟦Over.mk 0⟧ = 0

Tactic:
pseudoApply_mk'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ ⟦Over.mk ((Over.mk 0).hom ≫ f)⟧ = 0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ pseudoApply 0 ⟦a'⟧ = ⟦Over.mk 0⟧

Tactic:
pseudoApply_mk'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ ⟦Over.mk (a'.hom ≫ 0)⟧ = ⟦Over.mk 0⟧
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
h : PseudoEqual G x y
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range

Tactic:
obtain ⟨P, p, q, hp, hq, H⟩ := h
  refine Submodule.ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
  · obtain ⟨a', ha'⟩ := ha
    obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective p).1 hp a'
    refine ⟨q a'', ?_⟩
    dsimp at ha' ⊢
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← H,
      ModuleCat.hom_comp, LinearMap.comp_apply, ha'', ha']
  · obtain ⟨a', ha'⟩ := ha
    obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective q).1 hq a'
    refine ⟨p a'', ?_⟩
    dsimp at ha' ⊢
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, H, ModuleCat.hom_comp, LinearMap.comp_apply,
      ha'', ha']

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
⊢ (NatTrans.rightDerivedToHomotopyCategory α).app X ≫ (P.isoRightDerivedToHomotopyCategoryObj G).hom =
    (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)

Tactic:
dsimp [isoRightDerivedToHomotopyCategoryObj, Functor.mapHomotopyCategoryFactors,
    NatTrans.rightDerivedToHomotopyCategory]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
⊢ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj
            ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) =
    ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex))) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ F.map f ≫
      (injectiveResolution Y).toRightDerivedZero' F ≫
        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex).homologyπ 0 ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex) =
    ((injectiveResolution X).toRightDerivedZero' F ≫
        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (F.rightDerivedToHomotopyCategory.map f)

Tactic:
rw [assoc, assoc, InjectiveResolution.toRightDerivedZero'_naturality_assoc f
      (injectiveResolution X) (injectiveResolution Y)
      (InjectiveResolution.desc f _ _) (by simp),
      ← HomologicalComplex.homologyπ_naturality_assoc]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        HomologicalComplex.homologyMap
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map
              (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X)))
            0 ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex) =
    (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (F.rightDerivedToHomotopyCategory.map f)
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: V : Type (u + 1)
inst✝³ : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst✝² : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝¹ : ConcreteCategory V FV
G : Type u_3
inst✝ : Monoid G
X : Action V G
x : ToType X
⊢ 1 • x = x

Tactic:
by
    change ConcreteCategory.hom (X.ρ 1) x = x
    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.PreservesMonomorphisms
this : L.mapArrow.EssSurj
x✝ : Mono f✝
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
⊢ Arrow.mk (L.map f) ≅ Arrow.mk (L.map (Abelian.image.ι f))

Tactic:
have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_factorThruImage

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.PreservesMonomorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Mono f✝
X Y : C
f : X ⟶ Y
hf : P.monoModSerre f
this : IsIso (L.map (Abelian.factorThruImage f))
⊢ Arrow.mk (L.map f) ≅ Arrow.mk (L.map (Abelian.image.ι f))
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
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G), F x = (lift (F.comp inl) (F.comp inr) ⋯) x

Tactic:
simp only [lift, MonoidHom.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk, ← map_mul,
    inl_left_mul_inr_right, forall_const]

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J (F ⋙ forget V G)

Tactic:
exact PreservesColimitsOfSize.preservesColimitsOfShape

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
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : RightRigidCategory V
⊢ RightRigidCategory (SingleObj H ⥤ V)

Tactic:
by
  infer_instance

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
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : LeftRigidCategory V
⊢ LeftRigidCategory (SingleObj H ⥤ V)

Tactic:
by
  infer_instance

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
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : RigidCategory V
⊢ RigidCategory (SingleObj H ⥤ V)

Tactic:
by
  infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
⊢ t.leftToRight.app X ≫ H.map (t.adj₁.unit.app X) = t.adj₂.unit.app (F.obj X)

Tactic:
simp [leftToRight_app]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ eqToHomTransIso e₁ ⋯ = (ρ_ (eqToHom e₁)).symm

Tactic:
ext
  subst e₁
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ eqToHomTransIso ⋯ e₁ = (λ_ (eqToHom e₁)).symm

Tactic:
ext
  subst e₁
  simp

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

Goal state before:
pp: B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    Quot.map (Hom₂.whisker_right h) ⋯ (Quot.map (Hom₂.whisker_left f) ⋯ η) =
      { 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 ≫
        Quot.map (Hom₂.whisker_left f) ⋯ (Quot.map (Hom₂.whisker_right 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

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

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᵖ C
α : F ⟶ G
a : B
⊢ (α.naturality (𝟙 a)).hom =
    (F.mapId a ▷ᵢ α.app a ≪≫ λ_ (α.app a) ≪≫ (ρ_ (α.app a)).symm ≪≫ α.app a ◁ᵢ (G.mapId a).symm).hom

Tactic:
simp [naturality_id_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Modification.Oplax

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

Tactic:
by
  simp_rw [← comp_whiskerRight, naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Core C
f g : X ⟶ Y
h : f.iso.hom = g.iso.hom
⊢ f = g

Tactic:
by
  apply CoreHom.ext
  exact Iso.ext h

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ (F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } })) ≫
      MonoidalCategoryStruct.whiskerRight (F.mapId { as := { as := () } }) (F.map (𝟙 { as := { as := () } })) =
    (MonoidalCategoryStruct.leftUnitor (F.map (𝟙 { as := { as := () } }))).inv

Tactic:
by
    simp only [tensorUnit_def, tensorObj_def, whiskerRight_def, Category.assoc, leftUnitor_def]
    rw [F.mapComp_id_left, unitors_equal, F.map₂_inv_hom_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : (decomposedTo J).obj ⟨j', { obj := X, property := hX }⟩ ⟶ (decomposedTo J).obj ⟨k', { obj := Y, property := hY }⟩
⊢ ∃ a, (decomposedTo J).map a = f

Tactic:
dsimp at f

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ ∃ a, (decomposedTo J).map a = f
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: α β : PartialFun
e : α ≃ β
⊢ ↑(⇑e.symm ∘ ⇑e) = 𝟙 α

Tactic:
simp only [Equiv.symm_comp_self, PFun.coe_id]

Goal state after:
α β : PartialFun
e : α ≃ β
⊢ PFun.id α = 𝟙 α
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y

Tactic:
injection Part.mem_unique h h' with e

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun x y ↦ Sum.inr x ∈ f y) a'
h₄ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
y : α
h' : Sum.inr y ∈ f a
e : a' = y
⊢ Acc (fun x y ↦ Sum.inr x ∈ f y) y
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x✝ : α
⊢ x✝ ∈ f.preimage Set.univ ↔ x✝ ∈ f.Dom

Tactic:
simp [mem_preimage, mem_dom]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝¹ : ChosenPullbacksAlong g
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst✝ : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂ ≫ fst f g = fst f' g' ≫ γ₁

Tactic:
by
  simp only [pullbackMap, lift_fst]

Goal state after: