awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Functor
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
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 := ⋯, 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)
⊢ 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' := ⋯ })

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Functor
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 : ι
h : (C.X i).map (h₁ ≫ h₂) = (C.X i).map h₁ ≫ (C.X i).map h₂
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Functor
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 : ι
h h₃ : (C.X i).map h₁ ≫ (C.X i).map h₂ = (C.X i).map h₁ ≫ (C.X i).map h₂
⊢ (C.X i).map (h₁ ≫ h₂) = (C.X i).map h₁ ≫ (C.X i).map h₂

Tactic:
rw [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.Functor
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'
h :
  ∀ (i : ι),
    Hom.f (X.asFunctor.map g ≫ { f := fun (i : ι) ↦ (f.f i).app t', comm' := ⋯ }) i =
      Hom.f
        ({ f := fun (i : ι) ↦ (f.f i).app t, comm' := ⋯ : (X.asFunctor.obj t).Hom (Y.asFunctor.obj t) } ≫
          Y.asFunctor.map g)
        i
⊢ 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

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Functor
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'
i : ι
⊢ Hom.f (X.asFunctor.map g ≫ { f := fun (i : ι) ↦ (f.f i).app t', comm' := ⋯ }) i =
    Hom.f
      ({ f := fun (i : ι) ↦ (f.f i).app t, comm' := ⋯ : (X.asFunctor.obj t).Hom (Y.asFunctor.obj t) } ≫
        Y.asFunctor.map g)
      i

Tactic:
(f.f i).naturality g

Premises used: HomologicalComplex.Hom.f, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Homology.Functor
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'
i : ι
⊢ Hom.f (X.asFunctor.map g ≫ { f := fun (i : ι) ↦ (f.f i).app t', comm' := ⋯ }) i =
    Hom.f
      ({ f := fun (i : ι) ↦ (f.f i).app t, comm' := ⋯ : (X.asFunctor.obj t).Hom (Y.asFunctor.obj t) } ≫
        Y.asFunctor.map g)
      i

Tactic:
exact (f.f i).naturality g

Premises used: HomologicalComplex.Hom.f, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Homology.Functor
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)
rw : ∀ (X : T), IsIso (X := S₁.homology.obj X) (Y := S₂.homology.obj X) (NatTrans.app (homologyMap f) X)
⊢ QuasiIso f

Tactic:
rw [quasiIso_iff, NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app, CategoryTheory.ShortComplex.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Functor
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)
⊢ ∀ (X : T), IsIso (X := S₁.homology.obj X) (Y := S₂.homology.obj X) (NatTrans.app (homologyMap f) X)

Tactic:
fun j ↦ ((MorphismProperty.isomorphisms V).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
      ((homologyFunctorIso ((evaluation T V).obj j)))).app (Arrow.mk f))).1
        ((quasiIso_iff _).1 (hf j))

Premises used: CategoryTheory.Functor, CategoryTheory.ShortComplex, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.Arrow.hom, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.ShortComplex.homologyFunctorIso, CategoryTheory.Functor.mapShortComplex, CategoryTheory.ShortComplex.quasiIso_iff, Iff.mp, CategoryTheory.evaluation, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.Functor
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)
⊢ ∀ (X : T), IsIso (X := S₁.homology.obj X) (Y := S₂.homology.obj X) (NatTrans.app (homologyMap f) X)

Tactic:
exact fun j ↦ ((MorphismProperty.isomorphisms V).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
      ((homologyFunctorIso ((evaluation T V).obj j)))).app (Arrow.mk f))).1
        ((quasiIso_iff _).1 (hf j))

Premises used: CategoryTheory.Functor, CategoryTheory.ShortComplex, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.Arrow.hom, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.ShortComplex.homologyFunctorIso, CategoryTheory.Functor.mapShortComplex, CategoryTheory.ShortComplex.quasiIso_iff, Iff.mp, CategoryTheory.evaluation, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.Functor
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 : ι
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))
⊢ 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

Tactic:
simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff_evaluation]

Premises used: CategoryTheory.ShortComplex.quasiIso_iff_evaluation, quasiIsoAt_iff
-- Module: Mathlib.Algebra.Homology.Functor
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 : ι
⊢ (∀ (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:
rfl
-- Module: Mathlib.Algebra.Homology.Functor
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₂
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
⊢ 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)

Tactic:
simp only [quasiIso_iff, quasiIsoAt_iff_evaluation]

Premises used: quasiIso_iff, HomologicalComplex.quasiIsoAt_iff_evaluation
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
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
h₁ : ∀ (i : ι), f.f i = g.f i
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
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 : ι
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))
⊢ f.f i = g.f i

Tactic:
obtain ⟨i, rfl⟩ := (equivShrink.{w} _).symm.surjective i

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
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 : 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:
simpa [emb] using congr_fun h i

Premises used: congr_fun
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
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))
⊢ 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
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
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))
hemb : Function.Injective emb
⊢ Small.{w, max t v} (K ⟶ L)

Tactic:
apply small_of_injective hemb

Premises used: small_of_injective
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
x : Category.{w, w'} J
h : IsFiltered.{w, w'} J
⊢ HasColimitsOfShape J (HomologicalComplex.{v, u, t} C c)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v, u} C
J : Type w
inst_2 : Category.{w', w} J
inst_3 : HasFiniteLimits.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
K : Type
x : SmallCategory K
x_1 : FinCategory K
F : K ⥤ J ⥤ HomologicalComplex.{v, u, t} C c
c_1 : Cone F
hc : IsLimit c_1
i : ι
e : Iso (C := (J ⥤ HomologicalComplex.{v, u, t} C c) ⥤ C) (colim ⋙ eval C c i)
  (Functor.obj (Functor.whiskeringRight J (HomologicalComplex.{v, u, t} C c) C) (eval C c i) ⋙ colim) :=
  preservesColimitNatIso (eval C c i)
⊢ IsLimit (F := (F ⋙ colim) ⋙ eval C c i) (Functor.mapCone (eval C c i) (Functor.mapCone colim c_1))

Tactic:
exact (IsLimit.postcomposeHomEquiv (Functor.isoWhiskerLeft F e) _).1
        (IsLimit.ofIsoLimit
          (isLimitOfPreserves ((Functor.whiskeringRight J _ _).obj (eval C c i) ⋙ colim) hc)
          (Cone.ext (e.symm.app _) (fun k ↦ (NatIso.naturality_2 e.symm _).symm)))
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFilteredColimitsOfSize.{w', w, v, u} C
inst_3 : HasFiniteLimits.{v, u} C
inst_4 : AB5OfSize.{w', w, v, u} C
J : Type w
x : Category.{w', w} J
h : IsFiltered.{w', w} J
⊢ HasExactColimitsOfShape J (HomologicalComplex.{v, u, t} C c)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
inst_3 : c.HasNoLoop
inst_4 : Small.{w, t} ι
⊢ HasCoproductsOfShape.{t, u, v} ι C

Tactic:
have : HasCoproductsOfShape ι C :=
      hasColimitsOfShape_of_equivalence (Discrete.equivalence (equivShrink.{w} ι)).symm
-- Module: Mathlib.Algebra.Homology.GrothendieckAbelian
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
inst_3 : c.HasNoLoop
inst_4 : Small.{w, t} ι
this : HasCoproductsOfShape.{t, u, v} ι C
⊢ HasSeparator (HomologicalComplex.{v, u, t} C c)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.HasNoLoop
j : ι
⊢ ¬c.Rel j j

Tactic:
HasNoLoop.not_rel_self j

Premises used: ComplexShape.HasNoLoop.not_rel_self
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.HasNoLoop
j j' : ι
h : j = j'
subst : ¬c.Rel j j
⊢ ¬c.Rel j j'

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.HasNoLoop
j : ι
⊢ ¬c.Rel j j

Tactic:
c.not_rel_self j

Premises used: ComplexShape.not_rel_self
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.HasNoLoop
j : ι
⊢ ¬c.Rel j j

Tactic:
exact c.not_rel_self j

Premises used: ComplexShape.not_rel_self
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.HasNoLoop
j : ι
⊢ (∃ (k : ι), c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Tactic:
grind +splitIndPred
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.HasNoLoop
j : ι
⊢ (∃ (i : ι), c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Tactic:
grind +splitIndPred
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
α : Type u_2
inst : AddZeroClass α
inst_1 : IsRightCancelAdd α
inst_2 : IsLeftCancelAdd α
a : α
ha : a ≠ 0
i : α
hi rw : i + a = i
rw₁ rw₂ : i = i
⊢ i + a = i + 0

Tactic:
rw [add_zero, hi]

Premises used: add_zero
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
α : Type u_2
inst : AddZeroClass α
inst_1 : IsRightCancelAdd α
inst_2 : IsLeftCancelAdd α
a : α
ha : a ≠ 0
⊢ (up' a).HasNoLoop

Tactic:
have := hasNoLoop_up' a ha
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
α : Type u_2
inst : AddZeroClass α
inst_1 : IsRightCancelAdd α
inst_2 : IsLeftCancelAdd α
a : α
ha : a ≠ 0
this : (up' a).HasNoLoop
⊢ (down' a).HasNoLoop

Tactic:
inferInstanceAs (up' a).symm.HasNoLoop

Premises used: _private.0.ComplexShape.hasNoLoop_down'._proof_1
-- Module: Mathlib.Algebra.Homology.HasNoLoop
Goal:
α : Type u_2
inst : AddZeroClass α
inst_1 : IsRightCancelAdd α
inst_2 : IsLeftCancelAdd α
a : α
ha : a ≠ 0
this : (up' a).HasNoLoop
⊢ (down' a).HasNoLoop

Tactic:
exact inferInstanceAs (up' a).symm.HasNoLoop