awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
a : ι
b : R
e_g :
  HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
      (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f) :
            (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
          v)
        a) =
    b • u (Sum.inl a)
e_g₁ : b • (u ∘ Sum.inl) a = b • u (Sum.inl a)
e_g₂ e_g₃ : b • u (Sum.inl a) = b • u (Sum.inl a)
⊢ HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
              (CC := carrier) S.f :
            (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
          (v a) :
        (↑S.X₂ : Type u_5)) =
    b • u (Sum.inl a)

Tactic:
rw [← Function.comp_apply (f := S.f), ← huv, Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
⊢ Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5))
    (cn.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f :
              (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
            (v a) :
          (↑S.X₂ : Type u_5)))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))

Tactic:
have hn' : (Finsupp.sum cn fun a b ↦ b • S.f (v a)) =
      (Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) := by
    congr; ext a b; rw [← Function.comp_apply (f := S.f), ← huv, Function.comp_apply]
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
hn' :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5))
    (cn.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f :
              (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
            (v a) :
          (↑S.X₂ : Type u_5)))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
rw :
  Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u))
    ((cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a)) + m')
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u))
    ((cn.sum fun (a : ι) (b : R) ↦
        HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
          ((Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (v a) : (↑S.X₂ : Type u_5))) +
      m')

Tactic:
rw [hn']
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
hn' :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5))
    (cn.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f :
              (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
            (v a) :
          (↑S.X₂ : Type u_5)))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
a :
  Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
a₁ : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m'
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u))
    ((cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a)) + m')

Tactic:
apply add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
hn' :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5))
    (cn.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f :
              (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
            (v a) :
          (↑S.X₂ : Type u_5)))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
a :
  ∃ (c : ι ⊕ β →₀ R),
    Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5)) (c.sum fun (i : ι ⊕ β) (a : R) ↦ a • u i)
      (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))

Tactic:
rw [Finsupp.mem_span_range_iff_exists_finsupp]

Premises used: Finsupp.mem_span_range_iff_exists_finsupp
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h_1 : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
hn' :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5))
    (cn.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f :
              (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
            (v a) :
          (↑S.X₂ : Type u_5)))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
h :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5)) (Finsupp.sum (Finsupp.mapDomain Sum.inl cn) fun (i : ι ⊕ β) (a : R) ↦ a • u i)
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
⊢ ∃ (c : ι ⊕ β →₀ R),
    Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5)) (c.sum fun (i : ι ⊕ β) (a : R) ↦ a • u i)
      (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))

Tactic:
use cn.mapDomain (Sum.inl)

Premises used: Finsupp.mapDomain, Sum.inl
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h_1 : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
hn' :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5))
    (cn.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f :
              (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
            (v a) :
          (↑S.X₂ : Type u_5)))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
h h₁ :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5)) (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
⊢ Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5)) (Finsupp.sum (Finsupp.mapDomain Sum.inl cn) fun (i : ι ⊕ β) (a : R) ↦ a • u i)
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))

Tactic:
rw [Finsupp.sum_mapDomain_index_inj Sum.inl_injective]

Premises used: Finsupp.sum_mapDomain_index_inj, Sum.inl_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
hn' :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5))
    (cn.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f :
              (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
            (v a) :
          (↑S.X₂ : Type u_5)))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
a : ∃ (c : ι ⊕ β →₀ R), (c.sum fun (i : ι ⊕ β) (a : R) ↦ a • u i) = m'
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m'

Tactic:
rw [Finsupp.mem_span_range_iff_exists_finsupp]

Premises used: Finsupp.mem_span_range_iff_exists_finsupp
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_5, u_3} R)
hS : S.Exact
v : ι → (↑S.X₁ : Type u_5)
β : Type u_4
u : ι ⊕ β → (↑S.X₂ : Type u_5)
huv :
  u ∘ Sum.inl =
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
            (CC := carrier) S.f) :
        (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) ∘
      v
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_5)) ⊤ (span R (range v))
hw :
  LE.le (α := Submodule R (↑S.X₃ : Type u_5)) ⊤
    (span R
      (range
        ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.g) :
            (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
          u ∘ Sum.inr)))
m : (↑S.X₂ : Type u_5)
h_1 : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
cm : β →₀ R
hm :
  Eq (α := (↑S.X₃ : Type u_5))
    (cm.sum fun (i : β) (a : R) ↦
        HSMul.hSMul (β := (↑S.X₃ : Type u_5)) a
          (((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦
                    (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC := carrier) S.g) :
                (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) ∘
              u ∘ Sum.inr)
            i) :
      (↑S.X₃ : Type u_5))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5)) (CC :=
            carrier) S.g :
          (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5))
        m :
      (↑S.X₃ : Type u_5))
m' : (↑S.X₂ : Type u_5) := cm.sum fun (j : β) (a : R) ↦ a • u (Sum.inr j)
n : (↑S.X₁ : Type u_5)
cn : ι →₀ R
hnm : (cn.sum fun (a : ι) (b : R) ↦ (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) (b • v a)) = m - m'
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
hn' :
  Eq.{u_5 + 1} (α := (↑S.X₂ : Type u_5))
    (cn.sum fun (a : ι) (b : R) ↦
      HSMul.hSMul (β := (↑S.X₂ : Type u_5)) b
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_5, u_3} R) ↦ (↑x1 : Type u_5) →ₗ[R] (↑x2 : Type u_5))
                (CC := carrier) S.f :
              (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5))
            (v a) :
          (↑S.X₂ : Type u_5)))
    (cn.sum fun (a : ι) (b : R) ↦ b • u (Sum.inl a))
h : (Finsupp.sum (Finsupp.mapDomain Sum.inr cm) fun (i : ι ⊕ β) (a : R) ↦ a • u i) = m'
⊢ ∃ (c : ι ⊕ β →₀ R), (c.sum fun (i : ι ⊕ β) (a : R) ↦ a • u i) = m'

Tactic:
use cm.mapDomain (Sum.inr)

Premises used: Finsupp.mapDomain, Sum.inr