mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := ⋯
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := ⋯
⊢ IsLimit (F.mapCone c)

Tactic:
apply IsLimit.ofIsoLimit _ ((Cone.functoriality _ F).mapIso (Fork.isoForkOfι c).symm)

Goal state after:
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
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := ⋯
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := ⋯
⊢ IsLimit ((Cone.functoriality (parallelPair f g) F).obj (Fork.ofι (Fork.ι c) ⋯))
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₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f

Tactic:
have : Mono S₁.f ↔ Mono S₂.f :=
    (MorphismProperty.monomorphisms C).arrow_mk_iso_iff
      (Arrow.isoMk (ShortComplex.π₁.mapIso e) (ShortComplex.π₂.mapIso e) e.hom.comm₁₂)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
this : Mono S₁.f ↔ Mono S₂.f
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel).hom ≫ (Arrow.mk S.fromOpcycles).hom =
    (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫
      (Iso.refl
          (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right).hom

Tactic:
apply Cofork.IsColimit.hom_ext hcc

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ Cofork.π cc ≫ (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel).hom ≫ (Arrow.mk S.fromOpcycles).hom =
    Cofork.π cc ≫
      (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫
        (Iso.refl
            (Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right).hom
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ S.g ≫ s.s = 𝟙 S.X₂ - s.r ≫ S.f

Tactic:
by rw [← s.id, add_sub_cancel_left]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ ((limit.isLimit (parallelPair (g.unop ≫ i.unop.hom) 0)).conePointUniqueUpToIso
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom ⋯)).hom ≫
      kernel.ι g.unop =
    kernel.ι (i.hom ≫ g).unop

Tactic:
· dsimp
          simp only [← Iso.eq_inv_comp, limit.conePointUniqueUpToIso_inv_comp,
            Fork.ofι_π_app]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom = 0

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ (kernel.ι S.g ≫ cokernel.π S.f) ≫ e₂.hom = 0
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
Z'✝ : C
u : S.X₂ ⟶ Z'✝
hu : S.f ≫ u = 0
⊢ kernel.ι S.g ≫ cokernel.π S.f ≫ cokernel.desc S.f u hu = 0

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
Z'✝ : C
u : S.X₂ ⟶ Z'✝
hu : S.f ≫ u = 0
⊢ (kernel.ι S.g ≫ cokernel.π S.f) ≫ cokernel.desc S.f u hu = 0
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          { I := underlying.obj f, m := f.arrow, m_mono := ⋯,
            e := Sigma.desc fun b ↦ Subtype.casesOn b fun g m ↦ underlying.map (homOfLE ⋯), fac := ⋯ }) ≫
      f.arrow =
    (sSup s).arrow

Tactic:
dsimp [sSup]

Goal state after:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          { I := underlying.obj f, m := f.arrow, m_mono := ⋯, e := Sigma.desc fun b ↦ underlying.map (homOfLE ⋯),
            fac := ⋯ }) ≫
      f.arrow =
    (mk (image.ι (smallCoproductDesc s))).arrow
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ (f'.π.app { as := j }).op =
    (f.π.app { as := j }).op ≫ (opProductIsoCoproduct' hf hc).hom ≫ hc.desc (Cofan.mk (op f'.pt) fun a ↦ (f'.proj a).op)

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ (f'.π.app { as := j }).op =
    ((f.π.app { as := j }).op ≫ (opProductIsoCoproduct' hf hc).hom) ≫
      hc.desc (Cofan.mk (op f'.pt) fun a ↦ (f'.proj a).op)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
⊢ (opProductIsoCoproduct' hf hc).inv ≫ (hf.lift f').op = hc.desc f'.op

Tactic:
refine (Iso.inv_comp_eq _).mpr (Quiver.Hom.unop_inj (hf.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))
  simp only [Discrete.functor_obj, unop_op, Quiver.Hom.unop_op, IsLimit.fac, Fan.op, unop_comp,
    Category.assoc, op_comp, op_unop, Quiver.Hom.op_unop]
  erw [← Category.assoc, proj_comp_opProductIsoCoproduct'_hom, IsColimit.fac]
  rfl

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

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
L' : C ⥤ D
e : L ≅ L'
Y : D
⊢ L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
revert L L' e
  suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseRightKanExtensionAt L F Y],
      HasPointwiseRightKanExtensionAt L' F Y from
    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
  intro L L' e _
  let Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso _ e.symm
  let e' : StructuredArrow.proj Y L' ⋙ F ≅
    Φ.functor ⋙ StructuredArrow.proj Y L ⋙ F := Iso.refl _
  exact hasLimit_of_iso e'.symm

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
a✝ : L.HasPointwiseLeftKanExtensionAt F Y
⊢ L'.HasPointwiseLeftKanExtensionAt F Y'

Tactic:
exact hasPointwiseLeftKanExtensionAt_of_equivalence L L' F E eL Y Y' e

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
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : C
⊢ colimit.ι G X ≫ (L.colimitIsoColimitGrothendieck G).hom =
    colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G)
      { base := L.obj X, fiber := CostructuredArrow.mk (𝟙 (L.obj X)) }

Tactic:
rw [← Iso.eq_comp_inv]
  exact (ι_colimitIsoColimitGrothendieck_inv L G ⟨L.obj X, .mk (𝟙 _)⟩).symm

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
s : yoneda.obj X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ op (CostructuredArrow.mk s) = op (CostructuredArrow.mk (mk s x).fst)

Tactic:
YonedaCollection.mk_fst

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
x : F.obj (op (CostructuredArrow.mk s))
⊢ op (CostructuredArrow.mk s) = op (CostructuredArrow.mk s)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ limit.π (StructuredArrow.proj X L ⋙ F) j =
    𝟙 (limit (StructuredArrow.proj X L ⋙ F)) ≫
      limit.lift (StructuredArrow.proj (L.obj j.right) L ⋙ F)
          { pt := limit (StructuredArrow.proj X L ⋙ F),
            π :=
              { app := fun g ↦ limit.π (StructuredArrow.proj X L ⋙ F) ((StructuredArrow.map j.hom).obj g),
                naturality := ⋯ } } ≫
        limit.π (StructuredArrow.proj (L.obj j.right) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj j.right)))

Tactic:
simp only [limit.lift_π, StructuredArrow.map_mk, id_comp]

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
j : StructuredArrow X L
⊢ limit.π (StructuredArrow.proj X L ⋙ F) j =
    limit.π (StructuredArrow.proj X L ⋙ F) (StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right)))
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this : (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j) ≫ m = s.ι.app (L.obj j)
⊢ (α.app j ≫ (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j)) ≫ m =
    c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }

Tactic:
rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app]

Goal state after:
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 ≫
      S.map (Subobject.underlyingIso f.unop.left.op).inv.unop ≫ (unop P).hom =
    A.hom

Tactic:
← Category.assoc,

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.mk f.unop.left.op).arrow.unop ≫ S.map (Subobject.underlyingIso f.unop.left.op).inv.unop) ≫
      (unop P).hom =
    A.hom
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)
inst✝ : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.π.app one = l ≫ s.π.app one

Tactic:
← s.app_zero (Classical.arbitrary J),

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.π.app zero ≫ f (Classical.arbitrary J) = l ≫ s.π.app zero ≫ f (Classical.arbitrary J)
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))
⊢ Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv)

Tactic:
suffices Epi (iX.inv ≫ lim.map f ≫ iY.hom) from inferInstance

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))
⊢ Epi (iX.inv ≫ lim.map f ≫ iY.hom)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype (ZMod n)ˣ
⊢ Fintype.card { x // x.val.Coprime n } = φ n

Tactic:
obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero NeZero.out
      simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ←
        Fin.sum_univ_eq_sum_range, @Nat.coprime_comm (m + 1)]
      rfl

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

Goal state before:
pp: case basic
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h : s✝ ∈ insert A S
⊢ s✝ ∈ S ∨ ∃ Q ∈ S, s✝ = A ∩ Q

Tactic:
cases h
    · exact Or.inr ⟨Set.univ, cond.univ_mem, by simpa⟩
    · exact Or.inl (by assumption)

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : a = 0
⊢ a = b

pp: case neg
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
⊢ a = b

Tactic:
· rw [ha', totient_zero, eq_comm, totient_eq_zero] at h'
    rw [h', ha']

Goal state after:
case neg
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
⊢ a = b
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 : α
⊢ toIocMod hp a b + toIocDiv hp a b • p = b

Tactic:
rw [toIocMod, sub_add_cancel]

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

Tactic:
← toIcoDiv_eq_of_sub_zsmul_mem_Ico hp hc,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
n : ℤ
hc : b - n • p ∈ Set.Ico a (a + p)
⊢ toIcoMod hp a b = b - toIcoDiv hp a b • p
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u_2
t₁ t₂ : TopologicalSpace X
⊢ (∀ (x : Set X), IsOpen[t₁] xᶜ ↔ IsOpen[t₂] xᶜ) ↔ ∀ (s : Set X), IsClosed[t₁] s ↔ IsClosed[t₂] s

Tactic:
simp only [@isOpen_compl_iff _ _ t₁, @isOpen_compl_iff _ _ t₂]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : ∃ n, c - b = n • p
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
rcases h with ⟨z, hz⟩
    rw [sub_eq_iff_eq_add] at hz
    rw [hz, toIcoMod_zsmul_add]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ Dense {x}ᶜ → ¬IsOpen {x}

Tactic:
intro hd ho
    exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)

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 : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ (∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)) → toIcoMod hp a b = a

Tactic:
rw [← not_exists, not_imp_comm]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
tfae_4_to_3 : toIcoMod hp a b + p = toIocMod hp a b → toIcoMod hp a b ≠ toIocMod hp a b
tfae_1_to_4 : toIcoMod hp a b = a → toIcoMod hp a b + p = toIocMod hp a b
⊢ ¬toIcoMod hp a b = a → ∃ x, b - x • p ∈ Set.Ioo a (a + p)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ⊆ s ↔ IsClosed s

Tactic:
closure_subset_iff_isClosed

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed s ↔ IsClosed s
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 c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬b ≡ a [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False

Tactic:
rw [modEq_comm] at h

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c
h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b
h : ¬a ≡ b [PMOD p] ∧ ¬c ≡ b [PMOD p] ∧ ¬a ≡ c [PMOD p]
⊢ False
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
⊢ p x ∈ g ⁻¹' q '' V → p x ∈ U

pp: case mp.mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
⊢ p x ∈ U → p x ∈ g ⁻¹' q '' V

Tactic:
· rintro ⟨y, hy, e'⟩
      obtain ⟨y, rfl⟩ := H ⟨_, ⟨x, rfl⟩, (e'.trans (congr_fun h x)).symm⟩
      rw [← hg ((congr_fun h y).trans e')]
      exact e.le hy

Goal state after:
case mp.mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
⊢ p x ∈ U → p x ∈ g ⁻¹' q '' V
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
sc_st : HasSeparatingCover s₂ t₂
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
obtain ⟨u, u_cov, u_props⟩ := sc_st

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
u : ℕ → Set X
u_cov : s₂ ⊆ ⋃ n, u n
u_props : ∀ (n : ℕ), IsOpen[inst✝] (u n) ∧ Disjoint (closure[inst✝] (u n)) t₂
⊢ HasSeparatingCover s₁ t₁
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
⊢ Continuous[t₁, t₂ ⊓ t₃] f ↔ Continuous[t₁, t₂] f ∧ Continuous[t₁, t₃] f

Tactic:
by
  simp only [continuous_iff_coinduced_le, le_inf_iff]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : DiscreteTopology X
inst✝ : DiscreteTopology Y
x✝ : X × Y
a : X
b : Y
⊢ 𝓝 (a, b) = pure (a, b)

Tactic:
by
    rw [nhds_prod_eq, nhds_discrete X, nhds_discrete Y, prod_pure_pure]

Goal state after: