awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
refine : ¬∃ (j : ℕ), (ComplexShape.up ℕ).Rel j 0
refine₁ refine₂ : ∀ (j : ℕ), ¬(ComplexShape.up ℕ).Rel j 0
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
classical
    refine dif_neg ?_
    push Not
    intro
    apply Nat.noConfusion

Premises used: dif_neg, Not, Nat.noConfusion
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
i : ℕ
⊢ (ComplexShape.up ℕ).prev (i + 1) = i

Tactic:
(ComplexShape.up ℕ).prev_eq' rfl

Premises used: ComplexShape.prev_eq', Nat, rfl, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
pos : ∀ (hij : c.Rel i j), f.f i ≫ B.d i j = A.d i j ≫ f.f j
neg : ∀ (hij : ¬c.Rel i j), f.f i ≫ B.d i j = A.d i j ≫ f.f j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
hij : c.Rel i j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
f.comm' i j hij

Premises used: HomologicalComplex.Hom.comm'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
hij : c.Rel i j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
exact f.comm' i j hij

Premises used: HomologicalComplex.Hom.comm'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
A B : HomologicalComplex.{v, u, u_1} V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
neg : f.f i ≫ B.d i j = 0 ≫ f.f j
neg₁ : f.f i ≫ 0 = 0 ≫ f.f j
neg₂ : Eq (α := A.X i ⟶ B.X j) 0 (0 ≫ f.f j)
neg₃ neg₄ : Eq.{v + 1} (α := A.X i ⟶ B.X j) 0 0
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
f₁ : f.f = g.f
⊢ f = g

Tactic:
apply Hom.ext

Premises used: HomologicalComplex.Hom.ext
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h f₁ : ∀ (x : ι), f.f x = g.f x
⊢ f.f = g.f

Tactic:
funext
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h : ∀ (i : ι), f.f i = g.f i
x : ι
⊢ f.f x = g.f x

Tactic:
apply h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
⊢ Hom.f (𝟙 C) i = 𝟙 (C.X i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ C₃ : HomologicalComplex.{v, u, u_1} V c
f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ (f ≫ g).f i = f.f i ≫ g.f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
h : C₁ = C₂
n : ι
subst : Hom.f (eqToHom ⋯) n = eqToHom ⋯
⊢ Hom.f (eqToHom h) n = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ : HomologicalComplex.{v, u, u_1} V c
n : ι
⊢ Hom.f (eqToHom ⋯) n = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
i : ι
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X i) (Hom.f 0 i) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
⊢ IsZero (C := HomologicalComplex.{v, u, u_1} V c) zero

Tactic:
⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩

Premises used: Unique.mk, Nonempty.intro, OfNat.ofNat, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
refine_1 : ∀ (X : HomologicalComplex.{v, u, u_1} V c) (f : zero ⟶ X), f = default
refine_2 : ∀ (X : HomologicalComplex.{v, u, u_1} V c) (f : X ⟶ zero), f = default
⊢ IsZero (C := HomologicalComplex.{v, u, u_1} V c) zero

Tactic:
refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : zero ⟶ X
refine_1 : ∀ (i : ι), f.f i = Hom.f default i
⊢ f = default

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : zero ⟶ X
i : ι
refine_1 : f.f i = Hom.f 0 i
⊢ f.f i = Hom.f default i

Tactic:
dsimp only [zero]

Premises used: HomologicalComplex.zero
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : zero ⟶ X
i : ι
⊢ f.f i = Hom.f 0 i

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : X ⟶ zero
refine_2 : ∀ (i : ι), f.f i = Hom.f default i
⊢ f = default

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : X ⟶ zero
i : ι
refine_2 : f.f i = Hom.f 0 i
⊢ f.f i = Hom.f default i

Tactic:
dsimp only [zero]

Premises used: HomologicalComplex.zero
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
inst_2 : HasZeroObject.{v, u} V
X : HomologicalComplex.{v, u, u_1} V c
f : X ⟶ zero
i : ι
⊢ f.f i = Hom.f 0 i

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasZeroObject.{v, u} V
⊢ HasZeroObject (HomologicalComplex.{v, u, u_1} V c)

Tactic:
⟨⟨zero, isZero_zero⟩⟩

Premises used: CategoryTheory.Limits.HasZeroObject.mk, HomologicalComplex.isZero_zero, Exists.intro, HomologicalComplex.zero
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
w : f = g
i : ι
⊢ f.f i = g.f i

Tactic:
congr_fun (congr_arg Hom.f w) i

Premises used: HomologicalComplex.Hom.f, congr_arg, congr_fun
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : Z ⟶ K
eq : g ≫ φ = h ≫ φ
h₁ : ∀ (i : ι), g.f i = h.f i
⊢ g = h

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : Z ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
h₁ : g.f i ≫ φ.f i = h.f i ≫ φ.f i
⊢ g.f i = h.f i

Tactic:
rw [← cancel_mono (φ.f i)]

Premises used: HomologicalComplex.Hom.f, CategoryTheory.cancel_mono
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : Z ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
⊢ g.f i ≫ φ.f i = h.f i ≫ φ.f i

Tactic:
congr_hom eq i

Premises used: HomologicalComplex.congr_hom
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Mono (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : Z ⟶ K
eq : g ≫ φ = h ≫ φ
i : ι
⊢ g.f i ≫ φ.f i = h.f i ≫ φ.f i

Tactic:
exact congr_hom eq i

Premises used: HomologicalComplex.congr_hom
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : L ⟶ Z
eq : φ ≫ g = φ ≫ h
h₁ : ∀ (i : ι), g.f i = h.f i
⊢ g = h

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : L ⟶ Z
eq : φ ≫ g = φ ≫ h
i : ι
h₁ : φ.f i ≫ g.f i = φ.f i ≫ h.f i
⊢ g.f i = h.f i

Tactic:
rw [← cancel_epi (φ.f i)]

Premises used: HomologicalComplex.Hom.f, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : L ⟶ Z
eq : φ ≫ g = φ ≫ h
i : ι
⊢ φ.f i ≫ g.f i = φ.f i ≫ h.f i

Tactic:
congr_hom eq i

Premises used: HomologicalComplex.congr_hom
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z : HomologicalComplex.{v, u, u_1} V c
g h : L ⟶ Z
eq : φ ≫ g = φ ≫ h
i : ι
⊢ φ.f i ≫ g.f i = φ.f i ≫ h.f i

Tactic:
exact congr_hom eq i

Premises used: HomologicalComplex.congr_hom
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C X Y : HomologicalComplex.{v, u, u_1} V c
a₁ a₂ : X ⟶ Y
h :
  Eq (α := Functor.obj (forget V c) X ⟶ Functor.obj (forget V c) Y) (CategoryTheory.Functor.map (forget V c) a₁)
    (CategoryTheory.Functor.map (forget V c) a₂)
h₁ : ∀ (i : ι), a₁.f i = a₂.f i
⊢ a₁ = a₂

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C X Y : HomologicalComplex.{v, u, u_1} V c
a₁ a₂ : X ⟶ Y
h :
  Eq (α := Functor.obj (forget V c) X ⟶ Functor.obj (forget V c) Y) (CategoryTheory.Functor.map (forget V c) a₁)
    (CategoryTheory.Functor.map (forget V c) a₂)
i : ι
⊢ a₁.f i = a₂.f i

Tactic:
congr_fun h i

Premises used: congr_fun
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C X Y : HomologicalComplex.{v, u, u_1} V c
a₁ a₂ : X ⟶ Y
h :
  Eq (α := Functor.obj (forget V c) X ⟶ Functor.obj (forget V c) Y) (CategoryTheory.Functor.map (forget V c) a₁)
    (CategoryTheory.Functor.map (forget V c) a₂)
i : ι
⊢ a₁.f i = a₂.f i

Tactic:
exact congr_fun h i

Premises used: congr_fun
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
n n' : ι
h : n = n'
subst : φ.f n ≫ (L.XIsoOfEq ⋯).hom = (K.XIsoOfEq ⋯).hom ≫ φ.f n
⊢ φ.f n ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ.f n'

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).hom = (K.XIsoOfEq ⋯).hom ≫ φ.f n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
n n' : ι
h : n = n'
subst : φ.f n ≫ (L.XIsoOfEq ⋯).inv = (K.XIsoOfEq ⋯).inv ≫ φ.f n
⊢ φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).inv = (K.XIsoOfEq ⋯).inv ≫ φ.f n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j j' : ι
rij : c.Rel i j
rij' : c.Rel i j'
obtain : ∀ (rij' : c.Rel i j), C.d i j ≫ eqToHom ⋯ = C.d i j
⊢ C.d i j' ≫ eqToHom ⋯ = C.d i j

Tactic:
obtain rfl := c.next_eq rij rij'

Premises used: ComplexShape.next_eq, rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
rij rij' : c.Rel i j
⊢ C.d i j ≫ eqToHom ⋯ = C.d i j

Tactic:
simp only [eqToHom_refl, comp_id]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i i' j : ι
rij : c.Rel i j
rij' : c.Rel i' j
obtain : ∀ (rij' : c.Rel i j), eqToHom ⋯ ≫ C.d i j = C.d i j
⊢ eqToHom ⋯ ≫ C.d i' j = C.d i j

Tactic:
obtain rfl := c.prev_eq rij rij'

Premises used: ComplexShape.prev_eq, rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
rij rij' : c.Rel i j
⊢ eqToHom ⋯ ≫ C.d i j = C.d i j

Tactic:
simp only [eqToHom_refl, id_comp]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasKernels.{v, u} V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
rw : kernelSubobject (C.d i j' ≫ eqToHom ⋯) = kernelSubobject (C.d i j')
⊢ kernelSubobject (C.d i j) = kernelSubobject (C.d i j')

Tactic:
rw [← d_comp_eqToHom C r r']

Premises used: HomologicalComplex.d_comp_eqToHom
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasKernels.{v, u} V
i j j' : ι
r : c.Rel i j
r' : c.Rel i j'
⊢ kernelSubobject (C.d i j' ≫ eqToHom ⋯) = kernelSubobject (C.d i j')

Tactic:
apply kernelSubobject_comp_mono

Premises used: CategoryTheory.Limits.kernelSubobject_comp_mono
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasImages.{v, u} V
inst_3 : HasEqualizers.{v, u} V
i i' j : ι
r : c.Rel i j
r' : c.Rel i' j
rw : imageSubobject (eqToHom ⋯ ≫ C.d i' j) = imageSubobject (C.d i' j)
⊢ imageSubobject (C.d i j) = imageSubobject (C.d i' j)

Tactic:
rw [← eqToHom_comp_d C r r']

Premises used: HomologicalComplex.eqToHom_comp_d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
inst_2 : HasImages.{v, u} V
inst_3 : HasEqualizers.{v, u} V
i i' j : ι
r : c.Rel i j
r' : c.Rel i' j
⊢ imageSubobject (eqToHom ⋯ ≫ C.d i' j) = imageSubobject (C.d i' j)

Tactic:
apply imageSubobject_iso_comp

Premises used: CategoryTheory.Limits.imageSubobject_iso_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
rw rw₁ : C.xPrev j = C.X (c.prev j)
⊢ C.xPrev j = C.X i

Tactic:
rw [← c.prev_eq' r]

Premises used: ComplexShape.prev_eq'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
hnc : ¬∃ (j_1 : ι), c.Rel j_1 j
⊢ (if h : ∃ (j_1 : ι), c.Rel j_1 j then h.choose (p := fun (a : ι) ↦ c.Rel a j) else j) = j

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
hnc : ∀ (j_1 : ι), ¬c.Rel j_1 j
⊢ ¬∃ (j_1 : ι), c.Rel j_1 j

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
i : ι
hi : c.Rel i j
⊢ c.prev j = i

Tactic:
have : c.prev j = i := c.prev_eq' hi
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
i : ι
hi : c.Rel i j
this : c.prev j = i
⊢ ¬c.Rel i j

Tactic:
rw [this] at h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
i : ι
hi : c.Rel i j
this : c.prev j = i
h₁ : ¬c.Rel i j
⊢ c.Rel i j

Tactic:
rw [this] at h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
i : ι
hi : c.Rel i j
this : c.prev j = i
h₁ : ¬c.Rel i j
hi₁ : c.Rel i j
⊢ c.prev j = i

Tactic:
rw [this] at h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j i : ι
h : ¬c.Rel i j
hi : c.Rel i j
this : c.prev j = i
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
rw rw₁ : C.xNext i = C.X (c.next i)
⊢ C.xNext i = C.X j

Tactic:
rw [← c.next_eq' r]

Premises used: ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
hnc : ¬∃ (j : ι), c.Rel i j
⊢ (if h : ∃ (j : ι), c.Rel i j then h.choose (p := c.Rel i) else i) = i

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
⊢ c.next i = j

Tactic:
have : c.next i = j := c.next_eq' hj
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
this : c.next i = j
⊢ ¬c.Rel i j

Tactic:
rw [this] at h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
this : c.next i = j
h₁ : ¬c.Rel i j
⊢ c.Rel i j

Tactic:
rw [this] at h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i : ι
h : ¬c.Rel i (c.next i)
j : ι
hj : c.Rel i j
this : c.next i = j
h₁ : ¬c.Rel i j
hj₁ : c.Rel i j
⊢ c.next i = j

Tactic:
rw [this] at h
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
h : ¬c.Rel i j
hj : c.Rel i j
this : c.next i = j
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j : ι
r : c.Rel i j
obtain : ∀ (r : c.Rel (c.prev j) j), C.dTo j = (C.xPrevIso r).hom ≫ C.d (c.prev j) j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d i j

Tactic:
obtain rfl := c.prev_eq' r

Premises used: ComplexShape.prev_eq', rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
r : c.Rel (c.prev j) j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d (c.prev j) j

Tactic:
(Category.id_comp _).symm

Premises used: Eq.mpr, CategoryTheory.eqToHom, Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
r : c.Rel (c.prev j) j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d (c.prev j) j

Tactic:
exact (Category.id_comp _).symm

Premises used: Eq.symm, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ C.dTo j = 0

Tactic:
simp [h]