mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : FibrantObject (Plus C)
n : ℤ
⊢ isInjective C (K.obj.obj.X n)

Tactic:
;

Goal state after:
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : FibrantObject (Plus C)
n : ℤ
⊢ isInjective C (K.obj.obj.X n)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: case succ
C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X : C
n : ℕ
hn : ∀ (Y : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
Y : C
I : InjectivePresentation Y := Classical.arbitrary (InjectivePresentation Y)
S : ShortComplex C := { X₁ := Y, X₂ := I.J, X₃ := cokernel I.f, f := I.f, g := cokernel.π I.f, zero := ⋯ }
this : Injective (S.map F).X₂
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y (n + 1))

Tactic:
have hS : S.ShortExact := { exact := ShortComplex.exact_cokernel I.f }

Goal state after:
case succ
C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X : C
n : ℕ
hn : ∀ (Y : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
Y : C
I : InjectivePresentation Y := Classical.arbitrary (InjectivePresentation Y)
S : ShortComplex C := { X₁ := Y, X₂ := I.J, X₃ := cokernel I.f, f := I.f, g := cokernel.π I.f, zero := ⋯ }
this : Injective (S.map F).X₂
hS : S.ShortExact
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y (n + 1))
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
X✝ Y✝ : CochainComplex.Plus (InjectiveObject C)
f✝ : X✝ ⟶ Y✝
⊢ (isomorphisms (Plus (InjectiveObject C))).inverseImage (L C).functor f✝ ↔
    (CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus f✝

Tactic:
;

Goal state after:
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
X✝ Y✝ : CochainComplex.Plus (InjectiveObject C)
f✝ : X✝ ⟶ Y✝
⊢ (isomorphisms (Plus (InjectiveObject C))).inverseImage (L C).functor f✝ ↔
    (CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus f✝
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
X✝ Y✝ : CochainComplex.Plus C
f✝ : X✝ ⟶ Y✝
⊢ (quasiIso C).inverseImage (R C).functor f✝ ↔ CochainComplex.Plus.quasiIso C f✝

Tactic:
;

Goal state after:
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
X✝ Y✝ : CochainComplex.Plus C
f✝ : X✝ ⟶ Y✝
⊢ (quasiIso C).inverseImage (R C).functor f✝ ↔ CochainComplex.Plus.quasiIso C f✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
this : ∀ (n : ℤ), Injective (L.X n)
i : ℤ
hi : autoParam (i < -d) isStrictlyGE_iff._auto_1
⊢ d < -i

Tactic:
;

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
this : ∀ (n : ℤ), Injective (L.X n)
i : ℤ
hi : autoParam (i < -d) isStrictlyGE_iff._auto_1
⊢ d < -i
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ (fun b_1 ↦ b_1 + { as := 1 }.as • b) x = (fun b_1 ↦ b_1 + { as := 1 }.as • b) x

Tactic:
;

Goal state after:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ (fun b_1 ↦ b_1 + { as := 1 }.as • b) x = (fun b_1 ↦ b_1 + { as := 1 }.as • b) x
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ X.objEqToHom ⋯ ≫ X.d x = X.d x ≫ X.objEqToHom ⋯

Tactic:
;

Goal state after:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ X.objEqToHom ⋯ ≫ X.d x = X.d x ≫ X.objEqToHom ⋯
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ X.objEqToHom ⋯ ≫ f.f x = f.f x ≫ Y.objEqToHom ⋯

Tactic:
;

Goal state after:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ X.objEqToHom ⋯ ≫ f.f x = f.f x ≫ Y.objEqToHom ⋯
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y : β
⊢ X.d x y ≫ eqToHom ⋯ = X.d x y

Tactic:
;

Goal state after:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y : β
⊢ X.d x y ≫ eqToHom ⋯ = X.d x y
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
w : ¬i + b = j
⊢ (if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) = 0

Tactic:
;

Goal state after:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
w : ¬i + b = j
⊢ (if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) = 0
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j k : β
hij : i + b = j
hjk : j + b = k
⊢ ((if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) ≫ if h : j + b = k then X.d j ≫ X.objEqToHom ⋯ else 0) = 0

Tactic:
;

Goal state after:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j k : β
hij : i + b = j
hjk : j + b = k
⊢ ((if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) ≫ if h : j + b = k then X.d j ≫ X.objEqToHom ⋯ else 0) = 0
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.restriction e).X i = K.X (e.f i)

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.restriction e).X i = K.X (e.f i)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (({ f := f.hom, comm := hf } ≫ { f := f.inv, comm := ⋯ }).f = (𝟙 X).f) ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (({ f := f.hom, comm := hf } ≫ { f := f.inv, comm := ⋯ }).f = (𝟙 X).f) ext._auto_1
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (f.hom ≫ f.inv = 𝟙 X.obj) ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (f.hom ≫ f.inv = 𝟙 X.obj) ext._auto_1
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (({ f := f.inv, comm := ⋯ } ≫ { f := f.hom, comm := hf }).f = (𝟙 Y).f) ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (({ f := f.inv, comm := ⋯ } ≫ { f := f.hom, comm := hf }).f = (𝟙 Y).f) ext._auto_1
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (f.inv ≫ f.hom = 𝟙 Y.obj) ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (f.inv ≫ f.hom = 𝟙 Y.obj) ext._auto_1
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
i✝ : ℤ
⊢ (i✝ + 1).negOnePow = -i✝.negOnePow

Tactic:
;

Goal state after:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
i✝ : ℤ
⊢ (i✝ + 1).negOnePow = -i✝.negOnePow
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
j✝ : ℤ
⊢ j✝.negOnePow = -(j✝ + 1).negOnePow

Tactic:
;

Goal state after:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
j✝ : ℤ
⊢ j✝.negOnePow = -(j✝ + 1).negOnePow
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
i✝ : ℕ
⊢ (-1) ^ (i✝ + 1) = -(-1) ^ i✝

Tactic:
;

Goal state after:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
i✝ : ℕ
⊢ (-1) ^ (i✝ + 1) = -(-1) ^ i✝
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
j✝ : ℕ
⊢ (-1) ^ j✝ = -(-1) ^ (j✝ + 1)

Tactic:
;

Goal state after:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
j✝ : ℕ
⊢ (-1) ^ j✝ = -(-1) ^ (j✝ + 1)
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
i : ι
⊢ (i ∈ Function.support fun x ↦ ↑(Module.finrank R ↑(X x))) ↔ i ∈ Function.support fun i ↦ Module.finrank R ↑(X i)

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
i : ι
⊢ (i ∈ Function.support fun x ↦ ↑(Module.finrank R ↑(X x))) ↔ i ∈ Function.support fun i ↦ Module.finrank R ↑(X i)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ : DifferentialObject S C
⊢ { f := F.map (𝟙 X✝).f, comm := ⋯ } = 𝟙 { obj := F.obj X✝.obj, d := F.map X✝.d ≫ η.app X✝.obj, d_squared := ⋯ }

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ : DifferentialObject S C
⊢ { f := F.map (𝟙 X✝).f, comm := ⋯ } = 𝟙 { obj := F.obj X✝.obj, d := F.map X✝.d ≫ η.app X✝.obj, d_squared := ⋯ }
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ : DifferentialObject S C
⊢ autoParam
    ({ f := F.map (𝟙 X✝).f, comm := ⋯ }.f =
      (𝟙 { obj := F.obj X✝.obj, d := F.map X✝.d ≫ η.app X✝.obj, d_squared := ⋯ }).f)
    DifferentialObject.ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ : DifferentialObject S C
⊢ autoParam
    ({ f := F.map (𝟙 X✝).f, comm := ⋯ }.f =
      (𝟙 { obj := F.obj X✝.obj, d := F.map X✝.d ≫ η.app X✝.obj, d_squared := ⋯ }).f)
    DifferentialObject.ext._auto_1
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ Z✝ : DifferentialObject S C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { f := F.map (f✝ ≫ g✝).f, comm := ⋯ } = { f := F.map f✝.f, comm := ⋯ } ≫ { f := F.map g✝.f, comm := ⋯ }

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ Z✝ : DifferentialObject S C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { f := F.map (f✝ ≫ g✝).f, comm := ⋯ } = { f := F.map f✝.f, comm := ⋯ } ≫ { f := F.map g✝.f, comm := ⋯ }
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ Z✝ : DifferentialObject S C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ autoParam
    ({ f := F.map (f✝ ≫ g✝).f, comm := ⋯ }.f = ({ f := F.map f✝.f, comm := ⋯ } ≫ { f := F.map g✝.f, comm := ⋯ }).f)
    DifferentialObject.ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ Z✝ : DifferentialObject S C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ autoParam
    ({ f := F.map (f✝ ≫ g✝).f, comm := ⋯ }.f = ({ f := F.map f✝.f, comm := ⋯ } ≫ { f := F.map g✝.f, comm := ⋯ }).f)
    DifferentialObject.ext._auto_1
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : HomSubtype S C X✝ Y✝
⊢ ⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = x✝

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : HomSubtype S C X✝ Y✝
⊢ ⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = x✝
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : HomSubtype S C X✝ Y✝
⊢ ↑⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = ↑x✝

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : HomSubtype S C X✝ Y✝
⊢ ↑⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = ↑x✝
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : X✝ ⟶ Y✝
⊢ ConcreteCategory.hom { f := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.f, ⋯⟩, comm := ⋯ }.f =
    ConcreteCategory.hom x✝.f

Tactic:
;

Goal state after:
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : X✝ ⟶ Y✝
⊢ ConcreteCategory.hom { f := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.f, ⋯⟩, comm := ⋯ }.f =
    ConcreteCategory.hom x✝.f
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : ¬↑n + 1 = ↑m
⊢ ¬n + 1 = m

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : ¬↑n + 1 = ↑m
⊢ ¬n + 1 = m
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : ¬Int.negSucc n + 1 = Int.negSucc m
⊢ ¬m + 1 = n

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : ¬Int.negSucc n + 1 = Int.negSucc m
⊢ ¬m + 1 = n
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam
    ({ f := (CategoryTheory.shiftFunctor C n).map (𝟙 X).f, comm := ⋯ }.f =
      (𝟙
          { obj := (CategoryTheory.shiftFunctor C n).obj X.obj,
            d := (CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom, d_squared := ⋯ }).f)
    ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam
    ({ f := (CategoryTheory.shiftFunctor C n).map (𝟙 X).f, comm := ⋯ }.f =
      (𝟙
          { obj := (CategoryTheory.shiftFunctor C n).obj X.obj,
            d := (CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom, d_squared := ⋯ }).f)
    ext._auto_1
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam ((CategoryTheory.shiftFunctor C n).map (𝟙 X.obj) = 𝟙 ((CategoryTheory.shiftFunctor C n).obj X.obj))
    ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ autoParam ((CategoryTheory.shiftFunctor C n).map (𝟙 X.obj) = 𝟙 ((CategoryTheory.shiftFunctor C n).obj X.obj))
    ext._auto_1
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    ({ f := (CategoryTheory.shiftFunctor C n).map (f ≫ g).f, comm := ⋯ }.f =
      ({ f := (CategoryTheory.shiftFunctor C n).map f.f, comm := ⋯ } ≫
          { f := (CategoryTheory.shiftFunctor C n).map g.f, comm := ⋯ }).f)
    ext._auto_1

Tactic:
;

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    ({ f := (CategoryTheory.shiftFunctor C n).map (f ≫ g).f, comm := ⋯ }.f =
      ({ f := (CategoryTheory.shiftFunctor C n).map f.f, comm := ⋯ } ≫
          { f := (CategoryTheory.shiftFunctor C n).map g.f, comm := ⋯ }).f)
    ext._auto_1