awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
pos :
  ∀ (hi : c.Rel i (c.next i)),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫
        (dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
      ((dNext (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        (extend.hom e h.hom))
neg :
  ∀ (hi : ¬c.Rel i (c.next i)),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫
        (dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
      ((dNext (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        (extend.hom e h.hom))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫
      (dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
    ((dNext (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
by_cases hi : c.Rel i (c.next i)

Premises used: ComplexShape.next, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi rwa rwa₁ rwa₂ rwa₃ : c.Rel i (c.next i)
⊢ c'.Rel (e.f i) (e.f (c.next i))

Tactic:
rwa [e.rel_iff]

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : c.Rel i (c.next i)
⊢ c'.Rel (e.f i) (e.f (c.next i))

Tactic:
have hi' : c'.Rel (e.f i) (e.f (c.next i)) := by rwa [e.rel_iff]
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : c.Rel i (c.next i)
hi' : c'.Rel (e.f i) (e.f (c.next i))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫
      (dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
    ((dNext (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
simp [dNext_eq _ hi, dNext_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]

Premises used: dNext_eq, HomologicalComplex.extend_d_eq, Homotopy.extend.hom_eq, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : ¬c.Rel i (c.next i)
neg :
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
    ((dNext (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫
      (dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
    ((dNext (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
rw [dNext_eq_zero _ _ hi]

Premises used: dNext_eq_zero
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : ¬c.Rel i (c.next i)
pos :
  ∀ (hi' : c'.Rel (e.f i) (c'.next (e.f i))),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
      ((dNext (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        (extend.hom e h.hom))
neg :
  ∀ (hi' : ¬c'.Rel (e.f i) (c'.next (e.f i))),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
      ((dNext (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        (extend.hom e h.hom))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
    ((dNext (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))

Premises used: ComplexShape.next, ComplexShape.Embedding.f, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : ¬c.Rel i (c.next i)
hi' : c'.Rel (e.f i) (c'.next (e.f i))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
    ((dNext (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
simp [dNext_eq _ hi', K.extend_d_from_eq_zero _ _ _ _ rfl hi]

Premises used: HomologicalComplex.extend_d_from_eq_zero, dNext_eq, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : ¬c.Rel i (c.next i)
hi' : ¬c'.Rel (e.f i) (c'.next (e.f i))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
    ((dNext (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
simp [dNext_eq_zero _ _ hi']

Premises used: dNext_eq_zero
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
pos :
  ∀ (hi : c.Rel (c.prev i) i),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫
        (prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
      ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        (extend.hom e h.hom))
neg :
  ∀ (hi : ¬c.Rel (c.prev i) i),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫
        (prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
      ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        (extend.hom e h.hom))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫
      (prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
    ((prevD (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
by_cases hi : c.Rel (c.prev i) i

Premises used: ComplexShape.prev, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi rwa rwa₁ rwa₂ rwa₃ : c.Rel (c.prev i) i
⊢ c'.Rel (e.f (c.prev i)) (e.f i)

Tactic:
rwa [e.rel_iff]

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : c.Rel (c.prev i) i
⊢ c'.Rel (e.f (c.prev i)) (e.f i)

Tactic:
have hi' : c'.Rel (e.f (c.prev i)) (e.f i) := by rwa [e.rel_iff]
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : c.Rel (c.prev i) i
hi' : c'.Rel (e.f (c.prev i)) (e.f i)
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫
      (prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
    ((prevD (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
simp [prevD_eq _ hi, prevD_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]

Premises used: prevD_eq, HomologicalComplex.extend_d_eq, Homotopy.extend.hom_eq, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : ¬c.Rel (c.prev i) i
neg :
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
    ((prevD (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫
      (prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e ⋯))
    ((prevD (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
rw [prevD_eq_zero _ _ hi]

Premises used: prevD_eq_zero
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : ¬c.Rel (c.prev i) i
pos :
  ∀ (hi' : c'.Rel (c'.prev (e.f i)) (e.f i)),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
      ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        (extend.hom e h.hom))
neg :
  ∀ (hi' : ¬c'.Rel (c'.prev (e.f i)) (e.f i)),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
      ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        (extend.hom e h.hom))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
    ((prevD (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
by_cases hi' : c'.Rel (c'.prev (e.f i)) (e.f i)

Premises used: ComplexShape.prev, ComplexShape.Embedding.f, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : ¬c.Rel (c.prev i) i
hi' : c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
    ((prevD (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
simp [prevD_eq _ hi', L.extend_d_to_eq_zero _ _ _ _ rfl hi]

Premises used: prevD_eq, HomologicalComplex.extend_d_to_eq_zero, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
hi : ¬c.Rel (c.prev i) i
hi' : ¬c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯))
    ((prevD (e.f i) :
        (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (extend.hom e h.hom))

Tactic:
simp [prevD_eq_zero _ _ hi']

Premises used: prevD_eq_zero
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
tauto tauto₁ : ∀ (i : ι), e.f i ≠ i'
tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ (i : ι), e.f i = i' → False
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ Hom.f (extendMap f e) i' =
    HAdd.hAdd (α := (K.extend e).X i' ⟶ (L.extend e).X i') (β := (K.extend e).X i' ⟶ (L.extend e).X i')
        ((dNext i' : (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X i' ⟶ (L.extend e).X i')
            (extend.hom e h.hom) :
          (K.extend e).X i' ⟶ (L.extend e).X i')
        ((prevD i' : (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X i' ⟶ (L.extend e).X i')
            (extend.hom e h.hom) :
          (K.extend e).X i' ⟶ (L.extend e).X i') +
      Hom.f (extendMap g e) i'

Tactic:
exact (isZero_extend_X _ _ _ (by tauto)).eq_of_src _ _

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i' j' : ι'
i j : ι
hi : e.f i = i'
hj : e.f j = j'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (hom (h.extend e) i' j')
    (Iso.hom (K.extendXIso e hi) ≫ h.hom i j ≫ Iso.inv (L.extendXIso e hj))

Tactic:
extend.hom_eq _ _ _ _

Premises used: Homotopy.extend.hom, Homotopy.extend.homAux, Homotopy.extend.hom_eq
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i j : ι
hij rwa rwa₁ rwa₂ rwa₃ : ¬c.Rel j i
⊢ ¬c'.Rel (e.f j) (e.f i)

Tactic:
rwa [e.rel_iff]

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i j : ι
hij : ¬c.Rel j i
rw :
  Eq (α := K.X i ⟶ L.X j)
    (CategoryStruct.comp (Y := (K.extend e).X (e.f i)) (Iso.inv (K.extendXIso e ⋯))
      (CategoryStruct.comp (Y := (L.extend e).X (e.f j)) 0 (Iso.hom (L.extendXIso e ⋯))))
    0
rw₁ : Eq (α := K.X i ⟶ L.X j) (CategoryStruct.comp (Y := (K.extend e).X (e.f i)) (Iso.inv (K.extendXIso e ⋯)) 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := K.X i ⟶ L.X j) 0 0
⊢ Eq (α := K.X i ⟶ L.X j) (Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0

Tactic:
rw [h.zero _ _ (by rwa [e.rel_iff]), zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, Homotopy.zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i : ι
⊢ Hom.f (extendMap f e) (e.f i) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Hom.f (extendMap g e) (e.f i)

Tactic:
have := h.comm (e.f i)
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i : ι
this :
  Hom.f (extendMap f e) (e.f i) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Hom.f (extendMap g e) (e.f i)
⊢ Iso.hom (K.extendXIso e ⋯) ≫ f.f i ≫ Iso.inv (L.extendXIso e ⋯) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Iso.hom (K.extendXIso e ⋯) ≫ g.f i ≫ Iso.inv (L.extendXIso e ⋯)

Tactic:
simp only [extendMap_f _ _ rfl] at this

Premises used: HomologicalComplex.extendMap_f, rfl