ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>S : Subsemigroup M<VAR>g : N →ₙ* P<VAR>f : M →ₙ* N<GOAL>Subsemigroup.map g (Subsemigroup.map f S) = Subsemigroup.map (g.comp f) S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Add M<VAR>Add N<VAR>Add P<VAR>S : AddSubsemigroup M<VAR>g : AddHom N P<VAR>f : AddHom M N<GOAL>AddSubsemigroup.map g (AddSubsemigroup.map f S) = AddSubsemigroup.map (g.comp f) S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<VAR>S : Subsemigroup M<VAR>x : M<GOAL>f x ∈ Subsemigroup.map f S ↔ x ∈ S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<VAR>S : AddSubsemigroup M<VAR>x : M<GOAL>f x ∈ AddSubsemigroup.map f S ↔ x ∈ S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>S : Subsemigroup M<VAR>T : Subsemigroup N<GOAL>Subsemigroup.map f S ≤ T ↔ S ≤ Subsemigroup.comap f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>S : AddSubsemigroup M<VAR>T : AddSubsemigroup N<GOAL>AddSubsemigroup.map f S ≤ T ↔ S ≤ AddSubsemigroup.comap f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>GaloisConnection (Subsemigroup.map f) (Subsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>GaloisConnection (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S : Subsemigroup M<VAR>T : Subsemigroup N<VAR>f : M →ₙ* N<GOAL>S ≤ Subsemigroup.comap f T → Subsemigroup.map f S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup M<VAR>T : AddSubsemigroup N<VAR>f : AddHom M N<GOAL>S ≤ AddSubsemigroup.comap f T → AddSubsemigroup.map f S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup M<VAR>T : AddSubsemigroup N<VAR>f : AddHom M N<GOAL>AddSubsemigroup.map f S ≤ T → S ≤ AddSubsemigroup.comap f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S : Subsemigroup M<VAR>T : Subsemigroup N<VAR>f : M →ₙ* N<GOAL>Subsemigroup.map f S ≤ T → S ≤ Subsemigroup.comap f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup M<VAR>f : AddHom M N<GOAL>S ≤ AddSubsemigroup.comap f (AddSubsemigroup.map f S)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S : Subsemigroup M<VAR>f : M →ₙ* N<GOAL>S ≤ Subsemigroup.comap f (Subsemigroup.map f S)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S : Subsemigroup N<VAR>f : M →ₙ* N<GOAL>Subsemigroup.map f (Subsemigroup.comap f S) ≤ S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup N<VAR>f : AddHom M N<GOAL>AddSubsemigroup.map f (AddSubsemigroup.comap f S) ≤ S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>Monotone (Subsemigroup.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>Monotone (AddSubsemigroup.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>Monotone (AddSubsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>Monotone (Subsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup M<VAR>f : AddHom M N<GOAL>AddSubsemigroup.map f (AddSubsemigroup.comap f (AddSubsemigroup.map f S)) = AddSubsemigroup.map f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S : Subsemigroup M<VAR>f : M →ₙ* N<GOAL>Subsemigroup.map f (Subsemigroup.comap f (Subsemigroup.map f S)) = Subsemigroup.map f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S : Subsemigroup N<VAR>f : M →ₙ* N<GOAL>Subsemigroup.comap f (Subsemigroup.map f (Subsemigroup.comap f S)) = Subsemigroup.comap f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup N<VAR>f : AddHom M N<GOAL>AddSubsemigroup.comap f (AddSubsemigroup.map f (AddSubsemigroup.comap f S)) = AddSubsemigroup.comap f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S T : Subsemigroup M<VAR>f : M →ₙ* N<GOAL>Subsemigroup.map f (S ⊔ T) = Subsemigroup.map f S ⊔ Subsemigroup.map f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S T : AddSubsemigroup M<VAR>f : AddHom M N<GOAL>AddSubsemigroup.map f (S ⊔ T) = AddSubsemigroup.map f S ⊔ AddSubsemigroup.map f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>ι : Sort u_5<VAR>f : M →ₙ* N<VAR>s : ι → Subsemigroup M<GOAL>Subsemigroup.map f (iSup s) = ⨆ i, Subsemigroup.map f (s i)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>ι : Sort u_5<VAR>f : AddHom M N<VAR>s : ι → AddSubsemigroup M<GOAL>AddSubsemigroup.map f (iSup s) = ⨆ i, AddSubsemigroup.map f (s i)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S T : Subsemigroup N<VAR>f : M →ₙ* N<GOAL>Subsemigroup.comap f (S ⊓ T) = Subsemigroup.comap f S ⊓ Subsemigroup.comap f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S T : AddSubsemigroup N<VAR>f : AddHom M N<GOAL>AddSubsemigroup.comap f (S ⊓ T) = AddSubsemigroup.comap f S ⊓ AddSubsemigroup.comap f T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>ι : Sort u_5<VAR>f : M →ₙ* N<VAR>s : ι → Subsemigroup N<GOAL>Subsemigroup.comap f (iInf s) = ⨅ i, Subsemigroup.comap f (s i)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>ι : Sort u_5<VAR>f : AddHom M N<VAR>s : ι → AddSubsemigroup N<GOAL>AddSubsemigroup.comap f (iInf s) = ⨅ i, AddSubsemigroup.comap f (s i)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>AddSubsemigroup.map f ⊥ = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>Subsemigroup.map f ⊥ = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>AddSubsemigroup.comap f ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>Subsemigroup.comap f ⊤ = ⊤
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Subsemigroup M<GOAL>Subsemigroup.map (MulHom.id M) S = S
<VAR>M : Type u_1<VAR>Add M<VAR>S : AddSubsemigroup M<GOAL>AddSubsemigroup.map (AddHom.id M) S = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<VAR>S : AddSubsemigroup M<GOAL>AddSubsemigroup.comap f (AddSubsemigroup.map f S) = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<VAR>S : Subsemigroup M<GOAL>Subsemigroup.comap f (Subsemigroup.map f S) = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Surjective (Subsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Surjective (AddSubsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (Subsemigroup.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (AddSubsemigroup.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<VAR>S T : AddSubsemigroup M<GOAL>AddSubsemigroup.comap f (AddSubsemigroup.map f S ⊓ AddSubsemigroup.map f T) = S ⊓ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<VAR>S T : Subsemigroup M<GOAL>Subsemigroup.comap f (Subsemigroup.map f S ⊓ Subsemigroup.map f T) = S ⊓ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>ι : Type u_5<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<VAR>S : ι → Subsemigroup M<GOAL>Subsemigroup.comap f (⨅ i, Subsemigroup.map f (S i)) = iInf S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>ι : Type u_5<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<VAR>S : ι → AddSubsemigroup M<GOAL>AddSubsemigroup.comap f (⨅ i, AddSubsemigroup.map f (S i)) = iInf S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<VAR>S T : AddSubsemigroup M<GOAL>AddSubsemigroup.comap f (AddSubsemigroup.map f S ⊔ AddSubsemigroup.map f T) = S ⊔ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<VAR>S T : Subsemigroup M<GOAL>Subsemigroup.comap f (Subsemigroup.map f S ⊔ Subsemigroup.map f T) = S ⊔ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>ι : Type u_5<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<VAR>S : ι → AddSubsemigroup M<GOAL>AddSubsemigroup.comap f (⨆ i, AddSubsemigroup.map f (S i)) = iSup S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>ι : Type u_5<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<VAR>S : ι → Subsemigroup M<GOAL>Subsemigroup.comap f (⨆ i, Subsemigroup.map f (S i)) = iSup S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<VAR>S T : AddSubsemigroup M<GOAL>AddSubsemigroup.map f S ≤ AddSubsemigroup.map f T ↔ S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<VAR>S T : Subsemigroup M<GOAL>Subsemigroup.map f S ≤ Subsemigroup.map f T ↔ S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Injective ⇑f<GOAL>StrictMono (Subsemigroup.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Injective ⇑f<GOAL>StrictMono (AddSubsemigroup.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<VAR>S : Subsemigroup N<GOAL>Subsemigroup.map f (Subsemigroup.comap f S) = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<VAR>S : AddSubsemigroup N<GOAL>AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (Subsemigroup.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (AddSubsemigroup.map f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective (AddSubsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective (Subsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<VAR>S T : AddSubsemigroup N<GOAL>AddSubsemigroup.map f (AddSubsemigroup.comap f S ⊓ AddSubsemigroup.comap f T) = S ⊓ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<VAR>S T : Subsemigroup N<GOAL>Subsemigroup.map f (Subsemigroup.comap f S ⊓ Subsemigroup.comap f T) = S ⊓ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>ι : Type u_5<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → AddSubsemigroup N<GOAL>AddSubsemigroup.map f (⨅ i, AddSubsemigroup.comap f (S i)) = iInf S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>ι : Type u_5<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → Subsemigroup N<GOAL>Subsemigroup.map f (⨅ i, Subsemigroup.comap f (S i)) = iInf S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<VAR>S T : Subsemigroup N<GOAL>Subsemigroup.map f (Subsemigroup.comap f S ⊔ Subsemigroup.comap f T) = S ⊔ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<VAR>S T : AddSubsemigroup N<GOAL>AddSubsemigroup.map f (AddSubsemigroup.comap f S ⊔ AddSubsemigroup.comap f T) = S ⊔ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>ι : Type u_5<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → Subsemigroup N<GOAL>Subsemigroup.map f (⨆ i, Subsemigroup.comap f (S i)) = iSup S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>ι : Type u_5<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → AddSubsemigroup N<GOAL>AddSubsemigroup.map f (⨆ i, AddSubsemigroup.comap f (S i)) = iSup S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<VAR>S T : Subsemigroup N<GOAL>Subsemigroup.comap f S ≤ Subsemigroup.comap f T ↔ S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<VAR>S T : AddSubsemigroup N<GOAL>AddSubsemigroup.comap f S ≤ AddSubsemigroup.comap f T ↔ S ≤ T
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<GOAL>StrictMono (AddSubsemigroup.comap f)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<GOAL>StrictMono (Subsemigroup.comap f)
<VAR>M : Type u_1<VAR>A : Type u_5<VAR>Mul M<VAR>SetLike A M<VAR>hA : MulMemClass A M<VAR>S' : A<VAR>x y : ↥S'<GOAL>↑(x * y) = ↑x * ↑y
<VAR>M : Type u_1<VAR>A : Type u_5<VAR>Add M<VAR>SetLike A M<VAR>hA : AddMemClass A M<VAR>S' : A<VAR>x y : ↥S'<GOAL>↑(x + y) = ↑x + ↑y
<VAR>M : Type u_1<VAR>A : Type u_5<VAR>Add M<VAR>SetLike A M<VAR>hA : AddMemClass A M<VAR>S' : A<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>A : Type u_5<VAR>Mul M<VAR>SetLike A M<VAR>hA : MulMemClass A M<VAR>S' : A<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>A : Type u_5<VAR>Add M<VAR>SetLike A M<VAR>hA : AddMemClass A M<VAR>S' : A<VAR>x y : ↥S'<GOAL>x + y = ⟨↑x + ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>A : Type u_5<VAR>Mul M<VAR>SetLike A M<VAR>hA : MulMemClass A M<VAR>S' : A<VAR>x y : ↥S'<GOAL>x * y = ⟨↑x * ↑y, ⋯⟩
<VAR>M : Type u_1<VAR>A : Type u_5<VAR>Mul M<VAR>SetLike A M<VAR>hA : MulMemClass A M<VAR>S' : A<GOAL>⇑(MulMemClass.subtype S') = Subtype.val
<VAR>M : Type u_1<VAR>A : Type u_5<VAR>Add M<VAR>SetLike A M<VAR>hA : AddMemClass A M<VAR>S' : A<GOAL>⇑(AddMemClass.subtype S') = Subtype.val
<VAR>M : Type u_1<VAR>Mul M<VAR>x : M<GOAL>↑(Subsemigroup.topEquiv.symm x) = x
<VAR>M : Type u_1<VAR>Add M<VAR>x : ↥⊤<GOAL>AddSubsemigroup.topEquiv x = ↑x
<VAR>M : Type u_1<VAR>Mul M<VAR>x : ↥⊤<GOAL>Subsemigroup.topEquiv x = ↑x
<VAR>M : Type u_1<VAR>Add M<VAR>x : M<GOAL>↑(AddSubsemigroup.topEquiv.symm x) = x
<VAR>M : Type u_1<VAR>Add M<GOAL>↑AddSubsemigroup.topEquiv = AddMemClass.subtype ⊤
<VAR>M : Type u_1<VAR>Mul M<GOAL>↑Subsemigroup.topEquiv = MulMemClass.subtype ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup M<VAR>f : AddHom 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>Mul M<VAR>Mul N<VAR>S : Subsemigroup 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>Mul M<VAR>s : Set M<GOAL>Subsemigroup.closure (Subtype.val ⁻¹' s) = ⊤
<VAR>M : Type u_1<VAR>Add M<VAR>s : Set M<GOAL>AddSubsemigroup.closure (Subtype.val ⁻¹' s) = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>s : Subsemigroup M<VAR>t : Subsemigroup N<GOAL>↑(s.prod t) = ↑s ×ˢ ↑t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>s : AddSubsemigroup M<VAR>t : AddSubsemigroup N<GOAL>↑(s.prod t) = ↑s ×ˢ ↑t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>s : AddSubsemigroup M<VAR>t : AddSubsemigroup 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>Mul M<VAR>Mul N<VAR>s : Subsemigroup M<VAR>t : Subsemigroup 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>Mul M<VAR>Mul N<VAR>s₁ s₂ : Subsemigroup M<VAR>t₁ t₂ : Subsemigroup 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>Add M<VAR>Add N<VAR>s₁ s₂ : AddSubsemigroup M<VAR>t₁ t₂ : AddSubsemigroup 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>Add M<VAR>Add N<VAR>s : AddSubsemigroup M<GOAL>s.prod ⊤ = AddSubsemigroup.comap (AddHom.fst M N) s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>s : Subsemigroup M<GOAL>s.prod ⊤ = Subsemigroup.comap (MulHom.fst M N) s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>s : Subsemigroup N<GOAL>⊤.prod s = Subsemigroup.comap (MulHom.snd M N) s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>s : AddSubsemigroup N<GOAL>⊤.prod s = AddSubsemigroup.comap (AddHom.snd M N) s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<GOAL>⊤.prod ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<GOAL>⊤.prod ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<GOAL>⊥.prod ⊥ = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<GOAL>⊥.prod ⊥ = ⊥
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<VAR>K : Subsemigroup M<VAR>x : N<GOAL>x ∈ Subsemigroup.map (↑f) K ↔ f.symm x ∈ K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<VAR>K : AddSubsemigroup M<VAR>x : N<GOAL>x ∈ AddSubsemigroup.map (↑f) K ↔ f.symm x ∈ K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<VAR>K : AddSubsemigroup M<GOAL>AddSubsemigroup.map (↑f) K = AddSubsemigroup.comap (↑f.symm) K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<VAR>K : Subsemigroup M<GOAL>Subsemigroup.map (↑f) K = Subsemigroup.comap (↑f.symm) K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : N ≃+ M<VAR>K : AddSubsemigroup M<GOAL>AddSubsemigroup.comap (↑f) K = AddSubsemigroup.map (↑f.symm) K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : N ≃* M<VAR>K : Subsemigroup M<GOAL>Subsemigroup.comap (↑f) K = Subsemigroup.map (↑f.symm) K
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : M ≃+ N<GOAL>AddSubsemigroup.map ↑f ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M ≃* N<GOAL>Subsemigroup.map ↑f ⊤ = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>s : Subsemigroup M<VAR>t : Subsemigroup N<VAR>u : Subsemigroup (M × N)<GOAL>u ≤ s.prod t ↔ Subsemigroup.map (MulHom.fst M N) u ≤ s ∧ Subsemigroup.map (MulHom.snd M N) u ≤ t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>s : AddSubsemigroup M<VAR>t : AddSubsemigroup N<VAR>u : AddSubsemigroup (M × N)<GOAL>u ≤ s.prod t ↔ AddSubsemigroup.map (AddHom.fst M N) u ≤ s ∧ AddSubsemigroup.map (AddHom.snd M N) u ≤ t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>↑f.srange = Set.range ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>↑f.srange = Set.range ⇑f
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>y : N<GOAL>y ∈ f.srange ↔ ∃ x, f x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>y : N<GOAL>y ∈ f.srange ↔ ∃ x, f x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>f.srange = AddSubsemigroup.map f ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>f.srange = Subsemigroup.map f ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Add M<VAR>Add N<VAR>Add P<VAR>g : AddHom N P<VAR>f : AddHom M N<GOAL>AddSubsemigroup.map g f.srange = (g.comp f).srange
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>g : N →ₙ* P<VAR>f : M →ₙ* N<GOAL>Subsemigroup.map g f.srange = (g.comp f).srange
<VAR>M : Type u_1<VAR>Add M<VAR>N : Type u_5<VAR>Add N<VAR>f : AddHom M N<GOAL>f.srange = ⊤ ↔ Function.Surjective ⇑f
<VAR>M : Type u_1<VAR>Mul M<VAR>N : Type u_5<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>f.srange = ⊤ ↔ Function.Surjective ⇑f
<VAR>M : Type u_1<VAR>Mul M<VAR>N : Type u_5<VAR>Mul N<VAR>f : M →ₙ* N<VAR>hf : Function.Surjective ⇑f<GOAL>f.srange = ⊤
<VAR>M : Type u_1<VAR>Add M<VAR>N : Type u_5<VAR>Add N<VAR>f : AddHom M N<VAR>hf : Function.Surjective ⇑f<GOAL>f.srange = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>s : Set N<GOAL>AddSubsemigroup.closure (⇑f ⁻¹' s) ≤ AddSubsemigroup.comap f (AddSubsemigroup.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>s : Set N<GOAL>Subsemigroup.closure (⇑f ⁻¹' s) ≤ Subsemigroup.comap f (Subsemigroup.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>s : Set M<GOAL>Subsemigroup.map f (Subsemigroup.closure s) = Subsemigroup.closure (⇑f '' s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>s : Set M<GOAL>AddSubsemigroup.map f (AddSubsemigroup.closure s) = AddSubsemigroup.closure (⇑f '' s)
<VAR>M : Type u_1<VAR>σ : Type u_4<VAR>Mul M<VAR>N : Type u_5<VAR>Mul N<VAR>SetLike σ M<VAR>MulMemClass σ M<VAR>f : M →ₙ* N<VAR>S : σ<VAR>x : ↥S<GOAL>(f.restrict S) x = f ↑x
<VAR>M : Type u_1<VAR>σ : Type u_4<VAR>Add M<VAR>N : Type u_5<VAR>Add N<VAR>SetLike σ M<VAR>AddMemClass σ M<VAR>f : AddHom M N<VAR>S : σ<VAR>x : ↥S<GOAL>(f.restrict S) x = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>σ : Type u_4<VAR>Mul M<VAR>Mul N<VAR>SetLike σ N<VAR>MulMemClass σ N<VAR>f : M →ₙ* N<VAR>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>σ : Type u_4<VAR>Add M<VAR>Add N<VAR>SetLike σ N<VAR>AddMemClass σ N<VAR>f : AddHom M N<VAR>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>Add M<VAR>N : Type u_5<VAR>Add N<VAR>f : AddHom M N<VAR>x : M<GOAL>↑(f.srangeRestrict x) = f x
<VAR>M : Type u_1<VAR>Mul M<VAR>N : Type u_5<VAR>Mul N<VAR>f : M →ₙ* N<VAR>x : M<GOAL>↑(f.srangeRestrict x) = f x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<GOAL>Function.Surjective ⇑f.srangeRestrict
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<GOAL>Function.Surjective ⇑f.srangeRestrict
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>Mul M'<VAR>Mul N'<VAR>f : M →ₙ* N<VAR>g : M' →ₙ* N'<VAR>S : Subsemigroup N<VAR>S' : Subsemigroup N'<GOAL>Subsemigroup.comap (f.prodMap g) (S.prod S') = (Subsemigroup.comap f S).prod (Subsemigroup.comap g S')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>Add M'<VAR>Add N'<VAR>f : AddHom M N<VAR>g : AddHom M' N'<VAR>S : AddSubsemigroup N<VAR>S' : AddSubsemigroup N'<GOAL>AddSubsemigroup.comap (f.prodMap g) (S.prod S') = (AddSubsemigroup.comap f S).prod (AddSubsemigroup.comap g S')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>N' : Subsemigroup N<VAR>x : ↥(Subsemigroup.comap f N')<GOAL>↑((f.subsemigroupComap N') x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>N' : AddSubsemigroup N<VAR>x : ↥(AddSubsemigroup.comap f N')<GOAL>↑((f.subsemigroupComap N') x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>M' : AddSubsemigroup M<VAR>x : ↥M'<GOAL>↑((f.subsemigroupMap M') x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>M' : Subsemigroup M<VAR>x : ↥M'<GOAL>↑((f.subsemigroupMap M') x) = f ↑x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>M' : Subsemigroup M<GOAL>Function.Surjective ⇑(f.subsemigroupMap M')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>M' : AddSubsemigroup M<GOAL>Function.Surjective ⇑(f.subsemigroupMap M')
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>Nonempty N<GOAL>(MulHom.fst M N).srange = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>Nonempty N<GOAL>(AddHom.fst M N).srange = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>Nonempty M<GOAL>(AddHom.snd M N).srange = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>Nonempty M<GOAL>(MulHom.snd M N).srange = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>Nonempty M<VAR>Nonempty N<VAR>s : Subsemigroup M<VAR>t : Subsemigroup N<GOAL>s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>Nonempty M<VAR>Nonempty N<VAR>s : AddSubsemigroup M<VAR>t : AddSubsemigroup N<GOAL>s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
<VAR>M : Type u_1<VAR>Add M<VAR>s : AddSubsemigroup M<GOAL>(AddMemClass.subtype s).srange = s
<VAR>M : Type u_1<VAR>Mul M<VAR>s : Subsemigroup M<GOAL>(MulMemClass.subtype s).srange = s