awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
pos : ∀ (hj' : ∃ (j : ι), e.f j = j'), QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
neg : ∀ (hj' : ¬∃ (j : ι), e.f j = j'), QuasiIsoAt (K := K.extend e) (extendMap φ e) j'
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j'

Tactic:
by_cases hj' : ∃ j, e.f j = j'
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
hj' : ∃ (j : ι), e.f j = j'
pos : ∀ (j : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f j)
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j'

Tactic:
obtain ⟨j, rfl⟩ := hj'

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j : ι
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f j)

Tactic:
h j
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j : ι
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f j)

Tactic:
exact h j
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ (j : ι), e.f j = j'
neg : (L.extend e).ExactAt j'
neg₁ : (K.extend e).ExactAt j'
⊢ QuasiIsoAt (K := K.extend e) (extendMap φ e) j'

Tactic:
rw [quasiIsoAt_iff_exactAt]

Premises used: quasiIsoAt_iff_exactAt
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ (j : ι), e.f j = j'
⊢ ∀ (j : ι), e.f j ≠ j'

Tactic:
simpa using hj'
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ (j : ι), e.f j = j'
⊢ (L.extend e).ExactAt j'

Tactic:
exact extend_exactAt _ _ _ (by simpa using hj')

Premises used: HomologicalComplex.extend_exactAt
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (K := K.extend e) (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ (j : ι), e.f j = j'
⊢ (K.extend e).ExactAt j'

Tactic:
exact extend_exactAt _ _ _ (by simpa using hj')

Premises used: HomologicalComplex.extend_exactAt
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
inst_4 : ∀ (j : ι), L.HasHomology j
inst_5 rwa rwa₁ rwa₂ rwa₃ : QuasiIso φ
⊢ QuasiIso (K := K.extend e) (extendMap φ e)

Tactic:
rwa [quasiIso_extendMap_iff]

Premises used: HomologicalComplex.quasiIso_extendMap_iff
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
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
φ : (i j : ι) → K.X i ⟶ L.X j
i' j' : Option ι
i j : ι
hi : i' = some i
hj : j' = some j
subst :
  Eq (α := extend.X K (some i) ⟶ extend.X L (some j)) (homAux φ (some i) (some j))
    (Iso.hom (extend.XIso K ⋯) ≫ φ i j ≫ Iso.inv (extend.XIso L ⋯))
⊢ Eq (α := extend.X K i' ⟶ extend.X L j') (homAux φ i' j')
    (Iso.hom (extend.XIso K hi) ≫ φ i j ≫ Iso.inv (extend.XIso L hj))

Tactic:
subst hi hj
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
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
φ : (i j : ι) → K.X i ⟶ L.X j
i j : ι
⊢ Eq (α := extend.X K (some i) ⟶ extend.X L (some j)) (homAux φ (some i) (some j))
    (Iso.hom (extend.XIso K ⋯) ≫ φ i j ≫ Iso.inv (extend.XIso L ⋯))

Tactic:
simp [homAux, extend.XIso, extend.X]

Premises used: Homotopy.extend.homAux, HomologicalComplex.extend.XIso, HomologicalComplex.extend.X
-- 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
e : c.Embedding c'
φ : (i j : ι) → K.X i ⟶ L.X j
i' j' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (hom e φ i' j') 0

Tactic:
(isZero_extend_X _ _ _ hi').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
e : c.Embedding c'
φ : (i j : ι) → K.X i ⟶ L.X j
i' j' : ι'
hj' : ∀ (j : ι), e.f j ≠ j'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (hom e φ i' j') 0

Tactic:
(isZero_extend_X _ _ _ hj').eq_of_tgt _ _

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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
e : c.Embedding c'
φ : (i j : ι) → K.X i ⟶ L.X j
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 e φ i' j')
    (Iso.hom (K.extendXIso e hi) ≫ φ i j ≫ Iso.inv (L.extendXIso e hj))

Tactic:
homAux_eq φ (e.r i') (e.r j') i j (e.r_eq_some hi) (e.r_eq_some hj)

Premises used: Homotopy.extend.hom, ComplexShape.Embedding.r_eq_some, Homotopy.extend.homAux_eq, HomologicalComplex.extend.X, ComplexShape.Embedding.r
-- 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' : ι'
hij' : ¬c'.Rel j' i'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0

Tactic:
by_cases hi' : ∃ i, e.f i = 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
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i' j' : ι'
hij' : ¬c'.Rel j' i'
hi' : ∃ (i : ι), e.f i = i'
pos :
  ∀ (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
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0

Tactic:
obtain ⟨i, rfl⟩ := hi'

Premises used: 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
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
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
⊢ 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'
-- 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
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
hj' : ∃ (j : ι), e.f j = j'
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
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (extend.hom e h.hom (e.f i) j') 0

Tactic:
obtain ⟨j, rfl⟩ := hj'

Premises used: 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 j : ι
hij' rwa rwa₁ rwa₂ rwa₃ : ¬c'.Rel (e.f j) (e.f i)
⊢ ¬c.Rel j 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 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
pos₃ pos₄ : Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) 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

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

Premises used: CategoryTheory.Limits.comp_zero, Homotopy.zero, CategoryTheory.Limits.zero_comp, 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
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
hj' : ¬∃ (j : ι), e.f j = j'
tauto tauto₁ : ∀ (j : ι), e.f j ≠ j'
tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ (j : ι), e.f j = j' → False
⊢ ∀ (j : ι), e.f j ≠ j'

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

Tactic:
exact extend.hom_eq_zero₂ _ _ _ _ (by tauto)

Premises used: Homotopy.extend.hom_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' j' : ι'
hij' : ¬c'.Rel j' 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' j' : ι'
hij' : ¬c'.Rel j' i'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j') (extend.hom e h.hom i' j') 0

Tactic:
exact extend.hom_eq_zero₁ _ _ _ _ (by tauto)

Premises used: Homotopy.extend.hom_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' : ∃ (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'
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'
⊢ 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'
-- 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'
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)
⊢ 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:
obtain ⟨i, rfl⟩ := hi'

Premises used: 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 : ι
pos :
  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))
⊢ 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:
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]

Premises used: HomologicalComplex.extendMap_f, add_left_inj, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, Homotopy.comm, 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 : ι
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))
pos₁ :
  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))
⊢ 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))

Tactic:
congr 1