mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ NormalMono.Z u
hl : cokernel.π f ≫ l = h
⊢ i ≫ cokernel.π f ≫ l = 0 ≫ l

Tactic:
rw [← Category.assoc, kernel.condition]

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

Goal state before:
pp: J : Type w
f : J → AddCommGrpCat
s : Fan f
x y : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) (x + y)) =
    (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x) + fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) y

Tactic:
simp only [Functor.const_obj_obj, map_add]

Goal state after:
J : Type w
f : J → AddCommGrpCat
s : Fan f
x y : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x + (ConcreteCategory.hom (s.π.app { as := j })) y) =
    (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x) + fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) y
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) (fun s ↦ s.ι ≫ prod.fst) ⋯ ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := epiIsCokernelOfKernel (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) hp1
Z : C
z : cokernel (diag A) ⟶ Z
hz : r A ≫ z = 0
h : prod.lift (𝟙 A) 0 ≫ cokernel.π (diag A) ≫ z = 0
t : (CokernelCofork.ofπ prod.snd hlp).pt ⟶ Z
ht : prod.snd ≫ t = cokernel.π (diag A) ≫ z
htt : t = 0
⊢ prod.snd ≫ t = cokernel.π (diag A) ≫ 0

Tactic:
htt,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) (fun s ↦ s.ι ≫ prod.fst) ⋯ ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := epiIsCokernelOfKernel (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) hp1
Z : C
z : cokernel (diag A) ⟶ Z
hz : r A ≫ z = 0
h : prod.lift (𝟙 A) 0 ≫ cokernel.π (diag A) ≫ z = 0
t : (CokernelCofork.ofπ prod.snd hlp).pt ⟶ Z
ht : prod.snd ≫ t = cokernel.π (diag A) ≫ z
htt : t = 0
⊢ prod.snd ≫ 0 = cokernel.π (diag A) ≫ 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext (Iso.refl ((parallelPair (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ (Iso.refl (KernelFork.ofι (F.map i) ⋯).pt).hom ≫
      Fork.ι ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i ⋯))) =
    Fork.ι (KernelFork.ofι (F.map i) ⋯)

Tactic:
change 𝟙 _ ≫ F.map i ≫ 𝟙 _ = F.map i

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext (Iso.refl ((parallelPair (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ 𝟙 (F.obj X) ≫ F.map i ≫ 𝟙 (F.obj Y) = F.map i
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
⊢ f ≫ d = (biprod.inl ≫ biprod.desc f (-g)) ≫ d

Tactic:
by rw [biprod.inl_desc]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : b ∉ (Hom.hom f).range
r : b⁻¹ ∈ (Hom.hom f).range
⊢ False

Tactic:
exact hb (inv_inv b ▸ Subgroup.inv_mem _ r)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ e = biprod.inl ≫ biprod.desc e 0

Tactic:
by rw [biprod.inl_desc]

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₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ (CokernelCofork.IsColimit.ofId S.f hf).desc (CokernelCofork.ofπ S.g ⋯) = 0

Tactic:
by
    change 𝟙 _ ≫ S.g = 0
    simp only [hg, comp_zero]

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 : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftRightHomologyComparison' h₁ h₂ = h₁.homologyIso.inv ≫ h₂.homologyIso.hom

Tactic:
by
  rw [leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap'
    S.homologyData h₁ h₂]
  dsimp only [LeftHomologyData.homologyIso, LeftHomologyData.leftHomologyIso,
    Iso.symm, Iso.trans, Iso.refl, leftHomologyMapIso', leftHomologyIso,
    RightHomologyData.homologyIso, RightHomologyData.rightHomologyIso,
    rightHomologyMapIso', rightHomologyIso]
  simp only [assoc, ← leftHomologyMap'_comp_assoc, id_comp, ← rightHomologyMap'_comp]

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
S S₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
hg' : g' = F.map h.g'
⊢ F.map h.ι ≫ g' = 0

Tactic:
rw [hg', ← F.map_comp, ι_g', F.map_zero]

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₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Tactic:
by
  have γ : RightHomologyMapData φ h₁ h₂ := default
  have γ' : RightHomologyMapData φ' h₁ h₂ := default
  simp only [γ.opcyclesMap'_eq, γ'.opcyclesMap'_eq,
    (γ.add γ').opcyclesMap'_eq, RightHomologyMapData.add_φQ]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
Z'✝ : C
k : cokernel S.f ⟶ Z'✝
hk : (kernel.ι S.g ≫ cokernel.π S.f) ≫ k = 0
⊢ kernel.ι S.g ≫ cokernel.π S.f ≫ k = 0

Tactic:
by simpa only [assoc] using hk

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

Goal state before:
pp: case h₁
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:
exact h₁.uniq (π₁.mapCocone s) _ (fun j => π₁.congr_map (hm j))

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ parallelPair ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0 ≅
    parallelPair S.toCycles 0

pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj (CokernelCofork.ofπ π ⋯) ≅ CokernelCofork.ofπ S.homologyπ ⋯

Tactic:
· exact parallelPair.ext (Iso.refl _) (S.isoCyclesOfIsLimit hkf)

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (Cocone.precompose
          (parallelPair.ext
              (Iso.refl
                ((parallelPair ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0).obj
                  WalkingParallelPair.zero))
              (S.isoCyclesOfIsLimit hkf) ⋯ ⋯).inv).obj
      (CokernelCofork.ofπ π ⋯) ≅
    CokernelCofork.ofπ S.homologyπ ⋯
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (Cocone.precompose
          (parallelPair.ext
              (Iso.refl
                ((parallelPair ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0).obj
                  WalkingParallelPair.zero))
              (S.isoCyclesOfIsLimit hkf) ⋯ ⋯).inv).obj
      (CokernelCofork.ofπ π ⋯) ≅
    CokernelCofork.ofπ S.homologyπ ⋯

Tactic:
exact Cofork.ext (isoHomology S hkf hcc fac) (by simp [Cofork.π])

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:
ShortComplex.homologyMap_mapNatTrans,

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✝⁸ : 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 ≫
      ((S.mapHomologyIso F).hom ≫ τ.app S.homology ≫ (S.mapHomologyIso G).inv) ≫ (S.mapHomologyIso G).hom
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
inst✝ : S.HasHomology
⊢ S.Exact ↔ IsZero S.homology

Tactic:
constructor
  · rintro ⟨⟨h', z⟩⟩
    exact IsZero.of_iso z h'.left.homologyIso
  · intro h
    exact ⟨⟨_, h⟩⟩

Goal state after:
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
inst✝ : HasZeroObject C
s : S.Splitting
⊢ S.LeftHomologyData

Tactic:
have hi := KernelFork.IsLimit.ofι S.f S.zero
    (fun x _ => x ≫ s.r)
    (fun x hx => by simp only [assoc, s.r_f, comp_sub, comp_id,
      sub_eq_self, reassoc_of% hx, zero_comp])
    (fun x _ b hb => by simp only [← hb, assoc, f_r, comp_id])

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
inst✝ : HasZeroObject C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
⊢ S.LeftHomologyData
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
Q : MonoOver X
e : (Quotient.mk'' Q).out ≅ Q
⊢ mk (arrow (Quotient.mk'' Q)) = Quotient.mk'' Q

Tactic:
exact Quotient.sound' ⟨MonoOver.isoMk (Iso.refl _) ≪≫ e⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
h : X ≤ mk f
⊢ Mono (X.ofLEMk f h)

Tactic:
dsimp only [ofLEMk]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ f = (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ g

Tactic:
equalizer.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ g = (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g ≫ g
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
W : C
h : W ⟶ X
inst✝ : HasPullbacks C
⊢ (equalizerSubobject (h ≫ f) (h ≫ g)).Factors ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow

Tactic:
apply equalizerSubobject_factors
    have := (Subobject.isPullback h (equalizerSubobject f g)).w
    rw [← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      ← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      equalizerSubobject_arrow_comp]

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

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
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) F

Tactic:
refine preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
X Y : C
f : X ⟶ Y
⊢ IsColimit (F.mapCocone (Cofork.ofπ (cokernel.π f) ⋯))
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L ⟶ S.map L :=
  { τ₁ := 𝟙 ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L).X₁,
    τ₂ := 𝟙 ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L).X₂,
    τ₃ := L.map (Abelian.factorThruCoimage S.g), comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (S.map L).Exact

Tactic:
apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).1

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
φ : { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L ⟶ S.map L := ⋯
⊢ ({ X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := coimage.π S.g, zero := ⋯ }.map L).Exact
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
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
⊢ L'.HasPointwiseRightKanExtensionAt F Y'

Tactic:
← hasPointwiseRightKanExtensionAt_iff_of_natIso_left F eL,

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
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F Y'
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 L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L'.HasPointwiseRightKanExtensionAt F' Y

Tactic:
by
  rw [hasPointwiseRightKanExtensionAt_iff_of_natIso_left _ e₁.symm]
  let e : StructuredArrow.proj Y L ⋙ F' ≅ StructuredArrow.proj Y L ⋙ F :=
    NatIso.ofComponents fun X ↦ (e₂.app _).symm
  rw [HasPointwiseRightKanExtensionAt, hasLimit_iff_of_iso e]
  infer_instance

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsSeparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsSeparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op Y
⊢ (h ≫ f.op).unop = (h ≫ g.op).unop
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCoseparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCoseparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : Cᵒᵖ
hG : P.op G
h : op X ⟶ G
⊢ (f.op ≫ h).unop = (g.op ≫ h).unop
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ (CommGrpCat.Hom.hom
        (((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm
          (f✝ ≫ g✝)))
      x✝ =
    (CommGrpCat.Hom.hom
        (abelianize.map f✝ ≫
          ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
      x✝

Tactic:
simp +instances only

Goal state after:
X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ (CommGrpCat.Hom.hom
        (((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm
          (f✝ ≫ g✝)))
      x✝ =
    (CommGrpCat.Hom.hom
        (abelianize.map f✝ ≫
          ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
      x✝
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b c : α
⊢ sbtw a b c ↔ ¬btw c b a

Tactic:
sbtw_iff_btw_not_btw

Goal state after:
α : Type u_1
inst✝ : CircularOrder α
a b c : α
⊢ btw a b c ∧ ¬btw c b a ↔ ¬btw c b a
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
x : ↥(supExtensionOfMaxSingleton i f y)
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
have mem1 : x.1 ∈ (_ : Set _) := x.2
  rw [Submodule.coe_sup] at mem1
  rcases mem1 with ⟨a, a_mem, b, b_mem : b ∈ (Submodule.span R _ : Submodule R N), eq1⟩
  rw [Submodule.mem_span_singleton] at b_mem
  rcases b_mem with ⟨z, eq2⟩
  exact ⟨⟨a, a_mem⟩, z, by rw [← eq1, ← eq2]⟩

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

Goal state before:
pp: case coprime.hd
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
hb : b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)
hab_pos : a * b ≠ 0
⊢ _root_.Disjoint a.factorization.support b.factorization.support

Tactic:
exact hab.disjoint_primeFactors

Goal state after: