awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
w : ι' → (↑S.X₃ : Type u_4)
hw : LinearIndependent R w
dsimp :
  LinearIndependent R (M := (↑S.X₃ : Type u_4))
    (Function.comp (β := (↑S.X₂ : Type u_4))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_4, u_3} R) ↦ (↑x1 : Type u_4) →ₗ[R] (↑x2 : Type u_4))
            (CC := carrier) S.g) :
        (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4))
      (Function.invFun (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4)) ∘ w))
⊢ LinearIndependent R (M := (↑S.X₃ : Type u_4))
    ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_4, u_3} R) ↦ (↑x1 : Type u_4) →ₗ[R] (↑x2 : Type u_4))
            (CC := carrier) S.g) :
        (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4)) ∘
      Sum.elim
          ((⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_4, u_3} R) ↦
                  (↑x1 : Type u_4) →ₗ[R] (↑x2 : Type u_4)) (CC := carrier) S.f) :
              (a : (↑S.X₁ : Type u_4)) → (↑S.X₂ : Type u_4)) ∘
            v)
          (Function.invFun (Hom.hom S.g).toFun ∘ w) ∘
        Sum.inr)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
w : ι' → (↑S.X₃ : Type u_4)
hw : LinearIndependent R w
⊢ LinearIndependent R w

Tactic:
hw
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
w : ι' → (↑S.X₃ : Type u_4)
hw : LinearIndependent R w
h :
  Function.comp (β := (↑S.X₂ : Type u_4))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_4, u_3} R) ↦ (↑x1 : Type u_4) →ₗ[R] (↑x2 : Type u_4))
            (CC := carrier) S.g) :
        (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4))
      (Function.invFun (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4)) ∘ w) =
    w
⊢ LinearIndependent R (M := (↑S.X₃ : Type u_4))
    (Function.comp (β := (↑S.X₂ : Type u_4))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_4, u_3} R) ↦ (↑x1 : Type u_4) →ₗ[R] (↑x2 : Type u_4))
            (CC := carrier) S.g) :
        (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4))
      (Function.invFun (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4)) ∘ w))

Tactic:
convert! hw
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
w : ι' → (↑S.X₃ : Type u_4)
hw : LinearIndependent R w
h :
  ∀ (x : ι'),
    Function.comp (β := (↑S.X₂ : Type u_4))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_4, u_3} R) ↦ (↑x1 : Type u_4) →ₗ[R] (↑x2 : Type u_4))
              (CC := carrier) S.g) :
          (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4))
        (Function.invFun (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4)) ∘ w) x =
      w x
⊢ Function.comp (β := (↑S.X₂ : Type u_4))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_4, u_3} R) ↦ (↑x1 : Type u_4) →ₗ[R] (↑x2 : Type u_4))
            (CC := carrier) S.g) :
        (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4))
      (Function.invFun (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4)) ∘ w) =
    w

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
w : ι' → (↑S.X₃ : Type u_4)
hw : LinearIndependent R w
x : ι'
⊢ Function.comp (β := (↑S.X₂ : Type u_4))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_4, u_3} R) ↦ (↑x1 : Type u_4) →ₗ[R] (↑x2 : Type u_4))
            (CC := carrier) S.g) :
        (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4))
      (Function.invFun (⇑(Hom.hom S.g) : (a : (↑S.X₂ : Type u_4)) → (↑S.X₃ : Type u_4)) ∘ w) x =
    w x

Tactic:
apply Function.rightInverse_invFun ((epi_iff_surjective _).mp hS'.epi_g)

Premises used: CategoryTheory.ShortComplex.ShortExact.epi_g, ModuleCat.epi_iff_surjective, Function.rightInverse_invFun, Iff.mp
-- 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)
_ :
  Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m →
    Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m →
    Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m

Tactic:
_
-- 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
⊢ Membership.mem (α := (↑S.X₃ : Type u_5)) (γ := 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)))
    ((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))

Tactic:
have hgm : S.g m ∈ span R (range (S.g ∘ u ∘ Sum.inr)) := hw mem_top
-- 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
hgm :
  Membership.mem (α := (↑S.X₃ : Type u_5)) (γ := 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)))
    ((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))
⊢ ∃ (c : β →₀ R),
    Eq (α := (↑S.X₃ : Type u_5))
      (c.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))

Tactic:
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hgm

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 : Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) ⊤ m
hgm :
  ∃ (c : β →₀ R),
    Eq (α := (↑S.X₃ : Type u_5))
      (c.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))
obtain :
  ∀ (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))),
    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)) m

Tactic:
obtain ⟨cm, hm⟩ := hgm
-- 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)
rw : m - m' ∈ (Hom.hom S.g).ker
⊢ m - m' ∈ (Hom.hom S.f).range

Tactic:
rw [hS.moduleCat_range_eq_ker]

Premises used: CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker
-- 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)
simp :
  Eq (α := (↑S.X₃ : Type u_5)) ((Hom.hom S.g : (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) m : (↑S.X₃ : Type u_5))
    ((Hom.hom S.g : (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) m' : (↑S.X₃ : Type u_5))
⊢ m - m' ∈ (Hom.hom S.g).ker

Tactic:
simp only [LinearMap.mem_ker, map_sub, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, LinearMap.mem_ker
-- 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)
rw :
  Eq.{u_5 + 1} (α := (↑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))
    (cm.sum fun (a : β) (b : R) ↦ (Hom.hom S.g : (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) (b • u (Sum.inr a)))
⊢ Eq (α := (↑S.X₃ : Type u_5)) ((Hom.hom S.g : (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) m : (↑S.X₃ : Type u_5))
    ((Hom.hom S.g : (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) m' : (↑S.X₃ : Type u_5))

Tactic:
rw [← hm, map_finsuppSum]

Premises used: map_finsuppSum
-- 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)
⊢ Eq.{u_5 + 1} (α := (↑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))
    (cm.sum fun (a : β) (b : R) ↦ (Hom.hom S.g : (a : (↑S.X₂ : Type u_5)) → (↑S.X₃ : Type u_5)) (b • u (Sum.inr a)))

Tactic:
simp only [Function.comp_apply, map_smul]

Premises used: Function.comp_apply, map_smul
-- 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)
⊢ m - m' ∈ (Hom.hom S.f).range

Tactic:
have hsub : m - m' ∈ LinearMap.range S.f.hom := by
    rw [hS.moduleCat_range_eq_ker]
    simp only [LinearMap.mem_ker, map_sub, sub_eq_zero]
    rw [← hm, map_finsuppSum]
    simp only [Function.comp_apply, map_smul]