ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>↑N ≤ ↑N' ↔ N ≤ N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>↑⊥ = {0}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>↑⊥ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>↑N = ⊥ ↔ N = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : Submodule R M<VAR>h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier<GOAL>{ toSubmodule := N, lie_mem := h } = ⊥ ↔ N = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>x : M<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>↑⊤ = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>↑N = ⊤ ↔ N = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : Submodule R M<VAR>h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier<GOAL>{ toSubmodule := N, lie_mem := h } = ⊤ ↔ N = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>x : M<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>↑(N ⊓ N') = ↑N ∩ ↑N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>↑(N ⊓ N') = ↑N ⊓ ↑N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>S : Set (LieSubmodule R L M)<GOAL>↑(sInf S) = sInf {x | ∃ s ∈ S, ↑s = x}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>S : Set (LieSubmodule R L M)<GOAL>↑(sInf S) = ⨅ N ∈ S, ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>↑(⨅ i, p i) = ⨅ i, ↑(p i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>S : Set (LieSubmodule R L M)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>↑(⨅ i, p i) = ⋂ i, ↑(p i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<VAR>x : M<GOAL>x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>↑(N ⊔ N') = ↑N ⊔ ↑N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>S : Set (LieSubmodule R L M)<GOAL>↑(sSup S) = sSup {x | ∃ s ∈ S, ↑s = x}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>S : Set (LieSubmodule R L M)<GOAL>↑(sSup S) = ⨆ N ∈ S, ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>↑(⨆ i, p i) = ⨆ i, ↑(p i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>b : M<VAR>N : ι → LieSubmodule R L M<VAR>i : ι<VAR>h : b ∈ N i<GOAL>b ∈ ⨆ i, N i
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, N i<VAR>hN : ∀ (i : ι), ∀ y ∈ N i, C y<VAR>h0 : C 0<VAR>hadd : ∀ (y z : M), C y → C z → C (y + z)<GOAL>C x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : (x : M) → x ∈ ⨆ i, N i → Prop<VAR>hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯<VAR>h0 : C 0 ⋯<VAR>hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, N i<GOAL>C x hx
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>Disjoint N N' ↔ Disjoint ↑N ↑N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>Codisjoint N N' ↔ Codisjoint ↑N ↑N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>IsCompl N N' ↔ IsCompl ↑N ↑N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Type u_1<VAR>N : ι → LieSubmodule R L M<GOAL>CompleteLattice.Independent N ↔ CompleteLattice.Independent fun i => ↑(N i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<GOAL>⨆ i, N i = ⊤ ↔ ⨆ i, ↑(N i) = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<GOAL>N + N' = N ⊔ N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<VAR>x : M<GOAL>x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<VAR>x : M<GOAL>x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>N = ⊥ ↔ ∀ m ∈ N, m = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>self : LieSubmodule R L M<GOAL>(LieSubmodule.toSubmodule_orderEmbedding R L M) self = ↑self
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>IsNoetherian R M<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>IsArtinian R M<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>Subsingleton (LieSubmodule R L M) ↔ Subsingleton M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>Nontrivial (LieSubmodule R L M) ↔ Nontrivial M
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>Nontrivial ↥↑N ↔ N ≠ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>↑N.incl = (↑N).subtype
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<VAR>m : ↥N<GOAL>N.incl m = ↑m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>⇑N.incl = Subtype.val
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>Function.Injective ⇑N.incl
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<VAR>h : N ≤ N'<VAR>m : ↥N<GOAL>↑((LieSubmodule.inclusion h) m) = ↑m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<VAR>h : N ≤ N'<VAR>m : ↥N<GOAL>(LieSubmodule.inclusion h) m = ⟨↑m, ⋯⟩
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N' : LieSubmodule R L M<VAR>h : N ≤ N'<GOAL>Function.Injective ⇑(LieSubmodule.inclusion h)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ LieSubmodule.lieSpan R L s ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>s : Set M<GOAL>s ⊆ ↑(LieSubmodule.lieSpan R L s)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>s : Set M<GOAL>Submodule.span R s ≤ ↑(LieSubmodule.lieSpan R L s)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>s : Set M<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.lieSpan R L s ≤ N ↔ s ⊆ ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>LieSubmodule.lieSpan R L s ≤ LieSubmodule.lieSpan R L t
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.lieSpan R L ↑N = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>p : Submodule R M<GOAL>↑(LieSubmodule.lieSpan R L ↑p) = p ↔ ∃ N, ↑N = p
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>LieSubmodule.lieSpan R L ∅ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<GOAL>LieSubmodule.lieSpan R L Set.univ = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>s : Set M<GOAL>LieSubmodule.lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>s t : Set M<GOAL>LieSubmodule.lieSpan R L (s ∪ t) = LieSubmodule.lieSpan R L s ⊔ LieSubmodule.lieSpan R L t
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>ι : Sort u_1<VAR>s : ι → Set M<GOAL>LieSubmodule.lieSpan R L (⋃ i, s i) = ⨆ i, LieSubmodule.lieSpan R L (s i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>m : M<GOAL>CompleteLattice.IsCompactElement (LieSubmodule.lieSpan R L {m})
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>sSup ((fun x => LieSubmodule.lieSpan R L {x}) '' ↑N) = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N : LieSubmodule R L M<GOAL>↑(LieSubmodule.map f N) = ⇑f '' ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N : LieSubmodule R L M<GOAL>↑(LieSubmodule.map f N) = Submodule.map ↑f ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N' : LieSubmodule R L M'<GOAL>↑(LieSubmodule.comap f N') = Submodule.comap ↑f ↑N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N : LieSubmodule R L M<VAR>N' : LieSubmodule R L M'<GOAL>LieSubmodule.map f N ≤ N' ↔ N ≤ LieSubmodule.comap f N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<GOAL>GaloisConnection (LieSubmodule.map f) (LieSubmodule.comap f)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N N₂ : LieSubmodule R L M<GOAL>LieSubmodule.map f (N ⊓ N₂) ≤ LieSubmodule.map f N ⊓ LieSubmodule.map f N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N N₂ : LieSubmodule R L M<VAR>hf : Function.Injective ⇑f<GOAL>LieSubmodule.map f (N ⊓ N₂) = LieSubmodule.map f N ⊓ LieSubmodule.map f N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N N₂ : LieSubmodule R L M<GOAL>LieSubmodule.map f (N ⊔ N₂) = LieSubmodule.map f N ⊔ LieSubmodule.map f N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N' N₂' : LieSubmodule R L M'<GOAL>LieSubmodule.comap f (N' ⊓ N₂') = LieSubmodule.comap f N' ⊓ LieSubmodule.comap f N₂'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<GOAL>LieSubmodule.map f (⨆ i, N i) = ⨆ i, LieSubmodule.map f (N i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N : LieSubmodule R L M<VAR>m' : M'<GOAL>m' ∈ LieSubmodule.map f N ↔ ∃ m ∈ N, f m = m'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N : LieSubmodule R L M<VAR>m : M<VAR>h : m ∈ N<GOAL>f m ∈ LieSubmodule.map f N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N' : LieSubmodule R L M'<VAR>m : M<GOAL>m ∈ LieSubmodule.comap f N' ↔ f m ∈ N'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N₂ : LieSubmodule R L M<GOAL>LieSubmodule.comap N.incl N₂ = ⊤ ↔ N ≤ N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N N₂ : LieSubmodule R L M<GOAL>LieSubmodule.comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N N₂ : LieSubmodule R L M<VAR>h : N ≤ N₂<GOAL>LieSubmodule.map f N ≤ LieSubmodule.map f N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N : LieSubmodule R L M<VAR>M'' : Type u_1<VAR>AddCommGroup M''<VAR>Module R M''<VAR>LieRingModule L M''<VAR>g : M' →ₗ⁅R,L⁆ M''<GOAL>LieSubmodule.map (g.comp f) N = LieSubmodule.map g (LieSubmodule.map f N)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>N : LieSubmodule R L M<GOAL>LieSubmodule.map LieModuleHom.id N = N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<GOAL>LieSubmodule.map f ⊥ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>N N₂ : LieSubmodule R L M<VAR>hf : Function.Injective ⇑f<GOAL>LieSubmodule.map f N ≤ LieSubmodule.map f N₂ ↔ N ≤ N₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (LieSubmodule.map f)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>f : M →ₗ⁅R,L⁆ M'<VAR>hf : Function.Injective ⇑f<VAR>N : LieSubmodule R L M<GOAL>(LieSubmodule.mapOrderEmbedding hf) N = LieSubmodule.map f N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>e : M ≃ₗ⁅R,L⁆ M'<VAR>N : LieSubmodule R L M<GOAL>(LieSubmodule.orderIsoMapComap e) N = LieSubmodule.map e.toLieModuleHom N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>M' : Type w₁<VAR>CommRing R<VAR>LieRing L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>LieRingModule L M'<VAR>e : M ≃ₗ⁅R,L⁆ M'<VAR>N' : LieSubmodule R L M'<GOAL>(RelIso.symm (LieSubmodule.orderIsoMapComap e)) N' = LieSubmodule.comap e.toLieModuleHom N'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>lieIdealSubalgebra R L ⊤ = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>h : ↑(LieIdeal.map f I) = ⇑f '' ↑I<GOAL>↑(LieIdeal.map f I) = Submodule.map ↑f ↑I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>J : LieIdeal R L'<GOAL>↑(LieIdeal.comap f J) = Submodule.comap ↑f ↑J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>LieIdeal.map f I ≤ J ↔ ⇑f '' ↑I ⊆ ↑J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>x : L<VAR>hx : x ∈ I<GOAL>f x ∈ LieIdeal.map f I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>J : LieIdeal R L'<VAR>x : L<GOAL>x ∈ LieIdeal.comap f J ↔ f x ∈ J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>LieIdeal.map f I ≤ J ↔ I ≤ LieIdeal.comap f J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>GaloisConnection (LieIdeal.map f) (LieIdeal.comap f)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<GOAL>LieIdeal.map f (I ⊔ I₂) = LieIdeal.map f I ⊔ LieIdeal.map f I₂
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>J : LieIdeal R L'<GOAL>LieIdeal.map f (LieIdeal.comap f J) ≤ J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<GOAL>I ≤ LieIdeal.comap f (LieIdeal.map f I)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>Monotone (LieIdeal.map f)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>Monotone (LieIdeal.comap f)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : ⇑f '' ↑I = ↑J<GOAL>LieIdeal.map f I = J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>f.idealRange = LieSubmodule.lieSpan R L' ↑f.range
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>f.idealRange = LieIdeal.map f ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>f.IsIdealMorphism ↔ lieIdealSubalgebra R L' f.idealRange = f.range
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>hf : f.IsIdealMorphism<GOAL>lieIdealSubalgebra R L' f.idealRange = f.range
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>LieRing L'<VAR>LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<GOAL>f.IsIdealMorphism ↔ ∀ (x : L') (y : L), ∃ z, ⁅x, f y⁆ = f z