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

Tactic:
rw [Finsupp.sum_mapDomain_index_inj Sum.inr_injective]

Premises used: Finsupp.sum_mapDomain_index_inj, Sum.inr_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)
w : ι' → (↑S.X₃ : Type u_4)
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_4)) ⊤ (span R (range v))
hw : LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range w))
hE : Epi S.g
⊢ LE.le (α := Submodule R (↑S.X₂ : Type u_4)) ⊤
    (span R
      (range
        (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:
span_exact hS ?_ hv ?_

Premises used: Set.Mem, setOf, ModuleCat.span_exact
-- 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)
w : ι' → (↑S.X₃ : Type u_4)
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_4)) ⊤ (span R (range v))
hw : LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range w))
hE : Epi S.g
refine_1 :
  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.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_2 :
  LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤
    (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.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)))
⊢ LE.le (α := Submodule R (↑S.X₂ : Type u_4)) ⊤
    (span R
      (range
        (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:
refine span_exact hS ?_ hv ?_

Premises used: ModuleCat.span_exact
-- 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)
w : ι' → (↑S.X₃ : Type u_4)
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_4)) ⊤ (span R (range v))
hw : LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range w))
hE : Epi S.g
⊢ 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.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

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inl]

Premises used: Sum.elim_comp_inl, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom
-- 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)
w : ι' → (↑S.X₃ : Type u_4)
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_4)) ⊤ (span R (range v))
hw : LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range w))
hE : Epi S.g
⊢ LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range 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.Exact
v : ι → (↑S.X₁ : Type u_4)
w : ι' → (↑S.X₃ : Type u_4)
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_4)) ⊤ (span R (range v))
hw : LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range w))
hE : Epi S.g
h :
  (⇑(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 =
    w
⊢ LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤
    (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.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:
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.Exact
v : ι → (↑S.X₁ : Type u_4)
w : ι' → (↑S.X₃ : Type u_4)
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_4)) ⊤ (span R (range v))
hw : LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range w))
hE : Epi S.g
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
⊢ (⇑(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 =
    w

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, Sum.elim_comp_inr]

Premises used: Sum.elim_comp_inr, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom
-- 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)
w : ι' → (↑S.X₃ : Type u_4)
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_4)) ⊤ (span R (range v))
hw : LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range w))
hE : Epi S.g
⊢ Function.Surjective (α := (↑S.X₂ : Type u_4)) (β := (↑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))

Tactic:
rw [ModuleCat.epi_iff_surjective] at hE

Premises used: ModuleCat.epi_iff_surjective
-- 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)
w : ι' → (↑S.X₃ : Type u_4)
hv : LE.le (α := Submodule R (↑S.X₁ : Type u_4)) ⊤ (span R (range v))
hw : LE.le (α := Submodule R (↑S.X₃ : Type u_4)) ⊤ (span R (range w))
hE :
  Function.Surjective (α := (↑S.X₂ : Type u_4)) (β := (↑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))
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
h₁ : id ∘ w = w
h₂ h₃ : w = 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

Tactic:
rw [← Function.comp_assoc, Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE),
      Function.id_comp]

Premises used: Function.rightInverse_invFun, Function.RightInverse.comp_eq_id, Function.comp_assoc, Function.id_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
inst_1 : Free.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_2 : Free.{u_3, u_4} R (↑S.X₃ : Type u_4)
⊢ Free.{u_3, u_4} R (↑S.X₂ : Type u_4)

Tactic:
Module.Free.of_basis (Basis.ofShortExact hS' (Module.Free.chooseBasis R S.X₁)
    (Module.Free.chooseBasis R S.X₃))

Premises used: CategoryTheory.ShortComplex.X₁, Module.Free.of_basis, ModuleCat.carrier, ModuleCat.Basis.ofShortExact, CategoryTheory.ShortComplex.X₃, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
inst_1 : Free.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_2 : Free.{u_3, u_4} R (↑S.X₃ : Type u_4)
inst_3 : StrongRankCondition R
⊢ Free.{u_3, u_4} R (↑S.X₂ : Type u_4)

Tactic:
haveI := free_shortExact hS'
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
inst_1 : Free.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_2 : Free.{u_3, u_4} R (↑S.X₃ : Type u_4)
inst_3 : StrongRankCondition R
this : Free.{u_3, u_4} R (↑S.X₂ : Type u_4)
rw :
  Nonempty.{u_4 + 1}
    (Free.ChooseBasisIndex R (↑S.X₂ : Type u_4) ≃
      Free.ChooseBasisIndex R (↑S.X₁ : Type u_4) ⊕ Free.ChooseBasisIndex R (↑S.X₃ : Type u_4))
⊢ Module.rank R (↑S.X₂ : Type u_4) = Module.rank R (↑S.X₁ : Type u_4) + Module.rank R (↑S.X₃ : Type u_4)

Tactic:
rw [Module.Free.rank_eq_card_chooseBasisIndex, Module.Free.rank_eq_card_chooseBasisIndex R S.X₁,
    Module.Free.rank_eq_card_chooseBasisIndex R S.X₃, Cardinal.add_def, Cardinal.eq]

Premises used: CategoryTheory.ShortComplex.X₁, Cardinal.eq, ModuleCat.carrier, Module.Free.rank_eq_card_chooseBasisIndex, CategoryTheory.ShortComplex.X₃, Cardinal.add_def
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
inst_1 : Free.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_2 : Free.{u_3, u_4} R (↑S.X₃ : Type u_4)
inst_3 : StrongRankCondition R
this : Free.{u_3, u_4} R (↑S.X₂ : Type u_4)
⊢ Nonempty.{u_4 + 1}
    (Free.ChooseBasisIndex R (↑S.X₂ : Type u_4) ≃
      Free.ChooseBasisIndex R (↑S.X₁ : Type u_4) ⊕ Free.ChooseBasisIndex R (↑S.X₃ : Type u_4))

Tactic:
⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂) (Basis.ofShortExact hS'
    (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))⟩

Premises used: CategoryTheory.ShortComplex.X₁, Nonempty.intro, ModuleCat.carrier, ModuleCat.Basis.ofShortExact, Module.Basis.indexEquiv, CategoryTheory.ShortComplex.X₃, CategoryTheory.ShortComplex.X₂, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
inst_1 : Free.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_2 : Free.{u_3, u_4} R (↑S.X₃ : Type u_4)
inst_3 : StrongRankCondition R
this : Free.{u_3, u_4} R (↑S.X₂ : Type u_4)
⊢ Nonempty.{u_4 + 1}
    (Free.ChooseBasisIndex R (↑S.X₂ : Type u_4) ≃
      Free.ChooseBasisIndex R (↑S.X₁ : Type u_4) ⊕ Free.ChooseBasisIndex R (↑S.X₃ : Type u_4))

Tactic:
exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂) (Basis.ofShortExact hS'
    (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
n p : ℕ
inst_1 : Free.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_2 : Free.{u_3, u_4} R (↑S.X₃ : Type u_4)
inst_3 : Module.Finite.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_4 : Module.Finite.{u_3, u_4} R (↑S.X₃ : Type u_4)
hN : finrank.{u_3, u_4} R (↑S.X₁ : Type u_4) = n
hP : finrank.{u_3, u_4} R (↑S.X₃ : Type u_4) = p
inst_5 : StrongRankCondition R
h : Module.rank R (↑S.X₂ : Type u_4) = (↑(n + p) : Cardinal.{u_4})
⊢ finrank.{u_3, u_4} R (↑S.X₂ : Type u_4) = n + p

Tactic:
apply finrank_eq_of_rank_eq

Premises used: Module.finrank_eq_of_rank_eq
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
n p : ℕ
inst_1 : Free.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_2 : Free.{u_3, u_4} R (↑S.X₃ : Type u_4)
inst_3 : Module.Finite.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_4 : Module.Finite.{u_3, u_4} R (↑S.X₃ : Type u_4)
hN : finrank.{u_3, u_4} R (↑S.X₁ : Type u_4) = n
hP : finrank.{u_3, u_4} R (↑S.X₃ : Type u_4) = p
inst_5 : StrongRankCondition R
h :
  Module.rank R (↑S.X₁ : Type u_4) + Module.rank R (↑S.X₃ : Type u_4) =
    (↑(finrank.{u_3, u_4} R (↑S.X₁ : Type u_4) + finrank.{u_3, u_4} R (↑S.X₃ : Type u_4)) : Cardinal.{u_4})
⊢ Module.rank R (↑S.X₂ : Type u_4) = (↑(n + p) : Cardinal.{u_4})

Tactic:
rw [free_shortExact_rank_add hS', ← hN, ← hP]

Premises used: ModuleCat.free_shortExact_rank_add
-- Module: Mathlib.Algebra.Category.ModuleCat.Free
Goal:
R : Type u_3
inst : Ring R
S : ShortComplex (ModuleCat.{u_4, u_3} R)
hS' : S.ShortExact
n p : ℕ
inst_1 : Free.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_2 : Free.{u_3, u_4} R (↑S.X₃ : Type u_4)
inst_3 : Module.Finite.{u_3, u_4} R (↑S.X₁ : Type u_4)
inst_4 : Module.Finite.{u_3, u_4} R (↑S.X₃ : Type u_4)
hN : finrank.{u_3, u_4} R (↑S.X₁ : Type u_4) = n
hP : finrank.{u_3, u_4} R (↑S.X₃ : Type u_4) = p
inst_5 : StrongRankCondition R
⊢ Module.rank R (↑S.X₁ : Type u_4) + Module.rank R (↑S.X₃ : Type u_4) =
    (↑(finrank.{u_3, u_4} R (↑S.X₁ : Type u_4) + finrank.{u_3, u_4} R (↑S.X₃ : Type u_4)) : Cardinal.{u_4})

Tactic:
simp only [Nat.cast_add, finrank_eq_rank]

Premises used: Module.finrank_eq_rank, Nat.cast_add
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
⊢ Mono (image.ι f)

Tactic:
ConcreteCategory.mono_of_injective (image.ι f) Subtype.val_injective

Premises used: Subtype.val_injective, ModuleCat.image.ι, CategoryTheory.ConcreteCategory.mono_of_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
⊢ factorThruImage f ≫ ι f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ Mono F'.m

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
a : (↑(x + y) : (↑H : Type v)) = (↑x : (↑H : Type v)) + (↑y : (↑H : Type v))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          (F'.e ≫ F'.m) :
        (a : (↑G : Type v)) → (↑H : Type v))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type v)) ↦
              (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑(x + y) : (↑H : Type v)))
            ⋯) :
        (↑G : Type v)) =
    HAdd.hAdd (α := (↑H : Type v)) (β := (↑H : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) (F'.e ≫ F'.m) :
            (a : (↑G : Type v)) → (↑H : Type v))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type v)) ↦
                  (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
                ⋯) :
            (↑G : Type v)) :
        (↑H : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) (F'.e ≫ F'.m) :
            (a : (↑G : Type v)) → (↑H : Type v))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type v)) ↦ (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x = (↑y : (↑H : Type v)))
                ⋯) :
            (↑G : Type v)) :
        (↑H : Type v))

Tactic:
simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, Classical.indefiniteDescription, CategoryTheory.ConcreteCategory.hom, Eq, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ (↑(x + y) : (↑H : Type v)) = (↑x : (↑H : Type v)) + (↑y : (↑H : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
a : Mono F'.m
a₁ :
  Eq (α := (↑H : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) F'.m :
          (a : (↑F'.I : Type v)) → (↑H : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) F'.e :
              (a : (↑G : Type v)) → (↑F'.I : Type v))
            (↑(Classical.indefiniteDescription
                  (fun (x_1 : (↑G : Type v)) ↦
                    (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑(c • x) : (↑H : Type v)))
                  ⋯) :
              (↑G : Type v)) :
          (↑F'.I : Type v)) :
      (↑H : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) F'.m :
          (a : (↑F'.I : Type v)) → (↑H : Type v))
        (HSMul.hSMul (α := R) (β := (↑F'.1 : Type v)) ((RingHom.id R : (a : R) → R) c : R)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  carrier) F'.e :
                (a : (↑G : Type v)) → (↑F'.I : Type v))
              (↑(Classical.indefiniteDescription
                    (fun (x_1 : (↑G : Type v)) ↦
                      (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
                    ⋯) :
                (↑G : Type v)) :
            (↑F'.I : Type v))) :
      (↑H : Type v))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          F'.e :
        (a : (↑G : Type v)) → (↑F'.I : Type v))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type v)) ↦
              (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑(c • x) : (↑H : Type v)))
            ⋯) :
        (↑G : Type v)) =
    HSMul.hSMul (α := R) (β := (↑F'.1 : Type v)) ((RingHom.id R : (a : R) → R) c : R)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) F'.e :
            (a : (↑G : Type v)) → (↑F'.I : Type v))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type v)) ↦
                  (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
                ⋯) :
            (↑G : Type v)) :
        (↑F'.I : Type v))

Tactic:
apply (mono_iff_injective F'.m).1

Premises used: ModuleCat.mono_iff_injective, Iff.mp, CategoryTheory.Limits.MonoFactorisation.m
-- Module: Mathlib.Algebra.Category.ModuleCat.Images
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ Mono F'.m

Tactic:
infer_instance