ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : ℤ<VAR>hx : x ≠ 0<VAR>n d : ℤ<GOAL>Rat.divInt n x / Rat.divInt d x = Rat.divInt n d
<VAR>x : ℤ<VAR>hx : x ≠ 0<VAR>n d : ℤ<GOAL>Rat.divInt x n / Rat.divInt x d = Rat.divInt d n
<VAR>num : ℕ<VAR>den : ℤ<VAR>n : ℕ<GOAL>Rat.divInt (↑num) den ^ n = Rat.divInt (↑num ^ n) (den ^ n)
<VAR>n : ℕ<GOAL>↑n = Rat.divInt (↑n) 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : Rˣ<VAR>s : R<VAR>a : A<VAR>h : IsUnit (r • (algebraMap R A) s - a)<GOAL>↑h.subInvSMul⁻¹ = r • ↑h.unit⁻¹
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : Rˣ<VAR>s : R<VAR>a : A<VAR>h : IsUnit (r • (algebraMap R A) s - a)<GOAL>↑h.subInvSMul = (algebraMap R A) s - r⁻¹ • a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : R<VAR>a : A<GOAL>r ∈ spectrum R a ↔ ¬IsUnit ((algebraMap R A) r - a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : R<VAR>a : A<GOAL>r ∉ spectrum R a ↔ IsUnit ((algebraMap R A) r - a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<GOAL>0 ∈ spectrum R a ↔ ¬IsUnit a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<GOAL>0 ∉ spectrum R a ↔ IsUnit a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>ha : IsUnit a<GOAL>spectrum R a ⊆ {0}ᶜ
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : R<VAR>a b c : A<VAR>h₁ : ((algebraMap R A) r - a) * b = 1<VAR>h₂ : c * ((algebraMap R A) r - a) = 1<GOAL>r ∈ resolventSet R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : R<VAR>a : A<GOAL>r ∈ resolventSet R a ↔ IsUnit ((algebraMap R A) r - a)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>a : A<VAR>r : R<GOAL>(algebraMap R S) r ∈ spectrum S a ↔ r ∈ spectrum R a
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>a : A<GOAL>⇑(algebraMap R S) ⁻¹' spectrum S a = spectrum R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>Subsingleton A<VAR>a : A<GOAL>resolventSet R a = Set.univ
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>Subsingleton A<VAR>a : A<GOAL>spectrum R a = ∅
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r : R<VAR>h : r ∈ resolventSet R a<GOAL>resolvent a r = ↑(IsUnit.unit h)⁻¹
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : Rˣ<VAR>s : R<VAR>a : A<GOAL>r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : Rˣ<VAR>a : A<GOAL>r • resolvent a ↑r = resolvent (r⁻¹ • a) 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : R<VAR>a : A<GOAL>r ∈ resolventSet R a ↔ IsUnit (resolvent a r)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : Rˣ<VAR>a : Aˣ<VAR>h : ↑r ∈ resolventSet R ↑a<GOAL>↑r⁻¹ ∈ resolventSet R ↑a⁻¹
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>r : Rˣ<VAR>a : Aˣ<GOAL>↑r ∈ spectrum R ↑a ↔ ↑r⁻¹ ∈ spectrum R ↑a⁻¹
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : Aˣ<GOAL>0 ∈ resolventSet R ↑a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : Aˣ<VAR>r : R<VAR>hr : r ∈ spectrum R ↑a<GOAL>r ≠ 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r s : R<GOAL>r + s ∈ spectrum R a ↔ r ∈ spectrum R (-(algebraMap R A) s + a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r s : R<GOAL>r + s ∈ spectrum R ((algebraMap R A) s + a) ↔ r ∈ spectrum R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>s : R<VAR>r : Rˣ<GOAL>r • s ∈ spectrum R (r • a) ↔ s ∈ spectrum R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r : Rˣ<GOAL>spectrum R (r • a) = r • spectrum R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a b : A<VAR>r : Rˣ<GOAL>↑r ∈ spectrum R (a * b) ↔ ↑r ∈ spectrum R (b * a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a b : A<GOAL>Units.val ⁻¹' spectrum R (a * b) = Units.val ⁻¹' spectrum R (b * a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>InvolutiveStar R<VAR>StarRing A<VAR>StarModule R A<VAR>r : R<VAR>a : A<GOAL>star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>InvolutiveStar R<VAR>StarRing A<VAR>StarModule R A<VAR>a : A<GOAL>spectrum R (star a) = star (spectrum R a)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>SetLike S A<VAR>SubringClass S A<VAR>SMulMemClass S R A<VAR>s : S<VAR>a : ↥s<GOAL>spectrum R ↑a ⊆ spectrum R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>StarRing R<VAR>StarRing A<VAR>StarModule R A<VAR>S : StarSubalgebra R A<VAR>a : ↥S<GOAL>spectrum R ↑a ⊆ spectrum R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r : R<GOAL>{r} + spectrum R a = spectrum R ((algebraMap R A) r + a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r : R<GOAL>spectrum R a + {r} = spectrum R (a + (algebraMap R A) r)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r : R<GOAL>r +ᵥ spectrum R a = spectrum R ((algebraMap R A) r + a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<GOAL>-spectrum R a = spectrum R (-a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r : R<GOAL>{r} - spectrum R a = spectrum R ((algebraMap R A) r - a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>r : R<GOAL>spectrum R a - {r} = spectrum R (a - (algebraMap R A) r)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>Nontrivial A<GOAL>spectrum 𝕜 0 = {0}
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>Nontrivial A<VAR>k : 𝕜<GOAL>spectrum 𝕜 ((algebraMap 𝕜 A) k) = {k}
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>Nontrivial A<GOAL>spectrum 𝕜 1 = {1}
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>Nontrivial A<VAR>k : 𝕜<VAR>a : A<VAR>ha : (spectrum 𝕜 a).Nonempty<GOAL>spectrum 𝕜 (k • a) = k • spectrum 𝕜 a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a b : A<GOAL>spectrum 𝕜 (a * b) \ {0} = spectrum 𝕜 (b * a) \ {0}
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : Aˣ<GOAL>(spectrum 𝕜 ↑a)⁻¹ = spectrum 𝕜 ↑a⁻¹
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>Ring B<VAR>Algebra R B<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ : F<VAR>a : A<VAR>r : R<VAR>h : r ∈ resolventSet R a<GOAL>r ∈ resolventSet R (φ a)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>Ring B<VAR>Algebra R B<VAR>FunLike F A B<VAR>AlgHomClass F R A B<VAR>φ : F<VAR>a : A<GOAL>spectrum R (φ a) ⊆ spectrum R a
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>FunLike F A R<VAR>AlgHomClass F R A R<VAR>Nontrivial R<VAR>φ : F<VAR>a : A<GOAL>φ a ∈ spectrum R a
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>EquivLike F A B<VAR>AlgEquivClass F R A B<VAR>f : F<VAR>a : A<GOAL>spectrum R (f a) = spectrum R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>u : Aˣ<GOAL>spectrum R (↑u * a * ↑u⁻¹) = spectrum R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>a : A<VAR>u : Aˣ<GOAL>spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a
<VAR>M : Type u<VAR>R : Type v<VAR>Monoid M<VAR>Semiring R<VAR>self : MulSemiringAction M R<VAR>g : M<VAR>x y : R<GOAL>g • (x * y) = g • x * g • y
<VAR>M : Type u<VAR>R : Type v<VAR>Monoid M<VAR>Semiring R<VAR>self : MulSemiringAction M R<VAR>g : M<GOAL>g • 1 = 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>R : Type v<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>x : M<GOAL>∀ (x_1 : R), (MulSemiringAction.toRingHom M R x) x_1 = x • x_1
<VAR>M : Type u_1<VAR>Monoid M<VAR>R : Type v<VAR>Semiring R<VAR>MulSemiringAction M R<VAR>FaithfulSMul M R<GOAL>Function.Injective (MulSemiringAction.toRingHom M R)
<VAR>R : Type v<VAR>Semiring R<VAR>f : R →+* R<VAR>a : R<GOAL>f • a = f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<GOAL>⇑f.toMulHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α → β<VAR>h₁ : ∀ (x y : α), f (x * y) = f x * f y<VAR>h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y<GOAL>↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_mul' := h₁ }
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<GOAL>⇑f.toAddMonoidHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α → β<VAR>h₁ : ∀ (x y : α), f (x * y) = f x * f y<VAR>h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y<GOAL>↑{ toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_zero' := h₂, map_add' := h₃ }
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f g : α →ₙ+* β<GOAL>(∀ (x : α), f x = g x) → f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f g : α →ₙ+* β<GOAL>f = g ↔ ∀ (x : α), f x = g x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<VAR>h₁ : ∀ (x y : α), f (x * y) = f x * f y<VAR>h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : α), { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y<GOAL>{ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<GOAL>Function.Injective fun f => ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<GOAL>⇑0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>x : α<GOAL>0 x = 0
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>x : α<GOAL>(NonUnitalRingHom.id α) x = x
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<GOAL>↑(NonUnitalRingHom.id α) = AddMonoidHom.id α
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<GOAL>↑(NonUnitalRingHom.id α) = MulHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>δ : Type u_5<GOAL>∀ {x : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ), (h.comp g).comp f = h.comp (g.comp f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>g : β →ₙ+* γ<VAR>f : α →ₙ+* β<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>g : β →ₙ+* γ<VAR>f : α →ₙ+* β<VAR>x : α<GOAL>(g.comp f) x = g (f x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>g : β →ₙ+* γ<VAR>f : α →ₙ+* β<GOAL>{ toFun := ⇑g ∘ ⇑f, map_zero' := ⋯, map_add' := ⋯ } = (↑g).comp ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>g : β →ₙ+* γ<VAR>f : α →ₙ+* β<GOAL>{ toFun := ⇑g ∘ ⇑f, map_mul' := ⋯ } = (↑g).comp ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>g : β →ₙ+* γ<GOAL>g.comp 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>f : α →ₙ+* β<GOAL>NonUnitalRingHom.comp 0 f = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<GOAL>f.comp (NonUnitalRingHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<GOAL>(NonUnitalRingHom.id β).comp f = f
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<GOAL>1 = NonUnitalRingHom.id α
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<GOAL>⇑1 = id
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>f g : α →ₙ+* α<GOAL>f * g = f.comp g
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>f g : α →ₙ+* α<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>g₁ g₂ : β →ₙ+* γ<VAR>f : α →ₙ+* β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>g : β →ₙ+* γ<VAR>f₁ f₂ : α →ₙ+* β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), (↑↑f).toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β) (h₁ : (↑f).toFun 0 = 0) (h₂ : ∀ (x_2 y : α), (↑f).toFun (x_2 + y) = (↑f).toFun x_2 + (↑f).toFun y), ⇑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5} [inst : FunLike F α β] [inst_1 : RingHomClass F α β] (f : F), ⇑↑f = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ⇑f.toMonoidWithZeroHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β) (h₁ : (↑f).toFun 0 = 0) (h₂ : ∀ (x_2 y : α), (↑f).toFun (x_2 + y) = (↑f).toFun x_2 + (↑f).toFun y), ↑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f.toAddMonoidHom = ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α → β) (h₁ : f 1 = 1) (h₂ : ∀ (x_2 y : α), { toFun := f, map_one' := h₁ }.toFun (x_2 * y) = { toFun := f, map_one' := h₁ }.toFun x_2 * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x_2 y : α), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x_2 + y) = (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x_2 + (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y), ↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } = { toFun := f, map_zero' := h₃, map_add' := h₄ }
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β}, f = g → ∀ (x_2 : α), f x_2 = g x_2
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) {x_2 y : α}, x_2 = y → f x_2 = f y
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, ⇑f = ⇑g → f = g
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, (∀ (x_2 : α), f x_2 = g x_2) → f = g
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β}, f = g ↔ ∀ (x_2 : α), f x_2 = g x_2
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (h₁ : f 1 = 1) (h₂ : ∀ (x_2 y : α), { toFun := ⇑f, map_one' := h₁ }.toFun (x_2 * y) = { toFun := ⇑f, map_one' := h₁ }.toFun x_2 * { toFun := ⇑f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x_2 y : α), (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x_2 + y) = (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x_2 + (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y), { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } = f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, Function.Injective fun f => ↑f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f 1 = 1
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α), f (a + b) = f a + f b
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α), f (a * b) = f a * f b
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5} [inst : FunLike F α β] [inst_1 : RingHomClass F α β] (f : F) (p : Prop) [inst_2 : Decidable p], f (if p then 0 else 1) = if p then 0 else 1
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5} [inst : FunLike F α β] [inst_1 : RingHomClass F α β] (f : F) (p : Prop) [inst_2 : Decidable p], f (if p then 1 else 0) = if p then 1 else 0
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 ↔ f 1 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 ↔ ∀ (x_2 : α), f x_2 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) [inst : Nontrivial β], f 1 ≠ 0
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, (α →+* β) → ∀ [inst : Nontrivial β], Nontrivial α
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, (α →+* β) → ∀ [h : Subsingleton α], Subsingleton β
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocRing α<VAR>NonAssocRing β<VAR>f : α →+* β<VAR>x : α<GOAL>f (-x) = -f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocRing α<VAR>NonAssocRing β<VAR>f : α →+* β<VAR>x y : α<GOAL>f (x - y) = f x - f y
<VAR>α : Type u_2<GOAL>∀ {x : NonAssocSemiring α} (x_1 : α), (RingHom.id α) x_1 = x_1
<VAR>α : Type u_2<GOAL>∀ {x : NonAssocSemiring α}, ↑(RingHom.id α) = AddMonoidHom.id α
<VAR>α : Type u_2<GOAL>∀ {x : NonAssocSemiring α}, ↑(RingHom.id α) = MonoidHom.id α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {δ : Type u_5} {x_3 : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ), (h.comp g).comp f = h.comp (g.comp f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β), ⇑(hnp.comp hmn) = ⇑hnp ∘ ⇑hmn
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x_3 : α), (hnp.comp hmn) x_3 = hnp (hmn x_3)
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f.comp (RingHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), (RingHom.id β).comp f = f
<VAR>α : Type u_2<GOAL>∀ {x : NonAssocSemiring α}, 1 = RingHom.id α
<VAR>α : Type u_2<GOAL>∀ {x : NonAssocSemiring α} (f g : α →+* α), f * g = f.comp g
<VAR>α : Type u_2<GOAL>∀ {x : NonAssocSemiring α}, ⇑1 = id
<VAR>α : Type u_2<GOAL>∀ {x : NonAssocSemiring α} (f g : α →+* α), ⇑(f * g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<GOAL>∀ {x : NonAssocSemiring α} (f : α →+* α) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<GOAL>∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semiring α<VAR>Semiring β<VAR>f : α →+* β<VAR>a : α<VAR>n : ℕ<GOAL>f (a ^ n) = f a ^ n
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommRing α<VAR>IsDomain α<VAR>CommRing β<VAR>f : β →+ α<VAR>h : ∀ (x : β), f (x * x) = f x * f x<VAR>h_two : 2 ≠ 0<VAR>h_one : f 1 = 1<GOAL>⇑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommRing α<VAR>IsDomain α<VAR>CommRing β<VAR>f : β →+ α<VAR>h : ∀ (x : β), f (x * x) = f x * f x<VAR>h_two : 2 ≠ 0<VAR>h_one : f 1 = 1<GOAL>↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = f
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R →ₙ+* S<VAR>hf : ∀ (x y : R), Commute (f x) (f y)<GOAL>⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R →ₙ+* S<VAR>hf : ∀ (x y : R), Commute (f x) (f y)<GOAL>⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : αᵐᵒᵖ →ₙ+* βᵐᵒᵖ<GOAL>∀ (a : α), (NonUnitalRingHom.op.symm f) a = (↑(AddMonoidHom.mulUnop f.toAddMonoidHom)).toFun a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>f : α →ₙ+* β<GOAL>∀ (a : αᵐᵒᵖ), (NonUnitalRingHom.op f) a = (↑(AddMonoidHom.mulOp f.toAddMonoidHom)).toFun a
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : ∀ (x y : R), Commute (f x) (f y)<GOAL>⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>hf : ∀ (x y : R), Commute (f x) (f y)<GOAL>⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>f : αᵐᵒᵖ →+* βᵐᵒᵖ<GOAL>∀ (a : α), (RingHom.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))