ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>β : Type u_1<VAR>n : ℕ<VAR>s✝ : Finset β<VAR>f : β → Holor α ds<VAR>this : DecidableEq β := Classical.decEq β<VAR>x : β<VAR>s : Finset β<VAR>h_x_notin_s : x ∉ s<VAR>ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)<VAR>h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)<GOAL>CPRankMax (n + s.card * n) (f x + ∑ x ∈ s, f x)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>β : Type u_1<VAR>n : ℕ<VAR>s✝ : Finset β<VAR>f : β → Holor α ds<VAR>this : DecidableEq β := Classical.decEq β<VAR>x : β<VAR>s : Finset β<VAR>h_x_notin_s : x ∉ s<VAR>ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)<VAR>h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)<VAR>ih' : CPRankMax (s.card * n) (∑ x ∈ s, f x)<GOAL>CPRankMax (n + s.card * n) (f x + ∑ x ∈ s, f x)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α → α<VAR>hcomm : Commutative f<VAR>hassoc : Associative f<VAR>a b c : α<VAR>l : List α<GOAL>foldl f a (b :: c :: l) = f b (foldl f a (c :: l))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α → α<VAR>hcomm : Commutative f<VAR>hassoc : Associative f<VAR>a b c : α<VAR>l : List α<GOAL>foldl f (f (f a b) c) l = f b (foldl f (f a c) l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α → α<VAR>hcomm : Commutative f<VAR>hassoc : Associative f<VAR>a b c : α<VAR>l : List α<GOAL>foldl f (f (f a c) b) l = foldl f (f a c) (b :: l)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hS₀ : S ∈ Algebra.adjoin K {(ad K L) x}<VAR>hN : _root_.IsNilpotent N<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent N<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent N<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L) (α β : ↥H → K), y ∈ rootSpace H α → z ∈ rootSpace H β → S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅S y, z⁆ + ⁅y, S z⁆<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<VAR>S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<VAR>S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }<VAR>y : L<VAR>hy : (LieDerivation.ad K L) y = S'<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<VAR>S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }<VAR>y : L<VAR>hy : (LieDerivation.ad K L) y = S'<VAR>hy' : ∀ z ∈ H, ⁅y, z⁆ = 0<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<VAR>S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }<VAR>y : L<VAR>hy : (LieDerivation.ad K L) y = S'<VAR>hy' : y ∈ H<GOAL>((ad K L) x).IsSemisimple
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<VAR>S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }<VAR>y : L<VAR>hy : (LieDerivation.ad K L) y = S'<VAR>hy' : y ∈ H<GOAL>x = y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<VAR>S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }<VAR>y : L<VAR>hy : (LieDerivation.ad K L) y = S'<VAR>hy' : y ∈ H<GOAL>x - y = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<VAR>S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }<VAR>y : L<VAR>hy : (LieDerivation.ad K L) y = S'<VAR>hy' : y ∈ H<GOAL>_root_.IsNilpotent ((ad K L) (x - y))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>x : L<VAR>hx : x ∈ H<VAR>N S : Module.End K L<VAR>hN : _root_.IsNilpotent ((ad K L) x - S)<VAR>hS : S.IsSemisimple<VAR>hSN : (ad K L) x = N + S<VAR>hS₀ : Commute ((ad K L) x) S<VAR>x' : ↥H := ⟨x, hx⟩<VAR>aux : ∀ {α : ↥H → K} {y : L}, y ∈ rootSpace H α → S y = α x' • y<VAR>h_der : ∀ (y z : L), S ⁅y, z⁆ = ⁅y, S z⁆ - ⁅z, S y⁆<VAR>S' : LieDerivation K L L := { toLinearMap := S, leibniz' := h_der }<VAR>y : L<VAR>hy' : y ∈ H<VAR>hy : S = (ad K L) y<GOAL>_root_.IsNilpotent ((ad K L) (x - y))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<GOAL>s.card ≤ multiplicity E
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<GOAL>BddAbove {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>s : Finset E<VAR>hs : ∀ c ∈ s, ‖c‖ ≤ 2<VAR>h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖<GOAL>s.card ∈ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>x : V → ℝ<GOAL>(((toLinearMap₂' ℝ) (lapMatrix ℝ G)) x) x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>x : V → ℝ<GOAL>(∀ (i j : V), G.Adj i j → x i = x j) ↔ ∀ (i j : V), G.Reachable i j → x i = x j
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>x : V → ℝ<GOAL>(∀ (i j : V), G.Adj i j → x i = x j) → ∀ (i j : V), G.Reachable i j → x i = x j
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>h : ¬FiniteDimensional 𝕜 E<GOAL>∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>A : ‖c‖ < ‖c‖ + 1<GOAL>∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>A : ‖c‖ < ‖c‖ + 1<VAR>f : ℕ → E<VAR>hf : (∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖<GOAL>∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : LT α<VAR>a✝ b a : α<GOAL>↑a < ⊤
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<VAR>r : ↑Γ(↑U, ⊤)<GOAL>U.ι ''ᵁ (↑U).basicOpen r = X.basicOpen ((X.presheaf.map (eqToHom ⋯).op) r)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<VAR>r : ↑Γ(↑U, ⊤)<GOAL>X.basicOpen ((Hom.appIso (X.ofRestrict ⋯) ⊤).inv r) = X.basicOpen ((X.presheaf.map (eqToHom ⋯).op) r)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<VAR>r : ↑Γ(↑U, ⊤)<GOAL>X.basicOpen ((Hom.appIso (X.ofRestrict ⋯) ⊤).inv r) = X.basicOpen ((X.presheaf.map (eqToHom ⋯).op) ((X.presheaf.map (eqToHom ⋯).op) r))
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<VAR>r : ↑Γ(↑U, ⊤)<GOAL>X.basicOpen ((Hom.appIso (X.ofRestrict ⋯) ⊤).inv r) = X.basicOpen ((𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤)))) r)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<VAR>r : ↑Γ(↑U, ⊤)<GOAL>(Hom.appIso (X.ofRestrict ⋯) ⊤).inv = 𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤)))
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>x : Z<VAR>h : f ⁻¹' e.source ∈ 𝓝 x<GOAL>ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>x : Z<VAR>h : f ⁻¹' e.source ∈ 𝓝 x<VAR>hx : f x ∈ e.source<GOAL>ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>x : Z<VAR>h : f ⁻¹' e.source ∈ 𝓝 x<VAR>hx : f x ∈ e.source<VAR>h' : f ⁻¹' e.source ∈ 𝓝[univ] x<GOAL>ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f g : F<VAR>S T : Submodule R M<VAR>hS : Set.EqOn ⇑f ⇑g ↑S<VAR>hT : Set.EqOn ⇑f ⇑g ↑T<GOAL>Set.EqOn ⇑f ⇑g ↑(S ⊔ T)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f g : F<VAR>S T : Submodule R M<VAR>hS : S ≤ eqLocus f g<VAR>hT : T ≤ eqLocus f g<GOAL>S ⊔ T ≤ eqLocus f g
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<GOAL>a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<GOAL>0 ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = 0 ∧ c' * b' = b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<GOAL>∀ (x : R), IsUnit x → x ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = x ∧ c' * b' = b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CancelCommMonoidWithZero R<VAR>inst✝ : UniqueFactorizationMonoid R<VAR>a : R<GOAL>∀ (a p : R), a ≠ 0 → Prime p → (a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) → p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
<VAR>α : Type u_1<VAR>inst✝¹ : Ring α<VAR>inst✝ : LinearOrder α<VAR>a✝ b✝ a b : α<GOAL>|a| ∣ b ↔ a ∣ b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>hX : IsTerminal X<GOAL>IsZero X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>hX : IsTerminal X<GOAL>𝟙 X = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<GOAL>Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝ : CommMonoidWithZero P<VAR>f : S.LocalizationMap N<VAR>h : 0 ∈ S<VAR>a b : N<GOAL>a = b
<VAR>M : Type u_1<VAR>inst✝² : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝ : CommMonoidWithZero P<VAR>f : S.LocalizationMap N<VAR>h : 0 ∈ S<VAR>a b : N<GOAL>∃ c, ↑c * (↑(f.sec b).2 * (f.sec a).1) = ↑c * (↑(f.sec a).2 * (f.sec b).1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<VAR>x : α<GOAL>(∃ i, l.get? i = some (some x)) ↔ ∃ i, l.reduceOption.get? i = some x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>s : Set α<GOAL>IsOpen {l | s ∈ l}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hJ : M.Basis J Y<VAR>hJX : J ⊆ X<VAR>hIY : I ⊆ Y<GOAL>M.Basis I Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hJ : M.Basis J Y<VAR>hJX : J ⊆ X<VAR>hIY : I ⊆ Y<VAR>hI' : M.Basis I (X ∩ Y)<GOAL>M.Basis I Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hJ : M.Basis J Y<VAR>hJX : J ⊆ X<VAR>hIY : I ⊆ Y<VAR>hI' : M.Basis I (X ∩ Y)<VAR>hJ' : M.Basis J (X ∩ Y)<GOAL>M.Basis I Y