awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ∃ (i : ι), e.f i = i'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have pos : ∀ (i : ι) (hi : e.f i = i'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: obtain ⟨i, hi⟩ := hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have pos : (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: rw [f_eq φ hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
⊢ (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have pos : ∀ (hj' : ∃ (j : ι), e.f j = j'),
  (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
pos :
  ∀ (hj' : ∃ (j : ι), e.f j = j'),
    (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
⊢ (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have neg : ∀ (hj' : ¬∃ (j : ι), e.f j = j'),
  (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj' : ∃ (j : ι), e.f j = j'
⊢ (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have pos : ∀ (j : ι) (hj : e.f j = j'),
  (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: obtain ⟨j, hj⟩ := hj'
Cleared hypotheses: hj'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi)) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have pos : Eq (α := K.X i' ⟶ (L.extend e).X j')
  (CategoryStruct.comp (Y := (L.extend e).X i') (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi))
    (Iso.hom (L.extendXIso e hi) ≫ L.d i j ≫ Iso.inv (L.extendXIso e hj)))
  (K.d i' j' ≫ Iso.inv (K.restrictionXIso e hj) ≫ φ.f j ≫ Iso.inv (L.extendXIso e hj))
Tactic: rw [f_eq φ hj, L.extend_d_eq e hi hj]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j')
    (CategoryStruct.comp (Y := (L.extend e).X i')
      (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi))
      (Iso.hom (L.extendXIso e hi) ≫ L.d i j ≫ Iso.inv (L.extendXIso e hj)))
    (K.d i' j' ≫ Iso.inv (K.restrictionXIso e hj) ≫ φ.f j ≫ Iso.inv (L.extendXIso e hj))
have pos : ∀ (hij' : c'.Rel (e.f i) (e.f j)),
  Eq (α := K.X (e.f i) ⟶ (L.extend e).X (e.f j))
    (CategoryStruct.comp (Y := (L.extend e).X (e.f i))
      (Iso.inv (K.restrictionXIso e sorry) ≫ φ.f i ≫ Iso.inv (L.extendXIso e sorry))
      (Iso.hom (L.extendXIso e sorry) ≫ L.d i j ≫ Iso.inv (L.extendXIso e sorry)))
    (K.d (e.f i) (e.f j) ≫ Iso.inv (K.restrictionXIso e sorry) ≫ φ.f j ≫ Iso.inv (L.extendXIso e sorry))
Tactic: subst hi hj
Cleared hypotheses: i', j', hij', hi, hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have this : (L.extend e).d i' j' = 0
Tactic: have : (L.extend e).d i' j' = 0 := by
        apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_src
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ (i : ι), e.f i = i'
this : (L.extend e).d i' j' = 0
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have neg : Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
Tactic: rw [this, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ (i : ι), e.f i = i'
this : (L.extend e).d i' j' = 0
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
have pos : ∀ (hj' : ∃ (j : ι), e.f j = j'), Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ (i : ι), e.f i = i'
this : (L.extend e).d i' j' = 0
pos : ∀ (hj' : ∃ (j : ι), e.f j = j'), Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
have neg : ∀ (hj' : ¬∃ (j : ι), e.f j = j'), Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ (i : ι), e.f i = i'
this : (L.extend e).d i' j' = 0
hj' : ∃ (j : ι), e.f j = j'
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
have pos : ∀ (j : ι) (hij' : c'.Rel i' (e.f j))
  (this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0),
  Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ f φ (e.f j))
Tactic: obtain ⟨j, rfl⟩ := hj'
Cleared hypotheses: j', hij', this, hj'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
⊢ Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ f φ (e.f j))
have pos : Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0
  (K.d i' (e.f j) ≫ Iso.inv (K.restrictionXIso e sorry) ≫ φ.f j ≫ Iso.inv (L.extendXIso e sorry))
Tactic: rw [f_eq φ rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
⊢ Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0
    (K.d i' (e.f j) ≫ Iso.inv (K.restrictionXIso e ⋯) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))
have pos : Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ 𝟙 (K.X (e.f j)) ≫ φ.f j ≫ Iso.inv (L.extendXIso e sorry))
Tactic: dsimp [restrictionXIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
⊢ Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ 𝟙 (K.X (e.f j)) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))
have pos : Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ φ.f j ≫ Iso.inv (L.extendXIso e sorry))
Tactic: rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij'
          (by simpa using hi')) i' hij'), zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
pos : Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))
⊢ Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ 𝟙 (K.X (e.f j)) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))
have pos₁ : Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (0 ≫ Iso.inv (L.extendXIso e sorry))
Tactic: rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij'
          (by simpa using hi')) i' hij'), zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
pos : Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))
pos₁ : Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (0 ≫ Iso.inv (L.extendXIso e ⋯))
⊢ Eq (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 (K.d i' (e.f j) ≫ 𝟙 (K.X (e.f j)) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))
have pos₂ : Eq.{v_1 + 1} (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 0
Tactic: rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij'
          (by simpa using hi')) i' hij'), zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ (i : ι), e.f i = i'
this : (L.extend e).d i' j' = 0
hj' : ¬∃ (j : ι), e.f j = j'
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
have this₁ : Eq (α := K.X j' ⟶ (L.extend e).X j') (f φ j') 0
Tactic: have : f φ j' = 0 := by
          apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ (i : ι), e.f i = i'
this_1 : (L.extend e).d i' j' = 0
hj' : ¬∃ (j : ι), e.f j = j'
this : Eq (α := K.X j' ⟶ (L.extend e).X j') (f φ j') 0
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
have neg : Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ 0)
Tactic: rw [this, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ (i : ι), e.f i = i'
this_1 : (L.extend e).d i' j' = 0
hj' : ¬∃ (j : ι), e.f j = j'
this : Eq (α := K.X j' ⟶ (L.extend e).X j') (f φ j') 0
neg : Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ 0)
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
have neg₁ : Eq.{v_1 + 1} (α := K.X i' ⟶ (L.extend e).X j') 0 0
Tactic: rw [this, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i : ι
i' : ι'
h : e.f i = i'
⊢ Eq (α := (K.restriction e).X i ⟶ L.X i) (f ψ i)
    (Iso.hom (K.restrictionXIso e h) ≫ ψ.f i' ≫ Iso.hom (L.extendXIso e h))
have subst : Eq (α := (K.restriction e).X i ⟶ L.X i) (f ψ i)
  (Iso.hom (K.restrictionXIso e sorry) ≫ ψ.f (e.f i) ≫ Iso.hom (L.extendXIso e sorry))
Tactic: subst h
Cleared hypotheses: i', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i j : ι
⊢ Eq (α := (K.restriction e).X i ⟶ L.X j) (f ψ i ≫ L.d i j) (K.d (e.f i) (e.f j) ≫ f ψ j)
have dsimp : (ψ.f (e.f i) ≫ Iso.hom (L.extendXIso e sorry)) ≫ L.d i j = K.d (e.f i) (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e sorry)
Tactic: dsimp [f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
⊢ K.d i' (e.f j) ≫ Hom.f (e.homRestrict ψ) j = 0
have this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
Tactic: have : (L.extend e).d i' (e.f j) = 0 := by
    apply (L.isZero_extend_X e i' (hj.notMem hij')).eq_of_src
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
⊢ K.d i' (e.f j) ≫ Hom.f (e.homRestrict ψ) j = 0
have dsimp : K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
Tactic: dsimp [homRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e sorry) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e sorry)) 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
rw :
  Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯))
    0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw₁ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (eqToIso sorry) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e sorry)) 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
rw :
  Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯))
    0
rw₁ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (eqToIso ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw₂ : K.d i' (e.f j) ≫ Iso.hom (Iso.refl ((K.restriction e).X j)) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e sorry) = 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.HomEquiv (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0
rw :
  Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯))
    0
rw₁ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ Iso.hom (eqToIso ⋯) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₂ : K.d i' (e.f j) ≫ Iso.hom (Iso.refl ((K.restriction e).X j)) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
have rw₃ : K.d i' (e.f j) ≫ 𝟙 ((K.restriction e).X j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e sorry) = 0
Tactic: rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]