mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = -↑(0 + 1)
inst✝ : HasHomology K 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0
this : 0 ≠ 0
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (0 - 1) = m + 1

pp: case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = -↑(n✝ + 1 + 1)
inst✝ : HasHomology K (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n✝ + 1 - 1) = m + 1

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = -↑(0 + 1)
inst✝ : HasHomology K 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0
this : 0 ≠ 0
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (0 - 1) = m + 1

case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = -↑(n✝ + 1 + 1)
inst✝ : HasHomology K (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n✝ + 1 - 1) = m + 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = -↑(0 + 1)
inst✝ : HasHomology K 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0
this : 0 ≠ 0
⊢ -1 = m + 1

pp: case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = -↑(n✝ + 1 + 1)
inst✝ : HasHomology K (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ -1 - ↑n✝ = m + 1

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
inst✝¹ : NeZero 0
hm : m = -↑(0 + 1)
inst✝ : HasHomology K 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0
this : 0 ≠ 0
⊢ -1 = m + 1

case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst✝² : HasHomology h.cochainComplex m
n✝ : ℕ
inst✝¹ : NeZero (n✝ + 1)
hm : m = -↑(n✝ + 1 + 1)
inst✝ : HasHomology K (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ -1 - ↑n✝ = m + 1
Module: Mathlib.Algebra.Homology.GrothendieckAbelian

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝⁴ : HasZeroMorphisms C
J : Type w
inst✝³ : Category.{w', w} J
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
F : K ⥤ J ⥤ HomologicalComplex C c
c✝ : Cone F
hc : IsLimit c✝
i : ι
⊢ IsLimit ((eval C c i).mapCone (colim.mapCone c✝))

Tactic:
let e := preservesColimitNatIso (J := J) (eval C c i)

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝⁴ : HasZeroMorphisms C
J : Type w
inst✝³ : Category.{w', w} J
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
F : K ⥤ J ⥤ HomologicalComplex C c
c✝ : Cone F
hc : IsLimit c✝
i : ι
e : colim ⋙ eval C c i ≅ (Functor.whiskeringRight J (HomologicalComplex C c) C).obj (eval C c i) ⋙ colim :=
  preservesColimitNatIso (eval C c i)
⊢ IsLimit ((eval C c i).mapCone (colim.mapCone c✝))
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m : ℕ
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.ofNat m) = (𝟙 h.cochainComplex).f (Int.ofNat m)

pp: case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc 0) = (𝟙 h.cochainComplex).f (Int.negSucc 0)

pp: case negSucc.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m : ℕ
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc (m + 1)) = (𝟙 h.cochainComplex).f (Int.negSucc (m + 1))

Tactic:
<;>

Goal state after:
case ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m : ℕ
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.ofNat m) = (𝟙 h.cochainComplex).f (Int.ofNat m)

case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc 0) = (𝟙 h.cochainComplex).f (Int.negSucc 0)

case negSucc.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m : ℕ
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc (m + 1)) = (𝟙 h.cochainComplex).f (Int.negSucc (m + 1))
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.ofNat m) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.ofNat m)

pp: case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc 0) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc 0)

pp: case negSucc.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc (m + 1)) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc (m + 1))

Tactic:
<;>

Goal state after:
case ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.ofNat m) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.ofNat m)

case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc 0) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc 0)

case negSucc.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc (m + 1)) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc (m + 1))
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso ((twoδ₂Toδ₁ f g fg h).app 0)

pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso ((twoδ₂Toδ₁ f g fg h).app 1)

Tactic:
<;>

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso ((twoδ₂Toδ₁ f g fg h).app 0)

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso ((twoδ₂Toδ₁ f g fg h).app 1)
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso (𝟙 i)

pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso g

Tactic:
<;>

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso (𝟙 i)

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso g
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso ((twoδ₁Toδ₀ f g fg h).app 0)

pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso ((twoδ₁Toδ₀ f g fg h).app 1)

Tactic:
<;>

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso ((twoδ₁Toδ₀ f g fg h).app 0)

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso ((twoδ₁Toδ₀ f g fg h).app 1)
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso f

pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso (𝟙 k)

Tactic:
<;>

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso f

case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso (𝟙 k)
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ P.complex.d 1 0 ≫ P.π.f 0 = 0

Tactic:
by
  rw [← P.π.comm 1 0, single_obj_d, comp_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f

Tactic:
ext
  simp [lift, liftFZero, liftFOne]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ ((X.map ((toKaroubi C).map P.p)).f ≫ (φ.app ((toKaroubi C).obj P.X)).f) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (φ.app P).f

Tactic:
natTrans_eq φ P,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
P : Karoubi C
⊢ ((X.map ((toKaroubi C).map P.p)).f ≫ (φ.app ((toKaroubi C).obj P.X)).f) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (X.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ Y.map P.decompId_p).f
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P : ProjectiveResolution X
⊢ lift (𝟙 X) P P ≫ P.π = P.π ≫ (ChainComplex.single₀ C).map (𝟙 X)

pp: case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P : ProjectiveResolution X
⊢ 𝟙 P.complex ≫ P.π = P.π ≫ (ChainComplex.single₀ C).map (𝟙 X)

Tactic:
<;>

Goal state after:
case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P : ProjectiveResolution X
⊢ lift (𝟙 X) P P ≫ P.π = P.π ≫ (ChainComplex.single₀ C).map (𝟙 X)

case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P : ProjectiveResolution X
⊢ 𝟙 P.complex ≫ P.π = P.π ≫ (ChainComplex.single₀ C).map (𝟙 X)
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ lift (f ≫ g) P R ≫ R.π = P.π ≫ (ChainComplex.single₀ C).map (f ≫ g)

pp: case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ (lift f P Q ≫ lift g Q R) ≫ R.π = P.π ≫ (ChainComplex.single₀ C).map (f ≫ g)

Tactic:
<;>

Goal state after:
case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ lift (f ≫ g) P R ≫ R.π = P.π ≫ (ChainComplex.single₀ C).map (f ≫ g)

case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ (lift f P Q ≫ lift g Q R) ≫ R.π = P.π ≫ (ChainComplex.single₀ C).map (f ≫ g)
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective ((ofComplex Z).X 0)

pp: case succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective ((ofComplex Z).X (0 + 1))

pp: case succ.succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective ((ofComplex Z).X (0 + 1 + 1))

pp: case succ.succ.succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ Projective ((ofComplex Z).X (n + 1 + 1 + 1))

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective ((ofComplex Z).X 0)

case succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective ((ofComplex Z).X (0 + 1))

case succ.succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective ((ofComplex Z).X (0 + 1 + 1))

case succ.succ.succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ Projective ((ofComplex Z).X (n + 1 + 1 + 1))
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: case left
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := ⋯
⊢ IsIso (φ.app 0)

pp: case right
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := ⋯
⊢ IsIso (φ.app 1)

Tactic:
<;>

Goal state after:
case left
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := ⋯
⊢ IsIso (φ.app 0)

case right
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := ⋯
⊢ IsIso (φ.app 1)
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: case left
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (𝟙 i₀ ≫ f)

pp: case right
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (inv f ≫ 𝟙 i₀)

Tactic:
<;>

Goal state after:
case left
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (𝟙 i₀ ≫ f)

case right
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (inv f ≫ 𝟙 i₀)
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
⊢ IsZero ((X.H n).obj (mk₁ f))

Tactic:
let φ := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) (by simp) ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀)
  have : IsIso φ := by
    rw [isIso_iff₁]
    constructor <;> dsimp [φ] <;> infer_instance
  rw [IsZero.iff_id_eq_zero]
  rw [← cancel_mono ((X.H n).map φ), Category.id_comp, zero_comp,
    ← X.zero₂ f (inv f) (𝟙 _) (by simp), ← Functor.map_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape

Goal state before:
pp: case fst
u : ℤ × ℤ
i✝ j✝ j'✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i✝.fst + u.fst = ↑j'✝.fst ∧ ↑i✝.snd + u.snd = ↑j'✝.snd
⊢ j✝.fst = j'✝.fst

pp: case snd
u : ℤ × ℤ
i✝ j✝ j'✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i✝.fst + u.fst = ↑j'✝.fst ∧ ↑i✝.snd + u.snd = ↑j'✝.snd
⊢ j✝.snd = j'✝.snd

Tactic:
<;>

Goal state after:
case fst
u : ℤ × ℤ
i✝ j✝ j'✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i✝.fst + u.fst = ↑j'✝.fst ∧ ↑i✝.snd + u.snd = ↑j'✝.snd
⊢ j✝.fst = j'✝.fst

case snd
u : ℤ × ℤ
i✝ j✝ j'✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i✝.fst + u.fst = ↑j'✝.fst ∧ ↑i✝.snd + u.snd = ↑j'✝.snd
⊢ j✝.snd = j'✝.snd
Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape

Goal state before:
pp: case fst
u : ℤ × ℤ
i✝ i'✝ j✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i'✝.fst + u.fst = ↑j✝.fst ∧ ↑i'✝.snd + u.snd = ↑j✝.snd
⊢ i✝.fst = i'✝.fst

pp: case snd
u : ℤ × ℤ
i✝ i'✝ j✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i'✝.fst + u.fst = ↑j✝.fst ∧ ↑i'✝.snd + u.snd = ↑j✝.snd
⊢ i✝.snd = i'✝.snd

Tactic:
<;>

Goal state after:
case fst
u : ℤ × ℤ
i✝ i'✝ j✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i'✝.fst + u.fst = ↑j✝.fst ∧ ↑i'✝.snd + u.snd = ↑j✝.snd
⊢ i✝.fst = i'✝.fst

case snd
u : ℤ × ℤ
i✝ i'✝ j✝ : ℕ × ℕ
x✝¹ : ↑i✝.fst + u.fst = ↑j✝.fst ∧ ↑i✝.snd + u.snd = ↑j✝.snd
x✝ : ↑i'✝.fst + u.fst = ↑j✝.fst ∧ ↑i'✝.snd + u.snd = ↑j✝.snd
⊢ i✝.snd = i'✝.snd
Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape

Goal state before:
pp: case fst
l : ℕ
u : ℤ × ℤ
i✝ j✝ j'✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i✝.fst + u.fst = j'✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j'✝.snd
⊢ j✝.fst = j'✝.fst

pp: case snd
l : ℕ
u : ℤ × ℤ
i✝ j✝ j'✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i✝.fst + u.fst = j'✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j'✝.snd
⊢ ↑j✝.snd = ↑j'✝.snd

Tactic:
<;>

Goal state after:
case fst
l : ℕ
u : ℤ × ℤ
i✝ j✝ j'✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i✝.fst + u.fst = j'✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j'✝.snd
⊢ j✝.fst = j'✝.fst

case snd
l : ℕ
u : ℤ × ℤ
i✝ j✝ j'✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i✝.fst + u.fst = j'✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j'✝.snd
⊢ ↑j✝.snd = ↑j'✝.snd
Module: Mathlib.Algebra.Homology.SpectralSequence.ComplexShape

Goal state before:
pp: case fst
l : ℕ
u : ℤ × ℤ
i✝ i'✝ j✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i'✝.fst + u.fst = j✝.fst ∧ ↑↑i'✝.snd + u.snd = ↑↑j✝.snd
⊢ i✝.fst = i'✝.fst

pp: case snd
l : ℕ
u : ℤ × ℤ
i✝ i'✝ j✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i'✝.fst + u.fst = j✝.fst ∧ ↑↑i'✝.snd + u.snd = ↑↑j✝.snd
⊢ ↑i✝.snd = ↑i'✝.snd

Tactic:
<;>

Goal state after:
case fst
l : ℕ
u : ℤ × ℤ
i✝ i'✝ j✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i'✝.fst + u.fst = j✝.fst ∧ ↑↑i'✝.snd + u.snd = ↑↑j✝.snd
⊢ i✝.fst = i'✝.fst

case snd
l : ℕ
u : ℤ × ℤ
i✝ i'✝ j✝ : ℤ × Fin l
x✝¹ : i✝.fst + u.fst = j✝.fst ∧ ↑↑i✝.snd + u.snd = ↑↑j✝.snd
x✝ : i'✝.fst + u.fst = j✝.fst ∧ ↑↑i'✝.snd + u.snd = ↑↑j✝.snd
⊢ ↑i✝.snd = ↑i'✝.snd