awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
n : ℕ
ih :
  ∀ {M : ModuleCat.{v, u} R} {N : ModuleCat.{v', u'} R'}
    (e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
comm :
  Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
    (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
this_1 :
  (Hom.hom S.g).ker =
    Submodule.map (↑e2.symm : (↑S'.X₂ : Type v') →ₛₗ[(↑e.symm : R' →+* R)] (↑S.X₂ : Type v)) (Hom.hom S'.g).ker
eker : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₁ : Type v) (↑S'.X₁ : Type v') :=
  (LinearEquiv.ofEq (Hom.hom S.g).ker
        (Submodule.map (↑e2.symm : (↑S'.X₂ : Type v') →ₛₗ[(↑e.symm : R' →+* R)] (↑S.X₂ : Type v)) (Hom.hom S'.g).ker)
        this_1).trans
    (LinearEquiv.symm (e2.symm.submoduleMap (Hom.hom S'.g).ker))
this : HasProjectiveDimensionLT M.projectiveShortComplex.X₁ (n + 1)
⊢ HasProjectiveDimensionLE N (n + 1)

Tactic:
exact (S'_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mpr (ih eker)

Premises used: Iff.mpr, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff, inferInstance
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ
inst_4 : HasProjectiveDimensionLE M n
zero :
  ∀ {M : ModuleCat.{v, u} R} {N : ModuleCat.{v', u'} R'}
    (e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')) [HasProjectiveDimensionLE M 0],
    HasProjectiveDimensionLE N 0
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {M : ModuleCat.{v, u} R} {N : ModuleCat.{v', u'} R'}
        (e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')) [HasProjectiveDimensionLE M n],
        HasProjectiveDimensionLE N n)
    {M : ModuleCat.{v, u} R} {N : ModuleCat.{v', u'} R'}
    (e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')) [HasProjectiveDimensionLE M (n + 1)],
    HasProjectiveDimensionLE N (n + 1)
⊢ HasProjectiveDimensionLE N n

Tactic:
induction n generalizing M N e' with
  | zero =>
    have : HasProjectiveDimensionLE M 0 := ‹_›
    simp only [HasProjectiveDimensionLE, zero_add] at this ⊢
    rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at this ⊢
    exact Projective.of_equiv e'
  | succ n ih =>
    let S := M.projectiveShortComplex
    let S' := N.projectiveShortComplex
    have S_exact := M.shortExact_projectiveShortComplex
    have S'_exact := N.shortExact_projectiveShortComplex
    let eR : Shrink.{v} R ≃ₛₗ[RingHomClass.toRingHom e] Shrink.{v'} R' :=
      ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
    let e2 : S.X₂ ≃ₛₗ[RingHomClass.toRingHom e] S'.X₂ :=
      (Finsupp.mapDomain.linearEquiv (Shrink R) R e').trans (Finsupp.mapRange.linearEquiv eR)
    have comm : S'.g.hom.comp e2.toLinearMap = e'.toLinearMap.comp S.g.hom := by
      ext m r
      simp [S, S', e2, eR, Basis.constr_apply, map_smulₛₗ]
    have : S.g.hom.ker = Submodule.comap e2.toLinearMap S'.g.hom.ker := by
      rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]
    rw [Submodule.comap_equiv_eq_map_symm] at this
    let eker : S.X₁ ≃ₛₗ[RingHomClass.toRingHom e] S'.X₁ :=
      (LinearEquiv.ofEq _ _ this).trans (e2.symm.submoduleMap S'.g.hom.ker).symm
    have := (S_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mp ‹_›
    exact (S'_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mpr (ih eker)

Premises used: Submodule.comap_equiv_eq_map_symm, IsProjective.iff_projective, CategoryTheory.HasProjectiveDimensionLE, zero_add, CategoryTheory.projective_iff_hasProjectiveDimensionLT_one
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
⊢ projectiveDimension M = projectiveDimension N

Tactic:
eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
refine : ∀ (N_1 : WithBot ℕ∞), projectiveDimension M ≤ N_1 ↔ projectiveDimension N ≤ N_1
⊢ projectiveDimension M = projectiveDimension N

Tactic:
refine eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
⊢ projectiveDimension M ≤ ⊥ ↔ projectiveDimension N ≤ ⊥

Tactic:
simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e'.subsingleton_congr

Premises used: ModuleCat.isZero_iff_subsingleton, Equiv.subsingleton_congr, LinearEquiv.toAddEquiv, CategoryTheory.projectiveDimension_eq_bot_iff, AddEquiv.toEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
⊢ projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑⊤ : WithBot ℕ∞)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ
coe : HasProjectiveDimensionLE M n ↔ HasProjectiveDimensionLE N n
⊢ projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑n : WithBot ℕ∞)

Tactic:
simp only [projectiveDimension_le_iff]

Premises used: CategoryTheory.projectiveDimension_le_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ
⊢ HasProjectiveDimensionLE M n ↔ HasProjectiveDimensionLE N n

Tactic:
⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩

Premises used: LinearEquiv.symm, ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv, Iff.intro, RingEquiv.symm
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ
⊢ HasProjectiveDimensionLE M n ↔ HasProjectiveDimensionLE N n

Tactic:
exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ∞
coe : projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑⊤ : WithBot ℕ∞)
coe₁ : ∀ (n : ℕ), projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)
⊢ projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑n : WithBot ℕ∞)

Tactic:
induction n with
    | top => simp
    | coe n =>
      norm_cast
      simp only [projectiveDimension_le_iff]
      exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩

Premises used: CategoryTheory.projectiveDimension_le_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N_1 : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N_1 : Type v')
N : WithBot ℕ∞
bot : projectiveDimension M ≤ ⊥ ↔ projectiveDimension N_1 ≤ ⊥
coe : ∀ (n : ℕ∞), projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔ projectiveDimension N_1 ≤ (↑n : WithBot ℕ∞)
⊢ projectiveDimension M ≤ N ↔ projectiveDimension N_1 ≤ N

Tactic:
induction N with
  | bot => simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e'.subsingleton_congr
  | coe n =>
    induction n with
    | top => simp
    | coe n =>
      norm_cast
      simp only [projectiveDimension_le_iff]
      exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩

Premises used: ModuleCat.isZero_iff_subsingleton, Equiv.subsingleton_congr, LinearEquiv.toAddEquiv, CategoryTheory.projectiveDimension_le_iff, CategoryTheory.projectiveDimension_eq_bot_iff, AddEquiv.toEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : Small.{v', u} R
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u} R
e : LinearEquiv.{u, u, v, v'} (RingHom.id R) (↑M : Type v) (↑N : Type v')
n : ℕ
inst_3 : HasProjectiveDimensionLE M n
⊢ HasProjectiveDimensionLE N n

Tactic:
hasProjectiveDimensionLE_of_semiLinearEquiv (RingEquiv.refl R) e n

Premises used: RingEquiv.refl, ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : Small.{v', u} R
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u} R
e : LinearEquiv.{u, u, v, v'} (RingHom.id R) (↑M : Type v) (↑N : Type v')
⊢ projectiveDimension M = projectiveDimension N

Tactic:
projectiveDimension_eq_of_semiLinearEquiv (M := M) (N := N) (RingEquiv.refl R) e

Premises used: ModuleCat.projectiveDimension_eq_of_semiLinearEquiv, RingEquiv.refl
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
M : ModuleCat.{v, u} R
inst_1 : Nontrivial.{v} (↑M : Type v)
inst_2 : CategoryTheory.Projective M
⊢ projectiveDimension M = 0

Tactic:
simpa [projectiveDimension_eq_zero_iff, ModuleCat.isZero_iff_subsingleton,
    not_subsingleton_iff_nontrivial] using ⟨‹_›, ‹_›⟩

Premises used: ModuleCat.isZero_iff_subsingleton, not_subsingleton_iff_nontrivial, CategoryTheory.projectiveDimension_eq_zero_iff
-- Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
Goal:
b₀ b₁ : CommRingCat
f : b₀ ⟶ b₁
⊢ Eq.{u + 2} (α :=
    Quiver.Hom (V :=
      (↑(Cat.of (ModuleCat (↑b₀ : Type u))) : Type (u + 1)) ⥤ (↑(Cat.of (ModuleCat (↑b₁ : Type u))) : Type (u + 1)))
      (Cat.Hom.toFunctor
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (𝟙 b₀ ≫ f)))
      (Cat.Hom.toFunctor ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)))
    (Cat.Hom₂.toNatTrans
      (CategoryStruct.comp (Y :=
        CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₀)
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (𝟙 b₀))
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f))
        (Iso.hom
          ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
              Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
            (𝟙 b₀) f))
        (Bicategory.whiskerRight
            (Iso.hom
              ((fun (R : CommRingCat.{u}) ↦
                  (Cat.Hom.isoMk (extendScalarsId (↑R : Type u)) :
                    (extendScalars (Hom.hom (𝟙 R))).toCatHom ≅
                      Functor.toCatHom
                        (𝟭
                          (↑((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) R) :
                            Type (u + 1)))))
                b₀))
            ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f) ≫
          Iso.hom
            (Bicategory.leftUnitor
              ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)))))
    (Cat.Hom₂.toNatTrans (eqToHom ⋯))

Tactic:
apply extendScalars_id_comp

Premises used: ModuleCat.extendScalars_id_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
Goal:
b₀ b₁ : CommRingCat
f : b₀ ⟶ b₁
⊢ Eq.{u + 2} (α :=
    Quiver.Hom (V :=
      (↑(Cat.of (ModuleCat (↑b₀ : Type u))) : Type (u + 1)) ⥤ (↑(Cat.of (ModuleCat (↑b₁ : Type u))) : Type (u + 1)))
      (Cat.Hom.toFunctor
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (f ≫ 𝟙 b₁)))
      (Cat.Hom.toFunctor ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)))
    (Cat.Hom₂.toNatTrans
      (CategoryStruct.comp (Y :=
        CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₁)
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (𝟙 b₁)))
        (Iso.hom
          ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
              Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
            f (𝟙 b₁)))
        (Bicategory.whiskerLeft ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
            (Iso.hom
              ((fun (R : CommRingCat.{u}) ↦
                  (Cat.Hom.isoMk (extendScalarsId (↑R : Type u)) :
                    (extendScalars (Hom.hom (𝟙 R))).toCatHom ≅
                      Functor.toCatHom
                        (𝟭
                          (↑((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) R) :
                            Type (u + 1)))))
                b₁)) ≫
          Iso.hom
            (Bicategory.rightUnitor
              ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)))))
    (Cat.Hom₂.toNatTrans (eqToHom ⋯))

Tactic:
apply extendScalars_comp_id

Premises used: ModuleCat.extendScalars_comp_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X : Type v
inst_1 : Semiring X
inst_2 : Module R X
⊢ (↑(of R X) : Type v) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X : Type v
inst_1 : Semiring X
inst_2 : Module R X
⊢ (↑(of R X) : Type v) = X

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X : Type v
inst_1 : Semiring X
inst_2 : Module R X
⊢ (↑(of R X) : Type v) = X

Tactic:
with_reducible rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
⊢ of R (↑M : Type v) = M

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
⊢ of R (↑M : Type v) = M

Tactic:
with_reducible rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
⊢ Hom.hom (𝟙 M) = LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
x : (↑M : Type v)
⊢ (@ConcreteCategory.hom _ (moduleCategory R)
          (fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) carrier
          (fun (X Y : SemimoduleCat.{v, u} R) ↦
            (LinearMap.instFunLike : FunLike ((↑X : Type v) →ₗ[R] (↑Y : Type v)) (↑X : Type v) (↑Y : Type v)))
          _ _ _ (𝟙 M : M ⟶ M) :
        (a : (↑M : Type v)) → (↑M : Type v))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N O : SemimoduleCat.{v, u} R
f : M ⟶ N
g : N ⟶ O
⊢ Hom.hom (f ≫ g) = Hom.hom g ∘ₗ Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N O : SemimoduleCat.{v, u} R
f : M ⟶ N
g : N ⟶ O
x : (↑M : Type v)
⊢ Eq (α := (↑O : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) (f ≫ g) :
          (a : (↑M : Type v)) → (↑O : Type v))
        x :
      (↑O : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) g :
          (a : (↑N : Type v)) → (↑O : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) f :
              (a : (↑M : Type v)) → (↑N : Type v))
            x :
          (↑N : Type v)) :
      (↑O : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
f g : M ⟶ N
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: SemimoduleCat.Hom.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
f g : M.Hom N
h : f.hom = g.hom
mk :
  ∀ (hom' : (↑M : Type v) →ₗ[R] (↑N : Type v)) (h : { hom' := hom' : M.Hom N }.hom = g.hom),
    { hom' := hom' : M.Hom N } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
g : M.Hom N
hom' : (↑M : Type v) →ₗ[R] (↑N : Type v)
h : { hom' := hom' : M.Hom N }.hom = g.hom
mk :
  ∀ (hom'_1 : (↑M : Type v) →ₗ[R] (↑N : Type v)) (h : { hom' := hom' : M.Hom N }.hom = { hom' := hom'_1 }.hom),
    { hom' := hom' : M.Hom N } = { hom' := hom'_1 }
⊢ { hom' := hom' : M.Hom N } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
hom' hom'_1 : (↑M : Type v) →ₗ[R] (↑N : Type v)
h : { hom' := hom' : M.Hom N }.hom = { hom' := hom'_1 }.hom
⊢ { hom' := hom' : M.Hom N } = { hom' := hom'_1 }

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
⊢ Function.Injective.{v + 1, v + 1} (α := M.Hom N) Hom.hom

Tactic:
hom_bijective.injective

Premises used: Function.Bijective.injective, SemimoduleCat.hom_bijective
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
⊢ Function.Surjective.{v + 1, v + 1} (α := M.Hom N) Hom.hom

Tactic:
hom_bijective.surjective

Premises used: SemimoduleCat.hom_bijective, Function.Bijective.surjective
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X Y : Type v
inst_1 : AddCommMonoid X
inst_2 : Module R X
inst_3 : AddCommMonoid Y
inst_4 : Module R Y
f : X →ₗ[R] Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
f : M ⟶ N
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Quiver.Hom (V := SemimoduleCat.{v, u} R) (of R M) (of R M)) (ofHom LinearMap.id) (𝟙 (of R M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N O : Type v
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid O
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R O
f : M →ₗ[R] N
g : N →ₗ[R] O
⊢ ofHom (g ∘ₗ f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : Type v
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] N
x : M
⊢ Eq (α := (↑(of R N) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) (ofHom f) :
          (a : (↑(of R M) : Type v)) → (↑(of R N) : Type v))
        x :
      (↑(of R N) : Type v))
    ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
e : M ≅ N
x : (↑M : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) e.inv :
        (a : (↑N : Type v)) → (↑M : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) e.hom :
            (a : (↑M : Type v)) → (↑N : Type v))
          x :
        (↑N : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
e : M ≅ N
x : (↑N : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) e.hom :
        (a : (↑M : Type v)) → (↑N : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) e.inv :
            (a : (↑N : Type v)) → (↑M : Type v))
          x :
        (↑M : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
⊢ Functor.obj
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      M =
    (↑M : Type v)

Tactic:
rfl

Premises used: rfl