ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hfg : (f - g).LimZero<GOAL>(g - f).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>CauSeq.LimZero 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<GOAL>(CauSeq.const abv x).LimZero ↔ x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f1 f2 g1 g2 : CauSeq β abv<VAR>hf : f1 ≈ f2<VAR>hg : g1 ≈ g2<GOAL>f1 + g1 ≈ f2 + g2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : f ≈ g<GOAL>-f ≈ -g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f1 f2 g1 g2 : CauSeq β abv<VAR>hf : f1 ≈ f2<VAR>hg : g1 ≈ g2<GOAL>f1 - g1 ≈ f2 - g2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>h : f ≈ g<VAR>ε : α<VAR>ε0 : 0 < ε<GOAL>∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑g j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>h : f ≈ g<GOAL>f.LimZero ↔ g.LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (↑f j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : ℕ → β<VAR>g : CauSeq β abv<VAR>h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε<GOAL>IsCauSeq abv f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f ≈ 0<GOAL>¬f.LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>g : CauSeq β abv<VAR>f : CauSeq β abv<VAR>hf : f ≈ 0<GOAL>g * f ≈ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>g : CauSeq β abv<VAR>f : CauSeq β abv<VAR>hf : f ≈ 0<GOAL>f * g ≈ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>¬f * g ≈ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x y : β<GOAL>CauSeq.const abv x ≈ CauSeq.const abv y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f1 f2 g1 g2 : CauSeq β abv<VAR>hf : f1 ≈ f2<VAR>hg : g1 ≈ g2<GOAL>f1 * g1 ≈ f2 * g2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>G : Type u_3<VAR>SMul G β<VAR>IsScalarTower G β β<VAR>f1 f2 : CauSeq β abv<VAR>c : G<VAR>hf : f1 ≈ f2<GOAL>c • f1 ≈ c • f2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f1 f2 : CauSeq β abv<VAR>hf : f1 ≈ f2<VAR>n : ℕ<GOAL>f1 ^ n ≈ f2 ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>Ring β<VAR>IsDomain β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<GOAL>¬CauSeq.const abv 1 ≈ CauSeq.const abv 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>ε : α<GOAL>ε > 0 → ∃ i, ∀ j ≥ i, abv ((↑f j)⁻¹ - (↑f i)⁻¹) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>↑(f.inv hf) = (↑f)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>i : ℕ<GOAL>↑(f.inv hf) i = (↑f i)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>f.inv hf * f ≈ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>f * f.inv hf ≈ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrderedField α<VAR>DivisionRing β<VAR>abv : β → α<VAR>IsAbsoluteValue abv<VAR>x : β<VAR>hx : x ≠ 0<GOAL>CauSeq.const abv x⁻¹ = (CauSeq.const abv x).inv ⋯
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f : CauSeq α abs<GOAL>f.Pos → ¬f.LimZero
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>x : α<GOAL>(CauSeq.const abs x).Pos ↔ 0 < x
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<GOAL>f.Pos → g.Pos → (f + g).Pos
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<GOAL>f.Pos → g.LimZero → (f + g).Pos
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<GOAL>f.Pos → g.Pos → (f * g).Pos
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f : CauSeq α abs<GOAL>f.Pos ∨ f.LimZero ∨ (-f).Pos
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f < g<VAR>gh : g ≈ h<GOAL>f < h
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f ≈ g<VAR>gh : g < h<GOAL>f < h
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>fg : f < g<VAR>gh : g < h<GOAL>f < h
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f : CauSeq α abs<GOAL>¬f < f
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>hfg : f ≈ g<VAR>hgh : g ≤ h<GOAL>f ≤ h
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g h : CauSeq α abs<VAR>hfg : f ≤ g<VAR>hgh : g ≈ h<GOAL>f ≤ h
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>fg : f ≤ g<VAR>gf : g ≤ f<GOAL>f ≈ g
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<GOAL>f < g ∨ f ≈ g ∨ g < f
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<GOAL>f ≤ g ∨ g ≤ f
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>x y : α<GOAL>CauSeq.const abs x < CauSeq.const abs y ↔ x < y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>x y : α<GOAL>CauSeq.const abs x ≤ CauSeq.const abs y ↔ x ≤ y
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>h : ∃ i, ∀ j ≥ i, ↑f j ≤ ↑g j<GOAL>f ≤ g
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f : CauSeq α abs<GOAL>∃ a, f < CauSeq.const abs a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f : CauSeq α abs<GOAL>∃ a, CauSeq.const abs a < f
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>ε a₁ a₂ b₁ b₂ : α<GOAL>|a₁ - b₁| < ε → |a₂ - b₂| < ε → |a₁ ⊔ a₂ - b₁ ⊔ b₂| < ε
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>ε a₁ a₂ b₁ b₂ : α<GOAL>|a₁ - b₁| < ε → |a₂ - b₂| < ε → |a₁ ⊓ a₂ - b₁ ⊓ b₂| < ε
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<GOAL>↑(f ⊔ g) = ↑f ⊔ ↑g
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<GOAL>↑(f ⊓ g) = ↑f ⊓ ↑g
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>hf : f.LimZero<VAR>hg : g.LimZero<GOAL>(f ⊔ g).LimZero
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>f g : CauSeq α abs<VAR>hf : f.LimZero<VAR>hg : g.LimZero<GOAL>(f ⊓ g).LimZero
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a₁ b₁ a₂ b₂ : CauSeq α abs<VAR>ha : a₁ ≈ a₂<VAR>hb : b₁ ≈ b₂<GOAL>a₁ ⊔ b₁ ≈ a₂ ⊔ b₂
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a₁ b₁ a₂ b₂ : CauSeq α abs<VAR>ha : a₁ ≈ a₂<VAR>hb : b₁ ≈ b₂<GOAL>a₁ ⊓ b₁ ≈ a₂ ⊓ b₂
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>ha : a < c<VAR>hb : b < c<GOAL>a ⊔ b < c
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>hb : a < b<VAR>hc : a < c<GOAL>a < b ⊓ c
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : CauSeq α abs<GOAL>a ⊔ a = a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a : CauSeq α abs<GOAL>a ⊓ a = a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<GOAL>a ⊔ b = b ⊔ a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<GOAL>a ⊓ b = b ⊓ a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<VAR>h : a ≤ b<GOAL>a ⊔ b ≈ b
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<VAR>h : b ≤ a<GOAL>a ⊓ b ≈ b
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<VAR>h : b ≤ a<GOAL>a ⊔ b ≈ a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<VAR>h : a ≤ b<GOAL>a ⊓ b ≈ a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<GOAL>a ≤ a ⊔ b
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<GOAL>a ⊓ b ≤ a
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<GOAL>b ≤ a ⊔ b
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b : CauSeq α abs<GOAL>a ⊓ b ≤ b
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>ha : a ≤ c<VAR>hb : b ≤ c<GOAL>a ⊔ b ≤ c
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : CauSeq α abs<VAR>hb : a ≤ b<VAR>hc : a ≤ c<GOAL>a ≤ b ⊓ c
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : CauSeq α abs<GOAL>a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b c : CauSeq α abs<GOAL>a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieSubalgebra R L<VAR>x y : L<GOAL>x ∈ self.carrier → y ∈ self.carrier → ⁅x, y⁆ ∈ self.carrier
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<GOAL>0 ∈ L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x y : L<GOAL>x ∈ L' → y ∈ L' → x + y ∈ L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x y : L<GOAL>x ∈ L' → y ∈ L' → x - y ∈ L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>t : R<VAR>x : L<VAR>h : x ∈ L'<GOAL>t • x ∈ L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x y : L<VAR>hx : x ∈ L'<VAR>hy : y ∈ L'<GOAL>⁅x, y⁆ ∈ L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x : L<GOAL>x ∈ L'.carrier ↔ x ∈ ↑L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>S : Set L<VAR>h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S<VAR>h₂ : S 0<VAR>h₃ : ∀ (c : R) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier<VAR>h₄ : ∀ {x y : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → y ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, y⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier<VAR>x : L<GOAL>x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } ↔ x ∈ S
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x : L<GOAL>x ∈ L'.toSubmodule ↔ x ∈ L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x : L<GOAL>x ∈ ↑L' ↔ x ∈ L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x y : ↥L'<GOAL>↑⁅x, y⁆ = ⁅↑x, ↑y⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x y : ↥L'<GOAL>x = y ↔ ↑x = ↑y
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>x : ↥L'<GOAL>↑x = 0 ↔ x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₁' L₂' : LieSubalgebra R L<VAR>h : ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂'<GOAL>L₁' = L₂'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₁' L₂' : LieSubalgebra R L<GOAL>L₁' = L₂' ↔ ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>S : Set L<VAR>h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S<VAR>h₂ : S 0<VAR>h₃ : ∀ (c : R) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier<VAR>h₄ : ∀ {x y : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → y ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅x, y⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier<GOAL>↑{ carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } = S
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>p : Submodule R L<VAR>h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, y⁆ ∈ p.carrier<GOAL>{ toSubmodule := p, lie_mem' := h }.toSubmodule = p
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>Function.Injective SetLike.coe
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₁' L₂' : LieSubalgebra R L<GOAL>↑L₁' = ↑L₂' ↔ L₁' = L₂'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>Function.Injective LieSubalgebra.toSubmodule
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₁' L₂' : LieSubalgebra R L<GOAL>L₁'.toSubmodule = L₂'.toSubmodule ↔ L₁' = L₂'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<GOAL>↑L'.toSubmodule = ↑L'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>M : Type w<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>x : ↥L'<VAR>m : M<GOAL>⁅x, m⁆ = ⁅↑x, m⁆
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<VAR>M : Type w<VAR>AddCommGroup M<VAR>LieRingModule L M<VAR>N : Type w₁<VAR>AddCommGroup N<VAR>LieRingModule L N<VAR>Module R N<VAR>Module R M<VAR>f : M →ₗ⁅R,L⁆ N<GOAL>⇑(f.restrictLie L') = ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<GOAL>⇑L'.incl = Subtype.val
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L' : LieSubalgebra R L<GOAL>⇑L'.incl' = Subtype.val
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<GOAL>↑f.range = Set.range ⇑f
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>x : L₂<GOAL>x ∈ f.range ↔ ∃ y, f y = x
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>x : L<GOAL>f x ∈ f.range
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>x : L<GOAL>f.rangeRestrict x = ⟨f x, ⋯⟩
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<GOAL>Function.Surjective ⇑f.rangeRestrict
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>h : Function.Injective ⇑f<VAR>x : L<GOAL>(f.equivRangeOfInjective h) x = ⟨f x, ⋯⟩
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>p : Submodule R L<GOAL>(∃ K, K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<GOAL>K.incl.range = K
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K : LieSubalgebra R L<VAR>x : L₂<GOAL>x ∈ LieSubalgebra.map f K ↔ ∃ y ∈ K, f y = x
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>K : LieSubalgebra R L<VAR>e : L ≃ₗ⁅R⁆ L₂<VAR>x : L₂<GOAL>x ∈ LieSubalgebra.map e.toLieHom K ↔ x ∈ Submodule.map (↑e.toLinearEquiv) K.toSubmodule
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<GOAL>K ≤ K' ↔ ↑K ⊆ ↑K'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<GOAL>K.toSubmodule ≤ K'.toSubmodule ↔ K ≤ K'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>↑⊥ = {0}
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>⊥.toSubmodule = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>⊤.toSubmodule = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>x : L<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<GOAL>f.range = LieSubalgebra.map f ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<GOAL>↑(K ⊓ K') = ↑K ∩ ↑K'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>S : Set (LieSubalgebra R L)<GOAL>(sInf S).toSubmodule = sInf {x | ∃ s ∈ S, s.toSubmodule = x}
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>S : Set (LieSubalgebra R L)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>S : Set (LieSubalgebra R L)<GOAL>IsGLB S (sInf S)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<GOAL>K + K' = K ⊔ K'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<GOAL>(K ⊓ K').toSubmodule = K.toSubmodule ⊓ K'.toSubmodule
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>x : L<GOAL>x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<GOAL>K = ⊥ ↔ ∀ x ∈ K, x = 0
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>Subsingleton ↥⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>IsNoetherian R L<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<VAR>x : ↥K<GOAL>↑((LieSubalgebra.inclusion h) x) = ↑x
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<VAR>x : ↥K<GOAL>(LieSubalgebra.inclusion h) x = ⟨↑x, ⋯⟩
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<GOAL>Function.Injective ⇑(LieSubalgebra.inclusion h)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<VAR>x : ↥K'<GOAL>x ∈ LieSubalgebra.ofLe h ↔ ↑x ∈ K
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<GOAL>LieSubalgebra.ofLe h = LieSubalgebra.comap K'.incl K
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<GOAL>(LieSubalgebra.ofLe h).toSubmodule = LinearMap.range (Submodule.inclusion h)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<VAR>x : ↥K<GOAL>(LieSubalgebra.equivOfLe h) x = ⟨(LieSubalgebra.inclusion h) x, ⋯⟩
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K : LieSubalgebra R L<VAR>K' : LieSubalgebra R L₂<GOAL>LieSubalgebra.map f K ≤ K' ↔ K ≤ LieSubalgebra.comap f K'
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>L₂ : Type w<VAR>LieRing L₂<VAR>LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<GOAL>GaloisConnection (LieSubalgebra.map f) (LieSubalgebra.comap f)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>s : Set L<VAR>x : L<GOAL>x ∈ LieSubalgebra.lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>s : Set L<GOAL>s ⊆ ↑(LieSubalgebra.lieSpan R L s)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>s : Set L<GOAL>Submodule.span R s ≤ (LieSubalgebra.lieSpan R L s).toSubmodule
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>s : Set L<VAR>K : LieSubalgebra R L<GOAL>LieSubalgebra.lieSpan R L s ≤ K ↔ s ⊆ ↑K
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>s t : Set L<VAR>h : s ⊆ t<GOAL>LieSubalgebra.lieSpan R L s ≤ LieSubalgebra.lieSpan R L t
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>K : LieSubalgebra R L<GOAL>LieSubalgebra.lieSpan R L ↑K = K
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>p : Submodule R L<GOAL>(LieSubalgebra.lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>LieSubalgebra.lieSpan R L ∅ = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<GOAL>LieSubalgebra.lieSpan R L Set.univ = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>s t : Set L<GOAL>LieSubalgebra.lieSpan R L (s ∪ t) = LieSubalgebra.lieSpan R L s ⊔ LieSubalgebra.lieSpan R L t
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>ι : Sort u_1<VAR>s : ι → Set L<GOAL>LieSubalgebra.lieSpan R L (⋃ i, s i) = ⨆ i, LieSubalgebra.lieSpan R L (s i)
<VAR>R : Type u<VAR>L : Type v<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>s : Set L<VAR>p : L → Prop<VAR>x : L<VAR>h : x ∈ LieSubalgebra.lieSpan R L s<VAR>mem : ∀ x ∈ s, p x<VAR>zero : p 0<VAR>smul : ∀ (r : R) {x : L}, p x → p (r • x)<VAR>add : ∀ (x y : L), p x → p y → p (x + y)<VAR>lie : ∀ (x y : L), p x → p y → p ⁅x, y⁆<GOAL>p x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>f : L₁ →ₗ⁅R⁆ L₂<VAR>h : Function.Injective ⇑f<VAR>x : L₁<GOAL>↑((LieEquiv.ofInjective f h) x) = f x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>CommRing R<VAR>LieRing L₁<VAR>LieAlgebra R L₁<VAR>L L' : LieSubalgebra R L₁<VAR>h : ↑L = ↑L'<VAR>x : ↥L<GOAL>↑((LieEquiv.ofEq L L' h) x) = ↑x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>L₁'' : LieSubalgebra R L₁<VAR>e : L₁ ≃ₗ⁅R⁆ L₂<VAR>x : ↥L₁''<GOAL>↑((LieEquiv.lieSubalgebraMap L₁'' e) x) = e ↑x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>L₁' : LieSubalgebra R L₁<VAR>L₂' : LieSubalgebra R L₂<VAR>e : L₁ ≃ₗ⁅R⁆ L₂<VAR>h : LieSubalgebra.map e.toLieHom L₁' = L₂'<VAR>x : ↥L₁'<GOAL>↑((LieEquiv.ofSubalgebras L₁' L₂' e h) x) = e ↑x
<VAR>R : Type u<VAR>L₁ : Type v<VAR>L₂ : Type w<VAR>CommRing R<VAR>LieRing L₁<VAR>LieRing L₂<VAR>LieAlgebra R L₁<VAR>LieAlgebra R L₂<VAR>L₁' : LieSubalgebra R L₁<VAR>L₂' : LieSubalgebra R L₂<VAR>e : L₁ ≃ₗ⁅R⁆ L₂<VAR>h : LieSubalgebra.map e.toLieHom L₁' = L₂'<VAR>x : ↥L₂'<GOAL>↑((LieEquiv.ofSubalgebras L₁' L₂' e h).symm x) = e.symm ↑x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>AddCommGroup M<VAR>Module R M<VAR>LieRingModule L M<VAR>LieModule R L M<VAR>self : LieDerivation R L M<VAR>a b : L<GOAL>↑self ⁅a, b⁆ = ⁅a, ↑self b⁆ - ⁅b, ↑self a⁆