awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
⊢ Eq (α := K.extend e ⟶ L.extend e) (extendMap 0 e) 0
have h : ∀ (i' : ι'), Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
Tactic: ext i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
⊢ Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'),
  Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
pos :
  ∀ (hi' : ∃ (i : ι), e.f i = i'),
    Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
⊢ Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'),
  Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
have pos : ∀ (i : ι) (hi : e.f i = i'),
  Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
Tactic: obtain ⟨i, hi⟩ := hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
⊢ (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
have this : Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j' =
  (K.extend e).op.d i' j' ≫ Hom.f (Iso.inv (K.extendOpIso e)) j'
Tactic: have := (K.extendOpIso e).inv.comm i' j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
this :
  Eq (α := Opposite.op ((K.extend e).X i') ⟶ (K.op.extend e.op).X j')
    (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
    (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
⊢ (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
have rw : (K.op.extend e.op).d i' j' =
  CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
    (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
Tactic: rw [← this, ← comp_f_assoc, Iso.hom_inv_id, id_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
this :
  Eq (α := Opposite.op ((K.extend e).X i') ⟶ (K.op.extend e.op).X j')
    (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
    (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
rw :
  (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
⊢ (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
have rw₁ : (K.op.extend e.op).d i' j' =
  Hom.f (CategoryStruct.comp (Y := (K.extend e).op) (Iso.hom (K.extendOpIso e)) (Iso.inv (K.extendOpIso e))) i' ≫
    (K.op.extend e.op).d i' j'
Tactic: rw [← this, ← comp_f_assoc, Iso.hom_inv_id, id_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
this :
  Eq (α := Opposite.op ((K.extend e).X i') ⟶ (K.op.extend e.op).X j')
    (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
    (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
rw :
  (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
rw₁ :
  (K.op.extend e.op).d i' j' =
    Hom.f (CategoryStruct.comp (Y := (K.extend e).op) (Iso.hom (K.extendOpIso e)) (Iso.inv (K.extendOpIso e))) i' ≫
      (K.op.extend e.op).d i' j'
⊢ (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
have rw₂ : (K.op.extend e.op).d i' j' = Hom.f (𝟙 (K.op.extend e.op)) i' ≫ (K.op.extend e.op).d i' j'
Tactic: rw [← this, ← comp_f_assoc, Iso.hom_inv_id, id_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
this :
  Eq (α := Opposite.op ((K.extend e).X i') ⟶ (K.op.extend e.op).X j')
    (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
    (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
rw :
  (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
rw₁ :
  (K.op.extend e.op).d i' j' =
    Hom.f (CategoryStruct.comp (Y := (K.extend e).op) (Iso.hom (K.extendOpIso e)) (Iso.inv (K.extendOpIso e))) i' ≫
      (K.op.extend e.op).d i' j'
rw₂ : (K.op.extend e.op).d i' j' = Hom.f (𝟙 (K.op.extend e.op)) i' ≫ (K.op.extend e.op).d i' j'
⊢ (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
have rw₃ : (K.op.extend e.op).d i' j' = 𝟙 ((K.op.extend e.op).X i') ≫ (K.op.extend e.op).d i' j'
Tactic: rw [← this, ← comp_f_assoc, Iso.hom_inv_id, id_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
this :
  Eq (α := Opposite.op ((K.extend e).X i') ⟶ (K.op.extend e.op).X j')
    (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
    (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
rw :
  (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
rw₁ :
  (K.op.extend e.op).d i' j' =
    Hom.f (CategoryStruct.comp (Y := (K.extend e).op) (Iso.hom (K.extendOpIso e)) (Iso.inv (K.extendOpIso e))) i' ≫
      (K.op.extend e.op).d i' j'
rw₂ : (K.op.extend e.op).d i' j' = Hom.f (𝟙 (K.op.extend e.op)) i' ≫ (K.op.extend e.op).d i' j'
rw₃ : (K.op.extend e.op).d i' j' = 𝟙 ((K.op.extend e.op).X i') ≫ (K.op.extend e.op).d i' j'
⊢ (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
have rw₄ : (K.op.extend e.op).d i' j' = (K.op.extend e.op).d i' j'
Tactic: rw [← this, ← comp_f_assoc, Iso.hom_inv_id, id_f, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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
φ φ' : K ⟶ L
e : c.Embedding c'
⊢ extendMap (φ + φ') e = HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)
have h : ∀ (i' : ι'),
  Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
Tactic: ext i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
⊢ Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'),
  Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
pos :
  ∀ (hi' : ∃ (i : ι), e.f i = i'),
    Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
⊢ Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'),
  Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
have pos : ∀ (i : ι) (hi : e.f i = i'),
  Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
Tactic: obtain ⟨i, hi⟩ := hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) j' k') 0
have pos : ∀ (hj : ∃ (j : ι), e.f j = j'),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) j' k') 0
Tactic: by_cases hj : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
pos :
  ∀ (hj : ∃ (j : ι), e.f j = j'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
      (d (extend (Functor.obj (single C c i) X) e) j' k') 0
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) j' k') 0
have neg : ∀ (hj : ¬∃ (j : ι), e.f j = j'),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) j' k') 0
Tactic: by_cases hj : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ∃ (j : ι), e.f j = j'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) j' k') 0
have pos : ∀ (j : ι),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
Tactic: obtain ⟨j, rfl⟩ := hj
Cleared hypotheses: j', hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
k' : ι'
j : ι
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
have pos : ∀ (hk : ∃ (k : ι), e.f k = k'),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
Tactic: by_cases hk : ∃ k, e.f k = k'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
k' : ι'
j : ι
pos :
  ∀ (hk : ∃ (k : ι), e.f k = k'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
      (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
have neg : ∀ (hk : ¬∃ (k : ι), e.f k = k'),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
Tactic: by_cases hk : ∃ k, e.f k = k'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
k' : ι'
j : ι
hk : ∃ (k : ι), e.f k = k'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
have pos : ∀ (k : ι),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f k))
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) (e.f k)) 0
Tactic: obtain ⟨k, rfl⟩ := hk
Cleared hypotheses: k', hk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_1, u_3, u_2} C c') (extend (Functor.obj (single C c i) X) e)
      (extend (Functor.obj (single C c i) X) e))
    (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
      (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) ⋯)
      (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h)) ⋯))
    (𝟙 (extend (Functor.obj (single C c i) X) e))
have h₁ : ∀ (j' : ι'),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j')
    (Hom.f
      (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
        (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) sorry)
        (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h)) sorry))
      j')
    (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) j')
Tactic: ext j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j')
    (Hom.f
      (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
        (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) ⋯)
        (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h)) ⋯))
      j')
    (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) j')
have pos : ∀ (hj : ∃ (j : ι), e.f j = j'),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j')
    (Hom.f
      (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
        (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) sorry)
        (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h)) sorry))
      j')
    (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) j')
Tactic: by_cases hj : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (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 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
pos :
  ∀ (hj : ∃ (j : ι), e.f j = j'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j')
      (Hom.f
        (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
          (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) ⋯)
          (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h))
            ⋯))
        j')
      (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) j')
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j')
    (Hom.f
      (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
        (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) ⋯)
        (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h)) ⋯))
      j')
    (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) j')
have neg : ∀ (hj : ¬∃ (j : ι), e.f j = j'),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j')
    (Hom.f
      (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
        (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) sorry)
        (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h)) sorry))
      j')
    (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) j')
Tactic: by_cases hj : ∃ j, e.f j = j'