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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ Epi (Φ.shortComplexObj X).g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
⊢ Epi (Φ.colonπ Ψ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsPullback ((Φ.colon Ψ).ι.app X) ((Φ.colonπ Ψ).app X) (Φ.π.app X) (Ψ.ι.app (Φ.quotient.obj X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{?u.4, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
⊢ Φ.ι ≫ Φ.π = 0 ≫ Φ.quotient.whiskerLeft Ψ.ι ≫ Φ.quotient.rightUnitor.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
⊢ Over.Hom.left (Φ.toColon Ψ).hom ≫ Φ.colonπ Ψ = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ (Over.Hom.left (Φ.toColon Ψ).hom).app X ≫ (Φ.colon Ψ).ι.app X = Φ.ι.app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X)
⊢ (Over.Hom.left (Φ.toColon Ψ).hom).app X ≫ (Φ.colonπ Ψ).app X = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ HomologicalComplex.quasiIso C (ComplexShape.up ℤ) R.ι'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
⊢ (Φ.colon Ψ).ι.app X ≫ Φ.π.app X = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ { X₁ := I.cocomplex.X (n + 1), X₂ := I.cocomplex.X (n + 1 + 1), X₃ := I.cocomplex.X (n + 1 + 2),
          f := I.cocomplex.d (n + 1) (n + 1 + 1), g := I.cocomplex.d (n + 1 + 1) (n + 1 + 2), zero := ⋯ }.f ≫
      (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ f.f 0 = I.cocomplex.d 0 1 ≫ descHomotopyZeroZero f comm

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ f.f 1 = descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 + I.cocomplex.d 1 2 ≫ descHomotopyZeroOne f comm

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x)).hom =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
n : ℕ
x✝ :
  (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ×'
    (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
      f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f'
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = g ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ g'
⊢ f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
n : ℕ
x✝ :
  (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ×'
    (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
      f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f'
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = g ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ g'
⊢ f.f (n + 2) =
    ⟨g, ⟨g', w⟩⟩.snd.fst ≫ J.cocomplex.d (n + 1) (n + 2) +
      I.cocomplex.d (n + 2) (n + 3) ≫ descHomotopyZeroSucc f n g g' ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
I : InjectiveResolution Y
J : InjectiveResolution Z
g h : I.cocomplex ⟶ J.cocomplex
g_comm : I.ι ≫ g = (CochainComplex.single₀ C).map f ≫ J.ι
h_comm : I.ι ≫ h = (CochainComplex.single₀ C).map f ≫ J.ι
⊢ I.ι ≫ (g - h) = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
⊢ IsIso ((Over.Hom.left (Φ.toColon Ψ).hom).app X) ↔ IsZero (Ψ.r.obj (Φ.quotient.obj X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ Homotopy (desc (f ≫ g) K I) (desc f J I ≫ desc g K J)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X ≫ 𝟙 X) I I) (𝟙 I.cocomplex)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
⊢ IsIso (Φ.toColon Ψ) ↔ IsZero (Φ.quotient ⋙ Ψ.r)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X ≫ 𝟙 X) J J) (𝟙 J.cocomplex)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ I.ι ≫ (I.homotopyEquiv J).hom = J.ι

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ J.ι ≫ (I.homotopyEquiv J).inv = I.ι

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
x y : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ R.extEquivCohomologyClass.symm (x + y) = R.extEquivCohomologyClass.symm x + R.extEquivCohomologyClass.symm y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X : C
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X)) =
    𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ ∀ (x y : CohomologyClass ((singleFunctor C 0).obj X) R.cochainComplex ↑n),
    R.extEquivCohomologyClass.symm.toFun (x + y) =
      R.extEquivCohomologyClass.symm.toFun x + R.extEquivCohomologyClass.symm.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z✝) (injectiveResolution X✝)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
        (InjectiveResolution.desc f (injectiveResolution Y✝) (injectiveResolution X✝)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
        (InjectiveResolution.desc g (injectiveResolution Z✝) (injectiveResolution Y✝))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ ↑n + 1 = ↑m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ R.cochainComplex.d ↑n ↑m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ (injectiveResolutions C).map f ≫ J.iso.hom = I.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass (R.extMk f m hm hf) =
    CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ (f + g) ≫ R.cocomplex.d n m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ R.cochainComplex.d ↑n ↑m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ (g ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ R.cochainComplex.d ↑n ↑m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ I.iso.inv ≫ (injectiveResolutions C).map f = (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ ≫ J.iso.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
⊢ f ≫ d f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
⊢ f ≫ cokernel.π f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
⊢ { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ }.Exact

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z X₀✝ X₁✝ : C
f : X₀✝ ⟶ X₁✝
⊢ f ≫ d f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ (ofCocomplex Z).d 0 1 = d (Injective.ι Z)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (ComplexShape.up ℕ).prev (n + 1) = n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (ComplexShape.up ℕ).next (n + 1) = n + 1 + 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ (f - g) ≫ R.cocomplex.d n m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extMk f m hm hf - R.extMk g m hm hg = R.extMk (f - g) m hm ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ (-f) ≫ R.cocomplex.d n m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ HomologicalComplex.ExactAt (ofCocomplex Z) (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ R.cochainComplex.d ↑n ↑m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Injective ((ofCocomplex Z).X n)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫ (ofCocomplex Z).d 0 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ -R.extMk f m hm hf = R.extMk (-f) m hm ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ n m : ℕ
hm : n + 1 = m
⊢ 0 ≫ R.cocomplex.d n m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n m : ℕ
hm : n + 1 = m
⊢ R.extMk 0 m hm ⋯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ : ℕ
inst✝ : HasDerivedCategory C
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ ↑n + 1 = ↑m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Mono
    { X₁ := Z, X₂ := under Z, X₃ := syzygies (Injective.ι Z), f := Injective.ι Z, g := d (Injective.ι Z), zero := ⋯ }.f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ : ℕ
inst✝ : HasDerivedCategory C
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ R.cochainComplex.d ↑n ↑m = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ ↑p + 1 = ↑n

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : C
f : Over P
⊢ 𝟙 f.left ≫ f.hom = 𝟙 f.left ≫ f.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ (Iso.refl
          {
              X₁ :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                    ((CochainComplex.single₀ C).obj Z)).X₂,
              X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
              X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
              f :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                    (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
              g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
              zero := ⋯ }.X₁).hom ≫
      { X₁ := Z, X₂ := under Z, X₃ := syzygies (Injective.ι Z), f := Injective.ι Z, g := d (Injective.ι Z),
          zero := ⋯ }.f =
    {
          X₁ :=
            ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                ((CochainComplex.single₀ C).obj Z)).X₂,
          X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
          X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
          f :=
            ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
          g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
          zero := ⋯ }.f ≫
      (Iso.refl
          {
              X₁ :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
                    ((CochainComplex.single₀ C).obj Z)).X₂,
              X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
              X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
              f :=
                ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
                    (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
              g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g,
              zero := ⋯ }.X₂).hom

Tactic:
by

Goal state after: