mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.PreservesEpimorphisms
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
g : P ⟶ X✝
f : E✝ ⟶ X✝
x✝ : Epi f
⊢ ∃ f', f' ≫ f = g

Tactic:
obtain ⟨h, fac⟩ := hP.factors (F.map g) (F.map f)
    exact ⟨F.preimage h, F.map_injective (by simp [fac])⟩

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
F G : C ⥤ D
τ : F ⟶ G
S : ShortComplex C
inst✝⁶ : S.HasHomology
inst✝⁵ : F.PreservesZeroMorphisms
inst✝⁴ : G.PreservesZeroMorphisms
inst✝³ : F.PreservesLeftHomologyOf S
inst✝² : G.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : G.PreservesRightHomologyOf S
⊢ τ.app S.homology = (S.mapHomologyIso F).inv ≫ ShortComplex.homologyMap (S.mapNatTrans τ) ≫ (S.mapHomologyIso G).hom

Tactic:
rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id,
    comp_id, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : IsZero S.X₂
⊢ IsZero (HomologyData.ofZeros S ⋯ ⋯).left.H

Tactic:
exact h

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))

Tactic:
by
  let bc := BinaryBicone.ofColimitCocone i
  let presf : PreservesColimit (parallelPair bc.inr 0) F := by simpa
  let hf : IsColimit bc.inrCokernelCofork := BinaryBicone.isColimitInrCokernelCofork i
  exact
    (isColimitMapCoconeBinaryCofanEquiv F ι₁ ι₂).invFun
      (BinaryBicone.isBilimitOfCokernelFst (F.mapBinaryBicone bc)
          (isColimitMapCoconeCoforkEquiv' F bc.inr_fst (isColimitOfPreserves F hf))).isColimit

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S : ShortComplex C
inst✝⁴ : S.HasHomology
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : F.Faithful
h : (S.map F).Exact
⊢ S.Exact

Tactic:
rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero]

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S : ShortComplex C
inst✝⁴ : S.HasHomology
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : F.Faithful
h : (S.map F).Exact
⊢ 𝟙 S.leftHomologyData.H = 0
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
X₂ : Subobject X
A✝ : C
f✝ : A✝ ⟶ X
inst✝ : Mono f✝
h : (map f).obj (mk f✝) = (map f).obj X₂
⊢ mk f✝ = X₂

Tactic:
induction X₂ using Subobject.ind

Goal state after:
case h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝² : Mono f
A✝¹ : C
f✝¹ : A✝¹ ⟶ X
inst✝¹ : Mono f✝¹
A✝ : C
f✝ : A✝ ⟶ X
inst✝ : Mono f✝
h : (map f).obj (mk f✝¹) = (map f).obj (mk f✝)
⊢ mk f✝¹ = mk f✝
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
h : (map e.hom).obj A ≤ (map e.hom).obj B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B

Tactic:
exact h

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
⊢ ∀ (a : Subobject X), a ≤ Quotient.mk'' ⊤

Tactic:
refine Quotient.ind' fun f => ?_
    exact ⟨MonoOver.leTop f⟩

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

Goal state before:
pp: case insert.inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ s✝
⊢ (P i✝).Factors ((s✝.inf P).factorThru (P a✝¹ ⊓ s✝.inf P).arrow ⋯ ≫ (s✝.inf P).arrow)

Tactic:
apply factors_of_factors_right

Goal state after:
case insert.inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ s✝
⊢ (P i✝).Factors (s✝.inf P).arrow
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
pt : C
π : limit (F ⋙ coyoneda.obj (op pt))
⊢ Nonempty (Cone F)

Tactic:
exact ⟨⟨pt, (limitCompCoyonedaIsoCone F pt).hom π⟩⟩

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

Goal state before:
pp: case none
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
⊢ u ≫ limit.π (wideCospan s) none = v ≫ limit.π (wideCospan s) none

Tactic:
exact h

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

Goal state before:
pp: case some
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) none = v ≫ limit.π (wideCospan s) none

Tactic:
exact h

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
H : Type u_3
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : ∀ (F : C ⥤ H), L✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ ((L.ran ⋙ lim).map f ≫ ((L.ran.obj Y✝).limitIsoOfIsRightKanExtension (L.ranCounit.app Y✝)).hom) ≫ limit.π Y✝ i =
    (((L.ran.obj X✝).limitIsoOfIsRightKanExtension (L.ranCounit.app X✝)).hom ≫ lim.map f) ≫ limit.π Y✝ i

Tactic:
dsimp
      rw [assoc, assoc, limMap_π, limitIsoOfIsRightKanExtension_hom_π_assoc,
        limitIsoOfIsRightKanExtension_hom_π, limMap_π_assoc]
      congr 1
      exact congr_app (L.ranCounit.naturality f) i

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E
this :
  (hom (g.app (op X))) ((hom ((uliftYoneda.{max w v₂, v₁, u₁}.obj Y).map f.op)) { down := 𝟙 Y }) =
    (hom (((restrictedULiftYoneda A).obj E).map f.op)) ((hom (g.app (op Y))) { down := 𝟙 Y })
⊢ A.map f ≫ (uliftYonedaEquiv g).down = (uliftYonedaEquiv (uliftYoneda.{max v₂ w, v₁, u₁}.map f ≫ g)).down

Tactic:
dsimp [uliftYonedaEquiv, uliftYoneda] at this ⊢

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E
this : (hom (g.app (op X))) { down := f ≫ 𝟙 Y } = { down := A.map f ≫ ((hom (g.app (op Y))) { down := 𝟙 Y }).down }
⊢ A.map f ≫ ((hom (g.app (op Y))) { down := 𝟙 Y }).down = ((hom (g.app (op X))) { down := 𝟙 X ≫ f }).down
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
w✝¹ : C
h : P w✝¹
w✝ : S ⟶ T.obj w✝¹
⊢ P (mk w✝).right

Tactic:
exact h

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
w✝¹ : C
h : P w✝¹
w✝ : S.obj w✝¹ ⟶ T
⊢ P (mk w✝).left

Tactic:
exact h

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
⊢ Abelian C

Tactic:
haveI := hasKernels F G i

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this : HasKernels C
⊢ Abelian C
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
φ : Functor.LeftExtension.mk (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)) (uliftYonedaMap F X) ⟶ Y
⊢ φ = StructuredArrow.homMk (uliftYonedaEquiv.symm (uliftYonedaEquiv (StructuredArrow.hom Y))) ⋯

Tactic:
ext : 1

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
φ : Functor.LeftExtension.mk (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)) (uliftYonedaMap F X) ⟶ Y
⊢ StructuredArrow.Hom.right φ =
    StructuredArrow.Hom.right
      (StructuredArrow.homMk (uliftYonedaEquiv.symm (uliftYonedaEquiv (StructuredArrow.hom Y))) ⋯)
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) =
    (ConcreteCategory.hom (colimit.ι S.X₂ j)) y

Tactic:
exact colimit.w_apply S.X₂ e₁ y

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
x : F.obj X
u : F.Elements
v : u.fst ⟶ X
h : (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv (shrinkYonedaObjObjEquiv.symm v)))) u.snd = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) =
    G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)

Tactic:
simp only [Equiv.apply_symm_apply] at h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
x : F.obj X
u : F.Elements
v : u.fst ⟶ X
h : (ConcreteCategory.hom (F.map v)) u.snd = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) =
    G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: case pos
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : IsEmpty X
⊢ Mono (free.map f)

pp: case neg
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
⊢ Mono (free.map f)

Tactic:
· constructor
      intros
      apply (IsInitial.isInitialObj free _
        ((Types.initial_iff_empty X).2 hX).some).isZero.eq_of_tgt

Goal state after:
case neg
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
⊢ Mono (free.map f)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : GrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GrpCat).obj Y✝
⊢ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝) =
    free.map f✝ ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝

Tactic:
ext : 1

Goal state after:
X'✝ X✝ : Type u
Y✝ : GrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget GrpCat).obj Y✝
⊢ Hom.hom ((ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f✝ ≫ g✝)) =
    Hom.hom (free.map f✝ ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g✝)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X✝ : GrpCat
⊢ CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (𝟙 X✝)))) =
    𝟙 (CommGrpCat.of (Abelianization ↑X✝))

Tactic:
ext : 1

Goal state after:
X✝ : GrpCat
⊢ CommGrpCat.Hom.hom (CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (𝟙 X✝))))) =
    CommGrpCat.Hom.hom (𝟙 (CommGrpCat.of (Abelianization ↑X✝)))
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X✝ Y✝ Z✝ : GrpCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (f✝ ≫ g✝)))) =
    CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom f✝))) ≫
      CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom g✝)))

Tactic:
ext : 1

Goal state after:
X✝ Y✝ Z✝ : GrpCat
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ CommGrpCat.Hom.hom (CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (f✝ ≫ g✝))))) =
    CommGrpCat.Hom.hom
      (CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom f✝))) ≫
        CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom g✝))))
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: case fst
G H : AddCommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) G H)) (p, q)).1 = (p, q).1

pp: case snd
G H : AddCommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) G H)) (p, q)).2 = (p, q).2

Tactic:
· exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget AddCommGrpCat.{u}) G H) (p, q)

Goal state after:
case snd
G H : AddCommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) G H)) (p, q)).2 = (p, q).2
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c : α
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)

Tactic:
simp_rw [lt_iff_le_not_ge]
    grind

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ -f (x + (2 * n) • c) = -f x

Tactic:
h.even_zsmul_periodic

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ -f x = -f x
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Tactic:
rw [cast_div hm, cast_div hn, div_div_div_cancel_right₀ hd]

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑d ≠ 0
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case e_a
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = a + (r • y - snd i x • y)

Tactic:
rw [Subtype.coe_mk, add_sub, ← eq1]

Goal state after:
case e_a
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
eq3 :
  (extendIdealTo i f h y) r =
    ↑(extensionOfMax i f).toLinearPMap ⟨r • y - snd i x • y, ⋯⟩ + (extendIdealTo i f h y) (snd i x)
⊢ ↑(fst i x) = ↑x - snd i x • y
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = (RingHom.id R) r • ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩

Tactic:
← LinearPMap.map_smul

Goal state after:
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
r : R
x : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨r • x, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap ((RingHom.id R) r • ⟨x, ⋯⟩)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: case h
ι : Type u_1
ι' : Type u_2
⊢ ∀ (b : Finset (ι × ι')), ∃ a, b ⊆ a.1 ×ˢ a.2

Tactic:
intro b
    use (Finset.image Prod.fst b, Finset.image Prod.snd b)
    exact Finset.subset_product

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
han : 0 < a
ha : φ a ≤ 1
⊢ a ∣ 2

Tactic:
rcases totient_eq_one_iff.mp <| le_antisymm ha <| totient_pos.2 han with rfl | rfl

Goal state after:
case inl
han : 0 < 1
ha : φ 1 ≤ 1
⊢ 1 ∣ 2

case inr
han : 0 < 2
ha : φ 2 ≤ 1
⊢ 2 ∣ 2
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ (n.factorization.prod fun a b ↦ a ^ (b - 1) * (a - 1) * a) = n.factorization.prod fun a b ↦ a ^ b * (a - 1)

Tactic:
refine Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => ?_

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ p * φ n = (p - 1) * φ n

pp: p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n

Tactic:
totient_prime hp

Goal state after:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ (p - 1) * φ n = (p - 1) * φ n

p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ (p ^ k) ^ (p ^ (k - 1) * (p - 1)) / ∏ x ∈ (p ^ k).primeFactors, x ^ (p ^ (k - 1) * (p - 1) / (x - 1)) =
    p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
Nat.primeFactors_prime_pow hk.ne' hp,

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ (p ^ k) ^ (p ^ (k - 1) * (p - 1)) / ∏ x ∈ {p}, x ^ (p ^ (k - 1) * (p - 1) / (x - 1)) =
    p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (a + p) b = toIocDiv hp a b - 1

Tactic:
toIocDiv_add_right'

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b - 1 = toIocDiv hp a b - 1
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t

Tactic:
simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]
  refine (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq ?_
  simp only [inter_union_distrib_left, inter_assoc,
    inter_comm (closure t)]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) = ∅

Tactic:
have : interior (frontier s) ⊆ interior s ∩ (s \ interior s) :=
    subset_inter B (by simpa [A] using C)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
⊢ interior (frontier s) = ∅
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b : α
⊢ 𝓝 b = update pure a₀ l b

Tactic:
refine nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => ?_
  rcases eq_or_ne a a₀ with (rfl | ha)
  · filter_upwards [hs] with b hb
    rcases eq_or_ne b a with (rfl | hb)
    · exact hs
    · rwa [update_of_ne hb]
  · simpa only [update_of_ne ha, mem_pure, eventually_pure] using hs

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ range f = univ ↔ Surjective f

Tactic:
range_eq_univ

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ι : Type u_3
f : ι → α
⊢ Surjective f ↔ Surjective f