mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = 0

Tactic:
rw [show 0 = h.ι ≫ h.g' ≫ x by simp]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = h.ι ≫ h.g' ≫ x
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH

Tactic:
simp only [γ.homologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH

Tactic:
simp only [γ.homologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

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₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ = h₁.leftHomologyIso.hom ≫ γ.φH ≫ h₂.leftHomologyIso.inv

Tactic:
by
  dsimp [LeftHomologyData.leftHomologyIso, leftHomologyMapIso']
  rw [← γ.leftHomologyMap'_eq, ← leftHomologyMap'_comp,
    ← leftHomologyMap'_comp, id_comp, comp_id]
  rfl

Goal state after:
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 : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ h.p ≫ h.opcyclesIso.inv = S.pOpcycles

Tactic:
by
  dsimp [pOpcycles, RightHomologyData.opcyclesIso]
  simp only [p_opcyclesMap', id_τ₂, id_comp]

Goal state after:
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ = h₁.rightHomologyIso.hom ≫ γ.φH ≫ h₂.rightHomologyIso.inv

Tactic:
dsimp [RightHomologyData.rightHomologyIso, rightHomologyMapIso']

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ =
    rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData
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
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasLeftHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm

Tactic:
ext
  dsimp [mapCyclesIso, cyclesIso]
  simp only [map_cyclesMap', ← cyclesMap'_comp, Functor.map_id, comp_id,
    Functor.mapShortComplex_obj]

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m =
    { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
      comm₂₃ := ⋯ }

Tactic:
ext
    · exact h₁.uniq (π₁.mapCocone s) _ (fun j => π₁.congr_map (hm j))
    · exact h₂.uniq (π₂.mapCocone s) _ (fun j => π₂.congr_map (hm j))
    · exact h₃.uniq (π₃.mapCocone s) _ (fun j => π₃.congr_map (hm j))

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.Full
inst✝ : F.Faithful
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ F.map ((adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E✝)) ≫ g) = F.map f

Tactic:
simpa

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
refine ⟨biproduct.lift fun b => factorThru (g ≫ biproduct.π _ _) f, ?_⟩
    ext
    simp only [Category.assoc, biproduct.lift_π, comp_factorThru]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.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
G : D ⥤ C
adj : F ⊣ G
inst✝² : G.Full
inst✝¹ : G.Faithful
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ G.map (g ≫ inv (adj.counit.app Y) ≫ F.map w ≫ adj.counit.app I) = G.map f

Tactic:
simpa

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

Goal state before:
pp: S : ShortComplex Ab
x : ↑S.X₁
⊢ (ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x) = 0

Tactic:
rw [← ConcreteCategory.comp_apply, S.zero]
  rfl

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
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
⊢ PreservesLimit (parallelPair bc.snd 0) F

Tactic:
simpa

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 ι₁ ι₂)
bc : BinaryBicone X Y := BinaryBicone.ofColimitCocone i
⊢ PreservesColimit (parallelPair bc.inr 0) F

Tactic:
simpa

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

Goal state before:
pp: case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ (g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom =
    (h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom

Tactic:
simpa

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (kernel.lift S.g S.f ⋯)

Tactic:
← this

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (imageToKernel' S.f S.g ⋯)
⊢ Epi (factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯)
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
F : C ⥤ H
G : D ⥤ H
α : L ⋙ G ⟶ F
⊢ L.whiskerLeft (((L.ranAdjunction H).homEquiv G F) α) ≫ L.ranCounit.app F = α

Tactic:
simp [ranAdjunction]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive 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
X Y : C
f : X ⟶ Y
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasKernel f

Tactic:
← this

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive 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
X Y : C
f : X ⟶ Y
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasKernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasCokernel f

Tactic:
← this

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasCokernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
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✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
hfg :
  (StructuredArrow.hom (Functor.LeftExtension.mk L α)).app p.left ≫
      (StructuredArrow.right (Functor.LeftExtension.mk L α)).map p.hom ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
          ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) =
    ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)).app p
hg :
  (StructuredArrow.hom (Functor.LeftExtension.mk L α)).app ((CostructuredArrow.map f).obj p).left ≫
      (StructuredArrow.right (Functor.LeftExtension.mk L α)).map ((CostructuredArrow.map f).obj p).hom ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)).symm
          ((restrictedULiftYonedaHomEquiv' A Q X).symm g) =
    ((restrictedULiftYonedaHomEquiv' A Q X).symm g).app ((CostructuredArrow.map f).obj p)
⊢ ((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫ (restrictedULiftYonedaHomEquiv L α P X).symm (f ≫ g) =
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫ L.map f ≫ (restrictedULiftYonedaHomEquiv L α Q X).symm g

Tactic:
dsimp at hfg hg

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
hfg :
  α.app p.left ≫
      L.map p.hom ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
          ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)) =
    ((restrictedULiftYonedaHomEquiv' A P X).symm (f ≫ g)).app p
hg :
  α.app p.left ≫
      L.map (p.hom ≫ f) ≫
        (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α Q)).symm
          ((restrictedULiftYonedaHomEquiv' A Q X).symm g) =
    ((restrictedULiftYonedaHomEquiv' A Q X).symm g).app ((CostructuredArrow.map f).obj p)
⊢ ((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫ (restrictedULiftYonedaHomEquiv L α P X).symm (f ≫ g) =
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app p ≫ L.map f ≫ (restrictedULiftYonedaHomEquiv L α Q X).symm g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
h✝ : P.IsCoseparating
D : Type u_1
inst✝ : Category.{v_1, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : P Z
h : α.inverse.obj Y ⟶ Z
⊢ α.inverse.map f ≫ h = α.inverse.map g ≫ h

Tactic:
obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
h : P.IsCoseparating
D : Type u_1
inst✝ : Category.{v_1, u_1} D
α : C ≌ D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : P Z
h' : Y ⟶ α.symm.inverse.obj Z
⊢ α.inverse.map f ≫ (α.symm.toAdjunction.homEquiv Y Z).symm h' =
    α.inverse.map g ≫ (α.symm.toAdjunction.homEquiv Y Z).symm h'
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ ∀ {X Y : WalkingParallelFamily J} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map f

Tactic:
by
    rintro _ _ (_ | _) <;> cat_disch

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i ↦ StructuredArrow.mk (f i)
A' : StructuredArrow A G
⊢ ∃ i, Nonempty (B' i ⟶ A')

Tactic:
obtain ⟨i, _, t⟩ := g _ A'.hom

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i ↦ StructuredArrow.mk (f i)
A' : StructuredArrow A G
i : ι
w✝ : B i ⟶ A'.right
t : f i ≫ G.map w✝ = A'.hom
⊢ ∃ i, Nonempty (B' i ⟶ A')
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))

Tactic:
← this

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
⊢ Function.Surjective (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i })))
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
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.μ_snd (forget AddCommGrpCat.{u}) G H) (p, q)

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
u : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).map (shrinkYonedaObjObjEquiv u.snd)))
      ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).snd =
    u.snd

Tactic:
by
    simp [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
this : RootableBy.root a ↑n ^ ↑n = a
⊢ RootableBy.root a ↑n ^ n = a

Tactic:
simpa

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ RootableBy.root a ↑n ^ n = a

Tactic:
have := RootableBy.root_cancel a (show (n : ℤ) ≠ 0 from mod_cast hn)
    simpa

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

Goal state before:
pp: case mp
n : ℤ
⊢ n.negOnePow = 1 → Even n

pp: case mpr
n : ℤ
⊢ Even n → n.negOnePow = 1

Tactic:
· intro h
    rw [← Int.not_odd_iff_even]
    intro h'
    simp only [negOnePow_odd _ h'] at h
    contradiction

Goal state after:
case mpr
n : ℤ
⊢ Even n → n.negOnePow = 1
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case mpr
n : ℤ
⊢ Even n → n.negOnePow = 1

Tactic:
· exact negOnePow_even n

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

Goal state before:
pp: case mp
n : ℤ
⊢ n.negOnePow = -1 → Odd n

pp: case mpr
n : ℤ
⊢ Odd n → n.negOnePow = -1

Tactic:
· intro h
    rw [← Int.not_even_iff_odd]
    intro h'
    rw [negOnePow_even _ h'] at h
    contradiction

Goal state after:
case mpr
n : ℤ
⊢ Odd n → n.negOnePow = -1
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)
x y : ↥i.range
eq1 : i (Exists.choose ⋯ + Exists.choose ⋯) = ↑(x + y)
⊢ f (Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)

Tactic:
← (x + y).2.choose_spec

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)
x y : ↥i.range
eq1 : i (Exists.choose ⋯ + Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (Exists.choose ⋯) = f (Exists.choose ⋯) + f (Exists.choose ⋯)
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 (n • c + -x) = ↑n.negOnePow • f (-x)

Tactic:
add_comm

Goal state after:
α : 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)
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p b + count (fun k ↦ p (b + k)) a = count (fun k ↦ p (k + b)) a + count p b

Tactic:
add_comm

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count (fun k ↦ p (b + k)) a + count p b = count (fun k ↦ p (k + b)) a + count p b
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝¹ : DecidablePred p
q : ℕ → Prop
inst✝ : DecidablePred q
n : ℕ
hpq : ∀ k < n, p k → q k
⊢ ∀ x ∈ List.range n, decide (p x) = true → decide (q x) = true

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case zero
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime : ∀ (p : ℕ), Prime p → motive p
composite : ∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)
n p : ℕ
hp : Prime p
ha : motive 0
⊢ motive (p * 0)

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case inl
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 0 = (factorization 0).prod fun p k ↦ f (p ^ k)

Tactic:
simpa

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

Goal state before:
pp: n : ℕ
hn : 2 < n
this✝¹ : Fact (1 < n)
this✝ : NeZero n
this : 2 = orderOf (-1)
⊢ orderOf (-1) ∣ Fintype.card (ZMod n)ˣ

Tactic:
exact orderOf_dvd_card

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
this : a ∩ ⋂₀ ↑s ∈ S
⊢ ⋂₀ ↑(insert a s) ∈ S

Tactic:
simpa

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ = A
⊢ s✝ = A ∩ Set.univ

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ᶠ (n : ι) in l, p n
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
rw [frequently_iff_seq_frequently] at h
  obtain ⟨x, hx_tendsto, hx_freq⟩ := h
  obtain ⟨n_to_n, h_tendsto, h_freq⟩ := subseq_forall_of_frequently hx_tendsto hx_freq
  exact ⟨x ∘ n_to_n, h_tendsto, h_freq⟩

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 b : α
m : ℤ
⊢ b - toIcoDiv hp a b • p + m • p ∈ Set.Ico (a + m • p) (a + p + m • p)

Tactic:
simpa using sub_toIcoDiv_zsmul_mem_Ico hp a b

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 b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b + m) • p ∈ Set.Ioc a (a + p)

Tactic:
simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIocDiv_zsmul_mem_Ioc hp a b

Goal state after: