awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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))
⊢ 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))
have 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 sorry) ≫ 0 ≫ Iso.inv (L.extendXIso e sorry) : (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)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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)
⊢ h.ofExtend.extend e = h
have hom : ∀ (i' j' : ι'), hom (h.ofExtend.extend e) i' j' = h.hom i' j'
Tactic: ext i' j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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' : ι'
⊢ hom (h.ofExtend.extend e) i' j' = h.hom i' j'
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), hom (h.ofExtend.extend e) i' j' = h.hom i' j'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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'
⊢ hom (h.ofExtend.extend e) i' j' = h.hom i' j'
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), hom (h.ofExtend.extend e) i' j' = h.hom i' j'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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'
have 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')
Tactic: obtain ⟨i, rfl⟩ := hi'
Cleared hypotheses: i', hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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 : ι
⊢ 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')
have 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')
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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')
⊢ 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')
have 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')
Tactic: by_cases hj' : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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')
have 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))
Tactic: obtain ⟨j, rfl⟩ := hj'
Cleared hypotheses: j', hj'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : 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
⊢ ofExtend (h.extend e) = h
have hom : ∀ (i j : ι), (ofExtend (h.extend e)).hom i j = h.hom i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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
⊢ ∃ (a : K ⟶ L), CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a = φ
have 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 = φ
Tactic: obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K
Cleared hypotheses: K, φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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
⊢ ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ L),
    CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a = φ
have 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 = φ
Tactic: obtain ⟨L, rfl⟩ := HomotopyCategory.quotient_obj_surjective L
Cleared hypotheses: L, φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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)
⊢ ∃ (a : Functor.obj (HomotopyCategory.quotient C c) K ⟶ Functor.obj (HomotopyCategory.quotient C c) L),
    CategoryTheory.Functor.map (e.extendHomotopyFunctor C) a = φ
have 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') φ)
Tactic: obtain ⟨φ : K.extend e ⟶ L.extend e, rfl⟩ :=
      (HomotopyCategory.quotient C c').map_surjective φ
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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
⊢ ∃ (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') φ)
have 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) φ))
Tactic: obtain ⟨φ, rfl⟩ := (e.extendFunctor C).map_surjective φ
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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) φ₂)
⊢ φ₁ = φ₂
have 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
Cleared hypotheses: K, φ₁, φ₂, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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) φ₂)
⊢ φ₁ = φ₂
have 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
Cleared hypotheses: L, φ₁, φ₂, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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) φ₂)
⊢ φ₁ = φ₂
have 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 φ₁
Cleared hypotheses: φ₁, hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomotopy (goal)
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) φ₂)
⊢ CategoryTheory.Functor.map (HomotopyCategory.quotient C c) φ₁ = φ₂
have 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) φ₂)
Tactic: obtain ⟨φ₂, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ₂
Cleared hypotheses: φ₂, hφ
-- 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
i' : ι'
i : ι
hi : e.f 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))
have hi' : ∃ (k : ι), e.f k = i'
Tactic: have hi' : ∃ k, e.f k = i' := ⟨i, 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
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ (k : ι), e.f k = i'
⊢ e.f (hi'.choose (p := fun (k : ι) ↦ e.f k = i')) = e.f i
have rw : i' = e.f i
Tactic: rw [hi'.choose_spec, 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
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ (k : ι), e.f k = i'
rw : i' = e.f i
⊢ e.f (hi'.choose (p := fun (k : ι) ↦ e.f k = i')) = e.f i
have rw₁ : i' = i'
Tactic: rw [hi'.choose_spec, hi]
-- 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
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ (k : ι), e.f k = 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))
have this : hi'.choose (p := fun (k : ι) ↦ e.f k = i') = i
Tactic: have : hi'.choose = i := e.injective_f (by rw [hi'.choose_spec, 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' : ι'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have pos : ∀ (hij' : c'.Rel i' j'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: by_cases hij' : c'.Rel i' 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' : ι'
pos : ∀ (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'
have neg : ∀ (hij' : ¬c'.Rel i' j'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: by_cases hij' : c'.Rel i' 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'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- 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'
pos : ∀ (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'
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
Tactic: by_cases hi' : ∃ i, e.f i = i'