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 : 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
i : ι
hi : e.r i' = some i
⊢ (K.extend e).d i' j' = 0
have inr : ¬c.Rel i j
Tactic: rw [extend_d_eq K e (e.f_eq_of_r_eq_some 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 : 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
i : ι
hi : e.r i' = some i
hij : c.Rel i j
⊢ False
have hi₁ : e.r i' = some (c.prev j)
Tactic: obtain rfl := c.prev_eq' hij
Cleared hypotheses: i, hi, 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' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
hij : c.Rel i j
hi₁ : e.r i' = some (c.prev j)
⊢ False
have hij₁ : c.Rel (c.prev j) j
Tactic: obtain rfl := c.prev_eq' hij
Cleared hypotheses: i, hi, 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 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'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have pos : ∀ (hi : ∃ (i : ι), e.f i = i'),
  extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Tactic: by_cases hi : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
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'
pos :
  ∀ (hi : ∃ (i : ι), e.f i = i'),
    extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have neg : ∀ (hi : ¬∃ (i : ι), e.f i = i'),
  extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Tactic: by_cases hi : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
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 : ∃ (i : ι), e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have pos : ∀ (i : ι) (hi : e.f i = i'),
  extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Tactic: obtain ⟨i, hi⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
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.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have pos : ∀ (hj : ∃ (j : ι), e.f j = j'),
  extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Tactic: by_cases hj : ∃ j, e.f j = j'
-- 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.f i = i'
pos :
  ∀ (hj : ∃ (j : ι), e.f j = j'),
    extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have neg : ∀ (hj : ¬∃ (j : ι), e.f j = j'),
  extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Tactic: by_cases hj : ∃ j, e.f j = j'
-- 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.f i = i'
hj : ∃ (j : ι), e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have pos : ∀ (j : ι) (hj : e.f j = j'),
  extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Tactic: obtain ⟨j, hj⟩ := hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
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.f i = i'
j : ι
hj : e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have pos : Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j')
  (CategoryStruct.comp (Y := (L.extend e).X i') (Iso.hom (extend.XIso K sorry) ≫ φ.f i ≫ Iso.inv (extend.XIso L sorry))
    (Iso.hom (L.extendXIso e hi) ≫ L.d i j ≫ Iso.inv (L.extendXIso e hj)))
  (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 (extend.XIso K sorry) ≫ φ.f j ≫ Iso.inv (extend.XIso L sorry)))
Tactic: rw [K.extend_d_eq e hi hj, L.extend_d_eq e hi hj,
          extend.mapX_some φ (e.r_eq_some hi),
          extend.mapX_some φ (e.r_eq_some hj)]
-- 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.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have hj' : e.r j' = none
Tactic: have hj' := e.r_eq_none j' (fun j'' hj'' => hj ⟨j'', hj''⟩)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
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.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
hj' : e.r j' = none
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have neg : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
  (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
Tactic: dsimp [extend]
-- 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.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
hj' : e.r j' = none
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
have neg : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
  (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
Tactic: rw [extend.d_none_eq_zero' _ _ _ hj', extend.d_none_eq_zero' _ _ _ hj',
          comp_zero, 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' : ι'
h : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
hj' : e.r j' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
have neg₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0) (0 ≫ extend.mapX φ (e.r j'))
Tactic: rw [extend.d_none_eq_zero' _ _ _ hj', extend.d_none_eq_zero' _ _ _ hj',
          comp_zero, 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' : ι'
h : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
hj' : e.r j' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
neg₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0) (0 ≫ extend.mapX φ (e.r j'))
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
have neg₂ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 (0 ≫ extend.mapX φ (e.r j'))
Tactic: rw [extend.d_none_eq_zero' _ _ _ hj', extend.d_none_eq_zero' _ _ _ hj',
          comp_zero, 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' : ι'
h : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
hj' : e.r j' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
neg₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0) (0 ≫ extend.mapX φ (e.r j'))
neg₂ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 (0 ≫ extend.mapX φ (e.r j'))
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
have neg₃ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 0
Tactic: rw [extend.d_none_eq_zero' _ _ _ hj', extend.d_none_eq_zero' _ _ _ hj',
          comp_zero, zero_comp]
-- 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'
hi : ¬∃ (i : ι), e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have hi' : e.r i' = none
Tactic: have hi' := e.r_eq_none i' (fun i'' hi'' => hi ⟨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'
hi : ¬∃ (i : ι), e.f i = i'
hi' : e.r i' = none
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
have neg : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
  (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
Tactic: dsimp [extend]
-- 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 : ¬∃ (i : ι), e.f i = i'
hi' : e.r i' = none
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
have neg : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
  (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
Tactic: rw [extend.d_none_eq_zero _ _ _ hi', extend.d_none_eq_zero _ _ _ hi',
        comp_zero, 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' : ι'
h : c'.Rel i' j'
hi : ¬∃ (i : ι), e.f i = i'
hi' : e.r i' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
have neg₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0) (0 ≫ extend.mapX φ (e.r j'))
Tactic: rw [extend.d_none_eq_zero _ _ _ hi', extend.d_none_eq_zero _ _ _ hi',
        comp_zero, 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' : ι'
h : c'.Rel i' j'
hi : ¬∃ (i : ι), e.f i = i'
hi' : e.r i' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
neg₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0) (0 ≫ extend.mapX φ (e.r j'))
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
have neg₂ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 (0 ≫ extend.mapX φ (e.r j'))
Tactic: rw [extend.d_none_eq_zero _ _ _ hi', extend.d_none_eq_zero _ _ _ hi',
        comp_zero, 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' : ι'
h : c'.Rel i' j'
hi : ¬∃ (i : ι), e.f i = i'
hi' : e.r i' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
neg₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0) (0 ≫ extend.mapX φ (e.r j'))
neg₂ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 (0 ≫ extend.mapX φ (e.r j'))
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
have neg₃ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 0
Tactic: rw [extend.d_none_eq_zero _ _ _ hi', extend.d_none_eq_zero _ _ _ hi',
        comp_zero, 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 : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X i') (extend.mapX φ (e.r i'))
    (Iso.hom (K.extendXIso e h) ≫ φ.f i ≫ Iso.inv (L.extendXIso e h))
have rw : Eq (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Iso.hom (extend.XIso K sorry) ≫ φ.f i ≫ Iso.inv (extend.XIso L sorry))
  (Iso.hom (K.extendXIso e h) ≫ φ.f i ≫ Iso.inv (L.extendXIso e h))
Tactic: rw [extend.mapX_some φ (e.r_eq_some 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 : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X i') (extend.mapX φ (e.r i')) 0
have rw : Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') 0 0
Tactic: rw [extend.mapX_none φ (e.r_eq_none 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'
⊢ Eq (α := K.extend e ⟶ M.extend e) (extendMap (φ ≫ φ') e) (extendMap φ e ≫ extendMap φ' e)
have h : ∀ (i' : ι'),
  Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
Tactic: ext i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
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' : ι'
⊢ Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'),
  Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
pos :
  ∀ (hi' : ∃ (i : ι), e.f i = i'),
    Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
      (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
⊢ Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'),
  Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
have pos : ∀ (i : ι) (hi : e.f i = i'),
  Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
Tactic: obtain ⟨i, hi⟩ := hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
⊢ Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
⊢ Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
have pos : ∀ (i : ι) (hi : e.f i = i'), Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
Tactic: obtain ⟨i, hi⟩ := hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Extend (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
⊢ extendMap (𝟙 K) e = 𝟙 (K.extend e)
have h : ∀ (i : ι'), Hom.f (extendMap (𝟙 K) e) i = Hom.f (𝟙 (K.extend e)) i
Tactic: ext