mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0

Tactic:
by rw [hx, S.zero_assoc, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (leftHomologyMap' φ h₁ h₂')

Tactic:
rw [(LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).leftHomologyMap'_eq]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).φH
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0

Tactic:
by rw [hx, S.zero_assoc, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ + φ₃).τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂ + φ₄).τ₁

Tactic:
add_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ φ₁.τ₁ + φ₃.τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂ + φ₄).τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ φ₁.τ₁ + φ₃.τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂ + φ₄).τ₁

Tactic:
add_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ φ₁.τ₁ + φ₃.τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.lift f.op (cokernel.π f).op ⋯).unop ≫ (cokernel.desc f (kernel.ι f.op).unop ⋯).op.unop =
    (𝟙 (kernel f.op)).unop

Tactic:
← unop_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ ((cokernel.desc f (kernel.ι f.op).unop ⋯).op ≫ kernel.lift f.op (cokernel.π f).op ⋯).unop = (𝟙 (kernel f.op)).unop
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.lift f (cokernel.π f.op).unop ⋯).op.unop ≫ (cokernel.desc f.op (kernel.ι f).op ⋯).unop =
    (𝟙 (cokernel f.op)).unop

Tactic:
← unop_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f.op (kernel.ι f).op ⋯ ≫ (kernel.lift f (cokernel.π f.op).unop ⋯).op).unop = (𝟙 (cokernel f.op)).unop
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃

Tactic:
by rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
obtain ⟨h, h_eq⟩ := @Injective.factors C _ P _ _ _ (g ≫ i.inv) f mono

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ ∃ h, f ≫ h = g
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective Y
⊢ Injective X

Tactic:
refine Injective.mk (fun {A B} f e _ ↦ ?_)
  rcases i.factors (f ≫ h.i) e with ⟨g, hg⟩
  use g ≫ h.r
  simp [Category.assoc', hg]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
⊢ Mono S.op.f

Tactic:
by
    have := h.epi_g
    dsimp
    infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
⊢ Mono S.unop.f

Tactic:
by
    have := h.epi_g
    dsimp
    infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
x : Subobject Z
⊢ (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x)

Tactic:
induction x using Quotient.inductionOn' with | _ t
  exact Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
x : Subobject Z
⊢ (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x)

Tactic:
by
  induction x using Quotient.inductionOn' with | _ t
  exact Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ factorThruKernelSubobject f h w ≫ (kernelSubobject f).arrow = h

Tactic:
dsimp [factorThruKernelSubobject]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ (kernelSubobject f).factorThru h ⋯ ≫ (kernelSubobject f).arrow = h
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
⊢ P ⟶ S.X₁

Tactic:
have := hS.epi_toCycles
  exact Projective.factorThru (S.liftCycles f hf) S.toCycles

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
q : A.obj (op X)
q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm q)))
h : fst ⟨p, p'⟩ = fst ⟨q, q'⟩
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) (snd ⟨q, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = ⟨q, q'⟩

Tactic:
obtain rfl : p = q := yonedaEquiv.symm.injective h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = fst ⟨p, q'⟩
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) (snd ⟨p, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = ⟨p, q'⟩
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ IsIso φ → F''.IsLeftKanExtension α'

Tactic:
intro
    exact isLeftKanExtension_of_iso (asIso φ) α α' comm

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
⊢ Unique (b ⟶ y)

Tactic:
by
    let u : (LeftExtension.precomp₂ L' α).obj b ⟶
      (LeftExtension.precomp₂ L' α).obj y := hb.to _
    refine
      ⟨⟨StructuredArrow.homMk u.right <| by
          apply hα.hom_ext
          ext t
          have := congr_app u.w t
          dsimp at this
          simp only [precomp₂_obj_hom_app, assoc] at this
          simp [this]⟩, fun a => ?_⟩
    ext1
    apply hb.hom_ext
    ext t
    have := congr_app u.w t
    dsimp at this
    simp only [precomp₂_obj_hom_app, assoc] at this
    simp [this, ← a.w]

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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((coconeOfRepresentable P).pt.map f ≫ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk Y x)))) =
    (↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x)))) ≫ s.pt.map f

Tactic:
ext x
        have := s.w (Quiver.Hom.op (CategoryOfElements.homMk (P.elementsMk X x)
          (P.elementsMk Y (P.map f x)) f rfl))
        dsimp at this x ⊢
        rw [← this, uliftYonedaEquiv_comp]
        dsimp
        rw [uliftYonedaEquiv_apply, uliftYonedaEquiv_apply,
          ← NatTrans.naturality_apply]
        simp [uliftYoneda]

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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j) = (hom ((s.ι.app j).app X)) x

Tactic:
uliftYonedaEquiv_apply

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ (hom ((uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j).app (op (unop X)))) { down := 𝟙 (unop X) } =
    (hom ((s.ι.app j).app X)) x
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left✝ : IsIso α
right✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
P : Cᵒᵖ ⥤ Type (max (max w v₂) v₁)
⊢ IsColimit ((Functor.LeftExtension.mk L α).coconeAt P)

Tactic:
apply IsColimit.ofWhiskerEquivalence
      (CategoryOfElements.costructuredArrowULiftYonedaEquivalence _)

Goal state after:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left✝ : IsIso α
right✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
P : Cᵒᵖ ⥤ Type (max (max w v₂) v₁)
⊢ IsColimit
    (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
      ((Functor.LeftExtension.mk L α).coconeAt P))
Module: Mathlib.CategoryTheory.Subobject.Comma

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
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map ((Subobject.mk f.unop.left.op).arrow.unop ≫ (Subobject.underlyingIso f.unop.left.op).inv.unop) ≫ (unop P).hom =
    A.hom

Tactic:
← unop_comp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ (Subobject.mk f.unop.left.op).arrow).unop ≫ (unop P).hom = A.hom
Module: Mathlib.CategoryTheory.Subobject.Comma

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
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Tactic:
← unop_comp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
⊢ f = default

Tactic:
suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by
      apply this
    intro g
    suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer
    exact IsSplitEpi.mk' ⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le, by
      ext
      simp⟩

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
⊢ f = default

pp: case refine_2
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : X ⟶ G
⊢ f = default

Tactic:
· ext x
    have : x = 1 := Subsingleton.elim _ _
    rw [this, map_one, map_one]

Goal state after:
case refine_2
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : X ⟶ G
⊢ f = default
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
⊢ f = default

pp: case refine_2
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : X ⟶ G
⊢ f = default

Tactic:
· ext x
    have : x = 1 := Subsingleton.elim _ _
    rw [this, map_one, map_one]

Goal state after:
case refine_2
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : X ⟶ G
⊢ f = default
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ n • (LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m)) m = g ⟨n • m, hn⟩

Tactic:
LinearMap.toSpanSingleton_apply,

Goal state after:
case inr
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := g ⟨m, ⋯⟩
n : ℤ
hn : n • m ∈ ℤ ∙ m
⊢ n • m • DivisibleBy.div gₘ m = g ⟨n • m, hn⟩
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ Additive.toMul (n • Additive.ofMul u) = u ^ n

Tactic:
toMul_nsmul,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ Additive.toMul (Additive.ofMul u) ^ n = u ^ n
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ |↑n.negOnePow| = 1

Tactic:
abs_eq_natAbs,

Goal state after:
n : ℤ
⊢ ↑(↑n.negOnePow).natAbs = 1
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case neg
n₁ n₂ : ℤ
h₂ : ¬Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
· rw [Int.not_even_iff_odd] at h₂
    rw [negOnePow_odd _ h₂, Int.even_sub, negOnePow_eq_neg_one_iff,
      ← Int.not_odd_iff_even, ← Int.not_odd_iff_even]
    tauto

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
g : α → β
l : List (α → β)
ih : (∀ f ∈ l, Periodic f c) → Periodic l.prod c
hl : Periodic g c ∧ ∀ x ∈ l, Periodic x c
⊢ Periodic (g :: l).prod c

Tactic:
simpa only [List.prod_cons] using hl.1.mul (ih hl.2)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddCommGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (-x + n • c) = ↑n.negOnePow • f (-x)

Tactic:
exact h.add_zsmul_eq n

Goal state after:
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
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
y : N
z1 z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 + z2) • y, ⋯⟩ =
    ↑(extensionOfMax i f).toLinearPMap ⟨↑z1 • y, ⋯⟩ + ↑(extensionOfMax i f).toLinearPMap ⟨↑z2 • y, ⋯⟩

Tactic:
simp_rw [← (extensionOfMax i f).toLinearPMap.map_add]
    congr
    apply add_smul

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0

Tactic:
count_add',

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count (fun k ↦ p (k + 1)) n + count p 1 = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0
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
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r * ExtensionOfMaxAdjoin.snd i a) • y

Tactic:
mul_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
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ r • ↑(ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y =
    ↑(r • ExtensionOfMaxAdjoin.fst i a) + r • ExtensionOfMaxAdjoin.snd i a • y
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
obtain ⟨k : ℕ, - : k ≤ N, hku : ∀ l ≤ N, u l ≤ u k⟩ : ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k :=
    exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩

Goal state after:
β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
⊢ ∃ n ≥ N, ∀ k < n, u k < u n
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atBot

Tactic:
by
  rw [← prod_atBot_atBot_eq]
  exact hf.prodMap hg

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

Goal state before:
pp: n : ℕ
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
n : ℕ
hn : n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = ↑p - ↑p * (↑p)⁻¹

Tactic:
mul_inv_cancel₀ hp',

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = ↑p - 1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ a * p * d ≠ 0

Tactic:
rwa [mul_assoc]

Goal state after:
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 : α
⊢ toIcoMod hp a a = a

Tactic:
toIcoMod_eq_iff hp,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a ∈ Set.Ico a (a + p) ∧ ∃ z, a = a + z • p
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 : α
⊢ toIcoMod hp a (a + p) = a

Tactic:
toIcoMod_eq_iff hp,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a ∈ Set.Ico a (a + p) ∧ ∃ z, a + p = a + z • p
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 : α
⊢ toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1

Tactic:
simpa only [one_zsmul] using toIcoDiv_sub_zsmul' hp a b 1

Goal state after: