ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a b : R<VAR>hab : a ≤ b<VAR>c : R<GOAL>star c * a * c ≤ star c * b * c
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a b : R<VAR>hab : a ≤ b<VAR>c : R<GOAL>c * a * star c ≤ c * b * star c
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x y : R<GOAL>star x ≤ star y ↔ x ≤ y
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x y : R<GOAL>star x < star y ↔ x < y
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x y : R<GOAL>star x ≤ y ↔ x ≤ star y
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x y : R<GOAL>star x < y ↔ x < star y
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>0 ≤ star x ↔ 0 ≤ x
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>star x ≤ 0 ↔ x ≤ 0
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>0 < star x ↔ 0 < x
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>star x < 0 ↔ x < 0
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x y : R<VAR>h : x ≤ y<VAR>hx : IsSelfAdjoint x<GOAL>IsSelfAdjoint y
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<VAR>hx : 0 ≤ x<GOAL>IsSelfAdjoint x
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a b : R<VAR>hab : a < b<VAR>c : R<VAR>hc : IsRegular c<GOAL>star c * a * c < star c * b * c
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a b : R<VAR>hab : a < b<VAR>c : R<VAR>hc : IsRegular c<GOAL>c * a * star c < c * b * star c
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a : R<VAR>ha : 0 < a<VAR>c : R<VAR>hc : IsRegular c<GOAL>0 < star c * a * c
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>a : R<VAR>ha : 0 < a<VAR>c : R<VAR>hc : IsRegular c<GOAL>0 < c * a * star c
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>Nontrivial R<VAR>x : R<VAR>hx : IsRegular x<GOAL>0 < star x * x
<VAR>R : Type u<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>Nontrivial R<VAR>x : R<VAR>hx : IsRegular x<GOAL>0 < x * star x
<VAR>R : Type u<VAR>Semiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>1 ≤ star x ↔ 1 ≤ x
<VAR>R : Type u<VAR>Semiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>star x ≤ 1 ↔ x ≤ 1
<VAR>R : Type u<VAR>Semiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>1 < star x ↔ 1 < x
<VAR>R : Type u<VAR>Semiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>x : R<GOAL>star x < 1 ↔ x < 1
<VAR>R : Type u<VAR>A : Type u_1<VAR>Semiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NonUnitalRing A<VAR>StarRing A<VAR>PartialOrder A<VAR>StarOrderedRing A<VAR>Module R A<VAR>StarModule R A<VAR>NoZeroSMulDivisors R A<VAR>IsScalarTower R A A<VAR>SMulCommClass R A A<VAR>a b : A<VAR>c : R<VAR>hab : a < b<VAR>hc : 0 < c<GOAL>c • a < c • b
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>NonUnitalSemiring R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>NonUnitalSemiring S<VAR>PartialOrder S<VAR>StarRing S<VAR>StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x y : R<VAR>hxy : x ≤ y<GOAL>f x ≤ f y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>self : Module.FinitePresentation R M<GOAL>∃ s, Submodule.span R ↑s = ⊤ ∧ (LinearMap.ker (Finsupp.total { x // x ∈ s } M R Subtype.val)).FG
<VAR>R M : Type u<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>fp : Module.FinitePresentation R M<GOAL>∃ L x x_1 K x_2, Module.Free R L ∧ Module.Finite R L ∧ K.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>h : Module.Finite R M<GOAL>Module.FinitePresentation R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<GOAL>Module.FinitePresentation R M ↔ Module.Finite R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>hl' : (LinearMap.ker l).FG<GOAL>Module.FinitePresentation R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<GOAL>Module.FinitePresentation R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>h : Module.FinitePresentation R M<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>hl' : (LinearMap.ker l).FG<GOAL>Module.FinitePresentation R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Finite R M<VAR>h : Module.FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<GOAL>(LinearMap.ker l).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.FinitePresentation R M<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<GOAL>(LinearMap.ker l).FG ↔ Module.FinitePresentation R N
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>Module.FinitePresentation R ↥(LinearMap.ker l)<GOAL>Module.FinitePresentation R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_4<VAR>N' : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup N'<VAR>Module R N'<VAR>S : Submonoid R<VAR>f : N →ₗ[R] N'<VAR>IsLocalizedModule S f<VAR>h : Module.FinitePresentation R M<VAR>g : M →ₗ[R] N'<GOAL>∃ h s, f ∘ₗ h = s • g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup N'<VAR>Module R N'<VAR>S : Submonoid R<VAR>f : N →ₗ[R] N'<VAR>IsLocalizedModule S f<VAR>hM : Module.Finite R M<VAR>g₁ g₂ : M →ₗ[R] N<VAR>h : f ∘ₗ g₁ = f ∘ₗ g₂<GOAL>∃ s, s • g₁ = s • g₂
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>S : Submonoid R<VAR>M' : Type u_1<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>N' : Type u_2<VAR>AddCommGroup N'<VAR>Module R N'<VAR>g : N →ₗ[R] N'<VAR>IsLocalizedModule S g<VAR>Module.FinitePresentation R M<GOAL>IsLocalizedModule S (IsLocalizedModule.map S f g)
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p : α<VAR>a : α<GOAL>a ≡ a [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a : α<GOAL>a ≡ a [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>a ≡ b [PMOD p] ↔ b ≡ a [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b c : α<GOAL>a ≡ b [PMOD p] → b ≡ c [PMOD p] → a ≡ c [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>-a ≡ -b [PMOD p] ↔ a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>a ≡ b [PMOD -p] ↔ a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>a b : α<GOAL>a ≡ b [PMOD b - a]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>a b : α<GOAL>a ≡ b [PMOD 0] ↔ a = b
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p : α<GOAL>p ≡ 0 [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p : α<VAR>z : ℤ<GOAL>z • p ≡ 0 [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a : α<VAR>z : ℤ<GOAL>a + z • p ≡ a [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a : α<VAR>z : ℤ<GOAL>z • p + a ≡ a [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a : α<VAR>n : ℕ<GOAL>a + n • p ≡ a [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a : α<VAR>n : ℕ<GOAL>n • p + a ≡ a [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>z : ℤ<GOAL>a ≡ b [PMOD p] → a + z • p ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>z : ℤ<GOAL>a ≡ b [PMOD p] → z • p + a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>n : ℕ<GOAL>a ≡ b [PMOD p] → a + n • p ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>n : ℕ<GOAL>a ≡ b [PMOD p] → n • p + a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>z : ℤ<GOAL>a ≡ b [PMOD z • p] → a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>n : ℕ<GOAL>a ≡ b [PMOD n • p] → a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>z : ℤ<GOAL>a ≡ b [PMOD p] → z • a ≡ z • b [PMOD z • p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>n : ℕ<GOAL>a ≡ b [PMOD p] → n • a ≡ n • b [PMOD n • p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>z : ℤ<VAR>NoZeroSMulDivisors ℤ α<VAR>hn : z ≠ 0<GOAL>z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>n : ℕ<VAR>NoZeroSMulDivisors ℕ α<VAR>hn : n ≠ 0<GOAL>n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a₁ a₂ b₁ b₂ : α<GOAL>a₁ ≡ b₁ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p])
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a₁ a₂ b₁ b₂ : α<GOAL>a₂ ≡ b₂ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p])
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a₁ a₂ b₁ b₂ : α<GOAL>a₁ ≡ b₁ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p])
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a₁ a₂ b₁ b₂ : α<GOAL>a₂ ≡ b₂ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p])
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>c : α<VAR>h : a ≡ b [PMOD p]<GOAL>c + a ≡ c + b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>c : α<VAR>h : a ≡ b [PMOD p]<GOAL>c - a ≡ c - b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>c : α<VAR>h : a ≡ b [PMOD p]<GOAL>a + c ≡ b + c [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>c : α<VAR>h : a ≡ b [PMOD p]<GOAL>a - c ≡ b - c [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>c : α<GOAL>c + a ≡ c + b [PMOD p] → a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>c : α<GOAL>a + c ≡ b + c [PMOD p] → a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>c : α<GOAL>c - a ≡ c - b [PMOD p] → a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<VAR>c : α<GOAL>a - c ≡ b - c [PMOD p] → a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b c : α<GOAL>a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b c : α<GOAL>a ≡ b - c [PMOD p] ↔ a + c ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b c : α<GOAL>a - b ≡ c [PMOD p] ↔ a ≡ b + c [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b c : α<GOAL>a - b ≡ c [PMOD p] ↔ a ≡ c + b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>a ≡ b [PMOD p] ↔ ↑b = ↑a
<VAR>α : Type u_1<VAR>AddCommGroup α<VAR>p a b : α<GOAL>¬a ≡ b [PMOD p] ↔ ↑b ≠ ↑a
<VAR>a b z : ℤ<GOAL>a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]
<VAR>α : Type u_1<VAR>AddCommGroupWithOne α<VAR>CharZero α<VAR>a b z : ℤ<GOAL>↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]
<VAR>α : Type u_1<VAR>AddCommGroupWithOne α<VAR>CharZero α<VAR>a b : ℤ<VAR>n : ℕ<GOAL>↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]
<VAR>α : Type u_1<VAR>AddCommGroupWithOne α<VAR>CharZero α<VAR>a b n : ℕ<GOAL>↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>a b c p : α<VAR>hc : c ≠ 0<GOAL>a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD p * c]
<GOAL>∀ {X Y : Semigrp} (f : ↑X →ₙ* ↑Y), MonCat.adjoinOne.map f = WithOne.map f
<VAR>S : Semigrp<GOAL>MonCat.adjoinOne.obj S = MonCat.of (WithOne ↑S)
<VAR>S : AddSemigrp<GOAL>AddMonCat.adjoinZero.obj S = AddMonCat.of (WithZero ↑S)
<GOAL>∀ {X Y : AddSemigrp} (f : AddHom ↑X ↑Y), AddMonCat.adjoinZero.map f = WithZero.map f
<VAR>X : AddMonCat<GOAL>⇑(𝟙 X) = id
<VAR>X : MonCat<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : MonCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y Z : AddMonCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y : MonCat<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget MonCat).map f = ⇑f
<VAR>X Y : AddMonCat<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget AddMonCat).map f = ⇑f
<VAR>X Y : AddMonCat<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>X Y : MonCat<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>R : Type u<VAR>Monoid R<GOAL>↑(MonCat.of R) = R
<VAR>R : Type u<VAR>AddMonoid R<GOAL>↑(AddMonCat.of R) = R
<VAR>X Y : Type u<VAR>Monoid X<VAR>Monoid Y<VAR>f : X →* Y<VAR>x : X<GOAL>(MonCat.ofHom f) x = f x
<VAR>X Y : Type u<VAR>AddMonoid X<VAR>AddMonoid Y<VAR>f : X →+ Y<VAR>x : X<GOAL>(AddMonCat.ofHom f) x = f x
<VAR>X Y : AddMonCat<VAR>x : ↑X<GOAL>0 x = 0
<VAR>X Y : MonCat<VAR>x : ↑X<GOAL>1 x = 1
<VAR>A : Type u_1<VAR>Monoid A<GOAL>1 = 1
<VAR>A : Type u_1<VAR>AddMonoid A<GOAL>0 = 0
<VAR>A : Type u_1<VAR>Monoid A<VAR>a b : A<GOAL>a * b = a * b
<VAR>A : Type u_1<VAR>AddMonoid A<VAR>a b : A<GOAL>a + b = a + b
<VAR>X : AddMonCat<GOAL>AddMonCat.uliftFunctor.obj X = AddMonCat.of (ULift.{v, u} ↑X)
<VAR>X Y : AddMonCat<VAR>f : X ⟶ Y<GOAL>AddMonCat.uliftFunctor.map f = AddMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))
<VAR>X : MonCat<GOAL>MonCat.uliftFunctor.obj X = MonCat.of (ULift.{v, u} ↑X)
<VAR>X Y : MonCat<VAR>f : X ⟶ Y<GOAL>MonCat.uliftFunctor.map f = MonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))
<VAR>X : CommMonCat<GOAL>⇑(𝟙 X) = id
<VAR>X : AddCommMonCat<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : AddCommMonCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y Z : CommMonCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y : CommMonCat<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget CommMonCat).map f = ⇑f
<VAR>X Y : AddCommMonCat<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget AddCommMonCat).map f = ⇑f
<VAR>X Y : AddCommMonCat<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>X Y : CommMonCat<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>R : Type u<VAR>CommMonoid R<GOAL>↑(CommMonCat.of R) = R
<VAR>R : Type u<VAR>AddCommMonoid R<GOAL>↑(AddCommMonCat.of R) = R
<VAR>X Y : Type u<VAR>AddCommMonoid X<VAR>AddCommMonoid Y<VAR>f : X →+ Y<VAR>x : X<GOAL>(AddCommMonCat.ofHom f) x = f x
<VAR>X Y : Type u<VAR>CommMonoid X<VAR>CommMonoid Y<VAR>f : X →* Y<VAR>x : X<GOAL>(CommMonCat.ofHom f) x = f x
<VAR>X : CommMonCat<GOAL>CommMonCat.uliftFunctor.obj X = CommMonCat.of (ULift.{v, u} ↑X)
<VAR>X Y : CommMonCat<VAR>f : X ⟶ Y<GOAL>CommMonCat.uliftFunctor.map f = CommMonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))
<VAR>X Y : AddCommMonCat<VAR>f : X ⟶ Y<GOAL>AddCommMonCat.uliftFunctor.map f = AddCommMonCat.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))
<VAR>X : AddCommMonCat<GOAL>AddCommMonCat.uliftFunctor.obj X = AddCommMonCat.of (ULift.{v, u} ↑X)
<VAR>X Y : Type u<VAR>AddMonoid X<VAR>AddMonoid Y<VAR>e : X ≃+ Y<GOAL>e.toAddMonCatIso.hom = AddMonCat.ofHom e.toAddMonoidHom
<VAR>X Y : Type u<VAR>Monoid X<VAR>Monoid Y<VAR>e : X ≃* Y<GOAL>e.toMonCatIso.inv = MonCat.ofHom e.symm.toMonoidHom
<VAR>X Y : Type u<VAR>AddMonoid X<VAR>AddMonoid Y<VAR>e : X ≃+ Y<GOAL>e.toAddMonCatIso.inv = AddMonCat.ofHom e.symm.toAddMonoidHom
<VAR>X Y : Type u<VAR>Monoid X<VAR>Monoid Y<VAR>e : X ≃* Y<GOAL>e.toMonCatIso.hom = MonCat.ofHom e.toMonoidHom
<VAR>X Y : Type u<VAR>CommMonoid X<VAR>CommMonoid Y<VAR>e : X ≃* Y<GOAL>e.toCommMonCatIso.inv = CommMonCat.ofHom e.symm.toMonoidHom
<VAR>X Y : Type u<VAR>AddCommMonoid X<VAR>AddCommMonoid Y<VAR>e : X ≃+ Y<GOAL>e.toAddCommMonCatIso.hom = AddCommMonCat.ofHom e.toAddMonoidHom
<VAR>X Y : Type u<VAR>AddCommMonoid X<VAR>AddCommMonoid Y<VAR>e : X ≃+ Y<GOAL>e.toAddCommMonCatIso.inv = AddCommMonCat.ofHom e.symm.toAddMonoidHom
<VAR>X Y : Type u<VAR>CommMonoid X<VAR>CommMonoid Y<VAR>e : X ≃* Y<GOAL>e.toCommMonCatIso.hom = CommMonCat.ofHom e.toMonoidHom
<VAR>G : MonCat<VAR>H : Type u<VAR>Monoid H<VAR>f : ↑G →* H<GOAL>f.comp (𝟙 G) = f
<VAR>G : AddMonCat<VAR>H : Type u<VAR>AddMonoid H<VAR>f : ↑G →+ H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Type u<VAR>Monoid G<VAR>H : MonCat<VAR>f : G →* ↑H<GOAL>MonoidHom.comp (𝟙 H) f = f
<VAR>G : Type u<VAR>AddMonoid G<VAR>H : AddMonCat<VAR>f : G →+ ↑H<GOAL>AddMonoidHom.comp (𝟙 H) f = f
<VAR>G : AddCommMonCat<VAR>H : Type u<VAR>AddCommMonoid H<VAR>f : ↑G →+ H<GOAL>f.comp (𝟙 G) = f
<VAR>G : CommMonCat<VAR>H : Type u<VAR>CommMonoid H<VAR>f : ↑G →* H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Type u<VAR>AddCommMonoid G<VAR>H : AddCommMonCat<VAR>f : G →+ ↑H<GOAL>AddMonoidHom.comp (𝟙 H) f = f
<VAR>G : Type u<VAR>CommMonoid G<VAR>H : CommMonCat<VAR>f : G →* ↑H<GOAL>MonoidHom.comp (𝟙 H) f = f
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>self : DirectedSystem G f<VAR>i : ι<VAR>x : G i<VAR>h : i ≤ i<GOAL>f i i h x = x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>self : DirectedSystem G f<VAR>i j k : ι<VAR>hij : i ≤ j<VAR>hjk : j ≤ k<VAR>x : G i<GOAL>f j k hjk (f i j hij x) = f i k ⋯ x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>DirectedSystem G fun i j h => f i j h<VAR>i : ι<VAR>x : G i<VAR>h : i ≤ i<GOAL>f i i h x = x
<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>DirectedSystem G fun i j h => f i j h<VAR>i j k : ι<VAR>hij : i ≤ j<VAR>hjk : j ≤ k<VAR>x : G i<GOAL>f j k hjk (f i j hij x) = f i k ⋯ x
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i : ι<VAR>x : G i<VAR>h : i ≤ i<GOAL>(f i i h) x = x
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i j k : ι<VAR>hij : i ≤ j<VAR>hjk : j ≤ k<VAR>x : G i<GOAL>(f j k hjk) ((f i j hij) x) = (f i k ⋯) x
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : G i<GOAL>(Module.DirectLimit.of R ι G f j) ((f i j hij) x) = (Module.DirectLimit.of R ι G f i) x
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>z : Module.DirectLimit G f<GOAL>∃ i x, (Module.DirectLimit.of R ι G f i) x = z
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>C : Module.DirectLimit G f → Prop<VAR>z : Module.DirectLimit G f<VAR>ih : ∀ (i : ι) (x : G i), C ((Module.DirectLimit.of R ι G f i) x)<GOAL>C z
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>P : Type u₁<VAR>AddCommGroup P<VAR>Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>i : ι<VAR>x : G i<GOAL>(Module.DirectLimit.lift R ι G f g Hg) ((Module.DirectLimit.of R ι G f i) x) = (g i) x
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>P : Type u₁<VAR>AddCommGroup P<VAR>Module R P<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : Module.DirectLimit G f →ₗ[R] P<VAR>x : Module.DirectLimit G f<GOAL>F x = (Module.DirectLimit.lift R ι G f (fun i => F ∘ₗ Module.DirectLimit.of R ι G f i) ⋯) x
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>P : Type u₁<VAR>AddCommGroup P<VAR>Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>injective : ∀ (i : ι), Function.Injective ⇑(g i)<GOAL>Function.Injective ⇑(Module.DirectLimit.lift R ι G f g Hg)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>G' : ι → Type v'<VAR>(i : ι) → AddCommGroup (G' i)<VAR>(i : ι) → Module R (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j<VAR>g : (i : ι) → G i →ₗ[R] G' i<VAR>hg : ∀ (i j : ι) (h : i ≤ j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i<VAR>i : ι<VAR>x : G i<GOAL>(Module.DirectLimit.map g hg) ((Module.DirectLimit.of R ι G f i) x) = (Module.DirectLimit.of R ι G' f' i) ((g i) x)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<GOAL>Module.DirectLimit.map (fun i => LinearMap.id) ⋯ = LinearMap.id
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>G' : ι → Type v'<VAR>(i : ι) → AddCommGroup (G' i)<VAR>(i : ι) → Module R (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j<VAR>G'' : ι → Type v''<VAR>(i : ι) → AddCommGroup (G'' i)<VAR>(i : ι) → Module R (G'' i)<VAR>f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>g₁ : (i : ι) → G i →ₗ[R] G' i<VAR>g₂ : (i : ι) → G' i →ₗ[R] G'' i<VAR>hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i<VAR>hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i<GOAL>Module.DirectLimit.map g₂ hg₂ ∘ₗ Module.DirectLimit.map g₁ hg₁ = Module.DirectLimit.map (fun i => g₂ i ∘ₗ g₁ i) ⋯
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → AddCommGroup (G i)<VAR>(i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>DecidableEq ι<VAR>G' : ι → Type v'<VAR>(i : ι) → AddCommGroup (G' i)<VAR>(i : ι) → Module R (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → G i ≃ₗ[R] G' i<VAR>he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)<VAR>i : ι<VAR>g : G i<GOAL>(Module.DirectLimit.congr e he) ((Module.DirectLimit.of R ι G f i) g) = (Module.DirectLimit.of R ι G' f' i) ((e i) g)