awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
⊢ PreservesFiniteLimits (forget C (FC := FC) (CC := CC))

Tactic:
have : PreservesFiniteLimits (forget C) := by
    have : forget₂ C Ab ⋙ forget Ab = forget C := HasForget₂.forget_comp
    simpa only [← this] using comp_preservesFiniteLimits _ _
-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this_1 :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
this : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
⊢ Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ) :
          (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₃.X₁)
        (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
      CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.φ₁ ≫ D.v₂₃.τ₁) : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₃.X₁)
        (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
      CC D.L₃.X₁)

Tactic:
have eq := CategoryTheory.congr_fun (D.snd_δ)
    (Limits.Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this_1 :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
this : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
eq :
  Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ) :
          (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₃.X₁)
        (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
      CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.φ₁ ≫ D.v₂₃.τ₁) : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₃.X₁)
        (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
      CC D.L₃.X₁)
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.fst D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₁.X₂)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₂

Tactic:
have eq₁ := Concrete.pullbackMk_fst D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this_1 :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
this : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
eq :
  Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ) :
          (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₃.X₁)
        (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
      CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.φ₁ ≫ D.v₂₃.τ₁) : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₃.X₁)
        (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
      CC D.L₃.X₁)
eq₁ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.fst D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₁.X₂)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₂
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.snd D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₀.X₃)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₃

Tactic:
have eq₂ := Concrete.pullbackMk_snd D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this_1 :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
this : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
eq :
  Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.δ : (a : CC D.L₀.X₃) → CC D.L₃.X₁) x₃ : CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₂₃.τ₁ : (a : CC D.L₂.X₁) → CC D.L₃.X₁)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) D.φ₁ : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₂.X₁)
            (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
          CC D.L₂.X₁) :
      CC D.L₃.X₁)
eq₁ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.fst D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₁.X₂)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₂
eq₂ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.snd D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₀.X₃)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₃
⊢ Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.δ : (a : CC D.L₀.X₃) → CC D.L₃.X₁) x₃ : CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₂₃.τ₁ : (a : CC D.L₂.X₁) → CC D.L₃.X₁) x₁ : CC D.L₃.X₁)

Tactic:
eq.trans (CategoryTheory.congr_arg (D.v₂₃.τ₁) ?_)

Premises used: CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.congr_arg, CategoryTheory.ShortComplex.SnakeInput.v₂₃, Eq.trans
-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this_1 :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
this : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
eq :
  Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.δ : (a : CC D.L₀.X₃) → CC D.L₃.X₁) x₃ : CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₂₃.τ₁ : (a : CC D.L₂.X₁) → CC D.L₃.X₁)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) D.φ₁ : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₂.X₁)
            (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
          CC D.L₂.X₁) :
      CC D.L₃.X₁)
eq₁ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.fst D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₁.X₂)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₂
eq₂ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.snd D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₀.X₃)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₃
⊢ Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)

Tactic:
h₁.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 :
  HasForget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CD := AddCommGrpCat.carrier)
inst_4 : Abelian.{v, u} C
inst_5 :
  Functor.Additive
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
D : SnakeInput.{v, u} C
x₃ : ToType (FC := FC) (CC := CC) D.L₀.X₃
x₂ : ToType (FC := FC) (CC := CC) D.L₁.X₂
x₁ : ToType (FC := FC) (CC := CC) D.L₂.X₁
h₂ :
  Eq (α := CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₁.g : (a : CC D.L₁.X₂) → CC D.L₁.X₃) x₂ : CC D.L₁.X₃)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₀₁.τ₃ : (a : CC D.L₀.X₃) → CC D.L₁.X₃) x₃ : CC D.L₁.X₃)
h₁ :
  Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
this_1 :
  PreservesFiniteLimits
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
      (CD := AddCommGrpCat.carrier))
this : PreservesFiniteLimits (forget C (FC := FC) (CC := CC))
eq :
  Eq (α := CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.δ : (a : CC D.L₀.X₃) → CC D.L₃.X₁) x₃ : CC D.L₃.X₁)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₂₃.τ₁ : (a : CC D.L₂.X₁) → CC D.L₃.X₁)
        ((ConcreteCategory.hom (FC := FC) (CC := CC) D.φ₁ : (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₂.X₁)
            (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) :
          CC D.L₂.X₁) :
      CC D.L₃.X₁)
eq₁ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.fst D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₁.X₂)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₂
eq₂ :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (pullback.snd D.L₁.g D.v₀₁.τ₃) :
        (a : CC (pullback D.L₁.g D.v₀₁.τ₃)) → CC D.L₀.X₃)
      (Concrete.pullbackMk (FC := FC) (CC := CC) D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    x₃
⊢ Eq (α := CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.v₁₂.τ₂ : (a : CC D.L₁.X₂) → CC D.L₂.X₂) x₂ : CC D.L₂.X₂)
    ((ConcreteCategory.hom (FC := FC) (CC := CC) D.L₂.f : (a : CC D.L₂.X₁) → CC D.L₂.X₂) x₁ : CC D.L₂.X₂)

Tactic:
exact h₁.symm

Premises used: Eq.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
⊢ S.HasHomology

Tactic:
HasHomology.mk' h.condition.choose

Premises used: CategoryTheory.ShortComplex.Exact.condition, CategoryTheory.ShortComplex.HasHomology.mk', Exists.choose
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.Exact
⊢ HasZeroObject.{v_1, u_1} C

Tactic:
⟨h.condition.choose.left.H, h.condition.choose_spec⟩

Premises used: Exists.choose_spec, CategoryTheory.Limits.HasZeroObject.mk, CategoryTheory.ShortComplex.Exact.condition, CategoryTheory.ShortComplex.HomologyData.left, Exists.intro, Exists.choose, CategoryTheory.ShortComplex.LeftHomologyData.H
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
mp : S.Exact → IsZero.{v_1, u_1} S.homology
mpr : IsZero.{v_1, u_1} S.homology → S.Exact
⊢ S.Exact ↔ IsZero.{v_1, u_1} S.homology

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h' : S.HomologyData
z : IsZero.{v_1, u_1} h'.left.H
⊢ IsZero.{v_1, u_1} S.homology

Tactic:
IsZero.of_iso z h'.left.homologyIso

Premises used: CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.Limits.IsZero.of_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h' : S.HomologyData
z : IsZero.{v_1, u_1} h'.left.H
⊢ IsZero.{v_1, u_1} S.homology

Tactic:
exact IsZero.of_iso z h'.left.homologyIso

Premises used: CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.Limits.IsZero.of_iso
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
⊢ S.Exact

Tactic:
⟨⟨_, h⟩⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, Exists.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
⊢ S.Exact

Tactic:
exact ⟨⟨_, h⟩⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
rw : IsZero.{v_1, u_1} S.homology ↔ IsZero.{v_1, u_1} h.H
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.H

Tactic:
rw [S.exact_iff_isZero_homology]

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
⊢ IsZero.{v_1, u_1} S.homology ↔ IsZero.{v_1, u_1} h.H

Tactic:
Iso.isZero_iff h.homologyIso

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.Iso.isZero_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
⊢ IsZero.{v_1, u_1} S.homology ↔ IsZero.{v_1, u_1} h.H

Tactic:
exact Iso.isZero_iff h.homologyIso

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.Iso.isZero_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
rw : IsZero.{v_1, u_1} S.homology ↔ IsZero.{v_1, u_1} h.H
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.H

Tactic:
rw [S.exact_iff_isZero_homology]

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ IsZero.{v_1, u_1} S.homology ↔ IsZero.{v_1, u_1} h.H

Tactic:
Iso.isZero_iff h.homologyIso

Premises used: CategoryTheory.ShortComplex.RightHomologyData.homologyIso, CategoryTheory.Iso.isZero_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ IsZero.{v_1, u_1} S.homology ↔ IsZero.{v_1, u_1} h.H

Tactic:
exact Iso.isZero_iff h.homologyIso

Premises used: CategoryTheory.ShortComplex.RightHomologyData.homologyIso, CategoryTheory.Iso.isZero_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
⊢ S.Exact ↔ IsZero.{v_1, u_1} S.leftHomology

Tactic:
LeftHomologyData.exact_iff _

Premises used: CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.LeftHomologyData.exact_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
⊢ S.Exact ↔ IsZero.{v_1, u_1} S.rightHomology

Tactic:
RightHomologyData.exact_iff _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.RightHomologyData.exact_iff