awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
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
⊢ φ ≫ 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') (φ ≫ 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]
-- 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'
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
pos₁ : φ ≫ K.d j k = 0 ↔ Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have pos₂ : Eq (α := W ⟶ (K.extend e).X k') ((φ ≫ K.d j k) ≫ Iso.inv (K.extendXIso e hk')) (0 ≫ Iso.inv (K.extendXIso e hk')) ↔
  Eq (α := W ⟶ (K.extend e).X k') (φ ≫ 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]
-- 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'
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
pos₁ : φ ≫ K.d j k = 0 ↔ Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
pos₂ :
  Eq (α := W ⟶ (K.extend e).X k') ((φ ≫ K.d j k) ≫ Iso.inv (K.extendXIso e hk')) (0 ≫ Iso.inv (K.extendXIso e hk')) ↔
    Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have pos₃ : Eq (α := W ⟶ (K.extend e).X k') ((φ ≫ K.d j k) ≫ Iso.inv (K.extendXIso e hk')) 0 ↔
  Eq (α := W ⟶ (K.extend e).X k') (φ ≫ 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]
-- 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'
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
pos₁ : φ ≫ K.d j k = 0 ↔ Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
pos₂ :
  Eq (α := W ⟶ (K.extend e).X k') ((φ ≫ K.d j k) ≫ Iso.inv (K.extendXIso e hk')) (0 ≫ Iso.inv (K.extendXIso e hk')) ↔
    Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
pos₃ :
  Eq (α := W ⟶ (K.extend e).X k') ((φ ≫ K.d j k) ≫ Iso.inv (K.extendXIso e hk')) 0 ↔
    Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have pos₄ : Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0 ↔
  Eq (α := W ⟶ (K.extend e).X k') (φ ≫ 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]
-- 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
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have neg : φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
Tactic: simp only [K.shape _ _ hjk, comp_zero, true_iff]
-- 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
⊢ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
have neg : ¬c.Rel j (c.next j)
Tactic: rw [K.extend_d_from_eq_zero e j' k' j hj', comp_zero, comp_zero]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have pos : ∀ (hij : c.Rel i j), K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
Tactic: by_cases hij : c.Rel i j
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
pos : ∀ (hij : c.Rel i j), K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have neg : ∀ (hij : ¬c.Rel i j), K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
Tactic: by_cases hij : c.Rel i j
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
⊢ e.f i = i'
have rw : e.f i = c'.prev j'
Tactic: rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
rw : e.f i = c'.prev j'
⊢ e.f i = i'
have rw₁ : e.f i = c'.prev (e.f j)
Tactic: rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
rw : e.f i = c'.prev j'
rw₁ : e.f i = c'.prev (e.f j)
⊢ e.f i = i'
have rw₂ : e.f i = e.f i
Tactic: rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have hi'₁ : e.f i = i'
Tactic: have hi' : e.f i = i' := by rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'_1 : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have pos : K.d i j ≫ φ = 0 ↔
  Eq (α := (K.extend e).X i' ⟶ W)
    (CategoryStruct.comp (Y := (K.extend e).X j')
      (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj') ≫ φ))
    0
Tactic: rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
      ← cancel_epi (K.extendXIso e hi').hom, comp_zero]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'_1 : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
pos :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (CategoryStruct.comp (Y := (K.extend e).X j')
        (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have pos₁ : K.d i j ≫ φ = 0 ↔
  Eq (α := (K.extend e).X i' ⟶ W)
    (Iso.hom (K.extendXIso e hi') ≫
      CategoryStruct.comp (Y := (K.extend e).X j') (K.d i j ≫ Iso.inv (K.extendXIso e hj'))
        (Iso.hom (K.extendXIso e hj') ≫ φ))
    0
Tactic: rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
      ← cancel_epi (K.extendXIso e hi').hom, comp_zero]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'_1 : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
pos :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (CategoryStruct.comp (Y := (K.extend e).X j')
        (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₁ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (K.d i j ≫ Iso.inv (K.extendXIso e hj'))
          (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have pos₂ : K.d i j ≫ φ = 0 ↔
  Eq (α := (K.extend e).X i' ⟶ W)
    (Iso.hom (K.extendXIso e hi') ≫
      K.d i j ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj') ≫ φ))
    0
Tactic: rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
      ← cancel_epi (K.extendXIso e hi').hom, comp_zero]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'_1 : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
pos :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (CategoryStruct.comp (Y := (K.extend e).X j')
        (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₁ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (K.d i j ≫ Iso.inv (K.extendXIso e hj'))
          (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₂ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        K.d i j ≫
          CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
            (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have pos₃ : K.d i j ≫ φ = 0 ↔ Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
Tactic: rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
      ← cancel_epi (K.extendXIso e hi').hom, comp_zero]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'_1 : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
pos :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (CategoryStruct.comp (Y := (K.extend e).X j')
        (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₁ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (K.d i j ≫ Iso.inv (K.extendXIso e hj'))
          (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₂ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        K.d i j ≫
          CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
            (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₃ : K.d i j ≫ φ = 0 ↔ Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have pos₄ : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) (Iso.hom (K.extendXIso e hi') ≫ 0) ↔
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
Tactic: rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
      ← cancel_epi (K.extendXIso e hi').hom, comp_zero]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'_1 : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
pos :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (CategoryStruct.comp (Y := (K.extend e).X j')
        (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₁ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (K.d i j ≫ Iso.inv (K.extendXIso e hj'))
          (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₂ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        K.d i j ≫
          CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
            (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₃ : K.d i j ≫ φ = 0 ↔ Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
pos₄ :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) (Iso.hom (K.extendXIso e hi') ≫ 0) ↔
    Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have pos₅ : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0 ↔
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
Tactic: rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
      ← cancel_epi (K.extendXIso e hi').hom, comp_zero]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have neg : (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
Tactic: simp only [K.shape _ _ hij, zero_comp, true_iff]
-- 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
have neg : ¬c.Rel (c.prev j) j
Tactic: rw [K.extend_d_to_eq_zero e i' j' j hj', zero_comp]
-- 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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
⊢ (Fork.ι cone ≫ Iso.inv (K.extendXIso e hj')) ≫ (K.extend e).d j' k' = 0
have rw : Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
Tactic: rw [assoc, ← comp_d_eq_zero_iff K e hj' hk hk' cone.ι, cone.condition]
-- 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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
rw : Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
⊢ (Fork.ι cone ≫ Iso.inv (K.extendXIso e hj')) ≫ (K.extend e).d j' k' = 0
have rw₁ : Fork.ι cone ≫ K.d j k = 0
Tactic: rw [assoc, ← comp_d_eq_zero_iff K e hj' hk hk' cone.ι, cone.condition]
-- 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 L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
rw : Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
rw₁ : Fork.ι cone ≫ K.d j k = 0
⊢ (Fork.ι cone ≫ Iso.inv (K.extendXIso e hj')) ≫ (K.extend e).d j' k' = 0
have rw₂ : Eq.{v_1 + 1} (α := cone.pt ⟶ K.X k) 0 0
Tactic: rw [assoc, ← comp_d_eq_zero_iff K e hj' hk hk' cone.ι, cone.condition]
-- 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'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have pos : ∀ (hij : c.Rel i j), f' ≫ φ = 0 ↔ f'' ≫ φ = 0
Tactic: by_cases hij : c.Rel i j
-- 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'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
pos : ∀ (hij : c.Rel i j), f' ≫ φ = 0 ↔ f'' ≫ φ = 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have neg : ∀ (hij : ¬c.Rel i j), f' ≫ φ = 0 ↔ f'' ≫ φ = 0
Tactic: by_cases hij : c.Rel i j