awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
simpa using hj'
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'

Tactic:
apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi'
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'
⊢ (L.extend e).d i' j' = 0

Tactic:
apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_src

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'
⊢ (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
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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
neg : Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
rw [this, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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')
neg : ∀ (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')

Tactic:
by_cases hj' : ∃ j, e.f j = j'
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'
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))
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')

Tactic:
obtain ⟨j, rfl⟩ := hj'

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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) ≫ Iso.inv (K.restrictionXIso e ⋯) ≫ φ.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) ≫ f φ (e.f j))

Tactic:
rw [f_eq φ rfl]

Premises used: ComplexShape.Embedding.liftExtend.f_eq, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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) ≫ 𝟙 (K.X (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) ≫ Iso.inv (K.restrictionXIso e ⋯) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))

Tactic:
dsimp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi'
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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 ⋯))
pos₂ pos₃ : Eq.{v_1 + 1} (α := K.X i' ⟶ (L.extend e).X (e.f j)) 0 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 ⋯))

Tactic:
rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij'
          (by simpa using hi')) i' hij'), zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, ComplexShape.Embedding.boundaryGE, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
simpa using hj'
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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 j' ⟶ (L.extend e).X j') (f φ j') 0

Tactic:
apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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 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
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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)
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.X i' ⟶ (L.extend e).X j') 0 0
⊢ Eq (α := K.X i' ⟶ (L.extend e).X j') 0 (K.d i' j' ≫ f φ j')

Tactic:
rw [this, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
simp [HomologicalComplex.shape _ _ _ hij']

Premises used: HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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' : ι'
i : ι
hi : e.f i = i'
⊢ Eq (α := K.X i' ⟶ (L.extend e).X i') (Hom.f (e.liftExtend φ hφ) i')
    (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi))

Tactic:
apply liftExtend.f_eq

Premises used: ComplexShape.Embedding.liftExtend.f_eq
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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 K' : HomologicalComplex.{v_1, u_3, u_2} C c'
L L' : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
i : ι
hi : e.f i = i'
⊢ Iso.hom (Iso.symm (K.restrictionXIso e hi)) ≫ (Arrow.mk (φ.f i)).hom =
    (Arrow.mk (Y := (L.extend e).X i') (Hom.f (e.liftExtend φ hφ) i')).hom ≫ Iso.hom (L.extendXIso e hi)

Tactic:
simp [e.liftExtend_f φ hφ hi]

Premises used: ComplexShape.Embedding.liftExtend_f
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso (Y := (L.extend e).X i') (Hom.f (e.liftExtend φ hφ) i') ↔ IsIso (φ.f i)

Tactic:
(MorphismProperty.isomorphisms C).arrow_mk_iso_iff (e.liftExtendfArrowIso φ hφ hi)

Premises used: CategoryTheory.MorphismProperty.isomorphisms, ComplexShape.Embedding.liftExtendfArrowIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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' : ι'
i : ι
hi : e.f i = i'
⊢ Mono (Y := (L.extend e).X i') (Hom.f (e.liftExtend φ hφ) i') ↔ Mono (φ.f i)

Tactic:
(MorphismProperty.monomorphisms C).arrow_mk_iso_iff (e.liftExtendfArrowIso φ hφ hi)

Premises used: CategoryTheory.MorphismProperty.monomorphisms, ComplexShape.Embedding.liftExtendfArrowIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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' : ι'
i : ι
hi : e.f i = i'
⊢ Epi (Y := (L.extend e).X i') (Hom.f (e.liftExtend φ hφ) i') ↔ Epi (φ.f i)

Tactic:
(MorphismProperty.epimorphisms C).arrow_mk_iso_iff (e.liftExtendfArrowIso φ hφ hi)

Premises used: ComplexShape.Embedding.liftExtendfArrowIso, CategoryTheory.MorphismProperty.epimorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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'
subst :
  Eq (α := (K.restriction e).X i ⟶ L.X i) (f ψ i)
    (Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯))
⊢ 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))

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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 : ι
⊢ Eq (α := (K.restriction e).X i ⟶ L.X i) (f ψ i)
    (Iso.hom (K.restrictionXIso e ⋯) ≫ ψ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯))

Tactic:
simp [f, restrictionXIso]

Premises used: ComplexShape.Embedding.homRestrict.f, HomologicalComplex.restrictionXIso
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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 : ι
dsimp :
  (ψ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯)) ≫ L.d i j = K.d (e.f i) (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)
⊢ 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)

Tactic:
dsimp [f]

Premises used: ComplexShape.Embedding.homRestrict.f
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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 : ι
⊢ (ψ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯)) ≫ L.d i j = K.d (e.f i) (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)

Tactic:
simp only [assoc, ← ψ.comm_assoc, L.extend_d_eq e rfl rfl, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, HomologicalComplex.Hom.comm_assoc, HomologicalComplex.extend_d_eq, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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) (Hom.f (e.homRestrict ψ) i)
    (Iso.hom (K.restrictionXIso e h) ≫ ψ.f i' ≫ Iso.hom (L.extendXIso e h))

Tactic:
homRestrict.f_eq ψ h

Premises used: ComplexShape.Embedding.homRestrict.f, ComplexShape.Embedding.homRestrict.f_eq
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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)
⊢ Eq (α := (L.extend e).X i' ⟶ (L.extend e).X (e.f j)) ((L.extend e).d i' (e.f j)) 0

Tactic:
apply (L.isZero_extend_X e i' (hj.notMem hij')).eq_of_src

Premises used: ComplexShape.Embedding.BoundaryGE.notMem, HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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)
⊢ 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
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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
dsimp : K.d i' (e.f j) ≫ homRestrict.f ψ j = 0
⊢ K.d i' (e.f j) ≫ Hom.f (e.homRestrict ψ) j = 0

Tactic:
dsimp [homRestrict]

Premises used: ComplexShape.Embedding.homRestrict
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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
rw₃ : K.d i' (e.f j) ≫ 𝟙 ((K.restriction e).X j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯) = 0
rw₄ : Eq (α := K.X i' ⟶ L.X j) (K.d i' (e.f j) ≫ ψ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₅ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ (L.extend e).d i' (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) 0
rw₆ :
  Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ CategoryStruct.comp (Y := (L.extend e).X (e.f j)) 0 (Iso.hom (L.extendXIso e ⋯))) 0
rw₇ : Eq (α := K.X i' ⟶ L.X j) (ψ.f i' ≫ 0) 0
rw₈ rw₉ : Eq.{v_1 + 1} (α := K.X i' ⟶ L.X j) 0 0
⊢ K.d i' (e.f j) ≫ homRestrict.f ψ j = 0

Tactic:
rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.eqToIso_refl, HomologicalComplex.Hom.comm_assoc, CategoryTheory.Limits.zero_comp, ComplexShape.Embedding.homRestrict.f_eq, HomologicalComplex.restrictionXIso, CategoryTheory.Iso.refl_hom, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
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
h : ∀ (i' : ι'), Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'
⊢ e.liftExtend (e.homRestrict ψ) ⋯ = ψ

Tactic:
ext i'