awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (hypothesis)
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))
⊢ 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₁)
have this₁ : 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 _ _
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (hypothesis)
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) 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₁)
have 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₁)
Tactic: have eq := CategoryTheory.congr_fun (D.snd_δ)
    (Limits.Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (hypothesis)
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 (α := 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₁)
have 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₂
Tactic: have eq₁ := Concrete.pullbackMk_fst D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (hypothesis)
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₂
⊢ 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₁)
have 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₃
Tactic: have eq₂ := Concrete.pullbackMk_snd D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory (goal)
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₁)
have refine : (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₂) =
  x₁
Tactic: refine eq.trans (CategoryTheory.congr_arg (D.v₂₃.τ₁) ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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.homology
have mp : S.Exact → IsZero.{v_1, u_1} S.homology
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.Exact ↔ IsZero.{v_1, u_1} S.homology
have mpr : IsZero.{v_1, u_1} S.homology → S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.H
have rw : IsZero.{v_1, u_1} S.homology ↔ IsZero.{v_1, u_1} h.H
Tactic: rw [S.exact_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.H
have rw : IsZero.{v_1, u_1} S.homology ↔ IsZero.{v_1, u_1} h.H
Tactic: rw [S.exact_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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.HomologyData
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.left.H
have this : S.HasHomology
Tactic: haveI := HasHomology.mk' h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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.HomologyData
⊢ S.Exact ↔ IsZero.{v_1, u_1} h.right.H
have this : S.HasHomology
Tactic: haveI := HasHomology.mk' h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
inst_3 : HasZeroObject.{v_1, u_1} C
⊢ S.Exact ↔ Nonempty.{v_1 + 1} (S.homology ≅ 0)
have rw : IsZero.{v_1, u_1} S.homology ↔ Nonempty.{v_1 + 1} (S.homology ≅ 0)
Tactic: rw [exact_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
inst_3 : HasZeroObject.{v_1, u_1} C
⊢ IsZero.{v_1, u_1} S.homology ↔ Nonempty.{v_1 + 1} (S.homology ≅ 0)
have mp : IsZero.{v_1, u_1} S.homology → Nonempty.{v_1 + 1} (S.homology ≅ 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
inst_3 : HasZeroObject.{v_1, u_1} C
mp : IsZero.{v_1, u_1} S.homology → Nonempty.{v_1 + 1} (S.homology ≅ 0)
⊢ IsZero.{v_1, u_1} S.homology ↔ Nonempty.{v_1 + 1} (S.homology ≅ 0)
have mpr : Nonempty.{v_1 + 1} (S.homology ≅ 0) → IsZero.{v_1, u_1} S.homology
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h : S₁.Exact
⊢ S₂.Exact
have obtain : ∀ (h : S₁.HomologyData) (z : IsZero.{v_1, u_1} h.left.H), S₂.Exact
Tactic: obtain ⟨⟨h, z⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
have this : Mono S₁.f ↔ Mono S₂.f
Tactic: have : Mono S₁.f ↔ Mono S₂.f :=
    (MorphismProperty.monomorphisms C).arrow_mk_iso_iff
      (Arrow.isoMk (ShortComplex.π₁.mapIso e) (ShortComplex.π₂.mapIso e) e.hom.comm₁₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
this : Mono S₁.f ↔ Mono S₂.f
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
have rw : S₂.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
Tactic: rw [exact_iff_of_iso e, this]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
this : Mono S₁.f ↔ Mono S₂.f
rw : S₂.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
⊢ S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f
have rw₁ : S₂.Exact ∧ Mono S₂.f ↔ S₂.Exact ∧ Mono S₂.f
Tactic: rw [exact_iff_of_iso e, this]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
⊢ S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g
have this : Epi S₁.g ↔ Epi S₂.g
Tactic: have : Epi S₁.g ↔ Epi S₂.g :=
    (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
      (Arrow.isoMk (ShortComplex.π₂.mapIso e) (ShortComplex.π₃.mapIso e) e.hom.comm₂₃)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
this : Epi S₁.g ↔ Epi S₂.g
⊢ S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g
have rw : S₂.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g
Tactic: rw [exact_iff_of_iso e, this]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
this : Epi S₁.g ↔ Epi S₂.g
rw : S₂.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g
⊢ S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g
have rw₁ : S₂.Exact ∧ Epi S₂.g ↔ S₂.Exact ∧ Epi S₂.g
Tactic: rw [exact_iff_of_iso e, this]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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 : IsZero.{v_1, u_1} S.X₂
⊢ S.Exact
have rw : IsZero.{v_1, u_1} (HomologyData.ofZeros S sorry sorry).left.H
Tactic: rw [(HomologyData.ofZeros S (IsZero.eq_of_tgt h _ _) (IsZero.eq_of_src h _ _)).exact_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ S₁.Exact ↔ S₂.Exact
have mp : S₁.Exact → S₂.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
mp : S₁.Exact → S₂.Exact
⊢ S₁.Exact ↔ S₂.Exact
have mpr : S₂.Exact → S₁.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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.HomologyData
⊢ S.Exact ↔ h.left.i ≫ h.right.p = 0
have this : S.HasHomology
Tactic: haveI := HasHomology.mk' h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ h.left.i ≫ h.right.p = 0
have rw : IsZero.{v_1, u_1} h.left.H ↔ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
Tactic: rw [h.left.exact_iff, ← h.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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.HomologyData
this : S.HasHomology
⊢ IsZero.{v_1, u_1} h.left.H ↔ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
have mp : IsZero.{v_1, u_1} h.left.H → h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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.HomologyData
this : S.HasHomology
mp : IsZero.{v_1, u_1} h.left.H → h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
⊢ IsZero.{v_1, u_1} h.left.H ↔ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
have mpr : h.left.π ≫ h.iso.hom ≫ h.right.ι = 0 → IsZero.{v_1, u_1} h.left.H
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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.HomologyData
this : S.HasHomology
z : IsZero.{v_1, u_1} h.left.H
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
have mp : h.left.π ≫ 0 ≫ h.right.ι = 0
Tactic: rw [IsZero.eq_of_src z h.iso.hom 0, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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.HomologyData
this : S.HasHomology
z : IsZero.{v_1, u_1} h.left.H
mp : h.left.π ≫ 0 ≫ h.right.ι = 0
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
have mp₁ : Eq (α := h.left.K ⟶ h.right.Q) (h.left.π ≫ 0) 0
Tactic: rw [IsZero.eq_of_src z h.iso.hom 0, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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.HomologyData
this : S.HasHomology
z : IsZero.{v_1, u_1} h.left.H
mp : h.left.π ≫ 0 ≫ h.right.ι = 0
mp₁ : Eq (α := h.left.K ⟶ h.right.Q) (h.left.π ≫ 0) 0
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
have mp₂ : Eq.{v_1 + 1} (α := h.left.K ⟶ h.right.Q) 0 0
Tactic: rw [IsZero.eq_of_src z h.iso.hom 0, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
inst_3 : HasKernel S.g
inst_4 : HasCokernel S.f
⊢ S.Exact ↔ Eq (α := kernel S.g ⟶ cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0
have this : HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f sorry)
Tactic: haveI := HasLeftHomology.hasCokernel S