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 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
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
⊢ 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₁ : ∀ (j : ι) (hj : e.r j' = some j),
  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
-- 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
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
have inr : 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')) 0) 0
Tactic: rw [extend.d_none_eq_zero K _ _ hj', comp_zero]
-- 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
hj' : e.r j' = none
inr :
  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')) 0) 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₁ : 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 _ _ hj', comp_zero]
-- 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
j : ι
hj : e.r j' = some j
⊢ 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 : ∀ (hk' : e.r k' = 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 hk' | ⟨k, hk⟩ := (e.r k').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'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
inr :
  ∀ (hk' : e.r k' = 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₁ : ∀ (k : ι) (hk : e.r k' = some 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
Tactic: obtain hk' | ⟨k, hk⟩ := (e.r k').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'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
hk' : e.r k' = 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 inr : 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')) 0) 0
Tactic: rw [extend.d_none_eq_zero' K _ _ hk', comp_zero]
-- 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
j : ι
hj : e.r j' = some j
hk' : e.r k' = none
inr :
  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')) 0) 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₁ : 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 _ _ hk', comp_zero]
-- 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
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some 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 inr : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
  ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ extend.d K (e.r j') (e.r k')) 0
Tactic: rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]
-- 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
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ 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₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
  (CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj))
    (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
  0
Tactic: rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]
-- 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
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ extend.d K (e.r j') (e.r k')) 0
inr₁ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj))
      (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    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₂ : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
  (Iso.hom (extend.XIso K hi) ≫
    CategoryStruct.comp (Y := extend.X K (e.r j')) (K.d i j ≫ Iso.inv (extend.XIso K hj))
      (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
  0
Tactic: rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]
-- 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
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ extend.d K (e.r j') (e.r k')) 0
inr₁ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj))
      (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₂ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      CategoryStruct.comp (Y := extend.X K (e.r j')) (K.d i j ≫ Iso.inv (extend.XIso K hj))
        (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    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₃ : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
  (Iso.hom (extend.XIso K hi) ≫
    K.d i j ≫
      CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.inv (extend.XIso K hj))
        (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
  0
Tactic: rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]
-- 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
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ extend.d K (e.r j') (e.r k')) 0
inr₁ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj))
      (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₂ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      CategoryStruct.comp (Y := extend.X K (e.r j')) (K.d i j ≫ Iso.inv (extend.XIso K hj))
        (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₃ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      K.d i j ≫
        CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.inv (extend.XIso K hj))
          (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    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₄ : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
  (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)) 0
Tactic: rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]
-- 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
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ extend.d K (e.r j') (e.r k')) 0
inr₁ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj))
      (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₂ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      CategoryStruct.comp (Y := extend.X K (e.r j')) (K.d i j ≫ Iso.inv (extend.XIso K hj))
        (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₃ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      K.d i j ≫
        CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.inv (extend.XIso K hj))
          (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₄ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)) 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₅ : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) (Iso.hom (extend.XIso K hi) ≫ 0 ≫ Iso.inv (extend.XIso K hk)) 0
Tactic: rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]
-- 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
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ extend.d K (e.r j') (e.r k')) 0
inr₁ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj))
      (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₂ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      CategoryStruct.comp (Y := extend.X K (e.r j')) (K.d i j ≫ Iso.inv (extend.XIso K hj))
        (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₃ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      K.d i j ≫
        CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.inv (extend.XIso K hj))
          (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₄ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)) 0
inr₅ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) (Iso.hom (extend.XIso K hi) ≫ 0 ≫ Iso.inv (extend.XIso K hk)) 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₆ : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) (Iso.hom (extend.XIso K hi) ≫ 0) 0
Tactic: rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]
-- 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
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ extend.d K (e.r j') (e.r k')) 0
inr₁ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj))
      (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₂ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      CategoryStruct.comp (Y := extend.X K (e.r j')) (K.d i j ≫ Iso.inv (extend.XIso K hj))
        (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₃ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      K.d i j ≫
        CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.inv (extend.XIso K hj))
          (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₄ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)) 0
inr₅ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) (Iso.hom (extend.XIso K hi) ≫ 0 ≫ Iso.inv (extend.XIso K hk)) 0
inr₆ : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) (Iso.hom (extend.XIso K hi) ≫ 0) 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₇ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) 0 0
Tactic: rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]
-- 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' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
⊢ (K.extend e).d i' j' = 0
have inl : ∀ (hj' : e.r j' = none), (K.extend e).d i' 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
inl : ∀ (hj' : e.r j' = none), (K.extend e).d i' j' = 0
⊢ (K.extend e).d i' j' = 0
have inr : ∀ (j : ι) (hj : e.r j' = some j), (K.extend e).d i' 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ (K.extend e).d i' j' = 0
have inr : ¬c.Rel i j
Tactic: rw [extend_d_eq K e hi (e.f_eq_of_r_eq_some 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
hij : c.Rel i j
⊢ False
have hj₁ : e.r j' = some (c.next i)
Tactic: obtain rfl := c.next_eq' hij
Cleared hypotheses: j, hj, hij
-- 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' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
hij : c.Rel i j
hj₁ : e.r j' = some (c.next i)
⊢ False
have hij₁ : c.Rel i (c.next i)
Tactic: obtain rfl := c.next_eq' hij
Cleared hypotheses: j, hj, hij
-- 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' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
⊢ (K.extend e).d i' j' = 0
have inl : ∀ (hi' : e.r i' = none), (K.extend e).d i' 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
inl : ∀ (hi' : e.r i' = none), (K.extend e).d i' j' = 0
⊢ (K.extend e).d i' j' = 0
have inr : ∀ (i : ι) (hi : e.r i' = some i), (K.extend e).d i' j' = 0
Tactic: obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some