ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>MulOneClass G<VAR>MulOneClass H<VAR>f : Additive G ≃+ Additive H<VAR>a : G<GOAL>(MulEquiv.toAdditive.symm f) a = (MonoidHom.toAdditive.symm f.toAddMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>MulOneClass G<VAR>MulOneClass H<VAR>f : G ≃* H<VAR>a : Additive G<GOAL>(MulEquiv.toAdditive f) a = (MonoidHom.toAdditive f.toMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>MulOneClass G<VAR>MulOneClass H<VAR>f : G ≃* H<VAR>a : Additive H<GOAL>(MulEquiv.toAdditive f).symm a = (MonoidHom.toAdditive f.symm.toMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>MulOneClass G<VAR>MulOneClass H<VAR>f : Additive G ≃+ Additive H<VAR>a : H<GOAL>(MulEquiv.toAdditive.symm f).symm a = (MonoidHom.toAdditive.symm f.symm.toAddMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>MulOneClass G<VAR>AddZeroClass H<VAR>f : Additive G ≃+ H<VAR>a : G<GOAL>(AddEquiv.toMultiplicative' f) a = (AddMonoidHom.toMultiplicative' f.toAddMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>MulOneClass G<VAR>AddZeroClass H<VAR>f : G ≃* Multiplicative H<VAR>a : Additive G<GOAL>(AddEquiv.toMultiplicative'.symm f) a = (AddMonoidHom.toMultiplicative'.symm f.toMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>MulOneClass G<VAR>AddZeroClass H<VAR>f : Additive G ≃+ H<VAR>a : Multiplicative H<GOAL>(AddEquiv.toMultiplicative' f).symm a = (AddMonoidHom.toMultiplicative'' f.symm.toAddMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>MulOneClass G<VAR>AddZeroClass H<VAR>f : G ≃* Multiplicative H<VAR>a : H<GOAL>(AddEquiv.toMultiplicative'.symm f).symm a = (AddMonoidHom.toMultiplicative''.symm f.symm.toMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddZeroClass G<VAR>MulOneClass H<VAR>f : G ≃+ Additive H<VAR>a : Multiplicative G<GOAL>(AddEquiv.toMultiplicative'' f) a = (AddMonoidHom.toMultiplicative'' f.toAddMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddZeroClass G<VAR>MulOneClass H<VAR>f : G ≃+ Additive H<VAR>a : H<GOAL>(AddEquiv.toMultiplicative'' f).symm a = (AddMonoidHom.toMultiplicative' f.symm.toAddMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddZeroClass G<VAR>MulOneClass H<VAR>f : Multiplicative G ≃* H<VAR>a : Additive H<GOAL>(AddEquiv.toMultiplicative''.symm f).symm a = (AddMonoidHom.toMultiplicative'.symm f.symm.toMonoidHom) a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddZeroClass G<VAR>MulOneClass H<VAR>f : Multiplicative G ≃* H<VAR>a : G<GOAL>(AddEquiv.toMultiplicative''.symm f) a = (AddMonoidHom.toMultiplicative''.symm f.toMonoidHom) a
<VAR>M : Type u_3<VAR>MulOneClass M<VAR>f : M →* M<VAR>a : Additive M<GOAL>((monoidEndToAdditive M) f) a = Additive.ofMul (f (Additive.toMul a))
<VAR>M : Type u_3<VAR>MulOneClass M<VAR>f : Additive M →+ Additive M<VAR>a : M<GOAL>((monoidEndToAdditive M).symm f) a = Additive.toMul (f (Additive.ofMul a))
<VAR>A : Type u_3<VAR>AddZeroClass A<VAR>f : Multiplicative A →* Multiplicative A<VAR>a : A<GOAL>((addMonoidEndToMultiplicative A).symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))
<VAR>A : Type u_3<VAR>AddZeroClass A<VAR>f : A →+ A<VAR>a : Multiplicative A<GOAL>((addMonoidEndToMultiplicative A) f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))
<VAR>G : Type u_1<VAR>AddZeroClass G<VAR>a : Additive (Multiplicative G)<GOAL>(AddEquiv.additiveMultiplicative G) a = Multiplicative.toAdd (Additive.toMul a)
<VAR>G : Type u_1<VAR>AddZeroClass G<VAR>a : G<GOAL>(AddEquiv.additiveMultiplicative G).symm a = Additive.ofMul (Multiplicative.ofAdd a)
<VAR>H : Type u_2<VAR>MulOneClass H<VAR>a : Multiplicative (Additive H)<GOAL>(MulEquiv.multiplicativeAdditive H) a = Additive.toMul (Multiplicative.toAdd a)
<VAR>H : Type u_2<VAR>MulOneClass H<VAR>a : H<GOAL>(MulEquiv.multiplicativeAdditive H).symm a = Multiplicative.ofAdd (Additive.ofMul a)
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>self : NatPowAssoc M<VAR>x : M<GOAL>x ^ 1 = x
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>self : NatPowAssoc M<VAR>x : M<GOAL>x ^ 0 = 1
<VAR>M : Type u_2<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>self : NatPowAssoc M<VAR>k n : ℕ<VAR>x : M<GOAL>x ^ (k + n) = x ^ k * x ^ n
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>NatPowAssoc M<VAR>k n : ℕ<VAR>x : M<GOAL>x ^ (k + n) = x ^ k * x ^ n
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>NatPowAssoc M<VAR>x : M<GOAL>x ^ 0 = 1
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>NatPowAssoc M<VAR>x : M<GOAL>x ^ 1 = x
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>NatPowAssoc M<VAR>k m n : ℕ<VAR>x : M<GOAL>x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>NatPowAssoc M<VAR>m n : ℕ<VAR>x : M<GOAL>x ^ m * x ^ n = x ^ n * x ^ m
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>NatPowAssoc M<VAR>x : M<VAR>m n : ℕ<GOAL>x ^ (m * n) = (x ^ m) ^ n
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>Pow M ℕ<VAR>NatPowAssoc M<VAR>x : M<VAR>m n : ℕ<GOAL>x ^ (m * n) = (x ^ n) ^ m
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>a b : R<VAR>k : ℕ<GOAL>(-1) ^ k * a * b = (-1) ^ k * (a * b)
<VAR>R : Type u_2<VAR>NonAssocSemiring R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>n m : ℕ<GOAL>↑(n ^ m) = ↑n ^ m
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>Pow R ℕ<VAR>NatPowAssoc R<VAR>n : ℤ<VAR>m : ℕ<GOAL>↑(n ^ m) = ↑n ^ m
<VAR>M : Type u_1<VAR>Add M<VAR>z : M<VAR>self : IsAddCentral z<VAR>a c : M<GOAL>a + z + c = a + (z + c)
<VAR>M : Type u_1<VAR>Add M<VAR>z : M<VAR>self : IsAddCentral z<VAR>a : M<GOAL>z + a = a + z
<VAR>M : Type u_1<VAR>Add M<VAR>z : M<VAR>self : IsAddCentral z<VAR>a b : M<GOAL>a + b + z = a + (b + z)
<VAR>M : Type u_1<VAR>Add M<VAR>z : M<VAR>self : IsAddCentral z<VAR>b c : M<GOAL>z + (b + c) = z + b + c
<VAR>M : Type u_1<VAR>Mul M<VAR>z : M<VAR>self : IsMulCentral z<VAR>a c : M<GOAL>a * z * c = a * (z * c)
<VAR>M : Type u_1<VAR>Mul M<VAR>z : M<VAR>self : IsMulCentral z<VAR>b c : M<GOAL>z * (b * c) = z * b * c
<VAR>M : Type u_1<VAR>Mul M<VAR>z : M<VAR>self : IsMulCentral z<VAR>a b : M<GOAL>a * b * z = a * (b * z)
<VAR>M : Type u_1<VAR>Mul M<VAR>z : M<VAR>self : IsMulCentral z<VAR>a : M<GOAL>z * a = a * z
<VAR>M : Type u_1<VAR>a : M<VAR>Mul M<VAR>h : IsMulCentral a<VAR>b c : M<GOAL>a * (b * c) = b * (a * c)
<VAR>M : Type u_1<VAR>a : M<VAR>Add M<VAR>h : IsAddCentral a<VAR>b c : M<GOAL>a + (b + c) = b + (a + c)
<VAR>M : Type u_1<VAR>c : M<VAR>Add M<VAR>h : IsAddCentral c<VAR>a b : M<GOAL>a + b + c = a + c + b
<VAR>M : Type u_1<VAR>c : M<VAR>Mul M<VAR>h : IsMulCentral c<VAR>a b : M<GOAL>a * b * c = a * c * b
<VAR>M : Type u_1<VAR>Add M<VAR>z : M<GOAL>z ∈ Set.addCenter M ↔ IsAddCentral z
<VAR>M : Type u_1<VAR>Mul M<VAR>z : M<GOAL>z ∈ Set.center M ↔ IsMulCentral z
<VAR>M : Type u_1<VAR>S : Set M<VAR>Add M<VAR>c : M<GOAL>c ∈ S.addCentralizer ↔ ∀ m ∈ S, m + c = c + m
<VAR>M : Type u_1<VAR>S : Set M<VAR>Mul M<VAR>c : M<GOAL>c ∈ S.centralizer ↔ ∀ m ∈ S, m * c = c * m
<VAR>M : Type u_1<VAR>Mul M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ Set.center M<VAR>hz₂ : z₂ ∈ Set.center M<GOAL>z₁ * z₂ ∈ Set.center M
<VAR>M : Type u_1<VAR>Add M<VAR>z₁ z₂ : M<VAR>hz₁ : z₁ ∈ Set.addCenter M<VAR>hz₂ : z₂ ∈ Set.addCenter M<GOAL>z₁ + z₂ ∈ Set.addCenter M
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set M<GOAL>Set.center M ⊆ S.centralizer
<VAR>M : Type u_1<VAR>Add M<VAR>S : Set M<GOAL>Set.addCenter M ⊆ S.addCentralizer
<VAR>M : Type u_1<VAR>S T : Set M<VAR>Add M<VAR>h : S ⊆ T<GOAL>T.addCentralizer ⊆ S.addCentralizer
<VAR>M : Type u_1<VAR>S T : Set M<VAR>Mul M<VAR>h : S ⊆ T<GOAL>T.centralizer ⊆ S.centralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>Add M<GOAL>S ⊆ S.addCentralizer.addCentralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>Mul M<GOAL>S ⊆ S.centralizer.centralizer
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set M<GOAL>S.centralizer.centralizer.centralizer = S.centralizer
<VAR>M : Type u_1<VAR>Add M<VAR>S : Set M<GOAL>S.addCentralizer.addCentralizer.addCentralizer = S.addCentralizer
<VAR>M : Type u_1<VAR>Semigroup M<VAR>z : M<GOAL>z ∈ Set.center M ↔ ∀ (g : M), g * z = z * g
<VAR>M : Type u_1<VAR>AddSemigroup M<VAR>z : M<GOAL>z ∈ Set.addCenter M ↔ ∀ (g : M), g + z = z + g
<VAR>M : Type u_1<VAR>S : Set M<VAR>Semigroup M<VAR>a b : M<VAR>ha : a ∈ S.centralizer<VAR>hb : b ∈ S.centralizer<GOAL>a * b ∈ S.centralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddSemigroup M<VAR>a b : M<VAR>ha : a ∈ S.addCentralizer<VAR>hb : b ∈ S.addCentralizer<GOAL>a + b ∈ S.addCentralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>Semigroup M<GOAL>S.centralizer = Set.univ ↔ S ⊆ Set.center M
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddSemigroup M<GOAL>S.addCentralizer = Set.univ ↔ S ⊆ Set.addCenter M
<VAR>M : Type u_1<VAR>Semigroup M<GOAL>Set.univ.centralizer = Set.center M
<VAR>M : Type u_1<VAR>AddSemigroup M<GOAL>Set.univ.addCentralizer = Set.addCenter M
<VAR>M : Type u_1<VAR>CommSemigroup M<GOAL>Set.center M = Set.univ
<VAR>M : Type u_1<VAR>AddCommSemigroup M<GOAL>Set.addCenter M = Set.univ
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddCommSemigroup M<GOAL>S.addCentralizer = Set.univ
<VAR>M : Type u_1<VAR>S : Set M<VAR>CommSemigroup M<GOAL>S.centralizer = Set.univ
<VAR>M : Type u_1<VAR>AddZeroClass M<GOAL>0 ∈ Set.addCenter M
<VAR>M : Type u_1<VAR>MulOneClass M<GOAL>1 ∈ Set.center M
<VAR>M : Type u_1<VAR>S : Set M<VAR>MulOneClass M<GOAL>1 ∈ S.centralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddZeroClass M<GOAL>0 ∈ S.addCentralizer
<VAR>M : Type u_1<VAR>AddMonoid M<GOAL>AddUnits.val ⁻¹' Set.addCenter M ⊆ Set.addCenter (AddUnits M)
<VAR>M : Type u_1<VAR>Monoid M<GOAL>Units.val ⁻¹' Set.center M ⊆ Set.center Mˣ
<VAR>M : Type u_1<VAR>AddMonoid M<VAR>a : AddUnits M<VAR>ha : ↑a ∈ Set.addCenter M<GOAL>↑(-a) ∈ Set.addCenter M
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : Mˣ<VAR>ha : ↑a ∈ Set.center M<GOAL>↑a⁻¹ ∈ Set.center M
<VAR>M : Type u_1<VAR>Monoid M<VAR>a : M<VAR>Invertible a<VAR>ha : a ∈ Set.center M<GOAL>⅟a ∈ Set.center M
<VAR>M : Type u_1<VAR>SubtractionMonoid M<VAR>a : M<VAR>ha : a ∈ Set.addCenter M<GOAL>-a ∈ Set.addCenter M
<VAR>M : Type u_1<VAR>DivisionMonoid M<VAR>a : M<VAR>ha : a ∈ Set.center M<GOAL>a⁻¹ ∈ Set.center M
<VAR>M : Type u_1<VAR>DivisionMonoid M<VAR>a b : M<VAR>ha : a ∈ Set.center M<VAR>hb : b ∈ Set.center M<GOAL>a / b ∈ Set.center M
<VAR>M : Type u_1<VAR>SubtractionMonoid M<VAR>a b : M<VAR>ha : a ∈ Set.addCenter M<VAR>hb : b ∈ Set.addCenter M<GOAL>a - b ∈ Set.addCenter M
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddGroup M<VAR>a : M<VAR>ha : a ∈ S.addCentralizer<GOAL>-a ∈ S.addCentralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>Group M<VAR>a : M<VAR>ha : a ∈ S.centralizer<GOAL>a⁻¹ ∈ S.centralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>Group M<VAR>a b : M<VAR>ha : a ∈ S.centralizer<VAR>hb : b ∈ S.centralizer<GOAL>a / b ∈ S.centralizer
<VAR>M : Type u_1<VAR>S : Set M<VAR>AddGroup M<VAR>a b : M<VAR>ha : a ∈ S.addCentralizer<VAR>hb : b ∈ S.addCentralizer<GOAL>a - b ∈ S.addCentralizer
<VAR>G : Type u_1<VAR>Group G<VAR>g₁ g₂ : G<GOAL>⁅g₁, g₂⁆ = g₁ * g₂ * g₁⁻¹ * g₂⁻¹
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : AddSubmonoid (Additive M)<GOAL>↑((RelIso.symm Submonoid.toAddSubmonoid) S) = ⇑Additive.ofMul ⁻¹' ↑S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>↑(Submonoid.toAddSubmonoid S) = ⇑Additive.toMul ⁻¹' ↑S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Set M<GOAL>Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S)
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Set (Additive M)<GOAL>AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S) = Submonoid.closure (⇑Multiplicative.ofAdd ⁻¹' S)
<VAR>A : Type u_4<VAR>AddZeroClass A<VAR>S : AddSubmonoid A<GOAL>↑(AddSubmonoid.toSubmonoid S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
<VAR>A : Type u_4<VAR>AddZeroClass A<VAR>S : Submonoid (Multiplicative A)<GOAL>↑((RelIso.symm AddSubmonoid.toSubmonoid) S) = ⇑Multiplicative.ofAdd ⁻¹' ↑S
<VAR>A : Type u_4<VAR>AddZeroClass A<VAR>S : Set A<GOAL>AddSubmonoid.toSubmonoid (AddSubmonoid.closure S) = Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' S)
<VAR>A : Type u_4<VAR>AddZeroClass A<VAR>S : Set (Multiplicative A)<GOAL>Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (⇑Additive.ofMul ⁻¹' 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>S : Submonoid N<VAR>f : F<GOAL>↑(Submonoid.comap f S) = ⇑f ⁻¹' ↑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>S : AddSubmonoid N<VAR>f : F<GOAL>↑(AddSubmonoid.comap f S) = ⇑f ⁻¹' ↑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>S : AddSubmonoid N<VAR>f : F<VAR>x : M<GOAL>x ∈ AddSubmonoid.comap f S ↔ f x ∈ 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>S : Submonoid N<VAR>f : F<VAR>x : M<GOAL>x ∈ Submonoid.comap f S ↔ f x ∈ S
<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>S : Submonoid P<VAR>g : N →* P<VAR>f : M →* N<GOAL>Submonoid.comap f (Submonoid.comap g S) = Submonoid.comap (g.comp f) S
<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>S : AddSubmonoid P<VAR>g : N →+ P<VAR>f : M →+ N<GOAL>AddSubmonoid.comap f (AddSubmonoid.comap g S) = AddSubmonoid.comap (g.comp f) S
<VAR>P : Type u_3<VAR>MulOneClass P<VAR>S : Submonoid P<GOAL>Submonoid.comap (MonoidHom.id P) S = S
<VAR>P : Type u_3<VAR>AddZeroClass P<VAR>S : AddSubmonoid P<GOAL>AddSubmonoid.comap (AddMonoidHom.id P) 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>S : AddSubmonoid M<GOAL>↑(AddSubmonoid.map f S) = ⇑f '' ↑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>S : Submonoid M<GOAL>↑(Submonoid.map f S) = ⇑f '' ↑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>S : Submonoid M<VAR>y : N<GOAL>y ∈ Submonoid.map f S ↔ ∃ x ∈ S, f x = y
<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>S : AddSubmonoid M<VAR>y : N<GOAL>y ∈ AddSubmonoid.map f S ↔ ∃ x ∈ S, f x = y
<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>S : AddSubmonoid M<VAR>x : M<VAR>hx : x ∈ S<GOAL>f x ∈ AddSubmonoid.map f 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>S : Submonoid M<VAR>x : M<VAR>hx : x ∈ S<GOAL>f x ∈ Submonoid.map f 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>S : AddSubmonoid M<VAR>x : ↥S<GOAL>f ↑x ∈ AddSubmonoid.map f 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>S : Submonoid M<VAR>x : ↥S<GOAL>f ↑x ∈ Submonoid.map f S
<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>S : AddSubmonoid M<VAR>g : N →+ P<VAR>f : M →+ N<GOAL>AddSubmonoid.map g (AddSubmonoid.map f S) = AddSubmonoid.map (g.comp f) S
<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>S : Submonoid M<VAR>g : N →* P<VAR>f : M →* N<GOAL>Submonoid.map g (Submonoid.map f S) = Submonoid.map (g.comp f) 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 : Submonoid M<VAR>x : M<GOAL>f x ∈ Submonoid.map f S ↔ x ∈ 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.Injective ⇑f<VAR>S : AddSubmonoid M<VAR>x : M<GOAL>f x ∈ AddSubmonoid.map f S ↔ x ∈ 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>S : AddSubmonoid M<VAR>T : AddSubmonoid N<GOAL>AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f 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>S : Submonoid M<VAR>T : Submonoid N<GOAL>Submonoid.map f S ≤ T ↔ S ≤ Submonoid.comap f 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<GOAL>GaloisConnection (Submonoid.map f) (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<GOAL>GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Submonoid M<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>T : Submonoid N<VAR>f : F<GOAL>S ≤ Submonoid.comap f T → Submonoid.map f S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>S : AddSubmonoid M<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>T : AddSubmonoid N<VAR>f : F<GOAL>S ≤ AddSubmonoid.comap f T → AddSubmonoid.map f S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>S : AddSubmonoid M<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>T : AddSubmonoid N<VAR>f : F<GOAL>AddSubmonoid.map f S ≤ T → S ≤ AddSubmonoid.comap f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Submonoid M<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>T : Submonoid N<VAR>f : F<GOAL>Submonoid.map f S ≤ T → S ≤ Submonoid.comap f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Submonoid M<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>S ≤ Submonoid.comap f (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 : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<GOAL>S ≤ AddSubmonoid.comap f (AddSubmonoid.map f 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>S : AddSubmonoid N<VAR>f : F<GOAL>AddSubmonoid.map f (AddSubmonoid.comap f S) ≤ 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>S : Submonoid N<VAR>f : F<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<GOAL>Monotone (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<GOAL>Monotone (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<GOAL>Monotone (AddSubmonoid.comap 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<GOAL>Monotone (Submonoid.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>S : AddSubmonoid M<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : AddMonoidHomClass F M N<VAR>f : F<GOAL>AddSubmonoid.map f (AddSubmonoid.comap f (AddSubmonoid.map f S)) = AddSubmonoid.map f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>MulOneClass N<VAR>S : Submonoid M<VAR>F : Type u_4<VAR>FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : F<GOAL>Submonoid.map f (Submonoid.comap f (Submonoid.map f S)) = Submonoid.map f 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>S : Submonoid N<VAR>f : F<GOAL>Submonoid.comap f (Submonoid.map f (Submonoid.comap f S)) = Submonoid.comap f 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>S : AddSubmonoid N<VAR>f : F<GOAL>AddSubmonoid.comap f (AddSubmonoid.map f (AddSubmonoid.comap f S)) = AddSubmonoid.comap f 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>S T : Submonoid M<VAR>f : F<GOAL>Submonoid.map f (S ⊔ T) = Submonoid.map f S ⊔ Submonoid.map f 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>S T : AddSubmonoid M<VAR>f : F<GOAL>AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f 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>ι : Sort u_5<VAR>f : F<VAR>s : ι → Submonoid M<GOAL>Submonoid.map f (iSup s) = ⨆ i, Submonoid.map f (s i)
<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>ι : Sort u_5<VAR>f : F<VAR>s : ι → AddSubmonoid M<GOAL>AddSubmonoid.map f (iSup s) = ⨆ i, AddSubmonoid.map f (s i)
<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>S T : Submonoid N<VAR>f : F<GOAL>Submonoid.comap f (S ⊓ T) = Submonoid.comap f S ⊓ Submonoid.comap f 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>S T : AddSubmonoid N<VAR>f : F<GOAL>AddSubmonoid.comap f (S ⊓ T) = AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f 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>ι : Sort u_5<VAR>f : F<VAR>s : ι → AddSubmonoid N<GOAL>AddSubmonoid.comap f (iInf s) = ⨅ i, AddSubmonoid.comap f (s i)
<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>ι : Sort u_5<VAR>f : F<VAR>s : ι → Submonoid N<GOAL>Submonoid.comap f (iInf s) = ⨅ i, Submonoid.comap f (s i)
<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<GOAL>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<GOAL>AddSubmonoid.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<GOAL>AddSubmonoid.comap 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<GOAL>Submonoid.comap f ⊤ = ⊤
<VAR>M : Type u_1<VAR>AddZeroClass M<VAR>S : AddSubmonoid M<GOAL>AddSubmonoid.map (AddMonoidHom.id M) S = S
<VAR>M : Type u_1<VAR>MulOneClass M<VAR>S : Submonoid M<GOAL>Submonoid.map (MonoidHom.id M) S = 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 : Submonoid M<GOAL>Submonoid.comap f (Submonoid.map 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.Injective ⇑f<VAR>S : AddSubmonoid M<GOAL>AddSubmonoid.comap f (AddSubmonoid.map f S) = 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<GOAL>Function.Surjective (Submonoid.comap f)