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'
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
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 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
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 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
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 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
hij : c.Rel i j
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 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 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
hij : c.Rel i j
hi'' : e.f i = i'
⊢ Iso.hom (K.extendXIso e hi'') ≫ f' = f''
have apply : (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
Tactic: apply Fork.IsLimit.hom_ext hcone
-- 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
hij : c.Rel i j
hi'' : e.f i = i'
⊢ (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
have rw : Iso.hom (K.extendXIso e hi'') ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
Tactic: rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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
hij : c.Rel i j
hi'' : e.f i = i'
rw : Iso.hom (K.extendXIso e hi'') ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
⊢ (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
have rw₁ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j = f'' ≫ Fork.ι cone
Tactic: rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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
hij : c.Rel i j
hi'' : e.f i = i'
rw : Iso.hom (K.extendXIso e hi'') ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
rw₁ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j = f'' ≫ Fork.ι cone
⊢ (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
have rw₂ : Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
  ((Iso.hom (K.extendXIso e hi'') ≫ K.d i j) ≫ Iso.inv (K.extendXIso e hj'))
  ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
Tactic: rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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
hij : c.Rel i j
hi'' : e.f i = i'
rw : Iso.hom (K.extendXIso e hi'') ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
rw₁ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j = f'' ≫ Fork.ι cone
rw₂ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    ((Iso.hom (K.extendXIso e hi'') ≫ K.d i j) ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
⊢ (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
have rw₃ : Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j') (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
  ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
Tactic: rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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
hij : c.Rel i j
hi'' : e.f i = i'
rw : Iso.hom (K.extendXIso e hi'') ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
rw₁ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j = f'' ≫ Fork.ι cone
rw₂ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    ((Iso.hom (K.extendXIso e hi'') ≫ K.d i j) ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
rw₃ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
⊢ (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
have rw₄ : Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j') (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
  (f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj'))
Tactic: rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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
hij : c.Rel i j
hi'' : e.f i = i'
rw : Iso.hom (K.extendXIso e hi'') ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
rw₁ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j = f'' ≫ Fork.ι cone
rw₂ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    ((Iso.hom (K.extendXIso e hi'') ≫ K.d i j) ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
rw₃ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
rw₄ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
    (f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj'))
⊢ (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
have rw₅ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
Tactic: rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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
hij : c.Rel i j
hi'' : e.f i = i'
rw : Iso.hom (K.extendXIso e hi'') ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
rw₁ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j = f'' ≫ Fork.ι cone
rw₂ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    ((Iso.hom (K.extendXIso e hi'') ≫ K.d i j) ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
rw₃ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
rw₄ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
    (f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj'))
rw₅ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
⊢ (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
have rw₆ : Eq (α := (K.extend e).X i' ⟶ (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 hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
Tactic: rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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 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
hij : c.Rel i j
hi'' : e.f i = i'
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have this : Iso.hom (K.extendXIso e hi'') ≫ f' = f''
Tactic: have : (K.extendXIso e hi'').hom ≫ f' = f'' := by
      apply Fork.IsLimit.hom_ext hcone
      rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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
hij : c.Rel i j
hi'' : e.f i = i'
this : Iso.hom (K.extendXIso e hi'') ≫ f' = f''
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have pos : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) (Iso.hom (K.extendXIso e hi'') ≫ 0) ↔
  f'' ≫ φ = 0
Tactic: rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, 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'
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
hij : c.Rel i j
hi'' : e.f i = i'
this : Iso.hom (K.extendXIso e hi'') ≫ f' = f''
pos :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) (Iso.hom (K.extendXIso e hi'') ≫ 0) ↔
    f'' ≫ φ = 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have pos₁ : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔ f'' ≫ φ = 0
Tactic: rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, 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'
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
hij : c.Rel i j
hi'' : e.f i = i'
this : Iso.hom (K.extendXIso e hi'') ≫ f' = f''
pos :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) (Iso.hom (K.extendXIso e hi'') ≫ 0) ↔
    f'' ≫ φ = 0
pos₁ : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔ f'' ≫ φ = 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have pos₂ : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔
  Eq (α := (K.extend e).X i' ⟶ W) ((Iso.hom (K.extendXIso e hi'') ≫ f') ≫ φ) 0
Tactic: rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, 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'
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
hij : c.Rel i j
hi'' : e.f i = i'
this : Iso.hom (K.extendXIso e hi'') ≫ f' = f''
pos :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) (Iso.hom (K.extendXIso e hi'') ≫ 0) ↔
    f'' ≫ φ = 0
pos₁ : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔ f'' ≫ φ = 0
pos₂ :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W) ((Iso.hom (K.extendXIso e hi'') ≫ f') ≫ φ) 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have pos₃ : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0
Tactic: rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, 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'
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
hij : ¬c.Rel i j
⊢ f' = 0
have apply : f' ≫ Fork.ι cone = 0 ≫ Fork.ι cone
Tactic: apply Fork.IsLimit.hom_ext hcone
-- 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 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
hij : ¬c.Rel i j
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have h₁ : f' = 0
Tactic: have h₁ : f' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      simp only [zero_comp, hf', K.shape _ _ 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 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
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ f'' = 0
have apply : f'' ≫ Fork.ι cone = 0 ≫ Fork.ι cone
Tactic: apply Fork.IsLimit.hom_ext hcone
-- 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
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ f'' ≫ Fork.ι cone = 0 ≫ Fork.ι cone
have rw : ¬c.Rel (c.prev j) j
Tactic: rw [← cancel_mono (extendXIso K e hj').inv, assoc, hf'', zero_comp, zero_comp,
        K.extend_d_to_eq_zero e i' j' j hj']
-- 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 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
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
have h₂ : f'' = 0
Tactic: have h₂ : f'' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      dsimp
      rw [← cancel_mono (extendXIso K e hj').inv, assoc, hf'', zero_comp, zero_comp,
        K.extend_d_to_eq_zero e i' j' j hj']
      rw [hi]
      exact hij