awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
⊢ Eq (α := opcycles h.cochainComplex m ⟶ opcycles h'.cochainComplex m) (opcyclesMap (h.map h' fK fL f_comm) m)
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
      (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
      (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
        (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
          (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
            (opcyclesMap h'.restrictionLEIso.inv n)
            (Iso.hom
              (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))))))
have e_a : Eq (α := h.cochainComplex.X m ⟶ opcycles h'.cochainComplex m)
  (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
    (opcyclesMap (h.map h' fK fL f_comm) m))
  (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
      (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n sorry sorry sorry sorry))
      (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
        (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
          (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
            (opcyclesMap h'.restrictionLEIso.inv n)
            (Iso.hom
              (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n sorry sorry sorry sorry)))))))
Tactic: rw [← cancel_epi (HomologicalComplex.pOpcycles ..)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
⊢ Eq (α := h.cochainComplex.X m ⟶ opcycles h'.cochainComplex m)
    (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
      (opcyclesMap (h.map h' fK fL f_comm) m))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
      (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
        (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
          (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
              (opcyclesMap h'.restrictionLEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯)))))))
have e_a : ∀ [inst_7 : HasHomology h.cochainComplex (Int.negSucc n)] [inst_8 : HasHomology h'.cochainComplex (Int.negSucc n)],
  Eq (α := h.cochainComplex.X (Int.negSucc n) ⟶ opcycles h'.cochainComplex (Int.negSucc n))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex (Int.negSucc n)) (pOpcycles h.cochainComplex (Int.negSucc n))
      (opcyclesMap (h.map h' fK fL f_comm) (Int.negSucc n)))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex (Int.negSucc n)) (pOpcycles h.cochainComplex (Int.negSucc n))
      (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n sorry sorry sorry sorry))
        (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
          (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
              (opcyclesMap h'.restrictionLEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n sorry sorry sorry sorry)))))))
Tactic: obtain rfl : m = .negSucc n := hmn
Cleared hypotheses: m, hmn, inst_3, inst_5
-- 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 M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i : Option ι
j : ι
hj : i = some j
⊢ X K i = K.X j
have subst : X K (some j) = K.X j
Tactic: subst hj
Cleared hypotheses: i, hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i : Option ι
hi : i = none
⊢ IsZero.{v_1, u_3} (X K i)
have subst : IsZero.{v_1, u_3} (X K none)
Tactic: subst hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i j : Option ι
hi : i = none
⊢ Eq (α := X K i ⟶ X K j) (d K i j) 0
have subst : Eq (α := X K none ⟶ X K j) (d K none j) 0
Tactic: subst hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i j : Option ι
hj : j = none
⊢ Eq (α := X K i ⟶ X K j) (d K i j) 0
have subst : Eq (α := X K i ⟶ X K none) (d K i none) 0
Tactic: subst hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i : Option ι
⊢ Eq (α := X K i ⟶ X K none) (d K i none) 0
have none : Eq (α := X K none ⟶ X K none) (d K none none) 0
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i : Option ι
none : Eq (α := X K Option.none ⟶ X K Option.none) (d K Option.none Option.none) 0
⊢ Eq (α := X K i ⟶ X K Option.none) (d K i Option.none) 0
have some : ∀ (val : ι), Eq (α := X K (some val) ⟶ X K Option.none) (d K (some val) Option.none) 0
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i j : Option ι
a b : ι
hi : i = some a
hj : j = some b
⊢ Eq (α := X K i ⟶ X K j) (d K i j) (Iso.hom (XIso K hi) ≫ K.d a b ≫ Iso.inv (XIso K hj))
have subst : Eq (α := X K (some a) ⟶ X K (some b)) (d K (some a) (some b)) (Iso.hom (XIso K sorry) ≫ K.d a b ≫ Iso.inv (XIso K sorry))
Tactic: subst hi hj
Cleared hypotheses: i, j, hi, hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i_1 j_1 : Option ι
i j : ι
⊢ Eq (α := X K.op (some i) ⟶ Opposite.op (X K (some j)))
    (Iso.hom (XOpIso K (some i)) ≫ Quiver.Hom.op (d K (some j) (some i)))
    (d K.op (some i) (some j) ≫ Iso.hom (XOpIso K (some j)))
have dsimp : 𝟙 (X K.op (some i)) ≫ Quiver.Hom.op (d K (some j) (some i)) = d K.op (some i) (some j) ≫ 𝟙 (X K.op (some j))
Tactic: dsimp [XOpIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i_1 j_1 : Option ι
i j : ι
⊢ 𝟙 (X K.op (some i)) ≫ Quiver.Hom.op (d K (some j) (some i)) = d K.op (some i) (some j) ≫ 𝟙 (X K.op (some j))
have simp : Eq (α := X K.op (some i) ⟶ Opposite.op (X K (some j)))
  (Quiver.Hom.op (Iso.inv (XIso K sorry)) ≫ (K.d j i).op ≫ Quiver.Hom.op (Iso.hom (XIso K sorry)) :
    Opposite.op (X K (some i)) ⟶ Opposite.op (X K (some j)))
  (Iso.hom (XIso K.op sorry) ≫ K.op.d i j ≫ Iso.inv (XIso K.op sorry) : X K.op (some i) ⟶ X K.op (some j))
Tactic: simp only [d_eq _ rfl rfl, op_comp, assoc, id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
i : Option ι
a : ι
hi : i = some a
⊢ Eq (α := X K i ⟶ X L i) (mapX φ i) (Iso.hom (XIso K hi) ≫ φ.f a ≫ Iso.inv (XIso L hi))
have subst : Eq (α := X K (some a) ⟶ X L (some a)) (mapX φ (some a)) (Iso.hom (XIso K sorry) ≫ φ.f a ≫ Iso.inv (XIso L sorry))
Tactic: subst hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
a : ι
⊢ Eq (α := X K (some a) ⟶ X L (some a)) (mapX φ (some a)) (Iso.hom (XIso K ⋯) ≫ φ.f a ≫ Iso.inv (XIso L ⋯))
have dsimp : mapX φ (some a) = 𝟙 (K.X a) ≫ φ.f a ≫ 𝟙 (L.X a)
Tactic: dsimp [XIso, X]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = 𝟙 (K.X a) ≫ φ.f a ≫ 𝟙 (L.X a)
have rw : mapX φ (some a) = φ.f a
Tactic: rw [id_comp, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
i : Option ι
hi : i = none
⊢ Eq (α := X K i ⟶ X L i) (mapX φ i) 0
have subst : Eq (α := X K none ⟶ X L none) (mapX φ none) 0
Tactic: subst 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 ι'
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 M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
have inl : ∀ (hi' : e.r i' = none), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
Tactic: obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
-- 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 M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
inl : ∀ (hi' : e.r i' = none), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
have inr : ∀ (i : ι) (hi : e.r i' = some i), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
Tactic: obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
-- 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 M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
hi' : e.r i' = none
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
have inl : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) 0 0
Tactic: rw [extend.d_none_eq_zero K _ _ 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
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
have inr : ∀ (hj' : e.r j' = none), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
Tactic: obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some
-- 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 M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
inr : ∀ (hj' : e.r j' = none), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
have inr₁ : ∀ (j : ι) (hj : e.r j' = some j), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
Tactic: obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some
-- 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 M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
have inr : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) 0 0
Tactic: rw [extend.d_none_eq_zero' K _ _ 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
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
have inr : ¬c.Rel i j
Tactic: rw [extend.d_eq K hi hj, K.shape, zero_comp, comp_zero]
-- 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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ ¬c.Rel i j
have h₁ : ¬c'.Rel (e.f i) j'
Tactic: obtain rfl := e.f_eq_of_r_eq_some hi
Cleared hypotheses: i', h, 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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
h₁ : ¬c'.Rel (e.f i) j'
⊢ ¬c.Rel i j
have hi₁ : e.r (e.f i) = some i
Tactic: obtain rfl := e.f_eq_of_r_eq_some hi
Cleared hypotheses: i', h, 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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
j' : ι'
i j : ι
hj : e.r j' = some j
h : ¬c'.Rel (e.f i) j'
hi : e.r (e.f i) = some i
⊢ ¬c.Rel i j
have hj₁ : e.r (e.f j) = some j
Tactic: obtain rfl := e.f_eq_of_r_eq_some hj
Cleared hypotheses: j', hj, h
-- 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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
j' : ι'
i j : ι
hj : e.r j' = some j
h : ¬c'.Rel (e.f i) j'
hi : e.r (e.f i) = some i
hj₁ : e.r (e.f j) = some j
⊢ ¬c.Rel i j
have h₁ : ¬c'.Rel (e.f i) (e.f j)
Tactic: obtain rfl := e.f_eq_of_r_eq_some hj
Cleared hypotheses: j', hj, 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
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
have inl : ∀ (hi' : e.r i' = none),
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
Tactic: obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
-- 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 M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
inl :
  ∀ (hi' : e.r i' = none),
    Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
      (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
have inr : ∀ (i : ι) (hi : e.r i' = some i),
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
Tactic: obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
-- 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 M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
hi' : e.r i' = none
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
have inl : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
  (CategoryStruct.comp (Y := extend.X K (e.r j')) 0 (extend.d K (e.r j') (e.r k'))) 0
Tactic: rw [extend.d_none_eq_zero K _ _ hi', zero_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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
hi' : e.r i' = none
inl :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) 0 (extend.d K (e.r j') (e.r k'))) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
have inl₁ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) 0 0
Tactic: rw [extend.d_none_eq_zero K _ _ hi', zero_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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
i : ι
hi : e.r i' = some i
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
have inr : ∀ (hj' : e.r j' = none),
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
Tactic: obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some