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

Goal state before:
pp: case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex C c
g : double (𝟙 X) hi₀₁ ⟶ K
⊢ ((fun φ₀ ↦ mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯) ((fun g ↦ (doubleXIso₀ (𝟙 X) hi₀₁).inv ≫ g.f i₀) g)).f i₀ =
    g.f i₀

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos.negSucc.succ.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
hnm : Int.negSucc (0 + 1) + 1 = -1
hmp : -1 + 1 = 0
⊢ h.d (Int.negSucc (0 + 1)) (-1) ≫ h.d (-1) 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos.negSucc.succ.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n : ℕ
hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)
hmp : Int.negSucc (n + 1) + 1 = Int.negSucc n
⊢ h.d (Int.negSucc (n + 1 + 1)) (Int.negSucc (n + 1)) ≫ h.d (Int.negSucc (n + 1)) (Int.negSucc n) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
⊢ (ComplexShape.embeddingUpIntGE 0).f n = ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex C c
x✝ : (eval C c i₀ ⋙ coyoneda.obj (op X)).obj K
⊢ (fun g ↦ (doubleXIso₀ (𝟙 X) hi₀₁).inv ≫ g.f i₀) ((fun φ₀ ↦ mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
⊢ (ComplexShape.embeddingUpIntGE 0).f (n + 1) = ↑(n + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
X : C
Y✝ Y'✝ : HomologicalComplex C c
x✝¹ : Y✝ ⟶ Y'✝
x✝ : double (𝟙 X) hi₀₁ ⟶ Y✝
⊢ { toFun := fun g ↦ (doubleXIso₀ (𝟙 X) hi₀₁).inv ≫ g.f i₀,
        invFun := fun φ₀ ↦ mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ Y'✝.d i₀ i₁) ⋯ ⋯, left_inv := ⋯, right_inv := ⋯ }
      (x✝ ≫ x✝¹) =
    (ConcreteCategory.hom ((eval C c i₀ ⋙ coyoneda.obj (op X)).map x✝¹))
      ({ toFun := fun g ↦ (doubleXIso₀ (𝟙 X) hi₀₁).inv ≫ g.f i₀,
          invFun := fun φ₀ ↦ mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ Y✝.d i₀ i₁) ⋯ ⋯, left_inv := ⋯, right_inv := ⋯ }
        x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫ L.d n (n + 1) =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫
        L.d n (n + 1) ≫ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
i : ι
inst✝ : DecidableEq ι
hi : ∀ (j : ι), ¬c.Rel i j
X : C
K : HomologicalComplex C c
f : (eval C c i ⋙ coyoneda.obj (op X)).obj K
⊢ (fun g ↦ (singleObjXSelf c i X).inv ≫ g.f i) ((fun f ↦ mkHomFromSingle f ⋯) f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
i : ι
inst✝ : DecidableEq ι
hi : ∀ (j : ι), ¬c.Rel i j
X : C
⊢ ∀ {Y Y' : HomologicalComplex C c} (g : Y ⟶ Y') (f : (single C c i).obj X ⟶ Y),
    { toFun := fun g ↦ (singleObjXSelf c i X).inv ≫ g.f i, invFun := fun f ↦ mkHomFromSingle f ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        (f ≫ g) =
      (ConcreteCategory.hom ((eval C c i ⋙ coyoneda.obj (op X)).map g))
        ({ toFun := fun g ↦ (singleObjXSelf c i X).inv ≫ g.f i, invFun := fun f ↦ mkHomFromSingle f ⋯, left_inv := ⋯,
            right_inv := ⋯ }
          f)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d (n + 1) n =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫
        K.d (n + 1) n ≫ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom

Tactic:
simp

Goal state after:
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
inst✝ : HasHomology L 0
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
⊢ (ComplexShape.up ℕ).prev 0 = 0 - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
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)
inst✝ : HasHomology L (n✝ + 1)
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
⊢ (ComplexShape.up ℕ).prev (n✝ + 1) = n✝ + 1 - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.up ℕ).next n = n + 1

Tactic:
simp

Goal state after:
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
inst✝ : HasHomology L 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
this : 0 ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (0 - 1) = m - 1

Tactic:
simp

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
inst✝ : HasHomology L 0
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
this : 0 ≠ 0
⊢ 0 = m - 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
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)
inst✝ : HasHomology L (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (n✝ + 1 - 1) = m - 1

Tactic:
simp

Goal state after:
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)
inst✝ : HasHomology L (n✝ + 1)
this✝ : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n✝ + 1)
this : n✝ + 1 ≠ 0
⊢ ↑n✝ = m - 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1

Tactic:
have := NeZero.ne n; cases n <;> simp <;> lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f n = m

Tactic:
simp

Goal state after:
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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ ↑n = m
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case e'_3
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m₁ m₂ m₃ : S
X : DifferentialObject S C
e_1✝ :
  (((shiftFunctor C (m₁ + m₂ + m₃)).obj X).obj ⟶
      ((shiftFunctor C m₃).obj ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X)).obj) =
    ((CategoryTheory.shiftFunctor C (m₁ + m₂ + m₃)).obj X.obj ⟶
      (CategoryTheory.shiftFunctor C m₃).obj
        ((CategoryTheory.shiftFunctor C m₁ ⋙ CategoryTheory.shiftFunctor C m₂).obj X.obj))
⊢ (eqToHom ⋯).f ≫
      (CategoryTheory.shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X.obj ≫
        (CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).obj X.obj) =
    ((eqToHom ⋯).app X.obj ≫ (CategoryTheory.shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X.obj) ≫
      (CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).obj X.obj)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f (n + 1) = m + 1

Tactic:
simp

Goal state after:
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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ ↑n = m
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.up ℤ).prev m = m - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.up ℤ).next m = m + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.down ℕ).prev n = n + 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case e'_3
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
e_1✝ :
  (((shiftFunctor C (0 + n)).obj X).obj ⟶ ((shiftFunctor C 0 ⋙ shiftFunctor C n).obj X).obj) =
    ((CategoryTheory.shiftFunctor C (0 + n)).obj X.obj ⟶
      (CategoryTheory.shiftFunctor C 0 ⋙ CategoryTheory.shiftFunctor C n).obj X.obj)
⊢ (eqToHom ⋯ ≫ (shiftFunctor C n).map ((shiftZero C).inv.app X)).f =
    eqToHom ⋯ ≫ (CategoryTheory.shiftFunctor C n).map ((shiftFunctorZero C S).inv.app X.obj)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case e'_3
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
e_1✝ :
  (((shiftFunctor C (n + 0)).obj X).obj ⟶ ((shiftFunctor C n ⋙ shiftFunctor C 0).obj X).obj) =
    ((CategoryTheory.shiftFunctor C (n + 0)).obj X.obj ⟶
      (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor C 0).obj X.obj)
⊢ (eqToHom ⋯ ≫ (shiftZero C).inv.app ((shiftFunctor C n).obj X)).f =
    eqToHom ⋯ ≫ (shiftFunctorZero C S).inv.app ((CategoryTheory.shiftFunctor C n).obj X.obj)

Tactic:
simp

Goal state after:
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
⊢ (ComplexShape.down ℕ).next 0 = 0 - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
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)
⊢ (ComplexShape.down ℕ).next (n✝ + 1) = n✝ + 1 - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n + 1) = m - 1

Tactic:
simp

Goal state after:
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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ -1 - (↑n + 1) = m - 1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.embeddingUpIntLE (-1)).f n = m

Tactic:
simp

Goal state after:
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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ -1 - ↑n = m
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

Tactic:
simp

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
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
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:
simp

Goal state after:
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.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1

Tactic:
have := NeZero.ne n; cases n <;> simp <;> lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.up ℤ).prev m = m - 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.up ℤ).next m = m + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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
⊢ (𝟙 K).f 0 ≫ h.d₀ = h.d₀ ≫ (𝟙 L).f 0

Tactic:
simp

Goal state after:
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)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
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)

Tactic:
simp

Goal state after:
case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
⊢ (match -1 with
    | Int.ofNat n => 𝟙 (L.X n)
    | Int.negSucc n => 𝟙 (K.X n)) =
    𝟙 (K.X 0)