awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
h : IsColimit
  (AddCommGrpCat.FilteredColimits.colimitCocone.{v, u}
    (F ⋙
      forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
        (↑x1 : Type (max v u)) →+ (↑x2 : Type (max v u))) (CD := AddCommGrpCat.carrier))) :=
  AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit
    (F ⋙
      forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
        (↑x1 : Type (max v u)) →+ (↑x2 : Type (max v u))) (CD := AddCommGrpCat.carrier))
f : (↑(colimit F) : Type (max u v)) →+ (↑t.pt : Type (max u v)) :=
  AddCommGrpCat.Hom.hom
    (h.desc
      (Functor.mapCocone
        (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
          (↑x1 : Type (max v u)) →+ (↑x2 : Type (max v u))) (CD := AddCommGrpCat.carrier))
        t))
hf :
  ∀ {j : J} (x : (↑(F.obj j) : Type (max u v))),
    Eq (α := (↑t.pt : Type (max u v)))
      ((f : (a : (↑(colimit F) : Type (max u v))) → (↑t.pt : Type (max u v)))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) :
        (↑t.pt : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (t.ι.app j) :
            (a : (↑(F.obj j) : Type (max u v))) → (↑(((Functor.const J).obj t.pt).obj j) : Type (max u v)))
          x :
        (↑(Functor.obj (Functor.obj (Functor.const J) t.pt) j) : Type (max u v)))
r : R
x : (↑(M F) : Type (max u v))
obtain :
  ∀ (j : J) (x : (↑(F.obj j) : Type (max u v))),
    (↑f : ZeroHom (↑(colimit F) : Type (max u v)) (↑t.pt : Type (max u v))).toFun
        (HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x))) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
        ((↑f : ZeroHom (↑(colimit F) : Type (max u v)) (↑t.pt : Type (max u v))).toFun
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)))
⊢ (↑f : ZeroHom (↑(colimit F) : Type (max u v)) (↑t.pt : Type (max u v))).toFun (r • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      ((↑f : ZeroHom (↑(colimit F) : Type (max u v)) (↑t.pt : Type (max u v))).toFun x)

Tactic:
obtain ⟨j, x, rfl⟩ := M.mk_surjective F x

Premises used: ModuleCat.FilteredColimits.M.mk_surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
h : IsColimit
  (AddCommGrpCat.FilteredColimits.colimitCocone.{v, u}
    (F ⋙
      forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
        (↑x1 : Type (max v u)) →+ (↑x2 : Type (max v u))) (CD := AddCommGrpCat.carrier))) :=
  AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit
    (F ⋙
      forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
        (↑x1 : Type (max v u)) →+ (↑x2 : Type (max v u))) (CD := AddCommGrpCat.carrier))
f : (↑(colimit F) : Type (max u v)) →+ (↑t.pt : Type (max u v)) :=
  AddCommGrpCat.Hom.hom
    (h.desc
      (Functor.mapCocone
        (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
          (↑x1 : Type (max v u)) →+ (↑x2 : Type (max v u))) (CD := AddCommGrpCat.carrier))
        t))
hf :
  ∀ {j : J} (x : (↑(F.obj j) : Type (max u v))),
    Eq (α := (↑t.pt : Type (max u v)))
      ((f : (a : (↑(colimit F) : Type (max u v))) → (↑t.pt : Type (max u v)))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) :
        (↑t.pt : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (t.ι.app j) :
            (a : (↑(F.obj j) : Type (max u v))) → (↑(((Functor.const J).obj t.pt).obj j) : Type (max u v)))
          x :
        (↑(Functor.obj (Functor.obj (Functor.const J) t.pt) j) : Type (max u v)))
r : R
j : J
x : (↑(F.obj j) : Type (max u v))
⊢ (↑f : ZeroHom (↑(colimit F) : Type (max u v)) (↑t.pt : Type (max u v))).toFun
      (HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x))) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      ((↑f : ZeroHom (↑(colimit F) : Type (max u v)) (↑t.pt : Type (max u v))).toFun
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)))

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
j : J
⊢ (colimitCocone F).ι.app j ≫ colimitDesc F t = t.ι.app j

Tactic:
(forget₂ _ AddCommGrpCat).map_injective
    ((AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ _ _)).fac _ _)

Premises used: CategoryTheory.Limits.IsColimit.fac, AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit, CategoryTheory.Functor.comp, CategoryTheory.forget₂, AddCommGrpCat, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
t : Cocone F
j : J
⊢ (colimitCocone F).ι.app j ≫ colimitDesc F t = t.ι.app j

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
⊢ PreservesFilteredColimits
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier))

Tactic:
Limits.comp_preservesFilteredColimits (forget₂ (ModuleCat R) AddCommGrpCat)
    (forget AddCommGrpCat)

Premises used: ModuleCat, CategoryTheory.Functor.comp, CategoryTheory.forget₂, AddCommGrpCat, CategoryTheory.Limits.comp_preservesFilteredColimits, CategoryTheory.forget
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
huv :
  u ∘ Sum.inl =
    (⇑(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
rw :
  Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inr)))
    (span R
      (range
        ((⇑(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)))
⊢ Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))

Tactic:
rw [huv, disjoint_comm]

Premises used: disjoint_comm
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
huv :
  u ∘ Sum.inl =
    (⇑(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
⊢ Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inr)))
    (span R
      (range
        ((⇑(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)))

Tactic:
Disjoint.mono_right (span_mono (range_comp_subset_range _ _)) ?_

Premises used: Set.range_comp_subset_range, Submodule.span_mono, Disjoint.mono_right
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
huv :
  u ∘ Sum.inl =
    (⇑(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
refine :
  Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inr)))
    (span R
      (range (ι := (↑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.f) :
          (a : (↑S.X₁ : Type u_4)) → (↑S.X₂ : Type u_4))))
⊢ Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inr)))
    (span R
      (range
        ((⇑(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)))

Tactic:
refine Disjoint.mono_right (span_mono (range_comp_subset_range _ _)) ?_

Premises used: Set.range_comp_subset_range, Submodule.span_mono, Disjoint.mono_right
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
huv :
  u ∘ Sum.inl =
    (⇑(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
rw : Disjoint (span R (range (u ∘ Sum.inr))) (Hom.hom S.g).ker
⊢ Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inr)))
    (span R
      (range (ι := (↑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.f) :
          (a : (↑S.X₁ : Type u_4)) → (↑S.X₂ : Type u_4))))

Tactic:
rw [← LinearMap.coe_range, span_eq (LinearMap.range S.f.hom), hS.moduleCat_range_eq_ker]

Premises used: LinearMap.range, CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker, LinearMap.coe_range, Submodule.span_eq, CategoryTheory.ShortComplex.f, ModuleCat.Hom.hom
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
huv :
  u ∘ Sum.inl =
    (⇑(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
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (Hom.hom S.g).ker

Tactic:
range_ker_disjoint hw

Premises used: Submodule.range_ker_disjoint
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
huv :
  u ∘ Sum.inl =
    (⇑(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
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (Hom.hom S.g).ker

Tactic:
exact range_ker_disjoint hw

Premises used: Submodule.range_ker_disjoint
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
hm : Mono S.f
huv :
  u ∘ Sum.inl =
    (⇑(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
rw :
  LinearIndependent R (u ∘ Sum.inl) ∧
    LinearIndependent R (u ∘ Sum.inr) ∧
      Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))
⊢ LinearIndependent R u

Tactic:
rw [linearIndependent_sum]

Premises used: linearIndependent_sum
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
hm : Mono S.f
huv :
  u ∘ Sum.inl =
    (⇑(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
⊢ LinearIndependent R (u ∘ Sum.inl) ∧
    LinearIndependent R (u ∘ Sum.inr) ∧
      Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))

Tactic:
⟨?_, LinearIndependent.of_comp S.g.hom hw, disjoint_span_sum hS hw huv⟩

Premises used: LinearIndependent.of_comp, And.intro, ModuleCat.disjoint_span_sum, ModuleCat.Hom.hom, CategoryTheory.ShortComplex.g
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
hm : Mono S.f
huv :
  u ∘ Sum.inl =
    (⇑(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
refine : LinearIndependent R (u ∘ Sum.inl)
⊢ LinearIndependent R (u ∘ Sum.inl) ∧
    LinearIndependent R (u ∘ Sum.inr) ∧
      Disjoint (α := Submodule R (↑S.X₂ : Type u_4)) (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))

Tactic:
refine ⟨?_, LinearIndependent.of_comp S.g.hom hw, disjoint_span_sum hS hw huv⟩
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
hm : Mono S.f
huv :
  u ∘ Sum.inl =
    (⇑(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
rw : LinearIndependent R v
rw₁ : (Hom.hom S.f).ker = ⊥
⊢ LinearIndependent R (u ∘ Sum.inl)

Tactic:
rw [huv, LinearMap.linearIndependent_iff S.f.hom]

Premises used: LinearMap.linearIndependent_iff, CategoryTheory.ShortComplex.f, ModuleCat.Hom.hom
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
hm : Mono S.f
huv :
  u ∘ Sum.inl =
    (⇑(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
rw : Mono S.f
⊢ (Hom.hom S.f).ker = ⊥

Tactic:
rw [LinearMap.ker_eq_bot, ← mono_iff_injective]

Premises used: LinearMap.ker_eq_bot, ModuleCat.mono_iff_injective
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
hm : Mono S.f
huv :
  u ∘ Sum.inl =
    (⇑(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
⊢ Mono S.f

Tactic:
infer_instance
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
hm : Mono S.f
huv :
  u ∘ Sum.inl =
    (⇑(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
⊢ LinearIndependent R v

Tactic:
hv
-- 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.Exact
v : ι → (↑S.X₁ : Type u_4)
hv : LinearIndependent R v
u : ι ⊕ ι' → (↑S.X₂ : Type u_4)
hw :
  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)) ∘
      u ∘ Sum.inr)
hm : Mono S.f
huv :
  u ∘ Sum.inl =
    (⇑(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
⊢ LinearIndependent R v

Tactic:
exact hv
-- 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
apply :
  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)
⊢ LinearIndependent R
    (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))

Tactic:
apply linearIndependent_leftExact hS'.exact hv _ hS'.mono_f rfl

Premises used: CategoryTheory.ShortComplex.ShortExact.exact, CategoryTheory.ShortComplex.ShortExact.mono_f, ModuleCat.linearIndependent_leftExact