awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
rw :
  HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0)) =
    M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0)
rw₁ :
  Eq (α := (↑(M F) : Type (max u v)))
    (M.mk F
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))
        (HSMul.hSMul (β :=
          (↑(F.obj
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))) :
            Type (max u v)))
          r
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0) :
            (↑(F.obj
                  (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))) :
              Type (max u v))))))
    (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 0))
⊢ HSMul.hSMul (β := (↑(M F) : Type (max u v))) r 0 = 0
have rw₂ : Eq (α := (↑(M F) : Type (max u v)))
  (M.mk F
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
      (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some sorry) 0))
      0))
  (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some sorry) 0))
Tactic: rw [colimit_zero_eq _ (IsFiltered.nonempty.some : J), colimit_smul_mk_eq, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
x : (↑(M F) : Type (max u v))
⊢ HSMul.hSMul (α := R) 0 x = 0
have obtain : ∀ (j : J) (x : (↑(F.obj j) : Type (max u v))),
  HSMul.hSMul (α := R) (β := (↑(M F) : Type (max u v))) 0
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) =
    0
Tactic: obtain ⟨j, x, rfl⟩ := M.mk_surjective F x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (↑(M F) : Type (max u v))
⊢ r • (x + y) = r • x + r • y
have obtain : ∀ (i : J) (x : (↑(F.obj i) : Type (max u v))),
  r • (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x) + y) =
    HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
      r • y
Tactic: obtain ⟨i, x, rfl⟩ := M.mk_surjective F x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
y : (↑(M F) : Type (max u v))
i : J
x : (↑(F.obj i) : Type (max u v))
⊢ r • (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x) + y) =
    HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
      r • y
have obtain : ∀ (j : J) (y : (↑(F.obj j) : Type (max u v))),
  r •
      HAdd.hAdd (α := (↑(M F) : Type (max u v)))
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x))
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) =
    HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
      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 y))
Tactic: obtain ⟨j, y, rfl⟩ := M.mk_surjective F y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r s : R
x : (↑(M F) : Type (max u v))
⊢ (r + s) • x = r • x + s • x
have obtain : ∀ (i : J) (x : (↑(F.obj i) : Type (max u v))),
  HSMul.hSMul (β := (↑(M F) : Type (max u v))) (r + s)
      (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) =
    HSMul.hSMul (β := (↑(M F) : Type (max u v))) r
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) +
      HSMul.hSMul (β := (↑(M F) : Type (max u v))) s
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x))
Tactic: obtain ⟨i, x, rfl⟩ := M.mk_surjective F x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α := F.obj x ⟶ Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) (F.map f ≫ coconeMorphism F x_1)
    (CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const J) (colimit F)) x) (coconeMorphism F x)
      (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit F)) f))
have hf : ∀ (x_2 : (↑(F.obj x) : Type (max u v))),
  Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))
    ((Hom.hom (F.map f ≫ coconeMorphism F x_1) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))
    ((Hom.hom
            (CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const J) (colimit F)) x) (coconeMorphism F x)
              (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit F)) f)) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit F)) x_1) : Type (max u v)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
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))
⊢ (↑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)
have 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)))
Tactic: obtain ⟨j, x, rfl⟩ := M.mk_surjective F x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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.inl))) (span R (range (u ∘ Sum.inr)))
have 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)))
Tactic: rw [huv, disjoint_comm]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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)))
have 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))))
Tactic: refine Disjoint.mono_right (span_mono (range_comp_subset_range _ _)) ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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 (ι := (↑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))))
have rw : Disjoint (span R (range (u ∘ Sum.inr))) (Hom.hom S.g).ker
Tactic: rw [← LinearMap.coe_range, span_eq (LinearMap.range S.f.hom), hS.moduleCat_range_eq_ker]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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
have 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)))
Tactic: rw [linearIndependent_sum]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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)))
have refine : LinearIndependent R (u ∘ Sum.inl)
Tactic: refine ⟨?_, LinearIndependent.of_comp S.g.hom hw, disjoint_span_sum hS hw huv⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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
⊢ LinearIndependent R (u ∘ Sum.inl)
have rw₁ : (Hom.hom S.f).ker = ⊥
Tactic: rw [huv, LinearMap.linearIndependent_iff S.f.hom]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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
    (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))
have 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)
Tactic: apply linearIndependent_leftExact hS'.exact hv _ hS'.mono_f rfl
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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 (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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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 (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))
have 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
Tactic: convert! hw
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (hypothesis)
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 (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have 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))
Tactic: have hgm : S.g m ∈ span R (range (S.g ∘ u ∘ Sum.inr)) := hw mem_top