awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have 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))
Tactic: rw [Finsupp.mem_span_range_iff_exists_finsupp] at hgm
Cleared hypotheses: hgm
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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))
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have 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
Tactic: obtain ⟨cm, hm⟩ := hgm
Cleared hypotheses: hgm
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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
have rw : m - m' ∈ (Hom.hom S.g).ker
Tactic: rw [hS.moduleCat_range_eq_ker]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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.g).ker
have 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))
Tactic: simp only [LinearMap.mem_ker, map_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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 (α := (↑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))
have 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)))
Tactic: rw [← hm, map_finsuppSum]
-- 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
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)
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have hsub : 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]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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)
hsub : m - m' ∈ (Hom.hom S.f).range
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have obtain : ∀ (n : (↑S.X₁ : Type u_5)) (hnm : (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) n = m - m'),
  Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
Tactic: obtain ⟨n, hnm⟩ := hsub
Cleared hypotheses: hsub
-- 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
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)
hnm : (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) n = m - m'
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have hn : Membership.mem (γ := Submodule R (↑S.X₁ : Type u_5)) (span R (range v)) n
Tactic: have hn : n ∈ span R (range v) := hv mem_top
-- 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
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)
hnm : (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) n = m - m'
hn : Membership.mem (γ := Submodule R (↑S.X₁ : Type u_5)) (span R (range v)) n
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have hn₁ : ∃ (c : ι →₀ R), (c.sum fun (i : ι) (a : R) ↦ a • v i) = n
Tactic: rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Free (goal)
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)
hnm : (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) n = m - m'
hn : ∃ (c : ι →₀ R), (c.sum fun (i : ι) (a : R) ↦ a • v i) = n
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have obtain : ∀ (cn : ι →₀ R) (hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n),
  Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
Tactic: obtain ⟨cn, hn⟩ := hn
Cleared hypotheses: hn
-- 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
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)
hnm : (Hom.hom S.f : (a : (↑S.X₁ : Type u_5)) → (↑S.X₂ : Type u_5)) n = m - m'
cn : ι →₀ R
hn : (cn.sum fun (i : ι) (a : R) ↦ a • v i) = n
⊢ Membership.mem (γ := Submodule R (↑S.X₂ : Type u_5)) (span R (range u)) m
have 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'
Tactic: rw [← hn, map_finsuppSum] at hnm
Cleared hypotheses: hnm, hn