awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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 :
  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 ⋯)
pos :
  ∀ (hi : c.Rel i (c.next i)),
    Eq.{v_1 + 1} (α := (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))
      (Iso.hom (K.extendXIso e ⋯) ≫
          ((dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
              Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
            Iso.inv (L.extendXIso e ⋯) :
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
⊢ Eq.{v_1 + 1} (α := (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))
    (Iso.hom (K.extendXIso e ⋯) ≫
        ((dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have neg : ∀ (hi : ¬c.Rel i (c.next i)),
  Eq.{v_1 + 1} (α := (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))
    (Iso.hom (K.extendXIso e sorry) ≫
        ((dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e sorry) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e sorry)) ≫
          Iso.inv (L.extendXIso e sorry) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: by_cases hi : c.Rel i (c.next i)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (hypothesis)
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 :
  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 ⋯)
hi : c.Rel i (c.next i)
⊢ Eq.{v_1 + 1} (α := (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))
    (Iso.hom (K.extendXIso e ⋯) ≫
        ((dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have hi' : 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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 :
  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 ⋯)
hi : ¬c.Rel i (c.next i)
⊢ Eq.{v_1 + 1} (α := (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))
    (Iso.hom (K.extendXIso e ⋯) ≫
        ((dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have neg : Eq.{v_1 + 1} (α := (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))
  (Iso.hom (K.extendXIso e sorry) ≫ 0 ≫ Iso.inv (L.extendXIso e sorry) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: rw [dNext_eq_zero _ _ hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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 :
  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 ⋯)
hi : ¬c.Rel i (c.next i)
⊢ Eq.{v_1 + 1} (α := (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))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have pos : ∀ (hi' : c'.Rel (e.f i) (c'.next (e.f i))),
  Eq.{v_1 + 1} (α := (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))
    (Iso.hom (K.extendXIso e sorry) ≫ 0 ≫ Iso.inv (L.extendXIso e sorry) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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 :
  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 ⋯)
hi : ¬c.Rel i (c.next i)
pos :
  ∀ (hi' : c'.Rel (e.f i) (c'.next (e.f i))),
    Eq.{v_1 + 1} (α := (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))
      (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
⊢ Eq.{v_1 + 1} (α := (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))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have neg : ∀ (hi' : ¬c'.Rel (e.f i) (c'.next (e.f i))),
  Eq.{v_1 + 1} (α := (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))
    (Iso.hom (K.extendXIso e sorry) ≫ 0 ≫ Iso.inv (L.extendXIso e sorry) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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 :
  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 ⋯)
⊢ Eq.{v_1 + 1} (α := (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 ⋯) ≫
        ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have pos : ∀ (hi : c.Rel (c.prev i) i),
  Eq.{v_1 + 1} (α := (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 sorry) ≫
        ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e sorry) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e sorry)) ≫
          Iso.inv (L.extendXIso e sorry) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: by_cases hi : c.Rel (c.prev i) i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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 :
  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 ⋯)
pos :
  ∀ (hi : c.Rel (c.prev i) i),
    Eq.{v_1 + 1} (α := (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 ⋯) ≫
          ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
              Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
            Iso.inv (L.extendXIso e ⋯) :
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
⊢ Eq.{v_1 + 1} (α := (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 ⋯) ≫
        ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have neg : ∀ (hi : ¬c.Rel (c.prev i) i),
  Eq.{v_1 + 1} (α := (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 sorry) ≫
        ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e sorry) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e sorry)) ≫
          Iso.inv (L.extendXIso e sorry) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: by_cases hi : c.Rel (c.prev i) i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (hypothesis)
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 :
  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 ⋯)
hi : c.Rel (c.prev i) i
⊢ Eq.{v_1 + 1} (α := (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 ⋯) ≫
        ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have hi' : 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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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 :
  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 ⋯)
hi : ¬c.Rel (c.prev i) i
⊢ Eq.{v_1 + 1} (α := (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 ⋯) ≫
        ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have neg : Eq.{v_1 + 1} (α := (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 sorry) ≫ 0 ≫ Iso.inv (L.extendXIso e sorry) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: rw [prevD_eq_zero _ _ hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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 :
  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 ⋯)
hi : ¬c.Rel (c.prev i) i
⊢ Eq.{v_1 + 1} (α := (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 ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have pos : ∀ (hi' : c'.Rel (c'.prev (e.f i)) (e.f i)),
  Eq.{v_1 + 1} (α := (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 sorry) ≫ 0 ≫ Iso.inv (L.extendXIso e sorry) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: by_cases hi' : c'.Rel (c'.prev (e.f i)) (e.f i)