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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
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')
have pos : ∀ (j : ι) (hj : 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: obtain ⟨j, hj⟩ := hj
Cleared hypotheses: 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
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : 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')
have pos : ∀ (hij : j = i),
  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 hij : j = 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
pos :
  ∀ (hij : j = i),
    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 : ∀ (hij : ¬j = i),
  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 hij : j = 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
⊢ i' = j'
have rw : i' = e.f j
Tactic: rw [← hj, hij, h]
-- 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' : ι'
j : ι
hj : e.f j = j'
hij : j = i
rw : i' = e.f j
⊢ i' = j'
have rw₁ : i' = e.f i
Tactic: rw [← hj, hij, h]
-- 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' : ι'
j : ι
hj : e.f j = j'
hij : j = i
rw : i' = e.f j
rw₁ : i' = e.f i
⊢ i' = j'
have rw₂ : i' = i'
Tactic: rw [← hj, hij, h]
-- 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' : ι'
j : ι
hj : e.f j = j'
hij : j = i
⊢ 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 : e.f j = i'),
  Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i')
    (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))
      i')
    (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) i')
Tactic: obtain rfl : i' = j' := by rw [← hj, hij, h]
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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
⊢ Projective.{v_1, u_3} ((K.extend e).X i')
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Projective.{v_1, u_3} ((K.extend e).X 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Projective.{v_1, u_3} ((K.extend e).X i')
⊢ Projective.{v_1, u_3} ((K.extend e).X i')
have neg : ∀ (hi' : ∀ (i : ι), e.f i ≠ i'), Projective.{v_1, u_3} ((K.extend e).X 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ Projective.{v_1, u_3} ((K.extend e).X i')
have pos : ∀ (i : ι) (hi : e.f i = i'), Projective.{v_1, u_3} ((K.extend e).X 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
⊢ Injective.{v_1, u_3} ((K.extend e).X i')
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Injective.{v_1, u_3} ((K.extend e).X 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Injective.{v_1, u_3} ((K.extend e).X i')
⊢ Injective.{v_1, u_3} ((K.extend e).X i')
have neg : ∀ (hi' : ∀ (i : ι), e.f i ≠ i'), Injective.{v_1, u_3} ((K.extend e).X 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ Injective.{v_1, u_3} ((K.extend e).X i')
have pos : ∀ (i : ι) (hi : e.f i = i'), Injective.{v_1, u_3} ((K.extend e).X 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 ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i j : ι
h : c.Rel i j
⊢ (Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯)) ≫ L.d i j =
    K.d i j ≫ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)
have this : Eq (α := (Functor.obj (e.extendFunctor C) K).X (e.f i) ⟶ (Functor.obj (e.extendFunctor C) L).X (e.f j))
  (φ.f (e.f i) ≫ (Functor.obj (e.extendFunctor C) L).d (e.f i) (e.f j))
  ((Functor.obj (e.extendFunctor C) K).d (e.f i) (e.f j) ≫ φ.f (e.f j))
Tactic: have := φ.comm (e.f i) (e.f j)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i j : ι
h : c.Rel i j
this :
  Eq (α := (Functor.obj (e.extendFunctor C) K).X (e.f i) ⟶ (Functor.obj (e.extendFunctor C) L).X (e.f j))
    (φ.f (e.f i) ≫ (Functor.obj (e.extendFunctor C) L).d (e.f i) (e.f j))
    ((Functor.obj (e.extendFunctor C) K).d (e.f i) (e.f j) ≫ φ.f (e.f j))
⊢ (Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯)) ≫ L.d i j =
    K.d i j ≫ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)
have this₁ : φ.f (e.f i) ≫ Iso.hom (L.extendXIso e sorry) ≫ L.d i j ≫ Iso.inv (L.extendXIso e sorry) =
  (Iso.hom (K.extendXIso e sorry) ≫ K.d i j ≫ Iso.inv (K.extendXIso e sorry)) ≫ φ.f (e.f j)
Tactic: simp only [extendFunctor_obj, K.extend_d_eq e rfl rfl, L.extend_d_eq e rfl rfl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
⊢ CategoryTheory.Functor.map (e.extendFunctor C)
      { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ } =
    φ
have h : ∀ (i' : ι'),
  HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e sorry) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e sorry), comm' := sorry })
      i' =
    φ.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 ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i' : ι'
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
      i' =
    φ.f i'
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'),
  HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e sorry) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e sorry), comm' := sorry })
      i' =
    φ.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 ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i' : ι'
pos :
  ∀ (hi' : ∃ (i : ι), e.f i = i'),
    HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (e.extendFunctor C)
          { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
        i' =
      φ.f i'
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
      i' =
    φ.f i'
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'),
  HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e sorry) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e sorry), comm' := sorry })
      i' =
    φ.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 ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
      i' =
    φ.f i'
have pos : ∀ (i : ι),
  Eq (α := (Functor.obj (e.extendFunctor C) K).X (e.f i) ⟶ (Functor.obj (e.extendFunctor C) L).X (e.f i))
    (HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e sorry) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e sorry), comm' := sorry })
      (e.f i))
    (φ.f (e.f i))
Tactic: obtain ⟨i, rfl⟩ := hi'
Cleared hypotheses: i', hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
f : K ⟶ L
⊢ {
      f := fun (i : ι) ↦
        CategoryStruct.comp (Y := (K.extend e).X (e.f i)) (Iso.inv (K.extendXIso e ⋯))
          (CategoryStruct.comp (Y := (Functor.obj (e.extendFunctor C) L).X (e.f i))
            (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (e.extendFunctor C) f) (e.f i))
            (Iso.hom (L.extendXIso e ⋯))),
      comm' := ⋯ } =
    f
have h : ∀ (i : ι),
  HomologicalComplex.Hom.f
      {
        f := fun (i : ι) ↦
          CategoryStruct.comp (Y := (K.extend e).X (e.f i)) (Iso.inv (K.extendXIso e sorry))
            (CategoryStruct.comp (Y := (Functor.obj (e.extendFunctor C) L).X (e.f i))
              (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (e.extendFunctor C) f) (e.f i))
              (Iso.hom (L.extendXIso e sorry))),
        comm' := sorry }
      i =
    f.f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have pos : ∀ (hjk : c.Rel j k), φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
pos : ∀ (hjk : c.Rel j k), φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have neg : ∀ (hjk : ¬c.Rel j k), φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ e.f k = k'
have rw : e.f k = c'.next j'
Tactic: rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
rw : e.f k = c'.next j'
⊢ e.f k = k'
have rw₁ : e.f k = c'.next (e.f j)
Tactic: rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
rw : e.f k = c'.next j'
rw₁ : e.f k = c'.next (e.f j)
⊢ e.f k = k'
have rw₂ : e.f k = e.f k
Tactic: rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have hk'₁ : e.f k = k'
Tactic: have hk' : e.f k = k' := by rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk'_1 : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
hk' : e.f k = k'
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have pos : φ ≫ K.d j k = 0 ↔
  Eq (α := W ⟶ (K.extend e).X k')
    (φ ≫
      CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
        (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')))
    0
Tactic: rw [K.extend_d_eq e hj' hk', Iso.inv_hom_id_assoc,
      ← cancel_mono (K.extendXIso e hk').inv, zero_comp, assoc]