awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
rw :
  Function.Surjective (α := (↑S.X₁ : Type u)) (β := (↑S.abLeftHomologyData.K : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (AddCommGrpCat.ofHom S.abToCycles)) :
        (a : (↑S.X₁ : Type u)) → (↑S.abLeftHomologyData.K : Type u)) ↔
    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)
⊢ S.Exact ↔
    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:
rw [S.abLeftHomologyData.exact_iff_epi_f', abLeftHomologyData_f',
    AddCommGrpCat.epi_iff_surjective]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f', AddCommGrpCat.epi_iff_surjective, CategoryTheory.ShortComplex.abLeftHomologyData_f', CategoryTheory.ShortComplex.abLeftHomologyData
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
⊢ Function.Surjective (α := (↑S.X₁ : Type u)) (β := (↑S.abLeftHomologyData.K : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (AddCommGrpCat.ofHom S.abToCycles)) :
        (a : (↑S.X₁ : Type u)) → (↑S.abLeftHomologyData.K : Type u)) ↔
    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:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
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₂
⊢ 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₂

Tactic:
rw [exact_iff_surjective_abToCycles]

Premises used: CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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₂
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)
⊢ 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
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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))
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₂
⊢ ∃ (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₂⟩

Premises used: Subtype.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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)
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)
⊢ (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:
simpa only [Subtype.ext_iff, abToCycles_apply_coe] using hx₁

Premises used: CategoryTheory.ShortComplex.abToCycles_apply_coe, Subtype.ext_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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)
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:
exact ⟨x₁, by simpa only [Subtype.ext_iff, abToCycles_apply_coe] using hx₁⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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
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)
⊢ ∃ (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₂

Tactic:
obtain ⟨x₁, rfl⟩ := h x₂ hx₂

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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₂ :
  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:
⟨x₁, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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₂ :
  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:
exact ⟨x₁, rfl⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
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))
⊢ 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))

Tactic:
rw [S.ab_exact_iff]

Premises used: CategoryTheory.ShortComplex.ab_exact_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
Goal:
S : ShortComplex Ab
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)
⊢ (∀ (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:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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₂

Tactic:
⟨h, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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₂
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))
⊢ 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:
refine ⟨h, ?_⟩