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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W'✝ : C
x : W'✝ ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
⊢ x ≫ S₁.g ≫ φ.τ₃ = 0

Tactic:
reassoc_of% hx,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
W'✝ : C
x : W'✝ ⟶ S₁.X₂
hx : x ≫ S₁.g = 0
⊢ 0 ≫ φ.τ₃ = 0
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
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ h₂.homologyIso.hom = homologyMap φ ≫ h₂.homologyIso.hom
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₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ cyclesMap (opMap φ) = S₂.cyclesOpIso.hom ≫ S₂.cyclesOpIso.inv ≫ cyclesMap (opMap φ)

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ cyclesMap (opMap φ) = cyclesMap (opMap φ)
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
φ : S₁ ⟶ S₂
h : S₁.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝¹ : Epi (opMap φ).τ₁
this✝ : IsIso (opMap φ).τ₂
this : Mono (opMap φ).τ₃
⊢ S₂.RightHomologyData

Tactic:
exact (LeftHomologyData.ofEpiOfIsIsoOfMono' (opMap φ) h.op).unop

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
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
⊢ h.opcyclesIso.hom ≫ h.opcyclesIso.inv ≫ S.descOpcycles k hk = S.descOpcycles k hk

Tactic:
Iso.hom_inv_id_assoc

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
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
⊢ S.descOpcycles k hk = S.descOpcycles k hk
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ cyclesMap (F.mapShortComplex.map φ) =
    (S₁.mapCyclesIso F).hom ≫ (S₁.mapCyclesIso F).inv ≫ cyclesMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id_assoc

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ cyclesMap (F.mapShortComplex.map φ) = cyclesMap (F.mapShortComplex.map φ)
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap (F.mapShortComplex.map φ) =
    (S₁.mapLeftHomologyIso F).hom ≫ (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id_assoc

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasLeftHomology
inst✝² : S₂.HasLeftHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap (F.mapShortComplex.map φ) = leftHomologyMap (F.mapShortComplex.map φ)
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
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 ι
⊢ (isoHomology S hkf hcc fac).hom ≫ (isoHomology S hkf hcc fac).inv ≫ ι = ι

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
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 ι
⊢ ι = ι
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ opcyclesMap (F.mapShortComplex.map φ) =
    (S₁.mapOpcyclesIso F).hom ≫ (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id_assoc

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ opcyclesMap (F.mapShortComplex.map φ) = opcyclesMap (F.mapShortComplex.map φ)
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap (F.mapShortComplex.map φ) =
    (S₁.mapRightHomologyIso F).hom ≫ (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id_assoc

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap (F.mapShortComplex.map φ) = rightHomologyMap (F.mapShortComplex.map φ)
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) =
    (S₁.mapHomologyIso F).hom ≫ (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id_assoc

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) = homologyMap (F.mapShortComplex.map φ)
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) =
    (S₁.mapHomologyIso' F).hom ≫ (S₁.mapHomologyIso' F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
Iso.hom_inv_id_assoc

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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) = homologyMap (F.mapShortComplex.map φ)
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: case mp
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ IsIso (F.map γ.φH) → IsIso γ.φH

Tactic:
intro
    exact isIso_of_reflects_iso _ F

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

Goal state before:
pp: case mp
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
⊢ IsIso (F.map γ.φH) → IsIso γ.φH

Tactic:
intro
    exact isIso_of_reflects_iso _ F

Goal state after:
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
h : S.HomologyData
⊢ S.Exact ↔ IsZero h.right.H

Tactic:
have := HasHomology.mk' h
  exact RightHomologyData.exact_iff h.right

Goal state after:
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
hS : S.Exact
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ S.pOpcycles = 0

Tactic:
rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]

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
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map s.r ≫ F.map S.f + F.map S.g ≫ F.map s.s = 𝟙 (F.obj S.X₂)

Tactic:
simp only [← F.map_id, ← s.id, Functor.map_comp, Functor.map_add]

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
S : ShortComplex Cᵒᵖ
h : S.Splitting
⊢ (h.s.unop ≫ S.unop.f + S.unop.g ≫ h.r.unop).op = (𝟙 S.unop.X₂).op

Tactic:
simp only [unop_X₂, Opposite.op_unop, unop_X₁, unop_f, unop_X₃, unop_g, op_add,
      op_comp, Quiver.Hom.op_unop, op_id, ← h.id]
    abel

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ X.ofLEMk f h₁ ≫ ofMkLEMk f g h₂ = X.ofLEMk g ⋯

Tactic:
simp only [ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying,
    assoc, Iso.hom_inv_id_assoc]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
X : Subobject B
f : A₁ ⟶ B
inst✝¹ : Mono f
g : A₂ ⟶ B
inst✝ : Mono g
h₁ : X ≤ mk f
h₂ : mk f ≤ mk g
⊢ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso g).hom = underlying.map ⋯.hom ≫ (underlyingIso g).hom
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ (sup.obj f).obj g ⟶ h

Tactic:
refine homMk ?_ ?_

Goal state after:
case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ ((sup.obj f).obj g).obj.left ⟶ h.obj.left

case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ ?refine_1 ≫ h.arrow = ((sup.obj f).obj g).arrow
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinsetObj F),
        ι := Discrete.natTrans fun j ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    { pt := colimit (liftToFinsetObj F),
                ι :=
                  Discrete.natTrans fun j ↦
                    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.ι.app
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
⊢ colimit.ι (liftToFinsetObj F) t ≫ m =
    colimit.ι (liftToFinsetObj F) t ≫
      colimit.desc (liftToFinsetObj F)
        { pt := s.pt, ι := { app := fun x ↦ Sigma.desc fun x_1 ↦ s.ι.app ↑x_1, naturality := ⋯ } }

Tactic:
dsimp [liftToFinsetObj]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinsetObj F),
        ι := Discrete.natTrans fun j ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    { pt := colimit (liftToFinsetObj F),
                ι :=
                  Discrete.natTrans fun j ↦
                    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.ι.app
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
⊢ colimit.ι
        { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x, map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
          map_id := ⋯, map_comp := ⋯ }
        t ≫
      m =
    colimit.ι
        { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x, map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
          map_id := ⋯, map_comp := ⋯ }
        t ≫
      colimit.desc
        { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x, map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
          map_id := ⋯, map_comp := ⋯ }
        { pt := s.pt, ι := { app := fun x ↦ Sigma.desc fun x_1 ↦ s.ι.app ↑x_1, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
⊢ m ≫ limit.π (liftToFinsetObj F) t =
    limit.lift (liftToFinsetObj F)
        { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
      limit.π (liftToFinsetObj F) t

Tactic:
dsimp [liftToFinsetObj]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
⊢ m ≫
      limit.π
        { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
          map_id := ⋯, map_comp := ⋯ }
        t =
    limit.lift
        { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
          map_id := ⋯, map_comp := ⋯ }
        { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
      limit.π
        { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
          map_id := ⋯, map_comp := ⋯ }
        t
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
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫ 𝟙 ((StructuredArrow.right E).obj Y)

Tactic:
rw [← CostructuredArrow.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
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ F.map φ.left ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map (L.map φ.left ≫ g₂.hom)) ≫
      𝟙 ((StructuredArrow.right E).obj Y)
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✝ E'✝ : L.RightExtension F
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
⊢ φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫ (CostructuredArrow.hom E).app G.right

Tactic:
rw [← CostructuredArrow.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✝ E'✝ : L.RightExtension F
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
⊢ φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫
      (((whiskeringLeft C D H).obj L).map φ.left ≫ CostructuredArrow.hom E').app G.right
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop ⋯).op ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop =
    (𝟙 A).unop

pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
· simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc,
        cokernel.π_desc, Category.comp_id]

Goal state after:
case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : Category.{v_4, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom = colimit.ι F i

Tactic:
simp [colimitIsoOfIsLeftKanExtension]

Goal state after: