awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ :
  Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
    Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L)
obtain :
  ∀ (φ : K.extend e ⟶ L.extend e),
    ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L),
      Eq (α :=
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
          Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C c') φ)
⊢ ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L),
    CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a = φ

Tactic:
obtain ⟨φ : K.extend e ⟶ L.extend e, rfl⟩ :=
      (HomotopyCategory.quotient C c').map_surjective φ

Premises used: HomologicalComplex.extend, HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K.extend e ⟶ L.extend e
obtain :
  ∀ (φ : K ⟶ L),
    ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L),
      Eq (α :=
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
          Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a)
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C c') (CategoryTheory.Functor.map (e.extendFunctor C) φ))
⊢ ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L),
    Eq (α :=
      Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
      (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c') φ)

Tactic:
obtain ⟨φ, rfl⟩ := (e.extendFunctor C).map_surjective φ

Premises used: ComplexShape.Embedding.extendFunctor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
⊢ ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L),
    Eq (α :=
      Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
      (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c') (CategoryTheory.Functor.map (e.extendFunctor C) φ))

Tactic:
⟨(HomotopyCategory.quotient _ _).map φ, rfl⟩

Premises used: CategoryTheory.Functor.map, Exists.intro, HomotopyCategory.quotient, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
⊢ ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L),
    Eq (α :=
      Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
      (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c') (CategoryTheory.Functor.map (e.extendFunctor C) φ))

Tactic:
exact ⟨(HomotopyCategory.quotient _ _).map φ, rfl⟩
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomotopyCategory.{v_1, u_3, u_1} C c
φ₁ φ₂ : K ⟶ L
hφ :
  Eq (α := Functor.obj (e.extendHomotopyFunctor C) K ⟶ Functor.obj (e.extendHomotopyFunctor C) L)
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₁)
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₂)
obtain :
  ∀ (K : HomologicalComplex.{v_1, u_3, u_1} C c) (φ₁ φ₂ : Functor.obj (HomotopyCategory.quotient C c) K ⟶ L)
    (hφ :
      Eq (α :=
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
          Functor.obj (e.extendHomotopyFunctor C) L)
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₁)
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₂)),
    φ₁ = φ₂
⊢ φ₁ = φ₂

Tactic:
obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K

Premises used: HomotopyCategory.quotient_obj_surjective, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
L : HomotopyCategory.{v_1, u_3, u_1} C c
K : HomologicalComplex.{v_1, u_3, u_1} C c
φ₁ φ₂ : Functor.obj (HomotopyCategory.quotient C c) K ⟶ L
hφ :
  Eq (α :=
    Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
      Functor.obj (e.extendHomotopyFunctor C) L)
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₁)
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₂)
obtain :
  ∀ (L : HomologicalComplex.{v_1, u_3, u_1} C c)
    (φ₁ φ₂ : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L)
    (hφ :
      Eq (α :=
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
          Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₁)
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₂)),
    φ₁ = φ₂
⊢ φ₁ = φ₂

Tactic:
obtain ⟨L, rfl⟩ := HomotopyCategory.quotient_obj_surjective L

Premises used: HomotopyCategory.quotient_obj_surjective, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ₁ φ₂ : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L
hφ :
  Eq (α :=
    Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
      Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₁)
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₂)
obtain :
  ∀ (φ₁ : K ⟶ L)
    (hφ :
      Eq (α :=
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
          Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C)
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁))
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₂)),
    CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁ = φ₂
⊢ φ₁ = φ₂

Tactic:
obtain ⟨φ₁, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ₁

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ₂ : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L
φ₁ : K ⟶ L
hφ :
  Eq (α :=
    Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
      Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁))
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C) φ₂)
obtain :
  ∀ (φ₂ : K ⟶ L)
    (hφ :
      Eq (α :=
        Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
          Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C)
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁))
        (CategoryTheory.Functor.map (e.extendHomotopyFunctor C)
          (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₂))),
    Eq (α := Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₂)
⊢ CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁ = φ₂

Tactic:
obtain ⟨φ₂, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ₂

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ₁ φ₂ : K ⟶ L
hφ :
  Eq (α :=
    Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
      Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁))
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₂))
⊢ Eq (α := Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₂)

Tactic:
HomotopyCategory.eq_of_homotopy _ _
      (.ofExtend (HomotopyCategory.homotopyOfEq _ _ hφ))

Premises used: HomotopyCategory.eq_of_homotopy, Homotopy.ofExtend, HomotopyCategory.homotopyOfEq
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst : e.IsRelIff
C : Type u_3
inst_1 : Category.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
inst_3 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ₁ φ₂ : K ⟶ L
hφ :
  Eq (α :=
    Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
      Functor.obj (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) L))
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁))
    (CategoryTheory.Functor.map (e.extendHomotopyFunctor C)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₂))
⊢ Eq (α := Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₂)

Tactic:
exact HomotopyCategory.eq_of_homotopy _ _
      (.ofExtend (HomotopyCategory.homotopyOfEq _ _ hφ))

Premises used: HomotopyCategory.eq_of_homotopy, Homotopy.ofExtend, HomotopyCategory.homotopyOfEq
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
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 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
f : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
⊢ homotopyEquivalences C c' (X := K.extend e) (extendMap f e) ↔ homotopyEquivalences C c f

Tactic:
simp [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff,
    ← isIso_iff_of_reflects_iso _ (e.extendHomotopyFunctor C),
    dsimp% NatIso.isIso_map_iff (e.extendHomotopyFunctorFactors C) f]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, ComplexShape.Embedding.extendHomotopyFunctor, ComplexShape.Embedding.extendHomotopyFunctorFactors, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.NatIso.isIso_map_iff, CategoryTheory.MorphismProperty.inverseImage_iff, HomotopyCategory.inverseImage_quotient_isomorphisms
-- 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
i' : ι'
i : ι
hi : e.f i = i'
⊢ ∃ (k : ι), e.f k = i'

Tactic:
have hi' : ∃ k, e.f k = i' := ⟨i, 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
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ (k : ι), e.f k = i'
rw : i' = e.f i
rw₁ rw₂ : i' = i'
⊢ e.f (hi'.choose (p := fun (k : ι) ↦ e.f k = i')) = e.f i

Tactic:
rw [hi'.choose_spec, hi]

Premises used: Exists.choose_spec
-- 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
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ (k : ι), e.f k = i'
⊢ hi'.choose (p := fun (k : ι) ↦ e.f k = i') = i

Tactic:
have : hi'.choose = i := e.injective_f (by rw [hi'.choose_spec, 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
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ (k : ι), e.f k = i'
this : hi'.choose (p := fun (k : ι) ↦ e.f k = i') = i
⊢ Eq (α := K.X i' ⟶ (L.extend e).X i') (f φ i') (Iso.inv (K.restrictionXIso e hi) ≫ φ.f i ≫ Iso.inv (L.extendXIso e hi))

Tactic:
grind [f]

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' j' : ι'
pos : ∀ (hij' : c'.Rel i' j'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
neg : ∀ (hij' : ¬c'.Rel i' j'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
by_cases hij' : c'.Rel i' j'

Premises used: ComplexShape.Rel
-- 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'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
by_cases hi' : ∃ i, e.f i = i'
-- 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'
pos : ∀ (i : ι) (hi : e.f i = i'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
obtain ⟨i, hi⟩ := 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'
i : ι
hi : e.f i = i'
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'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
rw [f_eq φ hi]

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 : 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'
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'
⊢ (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'
-- 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'
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'
⊢ (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'
-- 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'
j : ι
hj : e.f j = j'
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))
⊢ (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 φ hj, L.extend_d_eq e hi hj]

Premises used: ComplexShape.Embedding.liftExtend.f_eq, HomologicalComplex.extend_d_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.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'
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 ⋯) ≫ φ.f i ≫ Iso.inv (L.extendXIso e ⋯))
        (Iso.hom (L.extendXIso e ⋯) ≫ L.d i j ≫ Iso.inv (L.extendXIso e ⋯)))
      (K.d (e.f i) (e.f j) ≫ Iso.inv (K.restrictionXIso e ⋯) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))
⊢ 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:
subst hi 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 (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 ⋯) ≫ φ.f i ≫ Iso.inv (L.extendXIso e ⋯))
      (Iso.hom (L.extendXIso e ⋯) ≫ L.d i j ≫ Iso.inv (L.extendXIso e ⋯)))
    (K.d (e.f i) (e.f j) ≫ Iso.inv (K.restrictionXIso e ⋯) ≫ φ.f j ≫ Iso.inv (L.extendXIso e ⋯))

Tactic:
simp [HomologicalComplex.restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso