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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (extend.hom e h.hom (e.f i) j') 0
have pos : ∀ (hj' : ∃ (j : ι), e.f j = j'), Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (extend.hom e h.hom (e.f i) j') 0
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
pos :
  ∀ (hj' : ∃ (j : ι), e.f j = j'),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (extend.hom e h.hom (e.f i) j') 0
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (extend.hom e h.hom (e.f i) j') 0
have neg : ∀ (hj' : ¬∃ (j : ι), e.f j = j'), Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (extend.hom e h.hom (e.f i) j') 0
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
hj' : ∃ (j : ι), e.f j = j'
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (extend.hom e h.hom (e.f i) j') 0
have pos : ∀ (j : ι) (hij' : ¬c'.Rel (e.f j) (e.f i)),
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (extend.hom e h.hom (e.f i) (e.f j)) 0
Tactic: obtain ⟨j, rfl⟩ := hj'
Cleared hypotheses: j', hij', hj'
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (extend.hom e h.hom (e.f i) (e.f j)) 0
have pos : Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j))
  (Iso.hom (K.extendXIso e sorry) ≫ h.hom i j ≫ Iso.inv (L.extendXIso e sorry)) 0
Tactic: rw [extend.hom_eq _ _ rfl rfl, h.zero _ _ (by rwa [← e.rel_iff]),
          zero_comp, comp_zero]
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
pos :
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j))
    (Iso.hom (K.extendXIso e ⋯) ≫ h.hom i j ≫ Iso.inv (L.extendXIso e ⋯)) 0
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (extend.hom e h.hom (e.f i) (e.f j)) 0
have pos₁ : Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (Iso.hom (K.extendXIso e sorry) ≫ 0 ≫ Iso.inv (L.extendXIso e sorry))
  0
Tactic: rw [extend.hom_eq _ _ rfl rfl, h.zero _ _ (by rwa [← e.rel_iff]),
          zero_comp, comp_zero]
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
pos :
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j))
    (Iso.hom (K.extendXIso e ⋯) ≫ h.hom i j ≫ Iso.inv (L.extendXIso e ⋯)) 0
pos₁ :
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯)) 0
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (extend.hom e h.hom (e.f i) (e.f j)) 0
have pos₂ : Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (Iso.hom (K.extendXIso e sorry) ≫ 0) 0
Tactic: rw [extend.hom_eq _ _ rfl rfl, h.zero _ _ (by rwa [← e.rel_iff]),
          zero_comp, comp_zero]
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
pos :
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j))
    (Iso.hom (K.extendXIso e ⋯) ≫ h.hom i j ≫ Iso.inv (L.extendXIso e ⋯)) 0
pos₁ :
  Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯)) 0
pos₂ : Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (Iso.hom (K.extendXIso e ⋯) ≫ 0) 0
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (extend.hom e h.hom (e.f i) (e.f j)) 0
have pos₃ : Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) 0 0
Tactic: rw [extend.hom_eq _ _ rfl rfl, h.zero _ _ (by rwa [← e.rel_iff]),
          zero_comp, comp_zero]
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
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'
have pos : ∀ (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: by_cases hi' : ∃ i, e.f 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i' : ι'
pos :
  ∀ (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'
⊢ 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'
have neg : ∀ (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: by_cases hi' : ∃ i, e.f 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
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'
have pos : ∀ (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))
            (extend.hom e 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))
            (extend.hom e 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: obtain ⟨i, rfl⟩ := hi'
Cleared hypotheses: i', 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
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))
            (extend.hom e 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))
            (extend.hom e h.hom) :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Hom.f (extendMap g e) (e.f i)
have pos : HAdd.hAdd (α := (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) h.hom ≫ Iso.inv (L.extendXIso e sorry))
    (Iso.hom (K.extendXIso e sorry) ≫
      (prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e sorry)) =
  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))
        (extend.hom e 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))
        (extend.hom e h.hom) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
Tactic: rw [extendMap_f _ _ rfl, extendMap_f _ _ rfl, h.comm i, Preadditive.add_comp,
        Preadditive.add_comp, Preadditive.comp_add, Preadditive.comp_add, add_left_inj]
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
⊢ HAdd.hAdd (α := (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 ⋯))
      (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 ⋯)) =
    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))
          (extend.hom e 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))
          (extend.hom e h.hom) :
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have pos : Eq (α := (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) h.hom ≫ Iso.inv (L.extendXIso e sorry))
  ((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: congr 1
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
pos :
  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))
⊢ HAdd.hAdd (α := (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 ⋯))
      (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 ⋯)) =
    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))
          (extend.hom e 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))
          (extend.hom e h.hom) :
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
have pos₁ : Eq (α := (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) h.hom ≫ Iso.inv (L.extendXIso e sorry))
  ((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: congr 1
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
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))
have 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 sorry) ≫
      (dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e sorry))
    ((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)
-- 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
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))
⊢ 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))
have 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 sorry) ≫
      (dNext i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) h.hom ≫ Iso.inv (L.extendXIso e sorry))
    ((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)
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
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))
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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
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))
have neg : Eq (α := (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))
  ((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]
-- 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i : ι
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 ⋯) ≫ 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))
have 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 sorry) ≫ 0 ≫ Iso.inv (L.extendXIso e sorry))
    ((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))