awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑y.left : Type u_2)
ha' : (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2)) a' = a
a'' : (↑P : Type u_2)
ha'' :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2)) (CC :=
          ModuleCat.carrier) q :
        (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
      a'' =
    a'
refine_2 :
  (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) p :
            (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
          a'' :
        (↑x.left : Type u_2)) =
    a
⊢ (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) p :
            (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
          a'' :
        (↑x.left : Type u_2)) =
    a

Tactic:
dsimp at ha' ⊢
-- Module: Mathlib.CategoryTheory.Abelian.Pseudoelements
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u_2, u_1} R
x y : Over G
P : ModuleCat.{u_2, u_1} R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : (↑G : Type u_2)
a' : (↑y.left : Type u_2)
ha' : (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2)) a' = a
a'' : (↑P : Type u_2)
ha'' :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2)) (CC :=
          ModuleCat.carrier) q :
        (a : (↑P : Type u_2)) → (↑y.left : Type u_2))
      a'' =
    a'
refine_2 :
  (ModuleCat.Hom.hom x.hom ∘ₗ
          ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
            (CC := ModuleCat.carrier) p :
        (a : (↑P : Type u_2)) → (↑G : Type u_2))
      a'' =
    a
refine_2₁ : (ModuleCat.Hom.hom (p ≫ x.hom) : (a : (↑P : Type u_2)) → (↑G : Type u_2)) a'' = a
refine_2₂ : (ModuleCat.Hom.hom (q ≫ y.hom) : (a : (↑P : Type u_2)) → (↑G : Type u_2)) a'' = a
refine_2₃ : (ModuleCat.Hom.hom y.hom ∘ₗ ModuleCat.Hom.hom q : (a : (↑P : Type u_2)) → (↑G : Type u_2)) a'' = a
refine_2₄ :
  (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2))
      ((ModuleCat.Hom.hom q : (a : (↑P : Type u_2)) → (↑y.left : Type u_2)) a'' : (↑y.left : Type u_2)) =
    a
refine_2₅ : (ModuleCat.Hom.hom y.hom : (a : (↑y.left : Type u_2)) → (↑G : Type u_2)) a' = a
refine_2₆ refine_2₇ : a = a
⊢ (ModuleCat.Hom.hom x.hom : (a : (↑x.left : Type u_2)) → (↑G : Type u_2))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_2, u_1} R) ↦ (↑x1 : Type u_2) →ₗ[R] (↑x2 : Type u_2))
              (CC := ModuleCat.carrier) p :
            (a : (↑P : Type u_2)) → (↑x.left : Type u_2))
          a'' :
        (↑x.left : Type u_2)) =
    a

Tactic:
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, H, ModuleCat.hom_comp, LinearMap.comp_apply,
      ha'', ha']

Premises used: LinearMap.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
mp : Epi f → ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
mpr : (∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f) → Epi f
⊢ Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : Epi f
A : C
a : A ⟶ Y
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ a = x ≫ f

Tactic:
⟨pullback a f, pullback.fst a f, inferInstance, pullback.snd a f, pullback.condition⟩

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.Limits.pullback.snd, inferInstance, CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
h : Epi f
A : C
a : A ⟶ Y
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ a = x ≫ f

Tactic:
exact ⟨pullback a f, pullback.fst a f, inferInstance, pullback.snd a f, pullback.condition⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
mpr : ∀ (A : C) (π : A ⟶ Y) (hπ : Epi π) (a' : A ⟶ X) (fac : π ≫ 𝟙 Y = a' ≫ f), Epi f
⊢ Epi f

Tactic:
obtain ⟨A, π, hπ, a', fac⟩ := hf (𝟙 Y)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π ≫ 𝟙 Y = a' ≫ f
⊢ π = a' ≫ f

Tactic:
rw [comp_id] at fac

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π = a' ≫ f
⊢ Epi f

Tactic:
epi_of_epi_fac fac.symm

Premises used: CategoryTheory.epi_of_epi_fac, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hf : ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
A : C
π : A ⟶ Y
hπ : Epi π
a' : A ⟶ X
fac : π = a' ≫ f
⊢ Epi f

Tactic:
exact epi_of_epi_fac fac.symm

Premises used: CategoryTheory.epi_of_epi_fac, Eq.symm
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_2 : Epi f
A : C
y : A ⟶ Y
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f

Tactic:
(epi_iff_surjective_up_to_refinements f).1 inferInstance y

Premises used: inferInstance, Iff.mp, CategoryTheory.epi_iff_surjective_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
rw :
  (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
⊢ S.Exact ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Tactic:
rw [S.exact_iff_epi_toCycles, epi_iff_surjective_up_to_refinements]

Premises used: CategoryTheory.ShortComplex.exact_iff_epi_toCycles, CategoryTheory.epi_iff_surjective_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
mp :
  (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles) →
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
mpr :
  (∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
mp :
  ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π) (x₁ : A' ⟶ S.X₁)
    (fac : Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles a ha) (x₁ ≫ S.toCycles)),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ a = x₁ ≫ S.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ a = x₁ ≫ S.f

Tactic:
obtain ⟨A', π, hπ, x₁, fac⟩ := hS (S.liftCycles a ha)

Premises used: CategoryTheory.ShortComplex.liftCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles a ha) (x₁ ≫ S.toCycles)
⊢ π ≫ a = x₁ ≫ S.f

Tactic:
simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.toCycles_i, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ y = x ≫ S.toCycles
A : C
a : A ⟶ S.X₂
ha : a ≫ S.g = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : Eq (α := A' ⟶ S.cycles) (π ≫ S.liftCycles a ha) (x₁ ≫ S.toCycles)
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ a = x₁ ≫ S.f

Tactic:
exact ⟨A', π, hπ, x₁, by simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
⊢ (a ≫ S.iCycles) ≫ S.g = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
mpr :
  ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π) (x₁ : A' ⟶ S.X₁) (fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ a = x ≫ S.toCycles
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ a = x ≫ S.toCycles

Tactic:
obtain ⟨A', π, hπ, x₁, fac⟩ := hS (a ≫ S.iCycles) (by simp)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f
⊢ π ≫ a = x₁ ≫ S.toCycles

Tactic:
simp only [← cancel_mono S.iCycles, assoc, toCycles_i, fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.toCycles_i, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
A : C
a : A ⟶ S.cycles
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.X₁
fac : π ≫ a ≫ S.iCycles = x₁ ≫ S.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S.X₁), π ≫ a = x ≫ S.toCycles

Tactic:
exact ⟨A', π, hπ, x₁, by simp only [← cancel_mono S.iCycles, assoc, toCycles_i, fac]⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
rw :
  ∀
    (hS :
      ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f)
    {A : C} (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements] at hS

Premises used: CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Tactic:
hS x₂ hx₂
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f

Tactic:
exact hS x₂ hx₂
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
obtain :
  ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π) (z : A' ⟶ S.cycles) (hz : π ≫ γ = z ≫ S.homologyπ),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ

Tactic:
obtain ⟨A', π, hπ, z, hz⟩ := surjective_up_to_refinements_of_epi S.homologyπ γ

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.surjective_up_to_refinements_of_epi
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
⊢ (z ≫ S.iCycles) ≫ S.g = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
refine : π ≫ γ = S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0), π ≫ γ = S.liftCycles z hz ≫ S.homologyπ

Tactic:
refine ⟨A', π, hπ, z ≫ S.iCycles, by simp, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
rw : Eq (α := A' ⟶ S.homology) (z ≫ S.homologyπ) (S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ)
⊢ π ≫ γ = S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ

Tactic:
rw [hz]
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
e_a : z = S.liftCycles (z ≫ S.iCycles) ⋯
⊢ Eq (α := A' ⟶ S.homology) (z ≫ S.homologyπ) (S.liftCycles (z ≫ S.iCycles) ⋯ ≫ S.homologyπ)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
A : C
γ : A ⟶ S.homology
A' : C
π : A' ⟶ A
hπ : Epi π
z : A' ⟶ S.cycles
hz : π ≫ γ = z ≫ S.homologyπ
e_a : z ≫ S.iCycles = CategoryStruct.comp (Y := S.cycles) (S.liftCycles (z ≫ S.iCycles) ⋯) S.iCycles
e_a₁ e_a₂ : z ≫ S.iCycles = z ≫ S.iCycles
⊢ z = S.liftCycles (z ≫ S.iCycles) ⋯

Tactic:
rw [← cancel_mono S.iCycles, liftCycles_i]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ y ≫ Cofork.π c = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f

Tactic:
⟨fun hy ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
refine_1 : ∀ (hy : y ≫ Cofork.π c = 0), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
refine_2 : (∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f) → y ≫ Cofork.π c = 0
⊢ y ≫ Cofork.π c = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f

Tactic:
refine ⟨fun hy ↦ ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
⊢ Cofork.π c ≫ Iso.hom (Iso.refl c.pt) =
    Cofork.π
      (CokernelCofork.ofπ
        { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
⊢ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact

Tactic:
have h := (ShortComplex.mk _ _ c.condition).exact_of_g_is_cokernel
      (IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _) (by simp)))
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h : { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
⊢ ∀ ⦃A : C⦄
    (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂),
    x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
        A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁),
        π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements] at h

Premises used: CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h :
  ∀ ⦃A : C⦄
    (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂),
    x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
        A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁),
        π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
refine_1 :
  ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π)
    (x₁ : A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁)
    (fac : π ≫ y = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f

Tactic:
obtain ⟨A', π, hπ, x₁, fac⟩ := h y hy
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h :
  ∀ ⦃A : C⦄
    (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂),
    x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
        A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁),
        π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁
fac : π ≫ y = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f

Tactic:
⟨A', π, hπ, x₁, fac⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h :
  ∀ ⦃A : C⦄
    (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂),
    x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ :
        A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁),
        π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁
fac : π ≫ y = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ X), π ≫ y = x ≫ f

Tactic:
exact ⟨A', π, hπ, x₁, fac⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
A' : C
π : A' ⟶ A
hπ : Epi π
x : A' ⟶ X
fac : π ≫ y = x ≫ f
⊢ y ≫ Cofork.π c = 0

Tactic:
simp [← cancel_epi π, reassoc_of% fac, condition]

Premises used: CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.cancel_epi