awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
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)
have 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)
Tactic: refine ⟨LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m), fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
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
⊢ 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)
have 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)
Tactic: rcases Submodule.mem_span_singleton.mp hn with ⟨n, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g,
    SetLike.mk_smul_mk]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g,
    SetLike.mk_smul_mk]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
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)
⊢ 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)
have inr₂ : n • gₘ = (g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) (n • m) hn)
Tactic: rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g,
    SetLike.mk_smul_mk]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
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)
⊢ 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)
have inr₃ : Eq (α := A)
  ((g : (a : ↥(ℤ ∙ m)) → A)
      (HSMul.hSMul (β := ↥(ℤ ∙ m)) n (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Ideal ℤ) (ℤ ∙ m) x) m sorry)) :
    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]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.Injective (goal)
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)
⊢ 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)
have inr₄ : Eq (α := A)
  ((g : (a : ↥(ℤ ∙ m)) → A) (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submodule ℤ ℤ) (ℤ ∙ m) x) (n • m) sorry) :
    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]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf : Mono f
hN : N.isFinite
⊢ M.isFinite
have 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))
Tactic: rw [AddCommGrpCat.mono_iff_injective] at hf
Cleared hypotheses: hf, hN
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
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
⊢ M.isFinite
have hN₁ : Finite.{u + 1} (↑N : Type u)
Tactic: simp only [prop_isFinite_iff] at hN ⊢
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
Goal:
M N : AddCommGrpCat
f : M ⟶ N
hf : Epi f
hM : M.isFinite
⊢ N.isFinite
have 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))
Tactic: rw [AddCommGrpCat.epi_iff_surjective] at hf
Cleared hypotheses: hf, hM
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
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
⊢ N.isFinite
have hM₁ : Finite.{u + 1} (↑M : Type u)
Tactic: simp only [prop_isFinite_iff] at hM ⊢
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : isFinite.{u} S.X₁
h₃ : isFinite.{u} S.X₃
⊢ isFinite.{u} S.X₂
have h₂ : Finite.{u + 1} (↑S.X₁ : Type u)
Tactic: simp only [prop_isFinite_iff] at h₁ h₃ ⊢
Cleared hypotheses: h₁, h₃
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
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)
⊢ isFinite.{u} S.X₂
have h₄ : Finite.{u + 1} (↑S.X₃ : Type u)
Tactic: simp only [prop_isFinite_iff] at h₁ h₃ ⊢
Cleared hypotheses: h₁, h₃
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
Goal:
S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite.{u + 1} (↑S.X₁ : Type u)
h₃ : Finite.{u + 1} (↑S.X₃ : Type u)
⊢ Finite.{u + 1} (↑S.X₂ : Type u)
have hg : Epi S.g
Tactic: have hg := hS.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
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
⊢ Finite.{u + 1} (↑S.X₂ : Type u)
have 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))
Tactic: rw [AddCommGrpCat.epi_iff_surjective] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (goal)
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))
⊢ Finite.{u + 1} (↑S.X₂ : Type u)
have 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)
Tactic: obtain ⟨s, hs⟩ := hg.hasRightInverse
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (goal)
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)
⊢ ∃ (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₂
have 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₂
Tactic: obtain ⟨x₁, hx₁⟩ := (ShortComplex.ab_exact_iff S).1 hS.exact (x₂ - s (S.g x₂))
        (by simp [hs (S.g x₂)])
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.IsFinite (hypothesis)
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))
⊢ Finite.{u + 1} (↑S.X₂ : Type u)
have hφ : Function.Surjective (β := (↑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₃)
Tactic: have hφ : Function.Surjective (fun (x₁, x₃) ↦ S.f x₁ + s x₃) := fun x₂ ↦ by
      obtain ⟨x₁, hx₁⟩ := (ShortComplex.ab_exact_iff S).1 hS.exact (x₂ - s (S.g x₂))
        (by simp [hs (S.g x₂)])
      exact ⟨⟨x₁, S.g x₂⟩, by simp [hx₁]⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LargeColimits (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
⊢ Nonempty (IsColimit c) ↔
    Function.Bijective (α := Colimits.Quot F) (β := (↑c.pt : Type w))
      (⇑(Quot.desc F c) : (a : Colimits.Quot F) → (↑c.pt : Type w))
have refine : Nonempty (IsColimit c) →
  ∀ (hc : IsColimit c),
    Function.Bijective (α := Colimits.Quot F) (β := (↑c.pt : Type w))
      (⇑(Quot.desc F c) : (a : Colimits.Quot F) → (↑c.pt : Type w))
Tactic: refine ⟨fun ⟨hc⟩ => ?_, fun h ↦ Nonempty.intro (isColimit_of_bijective_desc F c h)⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LargeColimits (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective (α := Colimits.Quot F) (β := (↑c.pt : Type w))
    (⇑(AddMonoidHom.toIntLinearMap (Quot.desc F c)) : (a : Colimits.Quot F) → (↑c.pt : Type w))
have rw : Function.Bijective (α := CharacterModule (↑c.pt : Type w)) (β := CharacterModule (Colimits.Quot F))
  (⇑(CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c))) :
    (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
Tactic: rw [← CharacterModule.dual_bijective_iff_bijective]
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LargeColimits (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
⊢ Function.Bijective (α := CharacterModule (↑c.pt : Type w)) (β := CharacterModule (Colimits.Quot F))
    (⇑(CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c))) :
      (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
have refine_1 : ∀ (χ ψ : CharacterModule (↑c.pt : Type w))
  (eq :
    Eq (α := CharacterModule (Colimits.Quot F))
      ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
            (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
          χ :
        CharacterModule (Colimits.Quot F))
      ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
            (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
          ψ :
        CharacterModule (Colimits.Quot F))),
  χ = ψ
Tactic: refine ⟨fun χ ψ eq ↦ ?_, fun χ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LargeColimits (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
refine_1 :
  ∀ (χ ψ : CharacterModule (↑c.pt : Type w))
    (eq :
      Eq (α := CharacterModule (Colimits.Quot F))
        ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
              (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
            χ :
          CharacterModule (Colimits.Quot F))
        ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
              (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
            ψ :
          CharacterModule (Colimits.Quot F))),
    χ = ψ
⊢ Function.Bijective (α := CharacterModule (↑c.pt : Type w)) (β := CharacterModule (Colimits.Quot F))
    (⇑(CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c))) :
      (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
have refine_2 : ∀ (χ : CharacterModule (Colimits.Quot F)),
  ∃ (a : CharacterModule (↑c.pt : Type w)),
    (CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
          (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
        a =
      χ
Tactic: refine ⟨fun χ ψ eq ↦ ?_, fun χ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.LargeColimits (goal)
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule (↑c.pt : Type w)
eq :
  Eq (α := CharacterModule (Colimits.Quot F))
    ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
          (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
        χ :
      CharacterModule (Colimits.Quot F))
    ((CharacterModule.dual (AddMonoidHom.toIntLinearMap (Quot.desc F c)) :
          (a : CharacterModule (↑c.pt : Type w)) → CharacterModule (Colimits.Quot F))
        ψ :
      CharacterModule (Colimits.Quot F))
⊢ χ = ψ
have refine_1 : Eq (α := (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
  ((AddEquiv.addMonoidHomCongrRightEquiv (AddEquiv.symm AddEquiv.ulift) :
        (a : (↑c.pt : Type w) →+ AddCircle 1) → (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle 1))
      χ :
    (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
  ((AddEquiv.addMonoidHomCongrRightEquiv (AddEquiv.symm AddEquiv.ulift) :
        (a : (↑c.pt : Type w) →+ AddCircle 1) → (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle 1))
      ψ :
    (↑c.pt : Type w) →+ ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1))
Tactic: apply AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv.injective