ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Function.Surjective (AddSubmonoid.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (AddSubmonoid.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (Submonoid.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S T : Submonoid M<GOAL>Submonoid.comap f (Submonoid.map f S ⊓ Submonoid.map f T) = S ⊓ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S T : AddSubmonoid M<GOAL>AddSubmonoid.comap f (AddSubmonoid.map f S ⊓ AddSubmonoid.map f T) = S ⊓ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>ι : Type u_5<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S : ι → Submonoid M<GOAL>Submonoid.comap f (⨅ i, Submonoid.map f (S i)) = iInf S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>ι : Type u_5<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S : ι → AddSubmonoid M<GOAL>AddSubmonoid.comap f (⨅ i, AddSubmonoid.map f (S i)) = iInf S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S T : Submonoid M<GOAL>Submonoid.comap f (Submonoid.map f S ⊔ Submonoid.map f T) = S ⊔ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S T : AddSubmonoid M<GOAL>AddSubmonoid.comap f (AddSubmonoid.map f S ⊔ AddSubmonoid.map f T) = S ⊔ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>ι : Type u_5<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S : ι → AddSubmonoid M<GOAL>AddSubmonoid.comap f (⨆ i, AddSubmonoid.map f (S i)) = iSup S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>ι : Type u_5<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S : ι → Submonoid M<GOAL>Submonoid.comap f (⨆ i, Submonoid.map f (S i)) = iSup S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S T : Submonoid M<GOAL>Submonoid.map f S ≤ Submonoid.map f T ↔ S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>S T : AddSubmonoid M<GOAL>AddSubmonoid.map f S ≤ AddSubmonoid.map f T ↔ S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>StrictMono (Submonoid.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>StrictMono (AddSubmonoid.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S : Submonoid N<GOAL>Submonoid.map f (Submonoid.comap f S) = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S : AddSubmonoid N<GOAL>AddSubmonoid.map f (AddSubmonoid.comap f S) = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (AddSubmonoid.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (Submonoid.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective (Submonoid.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective (AddSubmonoid.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S T : AddSubmonoid N<GOAL>AddSubmonoid.map f (AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T) = S ⊓ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S T : Submonoid N<GOAL>Submonoid.map f (Submonoid.comap f S ⊓ Submonoid.comap f T) = S ⊓ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>ι : Type u_5<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → Submonoid N<GOAL>Submonoid.map f (⨅ i, Submonoid.comap f (S i)) = iInf S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>ι : Type u_5<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → AddSubmonoid N<GOAL>AddSubmonoid.map f (⨅ i, AddSubmonoid.comap f (S i)) = iInf S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S T : AddSubmonoid N<GOAL>AddSubmonoid.map f (AddSubmonoid.comap f S ⊔ AddSubmonoid.comap f T) = S ⊔ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S T : Submonoid N<GOAL>Submonoid.map f (Submonoid.comap f S ⊔ Submonoid.comap f T) = S ⊔ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>ι : Type u_5<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → Submonoid N<GOAL>Submonoid.map f (⨆ i, Submonoid.comap f (S i)) = iSup S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>ι : Type u_5<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → AddSubmonoid N<GOAL>AddSubmonoid.map f (⨆ i, AddSubmonoid.comap f (S i)) = iSup S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S T : Submonoid N<GOAL>Submonoid.comap f S ≤ Submonoid.comap f T ↔ S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>S T : AddSubmonoid N<GOAL>AddSubmonoid.comap f S ≤ AddSubmonoid.comap f T ↔ S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>StrictMono (Submonoid.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>StrictMono (AddSubmonoid.comap f)
<VAR>A : Type u_4<VAR>M₁ : Type u_5<VAR>SetLike A M₁<VAR>Zero M₁<VAR>hA : ZeroMemClass A M₁<VAR>S' : A<GOAL>↑0 = 0
<VAR>A : Type u_4<VAR>M₁ : Type u_5<VAR>SetLike A M₁<VAR>One M₁<VAR>hA : OneMemClass A M₁<VAR>S' : A<GOAL>↑1 = 1
<VAR>A : Type u_4<VAR>M₁ : Type u_5<VAR>SetLike A M₁<VAR>Zero M₁<VAR>hA : ZeroMemClass A M₁<VAR>S' : A<VAR>x : ↥S'<GOAL>↑x = 0 ↔ x = 0
<VAR>A : Type u_4<VAR>M₁ : Type u_5<VAR>SetLike A M₁<VAR>One M₁<VAR>hA : OneMemClass A M₁<VAR>S' : A<VAR>x : ↥S'<GOAL>↑x = 1 ↔ x = 1
<VAR>A : Type u_4<VAR>M₁ : Type u_5<VAR>SetLike A M₁<VAR>Zero M₁<VAR>hA : ZeroMemClass A M₁<VAR>S' : A<GOAL>0 = ⟨0, ⋯⟩
<VAR>A : Type u_4<VAR>M₁ : Type u_5<VAR>SetLike A M₁<VAR>One M₁<VAR>hA : OneMemClass A M₁<VAR>S' : A<GOAL>1 = ⟨1, ⋯⟩
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>A : Type u_5<VAR>SetLike A M<VAR>AddSubmonoidClass A M<VAR>S : A<VAR>x : ↥S<VAR>n : ℕ<GOAL>↑(n • x) = n • ↑x
<VAR>M : Type u_6<VAR>Monoid M<VAR>A : Type u_5<VAR>SetLike A M<VAR>SubmonoidClass A M<VAR>S : A<VAR>x : ↥S<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>M : Type u_6<VAR>Monoid M<VAR>A : Type u_5<VAR>SetLike A M<VAR>SubmonoidClass A M<VAR>S : A<VAR>x : M<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩
<VAR>M : Type u_6<VAR>AddMonoid M<VAR>A : Type u_5<VAR>SetLike A M<VAR>AddSubmonoidClass A M<VAR>S : A<VAR>x : M<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>n • ⟨x, hx⟩ = ⟨n • x, ⋯⟩
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>A : Type u_4<VAR>SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<GOAL>⇑(SubmonoidClass.subtype S') = Subtype.val
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>A : Type u_4<VAR>SetLike A M<VAR>hA : AddSubmonoidClass A M<VAR>S' : A<GOAL>⇑(AddSubmonoidClass.subtype S') = Subtype.val
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<VAR>x y : ↥S<GOAL>↑(x + y) = ↑x + ↑y
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<VAR>x y : ↥S<GOAL>↑(x * y) = ↑x * ↑y
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>↑0 = 0
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>↑1 = 1
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<VAR>a : M<VAR>ha : a ∈ S<GOAL>⟨a, ha⟩ = 1 ↔ a = 1
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<VAR>a : M<VAR>ha : a ∈ S<GOAL>⟨a, ha⟩ = 0 ↔ a = 0
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<VAR>x y : M<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<VAR>x y : M<VAR>hx : x ∈ S<VAR>hy : y ∈ S<GOAL>⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<VAR>x y : ↥S<GOAL>x + y = ⟨↑x + ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<VAR>x y : ↥S<GOAL>x * y = ⟨↑x * ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>1 = ⟨1, ⋯⟩
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>0 = ⟨0, ⋯⟩
<VAR>M : Type u_5<VAR>Monoid M<VAR>S : Submonoid M<VAR>x : M<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>x ^ n ∈ S
<VAR>M : Type u_5<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>x : M<VAR>hx : x ∈ S<VAR>n : ℕ<GOAL>n • x ∈ S
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>⇑S.subtype = Subtype.val
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>⇑S.subtype = Subtype.val
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>x : M<GOAL>↑(AddSubmonoid.topEquiv.symm x) = x
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>x : ↥⊤<GOAL>AddSubmonoid.topEquiv x = ↑x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>x : M<GOAL>↑(Submonoid.topEquiv.symm x) = x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>x : ↥⊤<GOAL>Submonoid.topEquiv x = ↑x
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>↑Submonoid.topEquiv = ⊤.subtype
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>↑AddSubmonoid.topEquiv = ⊤.subtype
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>S : AddSubmonoid M<VAR>f : M →+ N<VAR>hf : Function.Injective ⇑f<VAR>x : ↥S<GOAL>↑((S.equivMapOfInjective f hf) x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Submonoid M<VAR>f : M →* N<VAR>hf : Function.Injective ⇑f<VAR>x : ↥S<GOAL>↑((S.equivMapOfInjective f hf) x) = f ↑x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>s : Set M<GOAL>Submonoid.closure (Subtype.val ⁻¹' s) = ⊤
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>s : Set M<GOAL>AddSubmonoid.closure (Subtype.val ⁻¹' s) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<VAR>t : AddSubmonoid N<GOAL>↑(s.prod t) = ↑s ×ˢ ↑t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<VAR>t : Submonoid N<GOAL>↑(s.prod t) = ↑s ×ˢ ↑t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<VAR>t : AddSubmonoid N<VAR>p : M × N<GOAL>p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<VAR>t : Submonoid N<VAR>p : M × N<GOAL>p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s₁ s₂ : AddSubmonoid M<VAR>t₁ t₂ : AddSubmonoid N<VAR>hs : s₁ ≤ s₂<VAR>ht : t₁ ≤ t₂<GOAL>s₁.prod t₁ ≤ s₂.prod t₂
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s₁ s₂ : Submonoid M<VAR>t₁ t₂ : Submonoid N<VAR>hs : s₁ ≤ s₂<VAR>ht : t₁ ≤ t₂<GOAL>s₁.prod t₁ ≤ s₂.prod t₂
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<GOAL>s.prod ⊤ = Submonoid.comap (MonoidHom.fst M N) s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<GOAL>s.prod ⊤ = AddSubmonoid.comap (AddMonoidHom.fst M N) s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid N<GOAL>⊤.prod s = AddSubmonoid.comap (AddMonoidHom.snd M N) s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid N<GOAL>⊤.prod s = Submonoid.comap (MonoidHom.snd M N) s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>⊤.prod ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>⊤.prod ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<GOAL>⊥.prod ⊥ = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<GOAL>⊥.prod ⊥ = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<GOAL>Submonoid.map (MonoidHom.inl M N) s = s.prod ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<GOAL>AddSubmonoid.map (AddMonoidHom.inl M N) s = s.prod ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid N<GOAL>Submonoid.map (MonoidHom.inr M N) s = ⊥.prod s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid N<GOAL>AddSubmonoid.map (AddMonoidHom.inr M N) s = ⊥.prod s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<VAR>t : Submonoid N<GOAL>s.prod ⊥ ⊔ ⊥.prod t = s.prod t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<VAR>t : AddSubmonoid N<GOAL>s.prod ⊥ ⊔ ⊥.prod t = s.prod t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M ≃* N<VAR>K : Submonoid M<VAR>x : N<GOAL>x ∈ Submonoid.map f.toMonoidHom K ↔ f.symm x ∈ K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M ≃+ N<VAR>K : AddSubmonoid M<VAR>x : N<GOAL>x ∈ AddSubmonoid.map f.toAddMonoidHom K ↔ f.symm x ∈ K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M ≃+ N<VAR>K : AddSubmonoid M<GOAL>AddSubmonoid.map f.toAddMonoidHom K = AddSubmonoid.comap f.symm.toAddMonoidHom K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M ≃* N<VAR>K : Submonoid M<GOAL>Submonoid.map f.toMonoidHom K = Submonoid.comap f.symm.toMonoidHom K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : N ≃+ M<VAR>K : AddSubmonoid M<GOAL>AddSubmonoid.comap f K = AddSubmonoid.map f.symm K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : N ≃* M<VAR>K : Submonoid M<GOAL>Submonoid.comap f K = Submonoid.map f.symm K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M ≃* N<GOAL>Submonoid.map f ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M ≃+ N<GOAL>AddSubmonoid.map f ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<VAR>t : Submonoid N<VAR>u : Submonoid (M × N)<GOAL>u ≤ s.prod t ↔ Submonoid.map (MonoidHom.fst M N) u ≤ s ∧ Submonoid.map (MonoidHom.snd M N) u ≤ t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<VAR>t : AddSubmonoid N<VAR>u : AddSubmonoid (M × N)<GOAL>u ≤ s.prod t ↔ AddSubmonoid.map (AddMonoidHom.fst M N) u ≤ s ∧ AddSubmonoid.map (AddMonoidHom.snd M N) u ≤ t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>s : Submonoid M<VAR>t : Submonoid N<VAR>u : Submonoid (M × N)<GOAL>s.prod t ≤ u ↔ Submonoid.map (MonoidHom.inl M N) s ≤ u ∧ Submonoid.map (MonoidHom.inr M N) t ≤ u
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>s : AddSubmonoid M<VAR>t : AddSubmonoid N<VAR>u : AddSubmonoid (M × N)<GOAL>s.prod t ≤ u ↔ AddSubmonoid.map (AddMonoidHom.inl M N) s ≤ u ∧ AddSubmonoid.map (AddMonoidHom.inr M N) t ≤ u
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>↑(MonoidHom.mrange f) = Set.range ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<GOAL>↑(AddMonoidHom.mrange f) = Set.range ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>y : N<GOAL>y ∈ MonoidHom.mrange f ↔ ∃ x, f x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>y : N<GOAL>y ∈ AddMonoidHom.mrange f ↔ ∃ x, f x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>MonoidHom.mrange f = Submonoid.map f ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<GOAL>AddMonoidHom.mrange f = AddSubmonoid.map f ⊤
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>AddMonoidHom.mrange (AddMonoidHom.id M) = ⊤
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>MonoidHom.mrange (MonoidHom.id M) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddZeroClass P<VAR>g : N →+ P<VAR>f : M →+ N<GOAL>AddSubmonoid.map g (AddMonoidHom.mrange f) = AddMonoidHom.mrange (g.comp f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>MulOneClass M<VAR>MulOneClass N<VAR>MulOneClass P<VAR>g : N →* P<VAR>f : M →* N<GOAL>Submonoid.map g (MonoidHom.mrange f) = MonoidHom.mrange (g.comp f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>MonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<GOAL>AddMonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>AddMonoidHom.mrange f = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>MonoidHom.mrange f = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>s : Set N<GOAL>Submonoid.closure (⇑f ⁻¹' s) ≤ Submonoid.comap f (Submonoid.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>s : Set N<GOAL>AddSubmonoid.closure (⇑f ⁻¹' s) ≤ AddSubmonoid.comap f (AddSubmonoid.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>s : Set M<GOAL>AddSubmonoid.map f (AddSubmonoid.closure s) = AddSubmonoid.closure (⇑f '' s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>s : Set M<GOAL>Submonoid.map f (Submonoid.closure s) = Submonoid.closure (⇑f '' s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<GOAL>AddSubmonoid.closure (Set.range ⇑f) = AddMonoidHom.mrange f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>Submonoid.closure (Set.range ⇑f) = MonoidHom.mrange f
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>N : Type u_6<VAR>S : Type u_7<VAR>MulOneClass N<VAR>SetLike S M<VAR>SubmonoidClass S M<VAR>f : M →* N<VAR>s : S<VAR>x : ↥s<GOAL>(f.restrict s) x = f ↑x
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>N : Type u_6<VAR>S : Type u_7<VAR>AddZeroClass N<VAR>SetLike S M<VAR>AddSubmonoidClass S M<VAR>f : M →+ N<VAR>s : S<VAR>x : ↥s<GOAL>(f.restrict s) x = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Submonoid M<VAR>f : M →* N<GOAL>MonoidHom.mrange (f.restrict S) = Submonoid.map f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>S : AddSubmonoid M<VAR>f : M →+ N<GOAL>AddMonoidHom.mrange (f.restrict S) = AddSubmonoid.map f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Type u_6<VAR>SetLike S N<VAR>SubmonoidClass S N<VAR>f : M →* N<VAR>s : S<VAR>h : ∀ (x : M), f x ∈ s<VAR>n : M<GOAL>(f.codRestrict s h) n = ⟨f n, ⋯⟩
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>S : Type u_6<VAR>SetLike S N<VAR>AddSubmonoidClass S N<VAR>f : M →+ N<VAR>s : S<VAR>h : ∀ (x : M), f x ∈ s<VAR>n : M<GOAL>(f.codRestrict s h) n = ⟨f n, ⋯⟩
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>N : Type u_6<VAR>AddZeroClass N<VAR>f : M →+ N<VAR>x : M<GOAL>↑(f.mrangeRestrict x) = f x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>N : Type u_6<VAR>MulOneClass N<VAR>f : M →* N<VAR>x : M<GOAL>↑(f.mrangeRestrict x) = f x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>f : M →+ N<GOAL>Function.Surjective ⇑f.mrangeRestrict
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>f : M →* N<GOAL>Function.Surjective ⇑f.mrangeRestrict
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<VAR>x : M<GOAL>x ∈ MonoidHom.mker f ↔ f x = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<VAR>x : M<GOAL>x ∈ AddMonoidHom.mker f ↔ f x = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>↑(MonoidHom.mker f) = ⇑f ⁻¹' {1}
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>F : Type u_5<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<GOAL>↑(AddMonoidHom.mker f) = ⇑f ⁻¹' {0}