awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i : ι
this :
  Iso.hom (K.extendXIso e ⋯) ≫ f.f i ≫ Iso.inv (L.extendXIso e ⋯) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Iso.hom (K.extendXIso e ⋯) ≫ g.f i ≫ Iso.inv (L.extendXIso e ⋯)
hi : c.Rel (c.prev i) i
⊢ c'.Rel (e.f (c.prev i)) (e.f i)

Tactic:
have hi' : c'.Rel (e.f (c.prev i)) (e.f i) := by rwa [e.rel_iff]
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i : ι
this :
  Iso.hom (K.extendXIso e ⋯) ≫ f.f i ≫ Iso.inv (L.extendXIso e ⋯) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Iso.hom (K.extendXIso e ⋯) ≫ g.f i ≫ Iso.inv (L.extendXIso e ⋯)
hi : c.Rel (c.prev i) i
hi' : c'.Rel (e.f (c.prev i)) (e.f i)
⊢ Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        h.hom :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫
        ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))

Tactic:
simp [prevD_eq _ hi, prevD_eq _ hi', L.extend_d_eq _ rfl rfl]

Premises used: prevD_eq, HomologicalComplex.extend_d_eq, rfl
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i : ι
this :
  Iso.hom (K.extendXIso e ⋯) ≫ f.f i ≫ Iso.inv (L.extendXIso e ⋯) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Iso.hom (K.extendXIso e ⋯) ≫ g.f i ≫ Iso.inv (L.extendXIso e ⋯)
hi : ¬c.Rel (c.prev i) i
neg :
  Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        h.hom :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
⊢ Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        h.hom :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫
        ((prevD i : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X i ⟶ L.X i) fun (i j : ι) ↦
            Iso.inv (K.extendXIso e ⋯) ≫ h.hom (e.f i) (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)) ≫
          Iso.inv (L.extendXIso e ⋯) :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))

Tactic:
rw [prevD_eq_zero _ _ hi]

Premises used: prevD_eq_zero
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i : ι
this :
  Iso.hom (K.extendXIso e ⋯) ≫ f.f i ≫ Iso.inv (L.extendXIso e ⋯) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Iso.hom (K.extendXIso e ⋯) ≫ g.f i ≫ Iso.inv (L.extendXIso e ⋯)
hi : ¬c.Rel (c.prev i) i
pos :
  ∀ (hi' : c'.Rel (c'.prev (e.f i)) (e.f i)),
    Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      ((prevD (e.f i) :
            (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
          h.hom :
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
neg :
  ∀ (hi' : ¬c'.Rel (c'.prev (e.f i)) (e.f i)),
    Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      ((prevD (e.f i) :
            (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
          h.hom :
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
      (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
⊢ Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        h.hom :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))

Tactic:
by_cases hi' : c'.Rel (c'.prev (e.f i)) (e.f i)

Premises used: ComplexShape.prev, ComplexShape.Embedding.f, ComplexShape.Rel
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i : ι
this :
  Iso.hom (K.extendXIso e ⋯) ≫ f.f i ≫ Iso.inv (L.extendXIso e ⋯) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Iso.hom (K.extendXIso e ⋯) ≫ g.f i ≫ Iso.inv (L.extendXIso e ⋯)
hi : ¬c.Rel (c.prev i) i
hi' : c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        h.hom :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))

Tactic:
simp [prevD_eq _ hi', extend_d_to_eq_zero _ _ _ _ _ rfl hi]

Premises used: prevD_eq, HomologicalComplex.extend_d_to_eq_zero, rfl
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i : ι
this :
  Iso.hom (K.extendXIso e ⋯) ≫ f.f i ≫ Iso.inv (L.extendXIso e ⋯) =
    HAdd.hAdd (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) (β :=
        (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((dNext (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        ((prevD (e.f i) :
              (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
            h.hom :
          (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i)) +
      Iso.hom (K.extendXIso e ⋯) ≫ g.f i ≫ Iso.inv (L.extendXIso e ⋯)
hi : ¬c.Rel (c.prev i) i
hi' : ¬c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ Eq.{v_1 + 1} (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    ((prevD (e.f i) :
          (a : (i j : ι') → (K.extend e).X i ⟶ (L.extend e).X j) → (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
        h.hom :
      (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))
    (Iso.hom (K.extendXIso e ⋯) ≫ 0 ≫ Iso.inv (L.extendXIso e ⋯) : (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f i))

Tactic:
simp [prevD_eq_zero _ _ hi']

Premises used: prevD_eq_zero
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
hom : ∀ (i' j' : ι'), Homotopy.hom (h.ofExtend.extend e) i' j' = h.hom i' j'
⊢ h.ofExtend.extend e = h

Tactic:
ext i' j'
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i' j' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), hom (h.ofExtend.extend e) i' j' = h.hom i' j'
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), hom (h.ofExtend.extend e) i' j' = h.hom i' j'
⊢ hom (h.ofExtend.extend e) i' j' = h.hom i' j'

Tactic:
by_cases hi' : ∃ i, e.f i = i'
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos :
  ∀ (i : ι),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (hom (h.ofExtend.extend e) (e.f i) j') (h.hom (e.f i) j')
⊢ hom (h.ofExtend.extend e) i' j' = h.hom i' j'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Premises used: rfl
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
j' : ι'
i : ι
pos :
  ∀ (hj' : ∃ (j : ι), e.f j = j'),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (hom (h.ofExtend.extend e) (e.f i) j') (h.hom (e.f i) j')
neg :
  ∀ (hj' : ¬∃ (j : ι), e.f j = j'),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (hom (h.ofExtend.extend e) (e.f i) j') (h.hom (e.f i) j')
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (hom (h.ofExtend.extend e) (e.f i) j') (h.hom (e.f i) j')

Tactic:
by_cases hj' : ∃ j, e.f j = j'
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ∃ (j : ι), e.f j = j'
pos :
  ∀ (j : ι),
    Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (hom (h.ofExtend.extend e) (e.f i) (e.f j))
      (h.hom (e.f i) (e.f j))
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (hom (h.ofExtend.extend e) (e.f i) j') (h.hom (e.f i) j')

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

Premises used: rfl
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i j : ι
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X (e.f j)) (hom (h.ofExtend.extend e) (e.f i) (e.f j))
    (h.hom (e.f i) (e.f j))

Tactic:
simp [extend_hom_eq _ e rfl rfl, ofExtend_hom]

Premises used: Homotopy.extend_hom_eq, Homotopy.ofExtend_hom, rfl
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ¬∃ (j : ι), e.f j = j'
tauto tauto₁ : ∀ (i : ι), e.f i ≠ j'
tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ (i : ι), e.f i = j' → False
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
tauto
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ¬∃ (j : ι), e.f j = j'
⊢ Eq (α := (K.extend e).X (e.f i) ⟶ (L.extend e).X j') (hom (h.ofExtend.extend e) (e.f i) j') (h.hom (e.f i) j')

Tactic:
exact (isZero_extend_X _ _ _ (by tauto)).eq_of_tgt _ _

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
tauto tauto₁ : ∀ (i : ι), e.f i ≠ i'
tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ (i : ι), e.f i = i' → False
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
tauto
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ hom (h.ofExtend.extend e) i' j' = h.hom i' j'

Tactic:
exact (isZero_extend_X _ _ _ (by tauto)).eq_of_src _ _

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_src
-- 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 g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
hom : ∀ (i j : ι), (ofExtend (h.extend e)).hom i j = h.hom i j
⊢ ofExtend (h.extend e) = h

Tactic:
ext i j
-- 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 g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst_3 : e.IsRelIff
i j : ι
⊢ (ofExtend (h.extend e)).hom i j = h.hom i j

Tactic:
simp [ofExtend_hom, h.extend_hom_eq e rfl rfl]

Premises used: Homotopy.extend_hom_eq, Homotopy.ofExtend_hom, rfl
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
x : Homotopy f g
⊢ (fun (h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)) ↦ h.ofExtend)
      ((fun (h : Homotopy f g) ↦ (h.extend e : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e))) x) =
    x

Tactic:
simp
-- 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 g : K ⟶ L
e : c.Embedding c'
inst_3 : e.IsRelIff
x : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)
⊢ (fun (h : Homotopy f g) ↦ (h.extend e : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)))
      ((fun (h : Homotopy (C := K.extend e) (extendMap f e) (extendMap g e)) ↦ h.ofExtend) x) =
    x

Tactic:
simp
-- 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
f₁ f₂ : K ⟶ L
h : Homotopy f₁ f₂
⊢ Eq (α :=
    Functor.obj (e.extendFunctor C ⋙ HomotopyCategory.quotient C c') K ⟶
      Functor.obj (e.extendFunctor C ⋙ HomotopyCategory.quotient C c') L)
    (CategoryTheory.Functor.map (e.extendFunctor C ⋙ HomotopyCategory.quotient C c') f₁)
    (CategoryTheory.Functor.map (e.extendFunctor C ⋙ HomotopyCategory.quotient C c') f₂)

Tactic:
HomotopyCategory.eq_of_homotopy _ _ (h.extend e)

Premises used: HomotopyCategory.eq_of_homotopy, Homotopy.extend
-- 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
f₁ f₂ : K ⟶ L
h : Homotopy f₁ f₂
⊢ Eq (α :=
    Functor.obj (e.extendFunctor C ⋙ HomotopyCategory.quotient C c') K ⟶
      Functor.obj (e.extendFunctor C ⋙ HomotopyCategory.quotient C c') L)
    (CategoryTheory.Functor.map (e.extendFunctor C ⋙ HomotopyCategory.quotient C c') f₁)
    (CategoryTheory.Functor.map (e.extendFunctor C ⋙ HomotopyCategory.quotient C c') f₂)

Tactic:
exact HomotopyCategory.eq_of_homotopy _ _ (h.extend e)

Premises used: HomotopyCategory.eq_of_homotopy, Homotopy.extend
-- 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
φ : Functor.obj (e.extendHomotopyFunctor C) K ⟶ Functor.obj (e.extendHomotopyFunctor C) L
obtain :
  ∀ (K : 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) L),
    ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ L),
      CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a = φ
⊢ ∃ (a : K ⟶ L), CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a = φ

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 (e.extendHomotopyFunctor C) (Functor.obj (HomotopyCategory.quotient C c) K) ⟶
    Functor.obj (e.extendHomotopyFunctor C) L
obtain :
  ∀ (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)),
    ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L),
      CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a = φ
⊢ ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ L),
    CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a = φ

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

Premises used: HomotopyCategory.quotient_obj_surjective, rfl