awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type)
hf : (↑x : (↑H : Type)) = (Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x
⊢ Eq (α := (↑H : Type))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
            (F'.e ≫ F'.m) :
          (a : (↑G : Type)) → (↑H : Type))
        (↑(Classical.indefiniteDescription
              (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
          (↑G : Type)) :
      (↑H : Type))
    ((Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x : (↑H : Type))

Tactic:
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, Classical.indefiniteDescription, Subtype.property
-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x : (↑(image f) : Type)
⊢ (↑x : (↑H : Type)) = (Hom.hom (ι f) : (a : (↑(image f) : Type)) → (↑H : Type)) x

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
I : Ideal ℤ
g : ↥I →ₗ[ℤ] A
rcases :
  ∀ (m : ℤ) (g : ↥(ℤ ∙ m) →ₗ[ℤ] A),
    ∃ (g' : ℤ →ₗ[ℤ] A),
      ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
        Eq (α := A) ((g' : (a : ℤ) → A) x : A)
          ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : x ∈ I),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A) ((g : (a : ↥I) → A) (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ I) x mem) : A)

Tactic:
rcases IsPrincipalIdealRing.principal I with ⟨m, rfl⟩

Premises used: IsPrincipalIdealRing.principal, rfl
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
inl :
  ∀ (g : ↥(ℤ ∙ 0) →ₗ[ℤ] A),
    ∃ (g' : ℤ →ₗ[ℤ] A),
      ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x),
        Eq (α := A) ((g' : (a : ℤ) → A) x : A)
          ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) x mem) : A)
inr :
  ∀ (h0 : m ≠ 0),
    ∃ (g' : ℤ →ₗ[ℤ] A),
      ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
        Eq (α := A) ((g' : (a : ℤ) → A) x : A)
          ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)

Tactic:
obtain rfl | h0 := eq_or_ne m 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) x mem) : A)

Tactic:
⟨0, fun n hn ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
inl :
  ∀ (n : ℤ) (hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) n),
    Eq.{u + 1} (α := A) ((0 : (a : ℤ) → A) n : A)
      ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) n hn) : A)
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) x mem) : A)

Tactic:
refine ⟨0, fun n hn ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) n
⊢ Membership.mem (γ := Ideal ℤ) ⊥ n

Tactic:
rw [Submodule.span_zero_singleton] at hn

Premises used: Submodule.span_zero_singleton
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn_1 : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) n
hn : Membership.mem (γ := Ideal ℤ) ⊥ n
inl :
  ∀ (hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) 0),
    Eq (α := A) ((0 : (a : ℤ) → A) 0 : A)
      ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) 0 hn) : A)
⊢ Eq.{u + 1} (α := A) ((0 : (a : ℤ) → A) n : A)
    ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) n hn_1) : A)

Tactic:
subst hn
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) 0
⊢ Eq (α := A) ((0 : (a : ℤ) → A) 0 : A)
    ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) 0 hn) : A)

Tactic:
(map_zero g).symm

Premises used: Set.Mem, map_zero, Eq.symm
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) 0
⊢ Eq (α := A) ((0 : (a : ℤ) → A) 0 : A)
    ((g : (a : ↥(ℤ ∙ 0)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ 0) x) 0 hn) : A)

Tactic:
exact (map_zero g).symm

Premises used: map_zero, Eq.symm
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := (g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) m ⋯)
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)

Tactic:
⟨LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m), fun n hn ↦ ?_⟩

Premises used: Int, DivisibleBy.div, Exists.intro, LinearMap.toSpanSingleton
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := (g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) m ⋯)
inr :
  ∀ (n : ℤ) (hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) n),
    Eq (α := A)
      ((LinearMap.toSpanSingleton ℤ A
              (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ gₘ m) :
            (a : ℤ) → A)
          n :
        A)
      ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) n hn) : A)
⊢ ∃ (g' : ℤ →ₗ[ℤ] A),
    ∀ (x : ℤ) (mem : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x),
      Eq (α := A) ((g' : (a : ℤ) → A) x : A)
        ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) x mem) : A)

Tactic:
refine ⟨LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m), fun n hn ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := (g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) m ⋯)
n : ℤ
hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) n
inr :
  ∀ (n : ℤ) (hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) (n • m)),
    Eq (α := A)
      ((LinearMap.toSpanSingleton ℤ A
              (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ gₘ m) :
            (a : ℤ) → A)
          (n • m) :
        A)
      ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) (n • m) hn) :
        A)
⊢ Eq (α := A)
    ((LinearMap.toSpanSingleton ℤ A
            (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ gₘ m) :
          (a : ℤ) → A)
        n :
      A)
    ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) n hn) : A)

Tactic:
rcases Submodule.mem_span_singleton.mp hn with ⟨n, rfl⟩

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
m : ℤ
g : ↥(ℤ ∙ m) →ₗ[ℤ] A
h0 : m ≠ 0
gₘ : A := (g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) m ⋯)
n : ℤ
hn : Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) (n • m)
inr :
  HSMul.hSMul (β := A) n
      ((LinearMap.toSpanSingleton ℤ A
              (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ gₘ m) :
            (a : ℤ) → A)
          m :
        A) =
    (g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) (n • m) hn)
inr₁ :
  n • m • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ gₘ m =
    (g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) (n • m) hn)
inr₂ :
  n • gₘ = (g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) (n • m) hn)
inr₃ :
  Eq (α := A)
    ((g : (a : ↥(ℤ ∙ m)) → A)
        (HSMul.hSMul (β := ↥(ℤ ∙ m)) n (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) m ⋯)) :
      A)
    ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) (n • m) hn) : A)
inr₄ inr₅ :
  Eq (α := A)
    ((g : (a : ↥(ℤ ∙ m)) → A)
        (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submodule ℤ ℤ) (ℤ ∙ m) x) (n • m) ⋯) :
      A)
    ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) (n • m) hn) : A)
⊢ Eq (α := A)
    ((LinearMap.toSpanSingleton ℤ A
            (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ gₘ m) :
          (a : ℤ) → A)
        (n • m) :
      A)
    ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) (n • m) hn) : A)

Tactic:
rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g,
    SetLike.mk_smul_mk]

Premises used: LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel, SetLike.mk_smul_mk, map_zsmul
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
⊢ Injective (C := ModuleCat ℤ) (ModuleCat.of ℤ A) ↔ Injective (of A)

Tactic:
((forget₂ (ModuleCat ℤ) AddCommGrpCat).asEquivalence.map_injective_iff (ModuleCat.of ℤ A)).symm

Premises used: CategoryTheory.Equivalence.map_injective_iff, ModuleCat, Int, CategoryTheory.Functor.asEquivalence, ModuleCat.of, CategoryTheory.forget₂, AddCommGrpCat, Iff.symm
-- Module: Mathlib.Algebra.Category.Grp.Injective
Goal:
A : Type u
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
⊢ Injective (of A)

Tactic:
(injective_as_module_iff A).mp <|
    Module.injective_object_of_injective_module (inj := (Module.Baer.of_divisible A).injective)

Premises used: AddCommGrpCat.injective_as_module_iff, Iff.mp, Module.injective_object_of_injective_module
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M : AddCommGrpCat
⊢ M.isFinite ↔ Finite.{u + 1} (↑M : Type u)

Tactic:
Iff.rfl

Premises used: Iff.rfl, AddCommGrpCat.isFinite
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
⊢ Finite.{u + 1} (↑(of PUnit.{u + 1}) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf : Mono f
hN : N.isFinite
⊢ Function.Injective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))

Tactic:
rw [AddCommGrpCat.mono_iff_injective] at hf

Premises used: AddCommGrpCat.mono_iff_injective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf : Mono f
hN : N.isFinite
hf₁ :
  Function.Injective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))
⊢ N.isFinite

Tactic:
rw [AddCommGrpCat.mono_iff_injective] at hf

Premises used: AddCommGrpCat.mono_iff_injective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf :
  Function.Injective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))
hN : N.isFinite
⊢ Finite.{u + 1} (↑N : Type u)

Tactic:
simp only [prop_isFinite_iff] at hN ⊢

Premises used: AddCommGrpCat.prop_isFinite_iff
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf :
  Function.Injective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))
hN : Finite.{u + 1} (↑N : Type u)
⊢ Finite.{u + 1} (↑M : Type u)

Tactic:
Finite.of_injective _ hf

Premises used: Finite.of_injective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf :
  Function.Injective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))
hN : Finite.{u + 1} (↑N : Type u)
⊢ Finite.{u + 1} (↑M : Type u)

Tactic:
exact Finite.of_injective _ hf

Premises used: Finite.of_injective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf : Epi f
hM : M.isFinite
⊢ Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))

Tactic:
rw [AddCommGrpCat.epi_iff_surjective] at hf

Premises used: AddCommGrpCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf : Epi f
hM : M.isFinite
hf₁ :
  Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))
⊢ M.isFinite

Tactic:
rw [AddCommGrpCat.epi_iff_surjective] at hf

Premises used: AddCommGrpCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf :
  Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))
hM : M.isFinite
⊢ Finite.{u + 1} (↑M : Type u)

Tactic:
simp only [prop_isFinite_iff] at hM ⊢

Premises used: AddCommGrpCat.prop_isFinite_iff
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf :
  Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))
hM : Finite.{u + 1} (↑M : Type u)
⊢ Finite.{u + 1} (↑N : Type u)

Tactic:
Finite.of_surjective _ hf

Premises used: Finite.of_surjective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf :
  Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          f) :
      (a : (↑M : Type u)) → (↑N : Type u))
hM : Finite.{u + 1} (↑M : Type u)
⊢ Finite.{u + 1} (↑N : Type u)

Tactic:
exact Finite.of_surjective _ hf

Premises used: Finite.of_surjective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : isFinite.{u} S.X₁
h₃ : isFinite.{u} S.X₃
⊢ Finite.{u + 1} (↑S.X₁ : Type u)

Tactic:
simp only [prop_isFinite_iff] at h₁ h₃ ⊢

Premises used: AddCommGrpCat.prop_isFinite_iff
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : isFinite.{u} S.X₁
h₃ : isFinite.{u} S.X₃
h₂ : Finite.{u + 1} (↑S.X₁ : Type u)
⊢ Finite.{u + 1} (↑S.X₃ : Type u)

Tactic:
simp only [prop_isFinite_iff] at h₁ h₃ ⊢

Premises used: AddCommGrpCat.prop_isFinite_iff
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
⊢ Epi S.g

Tactic:
have hg := hS.epi_g
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg : Epi S.g
⊢ Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))

Tactic:
rw [AddCommGrpCat.epi_iff_surjective] at hg

Premises used: AddCommGrpCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg :
  Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
obtain :
  ∀ (s : (↑S.X₃ : Type u) → (↑S.X₂ : Type u))
    (hs :
      Function.RightInverse s
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              carrier) S.g) :
          (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))),
    Finite.{u + 1} (↑S.X₂ : Type u)
⊢ Finite.{u + 1} (↑S.X₂ : Type u)

Tactic:
obtain ⟨s, hs⟩ := hg.hasRightInverse

Premises used: Function.Surjective.hasRightInverse
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg :
  Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
s : (↑S.X₃ : Type u) → (↑S.X₂ : Type u)
hs :
  Function.RightInverse s
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
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 := carrier)
            S.g :
          (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
        (x₂ -
          s
            ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  carrier) S.g :
                (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
              x₂)) :
      (↑S.X₃ : Type u))
    (0 : (↑S.X₃ : Type u))

Tactic:
simp [hs (S.g x₂)]

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Category.Grp.IsFinite
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
hg :
  Function.Surjective (α := (↑S.X₂ : Type u)) (β := (↑S.X₃ : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
s : (↑S.X₃ : Type u) → (↑S.X₂ : Type u)
hs :
  Function.RightInverse s
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
          S.g) :
      (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
x₂ : (↑S.X₂ : Type u)
obtain :
  ∀ (x₁ : (↑S.X₁ : Type u))
    (hx₁ :
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier)
              S.f :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
          x₁ =
        x₂ -
          s
            ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  carrier) S.g :
                (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
              x₂)),
    ∃ (a : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)),
      (fun (x : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)) ↦
            (match (motive := (↑S.X₁ : Type u) × (↑S.X₃ : Type u) → (↑S.X₂ : Type u)) x with
              | (x₁, x₃) =>
                HAdd.hAdd (α := (↑S.X₂ : Type u))
                  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                          (CC := carrier) S.f :
                        (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
                      x₁ :
                    (↑S.X₂ : Type u))
                  (s x₃) :
              (↑S.X₂ : Type u)))
          a =
        x₂
⊢ ∃ (a : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)),
    (fun (x : (↑S.X₁ : Type u) × (↑S.X₃ : Type u)) ↦
          (match (motive := (↑S.X₁ : Type u) × (↑S.X₃ : Type u) → (↑S.X₂ : Type u)) x with
            | (x₁, x₃) =>
              HAdd.hAdd (α := (↑S.X₂ : Type u))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                        carrier) S.f :
                      (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
                    x₁ :
                  (↑S.X₂ : Type u))
                (s x₃) :
            (↑S.X₂ : Type u)))
        a =
      x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := (ShortComplex.ab_exact_iff S).1 hS.exact (x₂ - s (S.g x₂))
        (by simp [hs (S.g x₂)])

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.ShortComplex.ShortExact.exact, HSub.hSub, CategoryTheory.ShortComplex.ab_exact_iff, Iff.mp, DFunLike.coe, CategoryTheory.ShortComplex.g