ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>Ring α<VAR>Ring β<VAR>f : α → β<VAR>hf : IsRingHom f<GOAL>IsAddGroupHom f
<VAR>α : Type u<VAR>β : Type v<VAR>rα : Semiring α<VAR>rβ : Semiring β<VAR>f : α → β<VAR>hf : IsSemiringHom f<GOAL>⇑(RingHom.of hf) = f
<VAR>α : Type u<VAR>β : Type v<VAR>rα : Semiring α<VAR>rβ : Semiring β<VAR>f : α →+* β<GOAL>IsSemiringHom ⇑f
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>Ring α<VAR>Ring γ<VAR>g : α →+* γ<GOAL>IsRingHom ⇑g
<VAR>α : Sort u<VAR>self : Lean.Meta.FastSubsingleton α<GOAL>Subsingleton α
<VAR>α : Sort u<VAR>self : Lean.Meta.FastIsEmpty α<GOAL>IsEmpty α
<VAR>α : Sort u<VAR>h : Lean.Meta.FastSubsingleton α<VAR>a b : α<GOAL>a = b
<VAR>F : Type u_1<VAR>Field F<VAR>S : Set F<VAR>self : IsSubfield S<VAR>x : F<GOAL>x ∈ S → x⁻¹ ∈ S
<VAR>F : Type u_1<VAR>Field F<VAR>S : Set F<VAR>hS : IsSubfield S<VAR>x y : F<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>x / y ∈ S
<VAR>F : Type u_1<VAR>Field F<VAR>a : F<VAR>n : ℤ<VAR>s : Set F<VAR>hs : IsSubfield s<VAR>h : a ∈ s<GOAL>a ^ n ∈ s
<VAR>F : Type u_1<VAR>Field F<GOAL>IsSubfield Set.univ
<VAR>F : Type u_1<VAR>Field F<VAR>K : Type u_2<VAR>Field K<VAR>f : F →+* K<VAR>s : Set K<VAR>hs : IsSubfield s<GOAL>IsSubfield (⇑f ⁻¹' s)
<VAR>F : Type u_1<VAR>Field F<VAR>K : Type u_2<VAR>Field K<VAR>f : F →+* K<VAR>s : Set F<VAR>hs : IsSubfield s<GOAL>IsSubfield (⇑f '' s)
<VAR>F : Type u_1<VAR>Field F<VAR>K : Type u_2<VAR>Field K<VAR>f : F →+* K<GOAL>IsSubfield (Set.range ⇑f)
<VAR>F : Type u_1<VAR>Field F<VAR>S : Set F<GOAL>Ring.closure S ⊆ Field.closure S
<VAR>F : Type u_1<VAR>Field F<VAR>S : Set F<GOAL>IsSubmonoid (Field.closure S)
<VAR>F : Type u_1<VAR>Field F<VAR>S : Set F<GOAL>IsSubfield (Field.closure S)
<VAR>F : Type u_1<VAR>Field F<VAR>S : Set F<VAR>a : F<VAR>ha : a ∈ S<GOAL>a ∈ Field.closure S
<VAR>F : Type u_1<VAR>Field F<VAR>S : Set F<GOAL>S ⊆ Field.closure S
<VAR>F : Type u_1<VAR>Field F<VAR>S T : Set F<VAR>hT : IsSubfield T<VAR>H : S ⊆ T<GOAL>Field.closure S ⊆ T
<VAR>F : Type u_1<VAR>Field F<VAR>s t : Set F<VAR>ht : IsSubfield t<GOAL>Field.closure s ⊆ t ↔ s ⊆ t
<VAR>F : Type u_1<VAR>Field F<VAR>s t : Set F<VAR>H : s ⊆ t<GOAL>Field.closure s ⊆ Field.closure t
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Type u_2<VAR>Nonempty ι<VAR>s : ι → Set F<VAR>hs : ∀ (i : ι), IsSubfield (s i)<VAR>directed : ∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k<GOAL>IsSubfield (⋃ i, s i)
<VAR>F : Type u_1<VAR>Field F<VAR>S₁ S₂ : Set F<VAR>hS₁ : IsSubfield S₁<VAR>hS₂ : IsSubfield S₂<GOAL>IsSubfield (S₁ ∩ S₂)
<VAR>F : Type u_1<VAR>Field F<VAR>ι : Sort u_2<VAR>S : ι → Set F<VAR>h : ∀ (y : ι), IsSubfield (S y)<GOAL>IsSubfield (Set.iInter S)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add α<VAR>Add β<VAR>f : α → β<VAR>self : IsAddHom f<VAR>x y : α<GOAL>f (x + y) = f x + f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul α<VAR>Mul β<VAR>f : α → β<VAR>self : IsMulHom f<VAR>x y : α<GOAL>f (x * y) = f x * f y
<VAR>α : Type u<VAR>Add α<GOAL>IsAddHom id
<VAR>α : Type u<VAR>Mul α<GOAL>IsMulHom id
<VAR>α : Type u<VAR>β : Type v<VAR>Mul α<VAR>Mul β<VAR>γ : Type u_1<VAR>Mul γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : IsMulHom f<VAR>hg : IsMulHom g<GOAL>IsMulHom (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>Add β<VAR>γ : Type u_1<VAR>Add γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : IsAddHom f<VAR>hg : IsAddHom g<GOAL>IsAddHom (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddSemigroup α<VAR>AddCommSemigroup β<VAR>f g : α → β<VAR>hf : IsAddHom f<VAR>hg : IsAddHom g<GOAL>IsAddHom fun a => f a + g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Semigroup α<VAR>CommSemigroup β<VAR>f g : α → β<VAR>hf : IsMulHom f<VAR>hg : IsMulHom g<GOAL>IsMulHom fun a => f a * g a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Mul α<VAR>CommGroup β<VAR>f : α → β<VAR>hf : IsMulHom f<GOAL>IsMulHom fun a => (f a)⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Add α<VAR>AddCommGroup β<VAR>f : α → β<VAR>hf : IsAddHom f<GOAL>IsAddHom fun a => -f a
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α → β<VAR>self : IsAddMonoidHom f<GOAL>f 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α → β<VAR>self : IsMonoidHom f<GOAL>f 1 = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>mM : AddZeroClass M<VAR>mN : AddZeroClass N<VAR>f : M → N<VAR>hf : IsAddMonoidHom f<GOAL>⇑(AddMonoidHom.of hf) = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>mM : MulOneClass M<VAR>mN : MulOneClass N<VAR>f : M → N<VAR>hf : IsMonoidHom f<GOAL>⇑(MonoidHom.of hf) = f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>mM : AddZeroClass M<VAR>mN : AddZeroClass N<VAR>f : M →+ N<GOAL>IsAddMonoidHom ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>mM : MulOneClass M<VAR>mN : MulOneClass N<VAR>f : M →* N<GOAL>IsMonoidHom ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>h : M ≃+ N<GOAL>IsAddHom ⇑h
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>h : M ≃* N<GOAL>IsMulHom ⇑h
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>h : M ≃* N<GOAL>IsMonoidHom ⇑h
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>h : M ≃+ N<GOAL>IsAddMonoidHom ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α → β<VAR>hf : IsMonoidHom f<VAR>x y : α<GOAL>f (x * y) = f x * f y
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α → β<VAR>hf : IsAddMonoidHom f<VAR>x y : α<GOAL>f (x + y) = f x + f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddZeroClass α<VAR>AddCommGroup β<VAR>f : α → β<VAR>hf : IsAddMonoidHom f<GOAL>IsAddMonoidHom fun a => -f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MulOneClass α<VAR>CommGroup β<VAR>f : α → β<VAR>hf : IsMonoidHom f<GOAL>IsMonoidHom fun a => (f a)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>Group β<VAR>f : α → β<VAR>hf : IsMulHom f<GOAL>IsMonoidHom f
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : IsAddHom f<GOAL>IsAddMonoidHom f
<VAR>α : Type u<VAR>MulOneClass α<GOAL>IsMonoidHom id
<VAR>α : Type u<VAR>AddZeroClass α<GOAL>IsAddMonoidHom id
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α → β<VAR>hf : IsAddMonoidHom f<VAR>γ : Type u_1<VAR>AddZeroClass γ<VAR>g : β → γ<VAR>hg : IsAddMonoidHom g<GOAL>IsAddMonoidHom (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α → β<VAR>hf : IsMonoidHom f<VAR>γ : Type u_1<VAR>MulOneClass γ<VAR>g : β → γ<VAR>hg : IsMonoidHom g<GOAL>IsMonoidHom (g ∘ f)
<VAR>γ : Type u_1<VAR>NonUnitalNonAssocSemiring γ<VAR>x : γ<GOAL>IsAddMonoidHom fun y => x * y
<VAR>γ : Type u_1<VAR>NonUnitalNonAssocSemiring γ<VAR>x : γ<GOAL>IsAddMonoidHom fun y => y * x
<VAR>G : Type u_1<VAR>H : Type u_2<GOAL>∀ {x : AddGroup G} {x_1 : AddGroup H} (f : G →+ H), IsAddGroupHom ⇑f
<VAR>G : Type u_1<VAR>H : Type u_2<GOAL>∀ {x : Group G} {x_1 : Group H} (f : G →* H), IsGroupHom ⇑f
<VAR>G : Type u_1<VAR>H : Type u_2<GOAL>∀ {x : Group G} {x_1 : Group H} (h : G ≃* H), IsGroupHom ⇑h
<VAR>G : Type u_1<VAR>H : Type u_2<GOAL>∀ {x : AddGroup G} {x_1 : AddGroup H} (h : G ≃+ H), IsAddGroupHom ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : ∀ (x y : α), f (x * y) = f x * f y<GOAL>IsGroupHom f
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : ∀ (x y : α), f (x + y) = f x + f y<GOAL>IsAddGroupHom f
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : IsGroupHom f<VAR>x y : α<GOAL>f (x * y) = f x * f y
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : IsGroupHom f<GOAL>IsMonoidHom f
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : IsAddGroupHom f<GOAL>IsAddMonoidHom f
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : IsGroupHom f<GOAL>f 1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : IsAddGroupHom f<GOAL>f 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : IsGroupHom f<VAR>a : α<GOAL>f a⁻¹ = (f a)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : IsAddGroupHom f<VAR>a : α<GOAL>f (-a) = -f a
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : IsGroupHom f<VAR>a b : α<GOAL>f (a / b) = f a / f b
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : IsAddGroupHom f<VAR>a b : α<GOAL>f (a - b) = f a - f b
<VAR>α : Type u<VAR>AddGroup α<GOAL>IsAddGroupHom id
<VAR>α : Type u<VAR>Group α<GOAL>IsGroupHom id
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : IsAddGroupHom f<VAR>γ : Type u_1<VAR>AddGroup γ<VAR>g : β → γ<VAR>hg : IsAddGroupHom g<GOAL>IsAddGroupHom (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : IsGroupHom f<VAR>γ : Type u_1<VAR>Group γ<VAR>g : β → γ<VAR>hg : IsGroupHom g<GOAL>IsGroupHom (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : IsAddGroupHom f<GOAL>Function.Injective f ↔ ∀ (a : α), f a = 0 → a = 0
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : IsGroupHom f<GOAL>Function.Injective f ↔ ∀ (a : α), f a = 1 → a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddCommGroup β<VAR>f g : α → β<VAR>hf : IsAddGroupHom f<VAR>hg : IsAddGroupHom g<GOAL>IsAddGroupHom fun a => f a + g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>CommGroup β<VAR>f g : α → β<VAR>hf : IsGroupHom f<VAR>hg : IsGroupHom g<GOAL>IsGroupHom fun a => f a * g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddCommGroup β<VAR>f : α → β<VAR>hf : IsAddGroupHom f<GOAL>IsAddGroupHom fun a => -f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Group α<VAR>CommGroup β<VAR>f : α → β<VAR>hf : IsGroupHom f<GOAL>IsGroupHom fun a => (f a)⁻¹
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>IsMonoidHom ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>IsAddMonoidHom ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<GOAL>IsAddGroupHom ⇑f
<VAR>α : Type u<VAR>AddCommGroup α<GOAL>IsAddGroupHom Neg.neg
<VAR>α : Type u<VAR>CommGroup α<GOAL>IsGroupHom Inv.inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddGroup α<VAR>AddCommGroup β<VAR>f g : α → β<VAR>hf : IsAddGroupHom f<VAR>hg : IsAddGroupHom g<GOAL>IsAddGroupHom fun a => f a - g a
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>f : M → N<VAR>hf : IsMonoidHom f<VAR>x : Mˣ<GOAL>↑((Units.map' hf) x) = f ↑x
<VAR>M : Type u_1<VAR>Monoid M<GOAL>IsMonoidHom fun x => ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Monoid M<VAR>Monoid N<VAR>f : M → N<VAR>hf : IsMonoidHom f<VAR>x : M<VAR>h : IsUnit x<GOAL>IsUnit (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>Mul α<VAR>Mul β<VAR>f : α → β<VAR>hf : IsMulHom f<GOAL>IsAddHom f
<VAR>α : Type u<VAR>β : Type v<VAR>Add α<VAR>Add β<VAR>f : α → β<VAR>hf : IsAddHom f<GOAL>IsMulHom f
<VAR>α : Type u<VAR>β : Type v<VAR>MulOneClass α<VAR>MulOneClass β<VAR>f : α → β<VAR>hf : IsMonoidHom f<GOAL>IsAddMonoidHom f
<VAR>α : Type u<VAR>β : Type v<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α → β<VAR>hf : IsAddMonoidHom f<GOAL>IsMonoidHom f
<VAR>α : Type u<VAR>β : Type v<VAR>Group α<VAR>Group β<VAR>f : α → β<VAR>hf : IsGroupHom f<GOAL>IsAddGroupHom f
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup α<VAR>AddGroup β<VAR>f : α → β<VAR>hf : IsAddGroupHom f<GOAL>IsGroupHom f
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>s : Set A<VAR>self : IsAddSubmonoid s<GOAL>0 ∈ s
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>s : Set A<VAR>self : IsAddSubmonoid s<VAR>a b : A<GOAL>a ∈ s → b ∈ s → a + b ∈ s
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>self : IsSubmonoid s<GOAL>1 ∈ s
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>self : IsSubmonoid s<VAR>a b : M<GOAL>a ∈ s → b ∈ s → a * b ∈ s
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>IsSubmonoid s → IsAddSubmonoid s
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>IsAddSubmonoid s ↔ IsSubmonoid s
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>s : Set A<GOAL>IsAddSubmonoid s → IsSubmonoid s
<VAR>A : Type u_2<VAR>AddMonoid A<VAR>s : Set A<GOAL>IsSubmonoid s ↔ IsAddSubmonoid s
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s₁ s₂ : Set M<VAR>is₁ : IsAddSubmonoid s₁<VAR>is₂ : IsAddSubmonoid s₂<GOAL>IsAddSubmonoid (s₁ ∩ s₂)
<VAR>M : Type u_1<VAR>Monoid M<VAR>s₁ s₂ : Set M<VAR>is₁ : IsSubmonoid s₁<VAR>is₂ : IsSubmonoid s₂<GOAL>IsSubmonoid (s₁ ∩ s₂)
<VAR>M : Type u_1<VAR>Monoid M<VAR>ι : Sort u_3<VAR>s : ι → Set M<VAR>h : ∀ (y : ι), IsSubmonoid (s y)<GOAL>IsSubmonoid (Set.iInter s)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>ι : Sort u_3<VAR>s : ι → Set M<VAR>h : ∀ (y : ι), IsAddSubmonoid (s y)<GOAL>IsAddSubmonoid (Set.iInter s)
<VAR>M : Type u_1<VAR>Monoid M<VAR>ι : Type u_3<VAR>hι : Nonempty ι<VAR>s : ι → Set M<VAR>hs : ∀ (i : ι), IsSubmonoid (s i)<VAR>Directed : ∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k<GOAL>IsSubmonoid (⋃ i, s i)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>ι : Type u_3<VAR>hι : Nonempty ι<VAR>s : ι → Set M<VAR>hs : ∀ (i : ι), IsAddSubmonoid (s i)<VAR>Directed : ∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k<GOAL>IsAddSubmonoid (⋃ i, s i)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : M<GOAL>0 ∈ multiples x
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<GOAL>1 ∈ powers x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : M<GOAL>x ∈ multiples x
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<GOAL>x ∈ powers x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x y z : M<GOAL>y ∈ multiples x → z ∈ multiples x → y + z ∈ multiples x
<VAR>M : Type u_1<VAR>Monoid M<VAR>x y z : M<GOAL>y ∈ powers x → z ∈ powers x → y * z ∈ powers x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : M<GOAL>IsAddSubmonoid (multiples x)
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<GOAL>IsSubmonoid (powers x)
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>IsAddSubmonoid Set.univ
<VAR>M : Type u_1<VAR>Monoid M<GOAL>IsSubmonoid Set.univ
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>N : Type u_3<VAR>AddMonoid N<VAR>f : M → N<VAR>hf : IsAddMonoidHom f<VAR>s : Set N<VAR>hs : IsAddSubmonoid s<GOAL>IsAddSubmonoid (f ⁻¹' s)
<VAR>M : Type u_1<VAR>Monoid M<VAR>N : Type u_3<VAR>Monoid N<VAR>f : M → N<VAR>hf : IsMonoidHom f<VAR>s : Set N<VAR>hs : IsSubmonoid s<GOAL>IsSubmonoid (f ⁻¹' s)
<VAR>M : Type u_1<VAR>Monoid M<VAR>γ : Type u_3<VAR>Monoid γ<VAR>f : M → γ<VAR>hf : IsMonoidHom f<VAR>s : Set M<VAR>hs : IsSubmonoid s<GOAL>IsSubmonoid (f '' s)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>γ : Type u_3<VAR>AddMonoid γ<VAR>f : M → γ<VAR>hf : IsAddMonoidHom f<VAR>s : Set M<VAR>hs : IsAddSubmonoid s<GOAL>IsAddSubmonoid (f '' s)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>γ : Type u_3<VAR>AddMonoid γ<VAR>f : M → γ<VAR>hf : IsAddMonoidHom f<GOAL>IsAddSubmonoid (Set.range f)
<VAR>M : Type u_1<VAR>Monoid M<VAR>γ : Type u_3<VAR>Monoid γ<VAR>f : M → γ<VAR>hf : IsMonoidHom f<GOAL>IsSubmonoid (Set.range f)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>a : M<VAR>hs : IsAddSubmonoid s<VAR>h : a ∈ s<VAR>n : ℕ<GOAL>n • a ∈ s
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>a : M<VAR>hs : IsSubmonoid s<VAR>h : a ∈ s<VAR>n : ℕ<GOAL>a ^ n ∈ s
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>a : M<VAR>hs : IsSubmonoid s<VAR>h : a ∈ s<GOAL>powers a ⊆ s
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>a : M<VAR>hs : IsAddSubmonoid s<VAR>h : a ∈ s<GOAL>multiples a ⊆ s
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>hs : IsAddSubmonoid s<VAR>l : List M<GOAL>(∀ x ∈ l, x ∈ s) → l.sum ∈ s
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>hs : IsSubmonoid s<VAR>l : List M<GOAL>(∀ x ∈ l, x ∈ s) → l.prod ∈ s
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>s : Set M<VAR>hs : IsSubmonoid s<VAR>m : Multiset M<GOAL>(∀ a ∈ m, a ∈ s) → m.prod ∈ s
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>s : Set M<VAR>hs : IsAddSubmonoid s<VAR>m : Multiset M<GOAL>(∀ a ∈ m, a ∈ s) → m.sum ∈ s
<VAR>M : Type u_3<VAR>A : Type u_4<VAR>CommMonoid M<VAR>s : Set M<VAR>hs : IsSubmonoid s<VAR>f : A → M<VAR>t : Finset A<GOAL>(∀ b ∈ t, f b ∈ s) → ∏ b ∈ t, f b ∈ s
<VAR>M : Type u_3<VAR>A : Type u_4<VAR>AddCommMonoid M<VAR>s : Set M<VAR>hs : IsAddSubmonoid s<VAR>f : A → M<VAR>t : Finset A<GOAL>(∀ b ∈ t, f b ∈ s) → ∑ b ∈ t, f b ∈ s
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<GOAL>IsAddSubmonoid (AddMonoid.Closure s)
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>IsSubmonoid (Monoid.Closure s)
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<GOAL>s ⊆ Monoid.Closure s
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<GOAL>s ⊆ AddMonoid.Closure s
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s t : Set M<VAR>ht : IsAddSubmonoid t<VAR>h : s ⊆ t<GOAL>AddMonoid.Closure s ⊆ t
<VAR>M : Type u_1<VAR>Monoid M<VAR>s t : Set M<VAR>ht : IsSubmonoid t<VAR>h : s ⊆ t<GOAL>Monoid.Closure s ⊆ t
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>AddMonoid.Closure s ⊆ AddMonoid.Closure t
<VAR>M : Type u_1<VAR>Monoid M<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>Monoid.Closure s ⊆ Monoid.Closure t
<VAR>M : Type u_1<VAR>Monoid M<VAR>x : M<GOAL>Monoid.Closure {x} = powers x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>x : M<GOAL>AddMonoid.Closure {x} = multiples x
<VAR>M : Type u_1<VAR>Monoid M<VAR>A : Type u_3<VAR>Monoid A<VAR>f : M → A<VAR>hf : IsMonoidHom f<VAR>s : Set M<GOAL>f '' Monoid.Closure s = Monoid.Closure (f '' s)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>A : Type u_3<VAR>AddMonoid A<VAR>f : M → A<VAR>hf : IsAddMonoidHom f<VAR>s : Set M<GOAL>f '' AddMonoid.Closure s = AddMonoid.Closure (f '' s)
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>s : Set M<VAR>a : M<VAR>h : a ∈ AddMonoid.Closure s<GOAL>∃ l, (∀ x ∈ l, x ∈ s) ∧ l.sum = a
<VAR>M : Type u_1<VAR>Monoid M<VAR>s : Set M<VAR>a : M<VAR>h : a ∈ Monoid.Closure s<GOAL>∃ l, (∀ x ∈ l, x ∈ s) ∧ l.prod = a
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>s t : Set M<VAR>x : M<GOAL>x ∈ AddMonoid.Closure (s ∪ t) ↔ ∃ y ∈ AddMonoid.Closure s, ∃ z ∈ AddMonoid.Closure t, y + z = x
<VAR>M : Type u_3<VAR>CommMonoid M<VAR>s t : Set M<VAR>x : M<GOAL>x ∈ Monoid.Closure (s ∪ t) ↔ ∃ y ∈ Monoid.Closure s, ∃ z ∈ Monoid.Closure t, y * z = x
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>S : AddSubmonoid M<GOAL>IsAddSubmonoid ↑S
<VAR>M : Type u_1<VAR>Monoid M<VAR>S : Submonoid M<GOAL>IsSubmonoid ↑S
<VAR>Y : AlgebraicGeometry.Scheme<VAR>U : Y.OpenCover<GOAL>AlgebraicGeometry.Scheme.zariskiPretopology.coverings Y (CategoryTheory.Presieve.ofArrows U.obj U.map)
<VAR>Y : AlgebraicGeometry.Scheme<VAR>U : Y.OpenCover<GOAL>AlgebraicGeometry.Scheme.zariskiTopology.sieves Y (CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows U.obj U.map))
<GOAL>CategoryTheory.Sheaf.Subcanonical AlgebraicGeometry.Scheme.zariskiTopology
<VAR>M : Type u_7<VAR>α : Sort u_8<VAR>AddCommMonoid M<VAR>f : α → M<GOAL>finsum f = if h : (Function.support (f ∘ PLift.down)).Finite then ∑ i ∈ h.toFinset, f i.down else 0
<VAR>M : Type u_7<VAR>α : Sort u_8<VAR>CommMonoid M<VAR>f : α → M<GOAL>finprod f = if h : (Function.mulSupport (f ∘ PLift.down)).Finite then ∏ i ∈ h.toFinset, f i.down else 1
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>f : α → M<VAR>hf : (Function.mulSupport (f ∘ PLift.down)).Finite<VAR>s : Finset (PLift α)<VAR>hs : hf.toFinset ⊆ s<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ s, f i.down
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>f : α → M<VAR>hf : (Function.support (f ∘ PLift.down)).Finite<VAR>s : Finset (PLift α)<VAR>hs : hf.toFinset ⊆ s<GOAL>∑ᶠ (i : α), f i = ∑ i ∈ s, f i.down
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Finset (PLift α)<VAR>hs : Function.mulSupport (f ∘ PLift.down) ⊆ ↑s<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ s, f i.down
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Finset (PLift α)<VAR>hs : Function.support (f ∘ PLift.down) ⊆ ↑s<GOAL>∑ᶠ (i : α), f i = ∑ i ∈ s, f i.down
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>AddCommMonoid M<GOAL>∑ᶠ (x : α), 0 = 0
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>CommMonoid M<GOAL>∏ᶠ (x : α), 1 = 1
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>IsEmpty α<VAR>f : α → M<GOAL>∑ᶠ (i : α), f i = 0
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>IsEmpty α<VAR>f : α → M<GOAL>∏ᶠ (i : α), f i = 1
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : False → M<GOAL>∑ᶠ (i : False), f i = 0
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : False → M<GOAL>∏ᶠ (i : False), f i = 1
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<VAR>ha : ∀ (x : α), x ≠ a → f x = 0<GOAL>∑ᶠ (x : α), f x = f a
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>ha : ∀ (x : α), x ≠ a → f x = 1<GOAL>∏ᶠ (x : α), f x = f a
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>Unique α<VAR>f : α → M<GOAL>∏ᶠ (i : α), f i = f default
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>Unique α<VAR>f : α → M<GOAL>∑ᶠ (i : α), f i = f default
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : True → M<GOAL>∑ᶠ (i : True), f i = f trivial
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : True → M<GOAL>∏ᶠ (i : True), f i = f trivial
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>p : Prop<VAR>Decidable p<VAR>f : p → M<GOAL>∏ᶠ (i : p), f i = if h : p then f h else 1
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>p : Prop<VAR>Decidable p<VAR>f : p → M<GOAL>∑ᶠ (i : p), f i = if h : p then f h else 0
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>p : Prop<VAR>Decidable p<VAR>x : M<GOAL>∏ᶠ (_ : p), x = if p then x else 1
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>p : Prop<VAR>Decidable p<VAR>x : M<GOAL>∑ᶠ (_ : p), x = if p then x else 0
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>f g : α → M<VAR>h : ∀ (x : α), f x = g x<GOAL>finsum f = finsum g
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>f g : α → M<VAR>h : ∀ (x : α), f x = g x<GOAL>finprod f = finprod g
<VAR>M : Type u_2<VAR>CommMonoid M<VAR>p q : Prop<VAR>f : p → M<VAR>g : q → M<VAR>hpq : p = q<VAR>hfg : ∀ (h : q), f ⋯ = g h<GOAL>finprod f = finprod g
<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>p q : Prop<VAR>f : p → M<VAR>g : q → M<VAR>hpq : p = q<VAR>hfg : ∀ (h : q), f ⋯ = g h<GOAL>finsum f = finsum g
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>f : α → M<VAR>p : M → Prop<VAR>hp₀ : p 0<VAR>hp₁ : ∀ (x y : M), p x → p y → p (x + y)<VAR>hp₂ : ∀ (i : α), p (f i)<GOAL>p (∑ᶠ (i : α), f i)
<VAR>M : Type u_2<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>f : α → M<VAR>p : M → Prop<VAR>hp₀ : p 1<VAR>hp₁ : ∀ (x y : M), p x → p y → p (x * y)<VAR>hp₂ : ∀ (i : α), p (f i)<GOAL>p (∏ᶠ (i : α), f i)
<VAR>α : Sort u_4<VAR>R : Type u_7<VAR>OrderedCommSemiring R<VAR>f : α → R<VAR>hf : ∀ (x : α), 0 ≤ f x<GOAL>0 ≤ ∏ᶠ (x : α), f x
<VAR>α : Sort u_4<VAR>M : Type u_7<VAR>OrderedCommMonoid M<VAR>f : α → M<VAR>hf : ∀ (i : α), 1 ≤ f i<GOAL>1 ≤ ∏ᶠ (i : α), f i
<VAR>α : Sort u_4<VAR>M : Type u_7<VAR>OrderedAddCommMonoid M<VAR>f : α → M<VAR>hf : ∀ (i : α), 0 ≤ f i<GOAL>0 ≤ ∑ᶠ (i : α), f i
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>g : α → M<VAR>h : (Function.support (g ∘ PLift.down)).Finite<GOAL>f (∑ᶠ (x : α), g x) = ∑ᶠ (x : α), f (g x)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>CommMonoid N<VAR>f : M →* N<VAR>g : α → M<VAR>h : (Function.mulSupport (g ∘ PLift.down)).Finite<GOAL>f (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), f (g x)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>p : Prop<VAR>f : M →+ N<VAR>g : p → M<GOAL>f (∑ᶠ (x : p), g x) = ∑ᶠ (x : p), f (g x)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>CommMonoid M<VAR>CommMonoid N<VAR>p : Prop<VAR>f : M →* N<VAR>g : p → M<GOAL>f (∏ᶠ (x : p), g x) = ∏ᶠ (x : p), f (g x)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>hf : ∀ (x : M), f x = 0 → x = 0<VAR>g : α → M<GOAL>f (∑ᶠ (i : α), g i) = ∑ᶠ (i : α), f (g i)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>CommMonoid N<VAR>f : M →* N<VAR>hf : ∀ (x : M), f x = 1 → x = 1<VAR>g : α → M<GOAL>f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>g : M →+ N<VAR>hg : Function.Injective ⇑g<VAR>f : α → M<GOAL>g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>CommMonoid N<VAR>g : M →* N<VAR>hg : Function.Injective ⇑g<VAR>f : α → M<GOAL>g (∏ᶠ (i : α), f i) = ∏ᶠ (i : α), g (f i)
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>CommMonoid M<VAR>CommMonoid N<VAR>g : M ≃* N<VAR>f : α → M<GOAL>g (∏ᶠ (i : α), f i) = ∏ᶠ (i : α), g (f i)