awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ S.Exact ↔
    ∀ (x₂ : (↑S.X₂ : Type u)),
      Eq (α := (↑S.X₃ : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.g :
                (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
              x₂ :
            (↑S.X₃ : Type u))
          (0 : (↑S.X₃ : Type u)) →
        ∃ (x₁ : (↑S.X₁ : Type u)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.f :
                (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
              x₁ =
            x₂
have rw : Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
    (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) ↔
  ∀ (x₂ : (↑S.X₂ : Type u)),
    Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂
Tactic: rw [exact_iff_surjective_abToCycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
      (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) ↔
    ∀ (x₂ : (↑S.X₂ : Type u)),
      Eq (α := (↑S.X₃ : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.g :
                (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
              x₂ :
            (↑S.X₃ : Type u))
          (0 : (↑S.X₃ : Type u)) →
        ∃ (x₁ : (↑S.X₁ : Type u)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.f :
                (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
              x₁ =
            x₂
have mp : Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
    (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) →
  ∀ (x₂ : (↑S.X₂ : Type u)),
    Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
mp :
  Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
      (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) →
    ∀ (x₂ : (↑S.X₂ : Type u)),
      Eq (α := (↑S.X₃ : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.g :
                (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
              x₂ :
            (↑S.X₃ : Type u))
          (0 : (↑S.X₃ : Type u)) →
        ∃ (x₁ : (↑S.X₁ : Type u)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.f :
                (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
              x₁ =
            x₂
⊢ Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
      (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) ↔
    ∀ (x₂ : (↑S.X₂ : Type u)),
      Eq (α := (↑S.X₃ : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.g :
                (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
              x₂ :
            (↑S.X₃ : Type u))
          (0 : (↑S.X₃ : Type u)) →
        ∃ (x₁ : (↑S.X₁ : Type u)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.f :
                (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
              x₁ =
            x₂
have mpr : (∀ (x₂ : (↑S.X₂ : Type u)),
    Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂) →
  Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
    (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
h :
  Function.Surjective (α := (↑S.X₁ : Type u)) (β := ↥(AddCommGrpCat.Hom.hom S.g).ker)
    (⇑S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker)
x₂ : (↑S.X₂ : Type u)
hx₂ :
  Eq (α := (↑S.X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.g :
          (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
        x₂ :
      (↑S.X₃ : Type u))
    (0 : (↑S.X₃ : Type u))
⊢ ∃ (x₁ : (↑S.X₁ : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.f :
          (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
        x₁ =
      x₂
have mp : ∀ (x₁ : (↑S.X₁ : Type u))
  (hx₁ :
    Eq (α := ↥(AddCommGrpCat.Hom.hom S.g).ker)
      ((S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) x₁ : ↥(AddCommGrpCat.Hom.hom S.g).ker)
      (Subtype.mk (p := fun (x : (↑S.X₂ : Type u)) ↦ x ∈ (AddCommGrpCat.Hom.hom S.g).ker) x₂ hx₂ :
        ↥(AddCommGrpCat.Hom.hom S.g).ker)),
  ∃ (x₁ : (↑S.X₁ : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.f :
          (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
        x₁ =
      x₂
Tactic: obtain ⟨x₁, hx₁⟩ := h ⟨x₂, hx₂⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
h :
  ∀ (x₂ : (↑S.X₂ : Type u)),
    Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂
x₂ : (↑S.X₂ : Type u)
hx₂ : x₂ ∈ (AddCommGrpCat.Hom.hom S.g).ker
⊢ ∃ (a : (↑S.X₁ : Type u)),
    (S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) a =
      Subtype.mk (p := fun (x : (↑S.X₂ : Type u)) ↦ x ∈ (AddCommGrpCat.Hom.hom S.g).ker) x₂ hx₂
have mpr : ∀ (x₁ : (↑S.X₁ : Type u))
  (hx₂ :
    Membership.mem (α := (↑S.X₂ : Type u)) (AddCommGrpCat.Hom.hom S.g).ker
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.f :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
          x₁ :
        (↑S.X₂ : Type u))),
  ∃ (a : (↑S.X₁ : Type u)),
    Eq (α := ↥(AddCommGrpCat.Hom.hom S.g).ker)
      ((S.abToCycles : (a : (↑S.X₁ : Type u)) → ↥(AddCommGrpCat.Hom.hom S.g).ker) a : ↥(AddCommGrpCat.Hom.hom S.g).ker)
      (Subtype.mk (p := fun (x : (↑S.X₂ : Type u)) ↦ x ∈ (AddCommGrpCat.Hom.hom S.g).ker)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁)
          hx₂ :
        ↥(AddCommGrpCat.Hom.hom S.g).ker)
Tactic: obtain ⟨x₁, rfl⟩ := h x₂ hx₂
Cleared hypotheses: x₂, hx₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ S.Exact ↔
    Function.Exact (M := (↑S.X₁ : Type u)) (N := (↑S.X₂ : Type u)) (P := (↑S.X₃ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.f) :
        (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.g) :
        (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
have rw : (∀ (x₂ : (↑S.X₂ : Type u)),
    Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂) ↔
  Function.Exact (M := (↑S.X₁ : Type u)) (N := (↑S.X₂ : Type u)) (P := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) S.f) :
      (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
Tactic: rw [S.ab_exact_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ (∀ (x₂ : (↑S.X₂ : Type u)),
      Eq (α := (↑S.X₃ : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.g :
                (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
              x₂ :
            (↑S.X₃ : Type u))
          (0 : (↑S.X₃ : Type u)) →
        ∃ (x₁ : (↑S.X₁ : Type u)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) S.f :
                (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
              x₁ =
            x₂) ↔
    Function.Exact (M := (↑S.X₁ : Type u)) (N := (↑S.X₂ : Type u)) (P := (↑S.X₃ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.f) :
        (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.g) :
        (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
have h : ∀ (a : (↑S.X₂ : Type u)),
  (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            a :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          a) ↔
    (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            a :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) ↔
      Membership.mem (γ := Set (↑S.X₂ : Type u))
        (Set.range (ι := (↑S.X₁ : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f) :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
        a)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
x₂ : (↑S.X₂ : Type u)
⊢ (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂) ↔
    (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) ↔
      Membership.mem (γ := Set (↑S.X₂ : Type u))
        (Set.range (ι := (↑S.X₁ : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f) :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
        x₂)
have h : (Eq (α := (↑S.X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂ :
        (↑S.X₃ : Type u))
      (0 : (↑S.X₃ : Type u)) →
    ∃ (x₁ : (↑S.X₁ : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.f :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
          x₁ =
        x₂) →
  (Eq (α := (↑S.X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂ :
        (↑S.X₃ : Type u))
      (0 : (↑S.X₃ : Type u)) ↔
    Membership.mem (γ := Set (↑S.X₂ : Type u))
      (Set.range (ι := (↑S.X₁ : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.f) :
          (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
      x₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
x₂ : (↑S.X₂ : Type u)
h :
  Eq (α := (↑S.X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂ :
        (↑S.X₃ : Type u))
      (0 : (↑S.X₃ : Type u)) →
    ∃ (x₁ : (↑S.X₁ : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.f :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
          x₁ =
        x₂
⊢ Eq (α := (↑S.X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂ :
        (↑S.X₃ : Type u))
      (0 : (↑S.X₃ : Type u)) ↔
    Membership.mem (γ := Set (↑S.X₂ : Type u))
      (Set.range (ι := (↑S.X₁ : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.f) :
          (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
      x₂
have h₁ : Membership.mem (γ := Set (↑S.X₂ : Type u))
    (Set.range (ι := (↑S.X₁ : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.f) :
        (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
    x₂ →
  Eq (α := (↑S.X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.g :
          (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
        x₂ :
      (↑S.X₃ : Type u))
    (0 : (↑S.X₃ : Type u))
Tactic: refine ⟨h, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
x₂ : (↑S.X₂ : Type u)
⊢ (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) ↔
      Membership.mem (γ := Set (↑S.X₂ : Type u))
        (Set.range (ι := (↑S.X₁ : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f) :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
        x₂) →
    Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂
have h : Eq (α := (↑S.X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) S.g :
          (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
        x₂ :
      (↑S.X₃ : Type u))
    (0 : (↑S.X₃ : Type u)) →
  Membership.mem (γ := Set (↑S.X₂ : Type u))
      (Set.range (ι := (↑S.X₁ : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.f) :
          (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
      x₂ →
    Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ S.Exact ↔ (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
have rw : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range ↔
  (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
Tactic: rw [ab_exact_iff_ker_le_range]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
⊢ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range ↔
    (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
have mp : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range →
  (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
mp :
  (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range →
    (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
⊢ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range ↔
    (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
have mpr : (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker →
  (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
⊢ (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
have mp : (AddCommGrpCat.Hom.hom S.f).range ≤ (AddCommGrpCat.Hom.hom S.g).ker
Tactic: refine le_antisymm ?_ h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
x₁ : (↑S.X₁ : Type u)
⊢ Membership.mem (α := (↑S.X₂ : Type u)) (AddCommGrpCat.Hom.hom S.g).ker
    ((AddCommGrpCat.Hom.hom S.f : (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)) x₁ : (↑S.X₂ : Type u))
have mp : Eq (α := (↑S.X₃ : Type u))
  ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
          (fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) AddCommGrpCat.carrier _ _ S.X₁ S.X₃ 0 :
        (a : (↑S.X₁ : Type u)) → (↑S.X₃ : Type u))
      x₁ :
    (↑S.X₃ : Type u))
  (0 : (↑S.X₃ : Type u))
Tactic: rw [AddMonoidHom.mem_ker, ← ConcreteCategory.comp_apply, S.zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker
⊢ (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
have mpr : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.g).ker
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (hypothesis)
Goal:
S : ShortComplex Ab
hS : S.Exact
inst : Finite.{u + 1} (↑S.X₁ : Type u)
inst_1 : Finite.{u + 1} (↑S.X₃ : Type u)
⊢ Finite.{u + 1} (↑S.X₂ : Type u)
have this : Finite.{u + 1} ↥(AddCommGrpCat.Hom.hom S.f).range
Tactic: have : Finite S.f.hom.range := Set.finite_range _