awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
N : ModuleCat.{v, u} R
inst_4 : Module.Finite.{u, v} R (↑N : Type v)
⊢ Module.Finite.{u, v} R (Ext N M 0)

Tactic:
exact Module.Finite.equiv (Ext.linearEquiv₀.trans ModuleCat.homLinearEquiv).symm

Premises used: LinearEquiv.symm, CategoryTheory.Abelian.Ext.linearEquiv₀, Module.Finite.equiv, LinearEquiv.trans
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
n : ℕ
ih : ∀ (N : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑N : Type v)], Module.Finite.{u, v} R (Ext N M n)
N : ModuleCat.{v, u} R
inst_4 : Module.Finite.{u, v} R (↑N : Type v)
succ :
  ∀ (N_1 : Type v) (w : AddCommGroup N_1) (w_1 : Module R N_1),
    Module.Free R N_1 →
      Module.Finite R N_1 →
        ∀ (f : N_1 →ₗ[R] (↑N : Type v))
          (surjf : Function.Surjective (α := N_1) (β := (↑N : Type v)) (⇑f : (a : N_1) → (↑N : Type v))),
          Module.Finite.{u, v} R (Ext N M (n + 1))
⊢ Module.Finite.{u, v} R (Ext N M (n + 1))

Tactic:
obtain ⟨N, _, _, _, _, f, surjf⟩ := Module.exists_finite_presentation R N

Premises used: Module.exists_finite_presentation, ModuleCat.carrier
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
n : ℕ
ih : ∀ (N : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑N : Type v)], Module.Finite.{u, v} R (Ext N M n)
N_1 : ModuleCat.{v, u} R
inst_4 : Module.Finite.{u, v} R (↑N_1 : Type v)
N : Type v
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Free R N
w_3 : Module.Finite R N
f : N →ₗ[R] (↑N_1 : Type v)
surjf : Function.Surjective (α := N) (β := (↑N_1 : Type v)) (⇑f : (a : N) → (↑N_1 : Type v))
exac : f.shortComplexKer.ShortExact := ⋯
⊢ Module.Finite.{u, v} R (Ext N_1 M (n + 1))

Tactic:
Module.Finite.of_surjective (exac.extClass.precompOfLinear R M (add_comm 1 n))
      (precomp_extClass_surjective_of_projective_X₂ M exac n)

Premises used: Module.Finite.of_surjective, precomp_extClass_surjective_of_projective_X₂, add_comm, CategoryTheory.Abelian.Ext.precompOfLinear, OfNat.ofNat, CategoryTheory.ShortComplex.ShortExact.extClass
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
n : ℕ
ih : ∀ (N : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑N : Type v)], Module.Finite.{u, v} R (Ext N M n)
N_1 : ModuleCat.{v, u} R
inst_4 : Module.Finite.{u, v} R (↑N_1 : Type v)
N : Type v
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Free R N
w_3 : Module.Finite R N
f : N →ₗ[R] (↑N_1 : Type v)
surjf : Function.Surjective (α := N) (β := (↑N_1 : Type v)) (⇑f : (a : N) → (↑N_1 : Type v))
exac : f.shortComplexKer.ShortExact := ⋯
⊢ Module.Finite.{u, v} R (Ext N_1 M (n + 1))

Tactic:
exact Module.Finite.of_surjective (exac.extClass.precompOfLinear R M (add_comm 1 n))
      (precomp_extClass_surjective_of_projective_X₂ M exac n)

Premises used: Module.Finite.of_surjective, precomp_extClass_surjective_of_projective_X₂, add_comm, CategoryTheory.Abelian.Ext.precompOfLinear, OfNat.ofNat, CategoryTheory.ShortComplex.ShortExact.extClass
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.Finite
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
N M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑N : Type v)
inst_4 : Module.Finite.{u, v} R (↑M : Type v)
i : ℕ
zero : ∀ (N : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑N : Type v)], Module.Finite.{u, v} R (Ext N M 0)
succ :
  ∀ (n : ℕ) (ih : ∀ (N : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑N : Type v)], Module.Finite.{u, v} R (Ext N M n))
    (N : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑N : Type v)], Module.Finite.{u, v} R (Ext N M (n + 1))
⊢ Module.Finite.{u, v} R (Ext N M i)

Tactic:
induction i generalizing N with
  | zero => exact Module.Finite.equiv (Ext.linearEquiv₀.trans ModuleCat.homLinearEquiv).symm
  | succ n ih =>
    obtain ⟨N, _, _, _, _, f, surjf⟩ := Module.exists_finite_presentation R N
    let exac := LinearMap.shortExact_shortComplexKer surjf
    exact Module.Finite.of_surjective (exac.extClass.precompOfLinear R M (add_comm 1 n))
      (precomp_extClass_surjective_of_projective_X₂ M exac n)

Premises used: LinearEquiv.symm, Module.exists_finite_presentation, CategoryTheory.Abelian.Ext.linearEquiv₀, ModuleCat.carrier, Module.Finite.equiv, LinearEquiv.trans
-- Module: Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
⊢ CategoryTheory.HasExt (ModuleCat.{v, u} R)

Tactic:
CategoryTheory.hasExt_of_enoughProjectives.{v} (ModuleCat.{v} R)

Premises used: ModuleCat, CategoryTheory.hasExt_of_enoughProjectives
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
N : ModuleCat R
n : ℕ
φ φ' : M.AlternatingMap N n
h :
  ∀ (x : Fin n → (↑M : Type v)),
    Eq (α := (↑N : Type (max u v)))
      ((φ : (a : Fin n → (↑M : Type v)) → (↑N : Type (max u v))) x : (↑N : Type (max u v)))
      ((φ' : (a : Fin n → (↑M : Type v)) → (↑N : Type (max u v))) x : (↑N : Type (max u v)))
⊢ φ = φ'

Tactic:
_root_.AlternatingMap.ext h

Premises used: ModuleCat.AlternatingMap, AlternatingMap.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
N : ModuleCat R
n : ℕ
φ : M.AlternatingMap N n
N' : ModuleCat R
g : N ⟶ N'
x : Fin n → (↑M : Type v)
⊢ Eq (α := (↑N' : Type (max u v)))
    ((φ.postcomp g : (a : Fin n → (↑M : Type v)) → (↑N' : Type (max u v))) x : (↑N' : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
            (CC := carrier) g :
          (a : (↑N : Type (max u v))) → (↑N' : Type (max u v)))
        ((φ : (a : Fin n → (↑M : Type v)) → (↑N : Type (max u v))) x) :
      (↑N' : Type (max u v)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : AlternatingMap.postcomp mk f = AlternatingMap.postcomp mk g
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : AlternatingMap.postcomp mk f = AlternatingMap.postcomp mk g
⊢ Hom.hom f = Hom.hom g

Tactic:
exteriorPower.linearMap_ext h

Premises used: Set.Mem, exteriorPower.linearMap_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : AlternatingMap.postcomp mk f = AlternatingMap.postcomp mk g
⊢ Hom.hom f = Hom.hom g

Tactic:
exact exteriorPower.linearMap_ext h

Premises used: exteriorPower.linearMap_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
n : ℕ
N : ModuleCat R
φ : M.AlternatingMap N n
x : Fin n → (↑M : Type v)
⊢ Eq (α := (↑N : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
            (CC := carrier) (desc φ) :
          (a : (↑(M.exteriorPower n) : Type (max u v))) → (↑N : Type (max u v)))
        ((mk : (a : Fin n → (↑M : Type v)) → (↑(M.exteriorPower n) : Type (max u v))) x) :
      (↑N : Type (max u v)))
    ((φ : (a : Fin n → (↑M : Type v)) → (↑N : Type (max u v))) x : (↑N : Type (max u v)))

Tactic:
apply exteriorPower.alternatingMapLinearEquiv_apply_ιMulti

Premises used: exteriorPower.alternatingMapLinearEquiv_apply_ιMulti
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
f : Fin 0 → (↑M : Type u)
⊢ Eq (α := (↑(of R R) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (iso₀ M).hom :
          (a : (↑(M.exteriorPower 0) : Type u)) → (↑(of R R) : Type u))
        ((mk : (a : Fin 0 → (↑M : Type u)) → (↑(M.exteriorPower 0) : Type u)) f : (↑(M.exteriorPower 0) : Type u)) :
      (↑(of R R) : Type u))
    (1 : (↑(of R R) : Type u))

Tactic:
exteriorPower.zeroEquiv_ιMulti _

Premises used: Set.Mem, exteriorPower.zeroEquiv_ιMulti
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ map f 0 ≫ (iso₀ N).hom = (iso₀ M).hom

Tactic:
ModuleCat.hom_ext (exteriorPower.zeroEquiv_naturality f.hom)

Premises used: exteriorPower.zeroEquiv_naturality, ModuleCat.hom_ext, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
f : Fin 1 → (↑M : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
          (iso₁ M).hom :
        (a : (↑(M.exteriorPower 1) : Type u)) → (↑M : Type u))
      ((mk : (a : Fin 1 → (↑M : Type u)) → (↑(M.exteriorPower 1) : Type u)) f : (↑(M.exteriorPower 1) : Type u)) =
    f 0

Tactic:
exteriorPower.oneEquiv_ιMulti _

Premises used: exteriorPower.oneEquiv_ιMulti
-- Module: Mathlib.Algebra.Category.ModuleCat.ExteriorPower
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ map f 1 ≫ (iso₁ N).hom = (iso₁ M).hom ≫ f

Tactic:
ModuleCat.hom_ext (exteriorPower.oneEquiv_naturality f.hom)

Premises used: exteriorPower.oneEquiv_naturality, ModuleCat.hom_ext, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
m : (↑(M F) : Type (max u v))
⊢ ∃ (j : J) (x : (↑(F.obj j) : Type (max u v))),
    mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x) = m

Tactic:
(F ⋙ forget (ModuleCat R)).ιColimitType_jointly_surjective m

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, ModuleCat, ModuleCat.FilteredColimits.M.mk, CategoryTheory.Functor.comp, CategoryTheory.Functor.ColimitType, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) ⟶ k) (g :
    y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) ⟶ k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj x.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))) :
        (↑(F.obj k) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (F.map g) :
            (a : (↑(F.obj y.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))) :
        (↑(F.obj k) : Type (max u v)))
⊢ Eq (α := (↑(M F) : Type (max u v))) (mk F x) (mk F y)

Tactic:
Quot.eqvGen_sound (Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel
    (F ⋙ forget (ModuleCat R)) x y h)

Premises used: Quot.eqvGen_sound, ModuleCat, ModuleCat.FilteredColimits.M.mk, CategoryTheory.Functor.comp, CategoryTheory.Functor.ColimitType, CategoryTheory.forget, CategoryTheory.Limits.Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
j k : J
f : j ⟶ k
x : (↑(F.obj j) : Type (max u v))
⊢ Eq (α := (↑(F.obj k) : Type (max u v)))
    ((@hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
            carrier
            (fun (X Y : ModuleCat R) ↦
              (LinearMap.instFunLike :
                FunLike ((↑X : Type (max u v)) →ₗ[R] (↑Y : Type (max u v))) (↑X : Type (max u v))
                  (↑Y : Type (max u v))))
            _ _ _
            (F.map
              (𝟙
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
                    ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC :=
                          carrier) (F.map f) :
                        (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
                      x))))) :
          (a :
              (↑(F.obj
                    ⟨k, (hom (F.map f) : (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) x⟩.fst) :
                Type (max u v))) →
            (↑(F.obj k) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
            ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC :=
                  carrier) (F.map f) :
                (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
              x))) :
      (↑(F.obj k) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj ⟨j, x⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j x)) :
      (↑(F.obj k) : Type (max u v)))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  Types.FilteredColimit.Rel
    (F ⋙
      forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
        (CC := carrier))
    x y
h₁ :
  ∃ (k : J) (f :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
          (r • x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))) ⟶
      k)
    (g :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
          (r • y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))) ⟶
      k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj ⟨x.fst, r • x.snd⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
              (r • x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))) :
        (↑(F.obj k) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (F.map g) :
            (a : (↑(F.obj ⟨y.fst, r • y.snd⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
              (r • y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))) :
        (↑(F.obj k) : Type (max u v)))
⊢ Eq (α := (↑(M F) : Type (max u v))) (colimitSMulAux F r x) (colimitSMulAux F r y)

Tactic:
apply M.mk_eq

Premises used: ModuleCat.FilteredColimits.M.mk_eq
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × (↑(F.obj j) : Type (max u v))
k : J
f :
  x.fst (β := fun (j : J) ↦
      (F ⋙
            forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
              (CC := carrier)).obj
        j) ⟶
    k
g :
  y.fst (β := fun (j : J) ↦
      (F ⋙
            forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
              (CC := carrier)).obj
        j) ⟶
    k
hfg :
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
      (F.obj k))
    ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj x.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
        (x.snd (β := fun (j : J) ↦
          ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.obj j))) :
      (↑(F.obj k) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.map g) :
          (a : (↑(F.obj y.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
        (y.snd (β := fun (j : J) ↦
          ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.obj j))) :
      (↑(F.obj k) : Type (max u v)))
⊢ Eq (α := (↑(F.obj k) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj ⟨x.fst, r • x.snd⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
            (r • x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))) :
      (↑(F.obj k) : Type (max u v)))
    ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
            (F.map g) :
          (a : (↑(F.obj ⟨y.fst, r • y.snd⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
            (r • y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))) :
      (↑(F.obj k) : Type (max u v)))

Tactic:
simp [hfg]
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x : (↑(M F) : Type (max u v))
refine :
  ∀ (a b : (j : J) × (↑(F.obj j) : Type (max u v)))
    (a_1 :
      ((((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 u v)) →+ (↑x2 : Type (max u v))) (CD :=
                    AddCommGrpCat.carrier)) ⋙
                forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                  (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
                  fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD :=
                  AddGrpCat.carrier)) ⋙
              forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
                (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
                (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
            forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
              AddMonCat.carrier)).ColimitTypeRel
        a b),
    Eq (α := (↑(M F) : Type (max u v))) (colimitSMulAux F r a) (colimitSMulAux F r b)
⊢ (↑(M F) : Type (max u v))

Tactic:
refine Quot.lift (colimitSMulAux F r) ?_ x

Premises used: Quot.lift, ModuleCat.FilteredColimits.colimitSMulAux
-- Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x_1 : (↑(M F) : Type (max u v))
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  ((((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 u v)) →+ (↑x2 : Type (max u v))) (CD :=
                AddCommGrpCat.carrier)) ⋙
            forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
              (CC := AddCommGrpCat.carrier) AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
              (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddGrpCat.carrier)) ⋙
          forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
            AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier)) ⋙
        forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
          AddMonCat.carrier)).ColimitTypeRel
    x y
h₁ :
  Types.FilteredColimit.Rel
    (F ⋙
      forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
        (CC := carrier))
    x y
⊢ Eq (α := (↑(M F) : Type (max u v))) (colimitSMulAux F r x) (colimitSMulAux F r y)

Tactic:
apply colimitSMulAux_eq_of_rel

Premises used: ModuleCat.FilteredColimits.colimitSMulAux_eq_of_rel