ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<VAR>r : ↥p<GOAL>f ↑r ∈ Submodule.map f p
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.map LinearMap.id p = p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomSurjective σ₁₂<VAR>RingHomSurjective σ₂₃<VAR>RingHomSurjective σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>p : Submodule R M<GOAL>Submodule.map (g.comp f) p = Submodule.map g (Submodule.map f p)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p p' : Submodule R M<GOAL>p ≤ p' → Submodule.map f p ≤ Submodule.map f p'
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>p : Submodule R M<VAR>RingHomSurjective σ₁₂<GOAL>Submodule.map 0 p = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>p : Submodule R M<VAR>RingHomSurjective σ₁₂<VAR>f g : M →ₛₗ[σ₁₂] M₂<GOAL>Submodule.map (f + g) p ≤ Submodule.map f p ⊔ Submodule.map g p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p q : Submodule R M<GOAL>Submodule.map f (p ⊓ q) ≤ Submodule.map f p ⊓ Submodule.map f q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p q : Submodule R M<VAR>hf : Function.Injective ⇑f<GOAL>Submodule.map f (p ⊓ q) = Submodule.map f p ⊓ Submodule.map f q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>N : Submodule R M<GOAL>(Set.range fun ϕ => Submodule.map ϕ N).Nonempty
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>i : Function.Injective ⇑f<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>↑((Submodule.equivMapOfInjective f i p) x) = f ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>i : Function.Injective ⇑f<VAR>p : Submodule R M<VAR>x : ↥(Submodule.map f p)<GOAL>f ↑((Submodule.equivMapOfInjective f i p).symm x) = ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R₂ M₂<GOAL>↑(Submodule.comap f p) = ⇑f ⁻¹' ↑p
<VAR>A : Type u_10<VAR>A₂ : Type u_11<VAR>AddCommGroup A<VAR>AddCommGroup A₂<VAR>f : A →+ A₂<VAR>s : AddSubgroup A₂<GOAL>Submodule.comap f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.comap f s)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>x : M<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R₂ M₂<GOAL>x ∈ Submodule.comap f p ↔ f x ∈ p
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Submodule.comap LinearMap.id p = p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R₂ M₂<VAR>Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>p : Submodule R₃ M₃<GOAL>Submodule.comap (g.comp f) p = Submodule.comap f (Submodule.comap g p)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>q q' : Submodule R₂ M₂<GOAL>q ≤ q' → Submodule.comap f q ≤ Submodule.comap f q'
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>f : M →ₗ[R] M<VAR>h : p ≤ Submodule.comap f p<VAR>k : ℕ<GOAL>p ≤ Submodule.comap (f ^ k) p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<GOAL>Submodule.map f p ≤ q ↔ p ≤ Submodule.comap f q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<GOAL>GaloisConnection (Submodule.map f) (Submodule.comap f)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<GOAL>Submodule.map f ⊥ = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>p p' : Submodule R M<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<GOAL>Submodule.map f (p ⊔ p') = Submodule.map f p ⊔ Submodule.map f p'
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>ι : Sort u_10<VAR>f : F<VAR>p : ι → Submodule R M<GOAL>Submodule.map f (⨆ i, p i) = ⨆ i, Submodule.map f (p i)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<GOAL>Submodule.comap f ⊤ = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>q q' : Submodule R₂ M₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<GOAL>Submodule.comap f (q ⊓ q') = Submodule.comap f q ⊓ Submodule.comap f q'
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>ι : Sort u_10<VAR>f : F<VAR>p : ι → Submodule R₂ M₂<GOAL>Submodule.comap f (⨅ i, p i) = ⨅ i, Submodule.comap f (p i)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<GOAL>Submodule.comap 0 q = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>q : Submodule R₂ M₂<GOAL>Submodule.map f (Submodule.comap f q) ≤ q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>p : Submodule R M<GOAL>p ≤ Submodule.comap f (Submodule.map f p)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>p : Submodule R₂ M₂<GOAL>Submodule.map f (Submodule.comap f p) = p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (Submodule.map f)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective (Submodule.comap f)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>p q : Submodule R₂ M₂<GOAL>Submodule.map f (Submodule.comap f p ⊔ Submodule.comap f q) = p ⊔ q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>ι : Sort u_10<VAR>S : ι → Submodule R₂ M₂<GOAL>Submodule.map f (⨆ i, Submodule.comap f (S i)) = iSup S
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>p q : Submodule R₂ M₂<GOAL>Submodule.map f (Submodule.comap f p ⊓ Submodule.comap f q) = p ⊓ q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>ι : Sort u_10<VAR>S : ι → Submodule R₂ M₂<GOAL>Submodule.map f (⨅ i, Submodule.comap f (S i)) = iInf S
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>p q : Submodule R₂ M₂<GOAL>Submodule.comap f p ≤ Submodule.comap f q ↔ p ≤ q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>StrictMono (Submodule.comap f)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>p : Submodule R M<GOAL>Submodule.comap f (Submodule.map f p) = p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Function.Surjective (Submodule.comap f)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (Submodule.map f)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>p q : Submodule R M<GOAL>Submodule.comap f (Submodule.map f p ⊓ Submodule.map f q) = p ⊓ q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>ι : Sort u_10<VAR>S : ι → Submodule R M<GOAL>Submodule.comap f (⨅ i, Submodule.map f (S i)) = iInf S
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>p q : Submodule R M<GOAL>Submodule.comap f (Submodule.map f p ⊔ Submodule.map f q) = p ⊔ q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>ι : Sort u_10<VAR>S : ι → Submodule R M<GOAL>Submodule.comap f (⨆ i, Submodule.map f (S i)) = iSup S
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>p q : Submodule R M<GOAL>Submodule.map f p ≤ Submodule.map f q ↔ p ≤ q
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>StrictMono (Submodule.map f)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>p : Submodule R₂ M₂<GOAL>(RelIso.symm (Submodule.orderIsoMapComapOfBijective f hf)) p = Submodule.comap f p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>p : Submodule R M<GOAL>(Submodule.orderIsoMapComapOfBijective f hf) p = Submodule.map f p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>EquivLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R₂ M₂<GOAL>(RelIso.symm (Submodule.orderIsoMapComap f)) p = Submodule.comap f p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>EquivLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<GOAL>(Submodule.orderIsoMapComap f) p = Submodule.map f p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>F : Type u_9<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>p : Submodule R M<VAR>p' : Submodule R₂ M₂<GOAL>Submodule.map f p ⊓ p' = Submodule.map f (p ⊓ Submodule.comap f p')
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Submodule.map p.subtype (Submodule.comap p.subtype p') = p ⊓ p'
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : ↥⊥<GOAL>b = 0
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>σ : R →+* R<VAR>RingHomSurjective σ<VAR>ι : Sort u_10<VAR>f : M →ₛₗ[σ] M<VAR>p : ι → Submodule R M<VAR>hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i<VAR>v : M<GOAL>v ∈ iInf p → f v ∈ iInf p
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>Disjoint p q ↔ Submodule.comap p.subtype q = ⊥
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : Submodule R M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>f : M →ₗ[R] M₂<GOAL>Submodule.map (-f) p = Submodule.map f p
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>f : M →ₗ[R] M₂<VAR>p : Submodule R M₂<GOAL>Submodule.comap (-f) p = Submodule.comap f p
<VAR>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>Semifield K<VAR>AddCommMonoid V<VAR>Module K V<VAR>AddCommMonoid V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V₂<VAR>a : K<VAR>h : a ≠ 0<GOAL>Submodule.comap (a • f) p = Submodule.comap f p
<VAR>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>Semifield K<VAR>AddCommMonoid V<VAR>Module K V<VAR>AddCommMonoid V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V<VAR>a : K<VAR>h : a ≠ 0<GOAL>Submodule.map (a • f) p = Submodule.map f p
<VAR>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>Semifield K<VAR>AddCommMonoid V<VAR>Module K V<VAR>AddCommMonoid V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V₂<VAR>a : K<GOAL>Submodule.comap (a • f) p = ⨅ (_ : a ≠ 0), Submodule.comap f p
<VAR>K : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>Semifield K<VAR>AddCommMonoid V<VAR>Module K V<VAR>AddCommMonoid V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>p : Submodule K V<VAR>a : K<GOAL>Submodule.map (a • f) p = ⨆ (_ : a ≠ 0), Submodule.map f p
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<VAR>hpq : p ≤ q<VAR>x : ↥p<GOAL>(Submodule.comapSubtypeEquivOfLe hpq).symm x = ⟨⟨↑x, ⋯⟩, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<VAR>hpq : p ≤ q<VAR>x : ↥(Submodule.comap q.subtype p)<GOAL>↑((Submodule.comapSubtypeEquivOfLe hpq) x) = ↑↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomInvPair τ₁₂ τ₂₁<VAR>RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>x : M₂<GOAL>x ∈ Submodule.map (↑e) p ↔ e.symm x ∈ p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomInvPair τ₁₂ τ₂₁<VAR>RingHomInvPair τ₂₁ τ₁₂<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>K : Submodule R M<GOAL>Submodule.map (↑e) K = Submodule.comap (↑e.symm) K
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomInvPair τ₁₂ τ₂₁<VAR>RingHomInvPair τ₂₁ τ₁₂<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>K : Submodule R₂ M₂<GOAL>Submodule.comap (↑e) K = Submodule.map (↑e.symm) K
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomInvPair τ₁₂ τ₂₁<VAR>RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>K : Submodule R₂ M₂<GOAL>Submodule.map e.symm K = p ↔ Submodule.map e p = K
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomInvPair τ₁₂ τ₂₁<VAR>RingHomInvPair τ₂₁ τ₁₂<VAR>e : M ≃ₛₗ[τ₁₂] M₂<VAR>p : Submodule R M<GOAL>(Submodule.orderIsoMapComap e) p = Submodule.comap e.symm p