awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n) (w :
    f ≫ HomologicalComplex.Hom.f (p K L) n = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n, X₃ := L.X n, f := f,
          g := HomologicalComplex.Hom.f (p K L) n, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
have refine_1 : Eq (α := (mappingCone (𝟙 (I K))).X n ⟶ L.X n)
  (CategoryStruct.comp (Y := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f biprod.inl n)
    (HomologicalComplex.Hom.f (p K L) n))
  0
Tactic: refine ⟨(mappingCone (𝟙 (I K))).X n, inferInstance,
    (biprod.inl :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_,
    (biprod.fst : (mappingCone (𝟙 (I K))) ⊞ L ⟶ _).f n,
    (biprod.inr :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
refine_1 :
  Eq (α := (mappingCone (𝟙 (I K))).X n ⟶ L.X n)
    (CategoryStruct.comp (Y := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f biprod.inl n)
      (HomologicalComplex.Hom.f (p K L) n))
    0
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n) (w :
    f ≫ HomologicalComplex.Hom.f (p K L) n = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n, X₃ := L.X n, f := f,
          g := HomologicalComplex.Hom.f (p K L) n, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
have refine_2 : ShortComplex.f
      (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
        (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry) ≫
    HomologicalComplex.Hom.f biprod.fst n =
  𝟙
    (ShortComplex.X₁
      (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
        (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry))
Tactic: refine ⟨(mappingCone (𝟙 (I K))).X n, inferInstance,
    (biprod.inl :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_,
    (biprod.fst : (mappingCone (𝟙 (I K))) ⊞ L ⟶ _).f n,
    (biprod.inr :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Factorizations.CM5b (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : EnoughInjectives.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
refine_1 :
  Eq (α := (mappingCone (𝟙 (I K))).X n ⟶ L.X n)
    (CategoryStruct.comp (Y := (mappingCone (𝟙 (I K)) ⊞ L).X n) (HomologicalComplex.Hom.f biprod.inl n)
      (HomologicalComplex.Hom.f (p K L) n))
    0
refine_2 :
  ShortComplex.f
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯) ≫
      HomologicalComplex.Hom.f biprod.fst n =
    𝟙
      (ShortComplex.X₁
        (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
          (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) ⋯))
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n) (w :
    f ≫ HomologicalComplex.Hom.f (p K L) n = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := (mappingCone (𝟙 (cm5b.I K)) ⊞ L).X n, X₃ := L.X n, f := f,
          g := HomologicalComplex.Hom.f (p K L) n, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
have refine_3 : CategoryStruct.comp (Y :=
    ShortComplex.X₂
      (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
        (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry))
    (HomologicalComplex.Hom.f biprod.inr n)
    (ShortComplex.g
      (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
        (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry)) =
  𝟙
    (ShortComplex.X₃
      (ShortComplex.mk (X₁ := (mappingCone (𝟙 (I K))).X n) (X₂ := (mappingCone (𝟙 (I K)) ⊞ L).X n)
        (HomologicalComplex.Hom.f biprod.inl n) (HomologicalComplex.Hom.f (p K L) n) sorry))
Tactic: refine ⟨(mappingCone (𝟙 (I K))).X n, inferInstance,
    (biprod.inl :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_,
    (biprod.fst : (mappingCone (𝟙 (I K))) ⊞ L ⟶ _).f n,
    (biprod.inr :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (hypothesis)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j : ι
h : ¬c.Rel i j
⊢ (C.d i j).app t = 0
have this : C.d i j = 0
Tactic: have := C.shape _ _ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (hypothesis)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j : ι
h : ¬c.Rel i j
this : C.d i j = 0
⊢ (C.d i j).app t = 0
have this₁ : ∀ (x : T), (C.d i j).app x = NatTrans.app 0 x
Tactic: rw [NatTrans.ext_iff, funext_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (hypothesis)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0
have this : C.d i j ≫ C.d j k = 0
Tactic: have := C.d_comp_d i j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (hypothesis)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
this : C.d i j ≫ C.d j k = 0
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0
have this₁ : ∀ (x : T), (C.d i j ≫ C.d j k).app x = NatTrans.app 0 x
Tactic: rw [NatTrans.ext_iff, funext_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, u_3} V c)
      { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }
      { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (i : ι) ↦ (C.X i).map (𝟙 t), comm' := ⋯ }
    (𝟙 { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ })
have h : ∀ (i : ι),
  Eq.{v_2 + 1} (α :=
    Quiver.Hom.{v_2, u_2} (V := V)
      (X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := sorry, d_comp_d' := sorry } i)
      (X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := sorry, d_comp_d' := sorry } i))
    (Hom.f { f := fun (i : ι) ↦ (C.X i).map (𝟙 t), comm' := sorry } i)
    (Hom.f (𝟙 { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := sorry, d_comp_d' := sorry }) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i : ι
⊢ Eq.{v_2 + 1} (α :=
    Quiver.Hom.{v_2, u_2} (V := V)
      (X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ } i)
      (X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ } i))
    (Hom.f { f := fun (i : ι) ↦ (C.X i).map (𝟙 t), comm' := ⋯ } i)
    (Hom.f (𝟙 { X := fun (i : ι) ↦ (C.X i).obj t, d := fun (i j : ι) ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }) i)
have h : (C.X i).map (𝟙 t) = 𝟙 ((C.X i).obj t)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
t : T
i : ι
⊢ (C.X i).map (𝟙 t) = 𝟙 ((C.X i).obj t)
have h : Eq.{v_2 + 1} (α := (C.X i).obj t ⟶ (C.X i).obj t) (𝟙 ((C.X i).obj t)) (𝟙 ((C.X i).obj t))
Tactic: rw [(C.X i).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
X Y Z : T
h₁ : X ⟶ Y
h₂ : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, u_3} V c)
      { X := fun (i : ι) ↦ (C.X i).obj X, d := fun (i j : ι) ↦ (C.d i j).app X, shape := ⋯, d_comp_d' := ⋯ }
      { X := fun (i : ι) ↦ (C.X i).obj Z, d := fun (i j : ι) ↦ (C.d i j).app Z, shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (i : ι) ↦ (C.X i).map (h₁ ≫ h₂), comm' := ⋯ }
    (CategoryStruct.comp (Y :=
      { X := fun (i : ι) ↦ (C.X i).obj Y, d := fun (i j : ι) ↦ (C.d i j).app Y, shape := ⋯, d_comp_d' := ⋯ })
      { f := fun (i : ι) ↦ (C.X i).map h₁, comm' := ⋯ } { f := fun (i : ι) ↦ (C.X i).map h₂, comm' := ⋯ })
have h : ∀ (i : ι),
  Eq.{v_2 + 1} (α :=
    Quiver.Hom.{v_2, u_2} (V := V)
      (HomologicalComplex.X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj X, d := fun (i j : ι) ↦ (C.d i j).app X, shape := sorry, d_comp_d' := sorry } i)
      (HomologicalComplex.X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj Z, d := fun (i j : ι) ↦ (C.d i j).app Z, shape := sorry, d_comp_d' := sorry } i))
    (Hom.f { f := fun (i : ι) ↦ (C.X i).map (h₁ ≫ h₂), comm' := sorry } i)
    (Hom.f
      (CategoryStruct.comp (Y :=
        { X := fun (i : ι) ↦ (C.X i).obj Y, d := fun (i j : ι) ↦ (C.d i j).app Y, shape := sorry, d_comp_d' := sorry })
        { f := fun (i : ι) ↦ (C.X i).map h₁, comm' := sorry } { f := fun (i : ι) ↦ (C.X i).map h₂, comm' := sorry })
      i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
X Y Z : T
h₁ : X ⟶ Y
h₂ : Y ⟶ Z
i : ι
⊢ Eq.{v_2 + 1} (α :=
    Quiver.Hom.{v_2, u_2} (V := V)
      (HomologicalComplex.X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj X, d := fun (i j : ι) ↦ (C.d i j).app X, shape := ⋯, d_comp_d' := ⋯ } i)
      (HomologicalComplex.X.{v_2, u_2, u_3} (c := c)
        { X := fun (i : ι) ↦ (C.X i).obj Z, d := fun (i j : ι) ↦ (C.d i j).app Z, shape := ⋯, d_comp_d' := ⋯ } i))
    (Hom.f { f := fun (i : ι) ↦ (C.X i).map (h₁ ≫ h₂), comm' := ⋯ } i)
    (Hom.f
      (CategoryStruct.comp (Y :=
        { X := fun (i : ι) ↦ (C.X i).obj Y, d := fun (i j : ι) ↦ (C.d i j).app Y, shape := ⋯, d_comp_d' := ⋯ })
        { f := fun (i : ι) ↦ (C.X i).map h₁, comm' := ⋯ } { f := fun (i : ι) ↦ (C.X i).map h₂, comm' := ⋯ })
      i)
have h : (C.X i).map (h₁ ≫ h₂) = (C.X i).map h₁ ≫ (C.X i).map h₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
X Y Z : T
h₁ : X ⟶ Y
h₂ : Y ⟶ Z
i : ι
⊢ (C.X i).map (h₁ ≫ h₂) = (C.X i).map h₁ ≫ (C.X i).map h₂
have h : (C.X i).map h₁ ≫ (C.X i).map h₂ = (C.X i).map h₁ ≫ (C.X i).map h₂
Tactic: rw [Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : HasZeroMorphisms.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
X Y : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
f : X ⟶ Y
t t' : T
g : t ⟶ t'
⊢ X.asFunctor.map g ≫ { f := fun (i : ι) ↦ (f.f i).app t', comm' := ⋯ } =
    { f := fun (i : ι) ↦ (f.f i).app t, comm' := ⋯ : (X.asFunctor.obj t).Hom (Y.asFunctor.obj t) } ≫ Y.asFunctor.map g
have h : ∀ (i : ι),
  Hom.f (X.asFunctor.map g ≫ { f := fun (i : ι) ↦ (f.f i).app t', comm' := sorry }) i =
    Hom.f
      ({ f := fun (i : ι) ↦ (f.f i).app t, comm' := sorry : (X.asFunctor.obj t).Hom (Y.asFunctor.obj t) } ≫
        Y.asFunctor.map g)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : Abelian.{v_2, u_2} V
S₁ S₂ : ShortComplex (Functor.{v_1, v_2, u_1, u_2} T V)
f : S₁ ⟶ S₂
hf :
  ∀ (j : T),
    QuasiIso (S₁ := Functor.obj (Functor.mapShortComplex (Functor.obj (evaluation T V) j)) S₁)
      (Functor.map (Functor.mapShortComplex (Functor.obj (evaluation T V) j)) f)
⊢ QuasiIso f
have rw : ∀ (X : T), IsIso (X := S₁.homology.obj X) (Y := S₂.homology.obj X) (NatTrans.app (homologyMap f) X)
Tactic: rw [quasiIso_iff, NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : Abelian.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
K₁ K₂ : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
f : K₁ ⟶ K₂
i : ι
⊢ QuasiIsoAt f i ↔
    ∀ (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
have simp : (∀ (j : T),
    ShortComplex.QuasiIso (S₁ :=
      Functor.obj (Functor.mapShortComplex (Functor.obj (evaluation T V) j))
        (Functor.obj (shortComplexFunctor (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c i) K₁))
      (CategoryTheory.Functor.map (Functor.mapShortComplex (Functor.obj (evaluation T V) j))
        (CategoryTheory.Functor.map (shortComplexFunctor (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c i) f))) ↔
  ∀ (t : T),
    ShortComplex.QuasiIso (S₁ :=
      Functor.obj (shortComplexFunctor V c i)
        (Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁))
      (CategoryTheory.Functor.map (shortComplexFunctor V c i)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f))
Tactic: simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff_evaluation]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : Abelian.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
K₁ K₂ : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
f : K₁ ⟶ K₂
⊢ QuasiIso f ↔
    ∀ (t : T),
      QuasiIso (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f)
have simp : (∀ (i : ι) (t : T),
    QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
      (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) ↔
  ∀ (t : T) (i : ι),
    QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
      (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
Tactic: simp only [quasiIso_iff, quasiIsoAt_iff_evaluation]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : Abelian.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
K₁ K₂ : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
f : K₁ ⟶ K₂
⊢ (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) ↔
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
have mp : (∀ (i : ι) (t : T),
    QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
      (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
  ∀ (t : T) (i : ι),
    QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
      (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.Functor (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : Abelian.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
K₁ K₂ : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
f : K₁ ⟶ K₂
mp :
  (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
⊢ (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) ↔
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
have mpr : (∀ (t : T) (i : ι),
    QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
      (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
  ∀ (i : ι) (t : T),
    QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
      (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.GrothendieckAbelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : Small.{w, t} ι
K L : HomologicalComplex.{v, u, t} C c
emb : (f : K ⟶ L) →
  (i : Shrink.{w, t} ι) →
    Shrink.{w, v}
      (K.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i) ⟶
        L.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i)) :=
  fun (f : K ⟶ L) (i : Shrink.{w, t} ι) ↦
    (equivShrink
          (K.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i) ⟶
            L.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i)) :
        (a :
            K.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i) ⟶
              L.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i)) →
          Shrink.{w, v}
            (K.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i) ⟶
              L.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i)))
      (f.f ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i))
f g : K ⟶ L
h : emb f = emb g
⊢ f = g
have h₁ : ∀ (i : ι), f.f i = g.f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.GrothendieckAbelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : Small.{w, t} ι
K L : HomologicalComplex.{v, u, t} C c
emb : (f : K ⟶ L) →
  (i : Shrink.{w, t} ι) →
    Shrink.{w, v}
      (K.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i) ⟶
        L.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i)) :=
  fun (f : K ⟶ L) (i : Shrink.{w, t} ι) ↦
    (equivShrink
          (K.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i) ⟶
            L.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i)) :
        (a :
            K.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i) ⟶
              L.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i)) →
          Shrink.{w, v}
            (K.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i) ⟶
              L.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i)))
      (f.f ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i))
f g : K ⟶ L
h : emb f = emb g
i : ι
⊢ f.f i = g.f i
have h₁ : ∀ (i : Shrink.{w, t} ι),
  Eq (α :=
    K.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i) ⟶
      L.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i))
    (f.f ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i))
    (g.f ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i))
Tactic: obtain ⟨i, rfl⟩ := (equivShrink.{w} _).symm.surjective i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.GrothendieckAbelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : Small.{w, t} ι
K L : HomologicalComplex.{v, u, t} C c
emb : (f : K ⟶ L) →
  (i : Shrink.{w, t} ι) →
    Shrink.{w, v}
      (K.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i) ⟶
        L.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i)) :=
  fun (f : K ⟶ L) (i : Shrink.{w, t} ι) ↦
    (equivShrink
          (K.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i) ⟶
            L.X ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i)) :
        (a :
            K.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i) ⟶
              L.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i)) →
          Shrink.{w, v}
            (K.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i) ⟶
              L.X (((equivShrink ι).symm : (a : Shrink.{w, t} ι) → ι) i)))
      (f.f ((Equiv.symm (equivShrink ι) : (a : Shrink.{w, t} ι) → ι) i))
⊢ Small.{w, max t v} (K ⟶ L)
have hemb : Function.Injective emb
Tactic: have hemb : Function.Injective emb := fun f g h ↦ by
      ext i
      obtain ⟨i, rfl⟩ := (equivShrink.{w} _).symm.surjective i
      simpa [emb] using congr_fun h i