awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
Goal:
D : Type u₂
inst : Category.{v₂, u₂} D
S' R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ CommRingCat
φ' : S' ⟶ R
X Y : Dᵒᵖ
f : X ⟶ Y
x : (↑(R.obj X) : Type u)
⊢ Eq (α := (↑(CommRingCat.KaehlerDifferential (φ'.app Y)) : Type u))
    ((ModuleCat.Hom.hom ((relativeDifferentials' φ').map f) :
          (a : (↑(CommRingCat.KaehlerDifferential (φ'.app X)) : Type u)) →
            (↑(CommRingCat.KaehlerDifferential (φ'.app Y)) : Type u))
        (CommRingCat.KaehlerDifferential.d x) :
      (↑(CommRingCat.KaehlerDifferential (φ'.app Y)) : Type u))
    (CommRingCat.KaehlerDifferential.d
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (R.map f) :
            (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u))
          x) :
      (↑(CommRingCat.KaehlerDifferential (φ'.app Y)) : Type u))

Tactic:
CommRingCat.KaehlerDifferential.map_d (φ'.naturality f) _

Premises used: CommRingCat.KaehlerDifferential.map_d, Ideal.Cotangent, CategoryTheory.NatTrans.naturality, KaehlerDifferential
-- Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ CommRingCat
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S' R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ CommRingCat
M N :
  PresheafOfModules.{v, v₂, u₂, u}
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
⊢ HasDifferentials.{u, v₂, v₂, u₂, u₂} (C := D) (D := D) (S := S') (F := 𝟭 D) (R := R) φ'

Tactic:
⟨_, _, ⟨isUniversal' φ'⟩⟩

Premises used: PresheafOfModules.DifferentialsConstruction.isUniversal', PresheafOfModules.HasDifferentials.mk, Nonempty.intro, Exists.intro
-- Module: Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
Goal:
R : Type u
inst : Ring R
⊢ EnoughInjectives.{v, v + 1} (ModuleCat ℤ)

Tactic:
EnoughInjectives.of_equivalence (forget₂ (ModuleCat ℤ) AddCommGrpCat)

Premises used: ModuleCat, CategoryTheory.EnoughInjectives.of_equivalence, Int, CategoryTheory.forget₂, AddCommGrpCat
-- Module: Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
Goal:
R : Type u
inst : Ring R
⊢ EnoughInjectives (ModuleCat R)

Tactic:
EnoughInjectives.of_adjunction (ModuleCat.restrictCoextendScalarsAdj.{max v u} (algebraMap ℤ R))

Premises used: Algebra.algebraMap, Int, ModuleCat.restrictCoextendScalarsAdj, CategoryTheory.EnoughInjectives.of_adjunction
-- Module: Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
⊢ EnoughInjectives (ModuleCat.{v, u} R)

Tactic:
letI := enoughInjectives.{v} (Shrink.{v} R)
  EnoughInjectives.of_equivalence (restrictScalars (equivShrink R).symm.ringEquiv.toRingHom)

Premises used: Equiv.ringEquiv, CategoryTheory.EnoughInjectives.of_equivalence, ModuleCat.restrictScalars, RingEquiv.toRingHom, Equiv.symm, equivShrink
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
inst_1 : Mono f
⊢ (Hom.hom f).ker = ⊥

Tactic:
LinearMap.ker_eq_bot_of_cancel fun u v h => ModuleCat.hom_ext_iff.mp <|
    (@cancel_mono _ _ _ _ _ f _ (↟u) (↟v)).1 <| ModuleCat.hom_ext_iff.mpr h

Premises used: Iff.mpr, CategoryTheory.cancel_mono, ModuleCat.hom_ext_iff, LinearMap.ker_eq_bot_of_cancel, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
inst_1 : Epi f
⊢ (Hom.hom f).range = ⊤

Tactic:
LinearMap.range_eq_top_of_cancel fun u v h => ModuleCat.hom_ext_iff.mp <|
    (@cancel_epi _ _ _ _ _ f _ (↟u) (↟v)).1 <| ModuleCat.hom_ext_iff.mpr h

Premises used: Iff.mpr, LinearMap.range_eq_top_of_cancel, ModuleCat.hom_ext_iff, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
hf : (Hom.hom f).ker = ⊥
⊢ Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v)) (⇑(Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v))

Tactic:
LinearMap.ker_eq_bot.1 hf

Premises used: LinearMap.ker_eq_bot, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
hf : (Hom.hom f).ker = ⊥
⊢ Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))

Tactic:
convert! LinearMap.ker_eq_bot.1 hf

Premises used: LinearMap.ker_eq_bot, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
rw :
  (Hom.hom f).ker = ⊥ ↔
    Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))
rw₁ rw₂ :
  Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v)) (⇑(Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)) ↔
    Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))
⊢ Mono f ↔
    Function.Injective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))

Tactic:
rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot, ModuleCat.mono_iff_ker_eq_bot
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
hf : (Hom.hom f).range = ⊤
⊢ Function.Surjective (α := (↑X : Type v)) (β := (↑Y : Type v)) (⇑(Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v))

Tactic:
LinearMap.range_eq_top.1 hf

Premises used: LinearMap.range_eq_top, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
hf : (Hom.hom f).range = ⊤
⊢ Function.Surjective (α := (↑X : Type v)) (β := (↑Y : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) f) :
      (a : (↑X : Type v)) → (↑Y : Type v))

Tactic:
convert! LinearMap.range_eq_top.1 hf

Premises used: LinearMap.range_eq_top, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
rw :
  (Hom.hom f).range = ⊤ ↔
    Function.Surjective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))
rw₁ rw₂ :
  Function.Surjective (α := (↑X : Type v)) (β := (↑Y : Type v)) (⇑(Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)) ↔
    Function.Surjective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))
⊢ Epi f ↔
    Function.Surjective (α := (↑X : Type v)) (β := (↑Y : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) f) :
        (a : (↑X : Type v)) → (↑Y : Type v))

Tactic:
rw [epi_iff_range_eq_top, LinearMap.range_eq_top]

Premises used: LinearMap.range_eq_top, ModuleCat.epi_iff_range_eq_top
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R (↑X : Type v)
⊢ Mono (↟U.subtype)

Tactic:
(mono_iff_ker_eq_bot _).mpr (Submodule.ker_subtype U)

Premises used: Iff.mpr, Submodule.ker_subtype, ModuleCat.mono_iff_ker_eq_bot
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f : X ⟶ Y
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Submodule R (↑X : Type v)
⊢ Epi (↟U.mkQ)

Tactic:
(epi_iff_range_eq_top _).mpr <| Submodule.range_mkQ _

Premises used: Iff.mpr, Submodule.range_mkQ, ModuleCat.epi_iff_range_eq_top
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f_1 : X ⟶ Y
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
X_1 Y_1 : ModuleCat.{v, u} R
f : X_1 ⟶ Y_1
hf rw : Epi f
⊢ Epi (X :=
    Functor.obj
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      X_1)
    (CategoryTheory.Functor.map
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      f)

Tactic:
rw [CategoryTheory.ofHom_epi_iff_surjective, ← epi_iff_surjective]

Premises used: ModuleCat.epi_iff_surjective, CategoryTheory.ofHom_epi_iff_surjective
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f_1 : X ⟶ Y
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
X_1 Y_1 : ModuleCat.{v, u} R
f : X_1 ⟶ Y_1
hf : Epi f
⊢ Epi f

Tactic:
hf
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f_1 : X ⟶ Y
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
X_1 Y_1 : ModuleCat.{v, u} R
f : X_1 ⟶ Y_1
hf : Epi f
⊢ Epi f

Tactic:
exact hf
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f_1 : X ⟶ Y
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
X_1 Y_1 : ModuleCat.{v, u} R
f : X_1 ⟶ Y_1
hf rw : Mono f
⊢ Mono (X :=
    Functor.obj
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      X_1)
    (CategoryTheory.Functor.map
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      f)

Tactic:
rw [CategoryTheory.ofHom_mono_iff_injective, ← mono_iff_injective]

Premises used: ModuleCat.mono_iff_injective, CategoryTheory.ofHom_mono_iff_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f_1 : X ⟶ Y
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
X_1 Y_1 : ModuleCat.{v, u} R
f : X_1 ⟶ Y_1
hf : Mono f
⊢ Mono f

Tactic:
hf
-- Module: Mathlib.Algebra.Category.ModuleCat.EpiMono
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{v, u} R
f_1 : X ⟶ Y
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
X_1 Y_1 : ModuleCat.{v, u} R
f : X_1 ⟶ Y_1
hf : Mono f
⊢ Mono f

Tactic:
exact hf
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
mem_ann : Membership.mem (γ := Ideal R) (Module.annihilator.{u, v} R (↑N : Type v)) r
n : ℕ
hf :
  ∀ (h : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)),
    Eq (α := (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯)) :
            (a : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)) → (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
          h :
        (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
      ((AddCommGrpCat.Hom.hom 0 :
            (a : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)) → (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
          h :
        (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
⊢ Eq (α := AddCommGrpCat.of (Ext N M n) ⟶ AddCommGrpCat.of (Ext N M n))
    (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯)) 0

Tactic:
ext h
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
mem_ann : Membership.mem (γ := Ideal R) (Module.annihilator.{u, v} R (↑N : Type v)) r
n : ℕ
h : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)
⊢ HSMul.hSMul (β := N ⟶ N) r (𝟙 N) = 0

Tactic:
simp [← ModuleCat.lsmul_eq_smul_id, Module.mem_annihilator_iff_lsmul_eq_zero.mp mem_ann]

Premises used: ModuleCat.lsmul_eq_smul_id, Module.mem_annihilator_iff_lsmul_eq_zero, Iff.mp
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
mem_ann : Membership.mem (γ := Ideal R) (Module.annihilator.{u, v} R (↑N : Type v)) r
n : ℕ
h : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)
⊢ HSMul.hSMul (β := N ⟶ N) r (𝟙 N) = 0

Tactic:
have : r • 𝟙 N = 0 := by
    simp [← ModuleCat.lsmul_eq_smul_id, Module.mem_annihilator_iff_lsmul_eq_zero.mp mem_ann]
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
mem_ann : Membership.mem (γ := Ideal R) (Module.annihilator.{u, v} R (↑N : Type v)) r
n : ℕ
h : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)
this : HSMul.hSMul (β := N ⟶ N) r (𝟙 N) = 0
⊢ r • h = comp (mk₀ (HSMul.hSMul (β := N ⟶ N) r (𝟙 N))) h ⋯

Tactic:
simp [Ext.mk₀_smul]

Premises used: CategoryTheory.Abelian.Ext.mk₀_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
mem_ann : Membership.mem (γ := Ideal R) (Module.annihilator.{u, v} R (↑N : Type v)) r
n : ℕ
h : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)
this : HSMul.hSMul (β := N ⟶ N) r (𝟙 N) = 0
⊢ r • h = comp (mk₀ (HSMul.hSMul (β := N ⟶ N) r (𝟙 N))) h ⋯

Tactic:
have smul_eq : r • h = (Ext.mk₀ (r • 𝟙 N)).comp h (zero_add n) := by simp [Ext.mk₀_smul]
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
mem_ann : Membership.mem (γ := Ideal R) (Module.annihilator.{u, v} R (↑N : Type v)) r
n : ℕ
h : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)
this : HSMul.hSMul (β := N ⟶ N) r (𝟙 N) = 0
smul_eq : r • h = comp (mk₀ (HSMul.hSMul (β := N ⟶ N) r (𝟙 N))) h ⋯
⊢ Eq (α := (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
    ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯)) :
          (a : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)) → (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
        h :
      (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
    ((AddCommGrpCat.Hom.hom 0 :
          (a : (↑(AddCommGrpCat.of (Ext N M n)) : Type v)) → (↑(AddCommGrpCat.of (Ext N M n)) : Type v))
        h :
      (↑(AddCommGrpCat.of (Ext N M n)) : Type v))

Tactic:
simp [Ext.mk₀_smul, this, smul_eq]

Premises used: CategoryTheory.Abelian.Ext.mk₀_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
i : ℕ
simp :
  Function.Injective (α := Ext N M i) (β := Ext N M i)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := AddCommGrpCat.of (Ext N M i))
            (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯))) :
        (a : Ext N M i) → Ext N M i) ↔
    Function.Injective (β := Ext N M i) fun (x : Ext N M i) ↦ r • x
⊢ Mono (X := AddCommGrpCat.of (Ext N M i))
      (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯)) ↔
    IsSMulRegular.{u, v} (Ext N M i) r

Tactic:
simp only [IsSMulRegular, AddCommGrpCat.mono_iff_injective]

Premises used: AddCommGrpCat.mono_iff_injective, IsSMulRegular
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
i : ℕ
a :
  ∀ (x : Ext N M i),
    Eq (α := (a : Ext N M i) → Ext N M i)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := AddCommGrpCat.of (Ext N M i))
            (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯))) :
        (a : Ext N M i) → Ext N M i)
      (HSMul.hSMul r)
⊢ Function.Injective (α := Ext N M i) (β := Ext N M i)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := AddCommGrpCat.of (Ext N M i))
            (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯))) :
        (a : Ext N M i) → Ext N M i) ↔
    Function.Injective (β := Ext N M i) fun (x : Ext N M i) ↦ r • x

Tactic:
congr!
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
i : ℕ
x : Ext N M i
a :
  ∀ (x : Ext N M i),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (X := AddCommGrpCat.of (Ext N M i))
            (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯)) :
          (a : Ext N M i) → Ext N M i)
        x =
      r • x
⊢ Eq (α := (a : Ext N M i) → Ext N M i)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (X := AddCommGrpCat.of (Ext N M i))
          (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯))) :
      (a : Ext N M i) → Ext N M i)
    (HSMul.hSMul r)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M N : ModuleCat.{v, u} R
r : R
i : ℕ
x x_1 : Ext N M i
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (X := AddCommGrpCat.of (Ext N M i))
          (AddCommGrpCat.ofHom (postcomp (mk₀ (HSMul.hSMul (β := M ⟶ M) r (𝟙 M))) N ⋯)) :
        (a : Ext N M i) → Ext N M i)
      x_1 =
    r • x_1

Tactic:
simp [Ext.mk₀_smul]

Premises used: CategoryTheory.Abelian.Ext.mk₀_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
h :
  Function.Surjective.{v + 1, v + 1} (α := (↑M : Type v) →₀ Shrink.{v, u} R) (β := (↑M : Type v))
    (⇑((Module.Basis.constr { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) } ℕ :
              (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v))
            id :
          ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v)) :
      (a : (↑M : Type v) →₀ Shrink.{v, u} R) → (↑M : Type v))
⊢ M.projectiveShortComplex.ShortExact

Tactic:
apply LinearMap.shortExact_shortComplexKer

Premises used: LinearMap.shortExact_shortComplexKer
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
⊢ Function.Surjective.{v + 1, v + 1} (α := (↑M : Type v) →₀ Shrink.{v, u} R) (β := (↑M : Type v))
    (⇑((Module.Basis.constr { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) } ℕ :
              (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v))
            id :
          ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v)) :
      (a : (↑M : Type v) →₀ Shrink.{v, u} R) → (↑M : Type v))

Tactic:
fun m ↦ ⟨Finsupp.single m 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat, Function.Surjective, Finsupp.single
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
h :
  ∀ (m : (↑M : Type v)),
    (((Module.Basis.constr { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) } ℕ :
                (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v))
              id :
            ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v)) :
          (a : (↑M : Type v) →₀ Shrink.{v, u} R) → (↑M : Type v))
        (Finsupp.single m 1) =
      m
⊢ Function.Surjective.{v + 1, v + 1} (α := (↑M : Type v) →₀ Shrink.{v, u} R) (β := (↑M : Type v))
    (⇑((Module.Basis.constr { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) } ℕ :
              (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v))
            id :
          ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v)) :
      (a : (↑M : Type v) →₀ Shrink.{v, u} R) → (↑M : Type v))

Tactic:
refine fun m ↦ ⟨Finsupp.single m 1, ?_⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
m : (↑M : Type v)
⊢ (((Module.Basis.constr { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) } ℕ :
              (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v))
            id :
          ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v)) :
        (a : (↑M : Type v) →₀ Shrink.{v, u} R) → (↑M : Type v))
      (Finsupp.single m 1) =
    m

Tactic:
simp [Module.Basis.constr_apply]

Premises used: Module.Basis.constr_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
Goal:
R : Type u
inst : CommRing R
M_1 : Type v
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Small.{v, u} R
M : ModuleCat.{v, u} R
⊢ Module.Free.{u, v} R (↑M.projectiveShortComplex.X₂ : Type v)

Tactic:
Module.Free.finsupp R _ _

Premises used: Module.Free.finsupp
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.ShortExact
n : ℕ
inst_2 : Projective S.X₂
⊢ Function.Surjective (α := Ext S.X₁ M n) (β := Ext S.X₃ M (n + 1))
    (⇑(Ext.precomp h.extClass M ⋯) : (a : Ext S.X₁ M n) → Ext S.X₃ M (n + 1))

Tactic:
fun x ↦ Ext.contravariant_sequence_exact₃ h M x (Ext.eq_zero_of_projective _) (add_comm 1 n)

Premises used: zero_add, add_comm, CategoryTheory.Abelian.Ext.comp, CategoryTheory.Localization.SmallHom.comp, HAdd.hAdd, CategoryTheory.Localization.SmallShiftedHom.comp, CategoryTheory.Abelian.Ext.eq_zero_of_projective, OfNat.ofNat, Function.Surjective, CategoryTheory.ShortComplex.g, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃, CategoryTheory.Abelian.Ext.mk₀
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : ShortComplex (ModuleCat.{v, u} R)
h : S.ShortExact
M : ModuleCat.{v, u} R
n : ℕ
inst_2 : Injective S.X₂
⊢ Function.Surjective (α := Ext M S.X₃ n) (β := Ext M S.X₁ (n + 1))
    (⇑(Ext.postcomp h.extClass M ⋯) : (a : Ext M S.X₃ n) → Ext M S.X₁ (n + 1))

Tactic:
fun x ↦ Ext.covariant_sequence_exact₁ M h x (Ext.eq_zero_of_injective _) rfl

Premises used: CategoryTheory.Abelian.Ext.comp, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Abelian.Ext.covariant_sequence_exact₁, HAdd.hAdd, CategoryTheory.Localization.SmallShiftedHom.comp, CategoryTheory.ShortComplex.f, add_zero, OfNat.ofNat, Function.Surjective, rfl, CategoryTheory.Abelian.Ext.mk₀, CategoryTheory.Abelian.Ext.eq_zero_of_injective