mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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₁
⊢ (double f hi₀₁).X i₁ = X₁

Tactic:
by

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₁
a b : ι
ha : a ≠ i₀
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)

Tactic:
by

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₁
a b : ι
hb : b ≠ i₁
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)

Tactic:
by

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

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : (shiftFunctor C 1).PreservesZeroMorphisms
X : DifferentialObject S C
f : { obj := 0, d := 0, d_squared := ⋯ } ⟶ X
⊢ f = default

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasShift C S
inst✝ : (shiftFunctor C 1).PreservesZeroMorphisms
X : DifferentialObject S C
f : X ⟶ { obj := 0, d := 0, d_squared := ⋯ }
⊢ f = default

Tactic:
by

Goal state after:
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
f : X✝ ⟶ Y✝
⊢ X✝.d ≫ (shiftFunctor C 1).map (ConcreteCategory.ofHom (ConcreteCategory.hom f.f)) =
    ConcreteCategory.ofHom (ConcreteCategory.hom f.f) ≫ Y✝.d

Tactic:
by

Goal state after:
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
f : HomSubtype S C X✝ Y✝
⊢ X✝.d ≫ (shiftFunctor C 1).map (ConcreteCategory.ofHom ↑f) = ConcreteCategory.ofHom ↑f ≫ Y✝.d

Tactic:
by

Goal state after:
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 { f := ConcreteCategory.ofHom ↑x✝, comm := ⋯ }.f, ⋯⟩ = x✝

Tactic:
by

Goal state after:
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✝
⊢ { f := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.f, ⋯⟩, comm := ⋯ } = x✝

Tactic:
by

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₁
K : HomologicalComplex C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ = φ'

Tactic:
by

Goal state after:
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
⊢ ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom) =
    0

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m : ℕ
⊢ h.d (Int.negSucc n) (Int.negSucc m) = K.d n m

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : Int.ofNat n + 1 ≠ Int.ofNat m
⊢ ¬(ComplexShape.up ℕ).Rel n m

Tactic:
by

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₁
K : HomologicalComplex C c
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ = φ'

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : Int.negSucc n + 1 ≠ Int.negSucc m
⊢ ¬(ComplexShape.down ℕ).Rel n m

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : Int.negSucc n + 1 ≠ Int.negSucc m
⊢ h.d (Int.negSucc n) (Int.negSucc m) = 0

Tactic:
by

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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : k = i₀
⊢ (double f hi₀₁).X k = (double f hi₀₁).X i₀

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m : ℤ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat 0
⊢ h.d (Int.negSucc 0) (Int.ofNat 0) = 0

Tactic:
by

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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : k = i₀
⊢ K.X i₀ = K.X k

Tactic:
by

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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ (double f hi₀₁).X k = (double f hi₀₁).X i₁

Tactic:
by

Goal state after:
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✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ { obj := (CategoryTheory.shiftFunctor C n).obj X✝.obj,
          d := (CategoryTheory.shiftFunctor C n).map X✝.d ≫ (shiftComm X✝.obj 1 n).hom, d_squared := ⋯ }.d ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.f) =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      { obj := (CategoryTheory.shiftFunctor C n).obj Y✝.obj,
          d := (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftComm Y✝.obj 1 n).hom, d_squared := ⋯ }.d

Tactic:
by

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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ K.X i₁ = K.X k

Tactic:
by

Goal state after:
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
⊢ { f := (CategoryTheory.shiftFunctor C n).map (𝟙 X).f, comm := ⋯ } =
    𝟙
      { obj := (CategoryTheory.shiftFunctor C n).obj X.obj,
        d := (CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom, d_squared := ⋯ }

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : Int.negSucc n + 1 ≠ Int.ofNat m
⊢ h.d (Int.negSucc n) (Int.ofNat m) = 0

Tactic:
by

Goal state after:
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✝
⊢ { f := (CategoryTheory.shiftFunctor C n).map (f ≫ g).f, comm := ⋯ } =
    { f := (CategoryTheory.shiftFunctor C n).map f.f, comm := ⋯ } ≫
      { f := (CategoryTheory.shiftFunctor C n).map g.f, comm := ⋯ }

Tactic:
by

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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
⊢ (if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
by

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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₀ = (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.ofNat n + 1 = m
⊢ m = Int.ofNat (n + 1)

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ p = Int.ofNat (n + 2)

Tactic:
by

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₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₁ = (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁

Tactic:
by

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
φ₀ : (eval C c i₀ ⋙ coyoneda.obj (op X)).obj K
⊢ φ₀ ≫ K.d i₀ i₁ = 𝟙 X ≫ φ₀ ≫ K.d i₀ i₁

Tactic:
by

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
φ₀ : (eval C c i₀ ⋙ coyoneda.obj (op X)).obj K
⊢ ∀ (k : ι), c.Rel i₁ k → (φ₀ ≫ K.d i₀ i₁) ≫ K.d i₁ k = 0

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc 0 + 1 = m
⊢ m = 0

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
hmp : 0 + 1 = p
hnm : Int.negSucc 0 + 1 = 0
⊢ p = 1

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc (0 + 1) + 1 = m
⊢ m = -1

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
hmp : -1 + 1 = p
hnm : Int.negSucc (0 + 1) + 1 = -1
⊢ p = 0

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.negSucc (n + 1 + 1) + 1 = m
⊢ m = Int.negSucc (n + 1)

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.negSucc (n + 1) + 1 = p
hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)
⊢ p = Int.negSucc n

Tactic:
by

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
g : double (𝟙 X) hi₀₁ ⟶ K
⊢ (fun φ₀ ↦ mkHomFromDouble hi₀₁ h φ₀ (φ₀ ≫ K.d i₀ i₁) ⋯ ⋯) ((fun g ↦ (doubleXIso₀ (𝟙 X) hi₀₁).inv ≫ g.f i₀) g) = g

Tactic:
by

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 : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
⊢ h.d n m ≫ h.d m p = 0

Tactic:
by

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:
by

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:
by

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:
by

Goal state after:
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
m n : S
⊢ shiftFunctor C (m + n) ≅ shiftFunctor C m ⋙ shiftFunctor C n

Tactic:
by

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:
by

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''
⊢ ∀ (i j : ℕ),
    (ComplexShape.up ℕ).Rel i j →
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫ L.d i j =
        (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).d i j ≫
          (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom

Tactic:
by

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.embeddingUpIntLE (-1)).f n = Int.negSucc n

Tactic:
by

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
g : (single C c i).obj X ⟶ K
⊢ (fun f ↦ mkHomFromSingle f ⋯) ((fun g ↦ (singleObjXSelf c i X).inv ≫ g.f i) g) = g

Tactic:
by

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.embeddingUpIntLE (-1)).f (n + 1) = Int.negSucc (n + 1)

Tactic:
by

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:
by

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:
by

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''
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d i j =
        (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).d i j ≫
          (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom

Tactic:
by

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 ℕ).prev n = n - 1

Tactic:
by

Goal state after: