mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝ : Functor.Linear R (L ⋙ G)
this : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
⊢ r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
⊢ IsSplitEpi π

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (ConcreteCategory.hom
        ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯))
      x.hom =
    (x.comp hS.extClass h).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
⊢ AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯) ≫ AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
⊢ inv (Q.map π) = Q.map (section_ π)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
K : CochainComplex C ℤ
w✝ : K.IsStrictlyLE i
π : K ⟶ (CochainComplex.singleFunctor C i).obj P
h : IsIso (Q.map π)
g : K ⟶ L
hπ : IsSplitEpi π
h₁ : inv (Q.map π) = Q.map (section_ π)
⊢ section_ π ≫ g = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i : ℤ
φ : Q.obj ((CochainComplex.singleFunctor C i).obj P) ⟶ Q.obj L
n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
⊢ φ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
P Y : C
n : ℕ
inst✝ : Projective P
e : Ext P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ↑n + 1 + -(↑n + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
P Y : C
n : ℕ
inst✝ : Projective P
e : Ext P Y (n + 1)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ -(↑n + 1) < 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
P Y : C
n : ℕ
inst✝ : Projective P
e : Ext P Y (n + 1)
⊢ e = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
⊢ Functor.Linear R F ↔ Functor.Linear R G

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex C :=
  { X₁ := kernel (Projective.π X), X₂ := Projective.over X, X₃ := X, f := kernel.ι (Projective.π X),
    g := Projective.π X, zero := ⋯ }
hS : S.ShortExact
x₃ : Ext S.X₃ Y (n + 1)
⊢ 1 + n = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughProjectives C
⊢ HasExt C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
⊢ { X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n), X₃ := AddCommGrpCat.of (Ext X S.X₃ n),
      f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
      zero := ⋯ }.Exact

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.postcomp X h) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ↑n₀ + 1 = ↑n₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
      X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.postcomp X h), zero := ⋯ }.Exact

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ AddCommGrpCat.ofHom (hS.extClass.postcomp X h) ≫ AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯) = 0

Tactic:
ext x
        dsimp
        simp only [comp_assoc_of_third_deg_zero, ShortComplex.ShortExact.extClass_comp,
          comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ AddCommGrpCat.ofHom (hS.extClass.postcomp X h) ≫ AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
⊢ (ComplexShape.up ℤ).prev i = i - 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
⊢ i - 1 < i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
⊢ r • x = x.comp (mk₀ (r • 𝟙 Y)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁵ : Ring R
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
inst✝ : HasDerivedCategory C
⊢ (r • x).hom = r • x.hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y Z : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
r : R
⊢ α.comp (r • β) h = r • α.comp β h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y Z : C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
r : R
⊢ (r • α).comp β h = r • α.comp β h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁵ : Ring R
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
⊢ ∀ (m : R) (x : Ext X Y n), homAddEquiv.toFun (m • x) = (RingHom.id R) m • homAddEquiv.toFun x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
r : R
f : X ⟶ Y
⊢ mk₀ (r • f) = r • mk₀ f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
m : R
x : Ext X Y 0
⊢ homEquiv₀.symm (addEquiv₀.toFun (m • x)) = homEquiv₀.symm ((RingHom.id R) m • addEquiv₀.toFun x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
R : Type t
inst✝¹ : CommRing R
inst✝ : Linear R C
X Y Z : C
a b c : ℕ
h : a + b = c
α : Ext X Y a
⊢ ∀ (x y : Ext Y Z b), α.comp (x + y) h = α.comp x h + α.comp y h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ { X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
      X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X h),
      g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.Exact

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
R : Type t
inst✝¹ : CommRing R
inst✝ : Linear R C
X Y Z : C
a b c : ℕ
h : a + b = c
α : Ext X Y a
⊢ ∀ (m : R) (x : Ext Y Z b), α.comp (m • x) h = (RingHom.id R) m • α.comp x h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
R : Type t
inst✝¹ : CommRing R
inst✝ : Linear R C
X Y Z : C
a b c : ℕ
h : a + b = c
⊢ ∀ (x y : Ext X Y a),
    { toFun := fun β ↦ (x + y).comp β h, map_add' := ⋯, map_smul' := ⋯ } =
      { toFun := fun β ↦ x.comp β h, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun β ↦ y.comp β h, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
R : Type t
inst✝¹ : CommRing R
inst✝ : Linear R C
X Y Z : C
a b c : ℕ
h : a + b = c
⊢ ∀ (m : R) (x : Ext X Y a),
    { toFun := fun β ↦ (m • x).comp β h, map_add' := ⋯, map_smul' := ⋯ } =
      (RingHom.id R) m • { toFun := fun β ↦ x.comp β h, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₁ : ℕ
x₁ : Ext X S.X₁ n₁
hx₁ : x₁.comp (mk₀ S.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = x₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
mem_ann : r ∈ Module.annihilator R ↑N
n : ℕ
h : ↑(AddCommGrpCat.of (Ext N M n))
⊢ r • 𝟙 N = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
mem_ann : r ∈ Module.annihilator R ↑N
n : ℕ
h : ↑(AddCommGrpCat.of (Ext N M n))
this : r • 𝟙 N = 0
⊢ r • h = (mk₀ (r • 𝟙 N)).comp h ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
mem_ann : r ∈ Module.annihilator R ↑N
n : ℕ
⊢ AddCommGrpCat.ofHom ((mk₀ (r • 𝟙 M)).postcomp N ⋯) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
i : ℕ
⊢ Mono (AddCommGrpCat.ofHom ((mk₀ (r • 𝟙 M)).postcomp N ⋯)) ↔ IsSMulRegular (Ext N M i) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
⊢ M.projectiveShortComplex.ShortExact

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
j : ℤ
ι : (singleFunctor C (j + 1)).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE (j + 1)
inst✝ : QuasiIsoAt ι (j + 1)
e : L.X (j + 1) ≅ opcycles L (j + 1) := pOpcyclesIso L (j + 1 - 1) (j + 1) ⋯ ⋯
α : I ⟶ L.X (j + 1) :=
  (singleObjHomologySelfIso (ComplexShape.up ℤ) (j + 1) I).inv ≫ homologyMap ι (j + 1) ≫ homologyι L (j + 1) ≫ e.inv
this : ι.f (j + 1) = (singleObjXSelf (ComplexShape.up ℤ) (j + 1) I).hom ≫ α
⊢ j < j + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ ∀ (i_1 : ℤ), (ComplexShape.up ℤ).Rel i_1 i → L.d i_1 i ≫ Injective.factorThru (𝟙 I) α = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
this : ι.f i = (singleObjXSelf (ComplexShape.up ℤ) i I).hom ≫ α
⊢ ι ≫ mkHomToSingle (Injective.factorThru (𝟙 I) α) ⋯ = 𝟙 ((singleFunctor C i).obj I)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
f : M ⟶ N
hf : Mono f
⊢ Function.Injective ⇑((mk₀ f).postcomp L ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : HasDerivedCategory C
X Y Z : C
f : X ⟶ Y
n : ℕ
x : Ext Y Z n
⊢ (singleFunctor C 0).map f ≫ x.hom = ((mk₀ f).comp x ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
⊢ IsSplitMono ι

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y✝ : C
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ ↑n₀ + 1 = ↑n₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
⊢ IsSplitMono ι

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
⊢ inv (Q.map ι) = Q.map (retraction ι)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
h₁ : inv (Q.map ι) = Q.map (retraction ι)
⊢ (g ≫ retraction ι).f i = HomologicalComplex.Hom.f 0 i

Tactic:
apply (K.isZero_of_isStrictlyGE n i hn).eq_of_src

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
h₁ : inv (Q.map ι) = Q.map (retraction ι)
⊢ g ≫ retraction ι = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ (ConcreteCategory.hom
        ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
          ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯))
      x.hom =
    (hS.extClass.comp x h).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
⊢ AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯) ≫ AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i : ℤ
φ : Q.obj K ⟶ Q.obj ((CochainComplex.singleFunctor C i).obj I)
n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
⊢ φ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X I : C
n : ℕ
inst✝ : Injective I
e : Ext X I (n + 1)
K : CochainComplex C ℤ := (CochainComplex.singleFunctor C 0).obj X
⊢ -↑n ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
N M : ModuleCat R
inst✝¹ : Module.Finite R ↑N
inst✝ : Module.Finite R ↑M
i : ℕ
⊢ Module.Finite R (Ext N M i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X I : C
n : ℕ
inst✝ : Injective I
e : Ext X I (n + 1)
K : CochainComplex C ℤ := (CochainComplex.singleFunctor C 0).obj X
this✝ : K.IsStrictlyGE (-↑n)
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ↑n + 1 + -(↑n + 1) = 0

Tactic:
by

Goal state after: