mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (p ≫ g) = G.map p ≫ G.map g

Tactic:
G.map_comp

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map p ≫ G.map g = G.map p ≫ G.map g
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
rw [← G.map_comp, hpq, G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (p ≫ g) = G.map p ≫ G.map g

Tactic:
G.map_comp

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map p ≫ G.map g = G.map p ≫ G.map g
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
rw [← G.map_comp, hpq, G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ Cofork.π (CokernelCofork.ofπ (Cofork.π (CokernelCofork.ofπ (F.map f) ⋯)) ⋯) ≫
      (Iso.refl (CokernelCofork.ofπ (Cofork.π (CokernelCofork.ofπ (F.map f) ⋯)) ⋯).pt).hom =
    Cofork.π ((Cocone.precomposeEquivalence (compNatIso F)).functor.obj (F.mapCocone (CokernelCofork.ofπ f ⋯)))

Tactic:
simp [compNatIso, Cofork.π]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = σ ≫ g

Tactic:
hfg

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ g = σ ≫ g
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case a.f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| a

pp: case a.g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| σ

Tactic:
← Category.comp_id a

Goal state after:
case a.f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| a ≫ 𝟙 Y

case a.g
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| 0

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
| σ
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
p : X ⟶ Y
inst✝³ : HasKernel p
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Epi (F.map p)
inst✝ : PreservesLimit (parallelPair p 0) F
⊢ IsColimit (F.mapCocone (CokernelCofork.ofπ p ⋯))

Tactic:
let e : parallelPair (kernel.ι p) 0 ⋙ F ≅ parallelPair (kernel.ι (F.map p)) 0 :=
    parallelPair.ext (asIso (kernelComparison p F)) (Iso.refl _) (by simp) (by simp)
  refine IsColimit.precomposeInvEquiv e _ ?_
  let hp := Abelian.epiIsCokernelOfKernel _ (kernelIsKernel (F.map p))
  refine IsColimit.ofIsoColimit hp (Cofork.ext (Iso.refl _) ?_)
  change F.map p ≫ 𝟙 _ = 𝟙 _ ≫ F.map p
  rw [Category.comp_id, Category.id_comp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g ≫ e₃.inv ≫ e₃.hom

Tactic:
e₃.inv_hom_id,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁ S₂ S₃ : ShortComplex C
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom
comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom
⊢ e₂.inv ≫ S₁.g ≫ e₃.hom = S₂.g ≫ 𝟙 S₂.X₃
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
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyData.op.opcyclesIso.hom ≫ S.leftHomologyData.f'.op = S.op.fromOpcycles

Tactic:
rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles,
    RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]

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
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ S.liftCycles k hk ≫ cyclesMap φ = S₁.liftCycles (k ≫ φ.τ₂) ⋯

Tactic:
by
  cat_disch

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.HomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : h.left.IsPreservedBy F
inst✝ : h.right.IsPreservedBy F
⊢ (h.left.map F).π ≫ (F.mapIso h.iso).hom ≫ (h.right.map F).ι = (h.left.map F).i ≫ (h.right.map F).p

Tactic:
simpa only [F.map_comp] using! F.congr_map h.comm

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 : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
⊢ PreservesColimit (parallelPair h'.f' 0) F

Tactic:
let e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
          parallelPair.ext (Iso.refl _) (ShortComplex.cyclesMapIso' (Iso.refl S) h h')
            (by simp) (by simp)

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 : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero))
    (ShortComplex.cyclesMapIso' (Iso.refl S) h h') ⋯ ⋯
⊢ PreservesColimit (parallelPair h'.f' 0) F
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
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

Tactic:
simp only [γ.opcyclesMap'_eq, γ.neg.opcyclesMap'_eq, RightHomologyMapData.neg_φQ]

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

Goal state before:
pp: case mpr
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)) →
    (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
· tauto

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
hS : S.Exact
inst✝ : HasZeroObject C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ Mono ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))

Tactic:
refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
      hS.mono_fromOpcycles

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
⊢ Arrow.mk ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) ≅
    Arrow.mk S.fromOpcycles
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y : D
f : L.obj X ⟶ Y
⊢ ((adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y) f =
    hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ R'.map (iD.map f) ≫ comm2.hom.app Y)

Tactic:
by
  -- This proof was just `simp [restrictFullyFaithful]` before https://github.com/leanprover-community/mathlib4/pull/16317
  apply hiC.map_injective
  simp only [homEquiv_apply, Functor.map_comp, map_restrictFullyFaithful_unit_app,
    Functor.id_obj, assoc, Functor.FullyFaithful.map_preimage]
  congr 2
  exact (comm2.hom.naturality _).symm

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver (e.functor.obj X)
⊢ Mono ((Over.post e.inverse).obj ((forget (e.functor.obj X)).obj f)).hom

Tactic:
dsimp
        infer_instance

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

Goal state before:
pp: case hf₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.op.f = 0

Tactic:
dsimp
    rw [hg₁, op_zero]

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
X' Y' : C
f' : X' ⟶ Y'
inst✝¹ : HasKernel f'
X'' Y'' : C
f'' : X'' ⟶ Y''
inst✝ : HasKernel f''
sq : Arrow.mk f ⟶ Arrow.mk f'
sq' : Arrow.mk f' ⟶ Arrow.mk f''
⊢ kernelSubobjectMap (sq ≫ sq') = kernelSubobjectMap sq ≫ kernelSubobjectMap sq'

Tactic:
by
  cat_disch

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
⊢ Epi ((imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow)

Tactic:
have := epi_image_of_epi f

Goal state after:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
this : Epi (image.ι f)
⊢ Epi ((imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow)
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv) ≫ (imageSubobject (Arrow.mk g).hom).arrow =
    ((imageSubobjectIso f).inv ≫ imageSubobjectMap sq) ≫ (imageSubobject (Arrow.mk g).hom).arrow

Tactic:
simpa using image.map_ι sq

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

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

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

Goal state after:
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.ι (smallCoproductDesc s) =
    (mk (image.ι (smallCoproductDesc s))).arrow

Tactic:
underlyingIso_hom_comp_eq_mk

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
⊢ (mk (image.ι (smallCoproductDesc s))).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
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = (c.ι.app { as := j }).op

Tactic:
← opCoproductIsoProduct'_inv_comp_inj hc hf

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ HasBinaryCoproduct (op A) (op B)

Tactic:
have : HasProduct fun x ↦ (WalkingPair.casesOn x A B : C) := ‹_›

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
⊢ HasBinaryCoproduct (op A) (op B)
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✝ : L.LeftExtension F
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
⊢ ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
    (StructuredArrow.hom E').app G.left ≫ (StructuredArrow.right E').map G.hom

Tactic:
← StructuredArrow.w φ

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✝ : L.LeftExtension F
Y : D
E E' : L.LeftExtension F
φ : E ⟶ E'
G : CostructuredArrow L Y
⊢ ((StructuredArrow.hom E).app G.left ≫ (StructuredArrow.right E).map G.hom) ≫ (StructuredArrow.Hom.right φ).app Y =
    (StructuredArrow.hom E ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.Hom.right φ)).app G.left ≫
      (StructuredArrow.right E').map G.hom
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 Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ (ConcreteCategory.hom (F.map (CostructuredArrow.mkPrecomp g f).op)) ((ConcreteCategory.hom (F.map (eqToHom ⋯))) x) =
    (ConcreteCategory.hom (F.map (eqToHom ⋯))) ((ConcreteCategory.hom (F.map (CostructuredArrow.mkPrecomp g' f).op)) x)

Tactic:
by
  cat_disch

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
⊢ map₁ (𝟙 F) = id

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} D
inst✝⁹ : Category.{v_2, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ ((Cocone.precompose (G.isoWhiskerLeft (preservesLimitNatIso F).symm).inv).obj
              (((whiskeringRight J C D).obj F ⋙ lim).mapCocone c)).ι.app
        i ≫
      ((preservesLimitNatIso F).symm.app c.pt).hom =
    (F.mapCocone (lim.mapCocone c)).ι.app i

Tactic:
simp only [Functor.comp_obj, lim_obj, Functor.mapCocone_pt, isoWhiskerLeft_inv, Iso.symm_inv,
        Cocone.precompose_obj_pt, whiskeringRight_obj_obj, Functor.const_obj_obj,
        Cocone.precompose_obj_ι, NatTrans.comp_app, whiskerLeft_app, preservesLimitNatIso_hom_app,
        Functor.mapCocone_ι_app, Functor.comp_map, whiskeringRight_obj_map, lim_map, Iso.app_hom,
        Iso.symm_hom, preservesLimitNatIso_inv_app, Category.assoc]

Goal state after:
C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} D
inst✝⁹ : Category.{v_2, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ (preservesLimitIso F (G.obj i)).hom ≫ limMap (whiskerRight (c.ι.app i) F) ≫ (preservesLimitIso F c.pt).inv =
    F.map (limMap (c.ι.app i))
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
⊢ HasCokernel f

Tactic:
have : PreservesColimits G := adj.leftAdjoint_preservesColimits
      have : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f := by
        simpa using NatIso.naturality_1 i f
      rw [← this]
      have : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
      apply Limits.hasCokernel_epi_comp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ IsSeparator (G ⨿ H) ↔ (ObjectProperty.pair G H).IsSeparating

Tactic:
refine (isSeparator_iff_of_isColimit_cofan (coprodIsCoprod G H)).trans ?_

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ (ObjectProperty.ofObj fun j ↦ WalkingPair.casesOn j G H).IsSeparating ↔ (ObjectProperty.pair G H).IsSeparating
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₁ u₂ : F.Elementsᵒᵖ
g : u₁ ⟶ u₂
⊢ (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).map g ≫
      ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₂).snd) =
    (↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₁).snd) ≫
      ((const F.Elementsᵒᵖ).obj (F.obj X)).map g

Tactic:
by
    ext f
    obtain ⟨f, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective f
    simp [shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
x : c.pt
⊢ ∃ i y, c.inj i y = x

Tactic:
by
  obtain ⟨⟨i⟩, y, rfl⟩ := hc.ι_jointly_surjective x
  exact ⟨i, y, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
x✝ : ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
h₁ : i₁ = i₂
h₂ : y₂ = cast ⋯ y₁
⊢ c.inj i₁ y₁ = c.inj i₂ y₂

Tactic:
subst h₁ h₂; rfl

Goal state after: