ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : _root_.Finite ι<VAR>b : Basis ι R M<VAR>f : ι →₀ R<VAR>i : ι<VAR>this : DecidableEq ι<GOAL>((Finsupp.total ι (Dual R M) R b.coord) f) (b i) = f i
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s<VAR>Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s<VAR>Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s<GOAL>∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s<VAR>Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s<GOAL>∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c✝ d : ℝ<VAR>f : ℝ → E<VAR>c : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (c * x) = ∫ (x : ℝ) in c * a..c * b, f x
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<GOAL>#↑(Ioi a) = 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<GOAL>𝔠 ≤ #↑(Ioi a)
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<GOAL>¬#↑(Ioi a) < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<GOAL>False
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<GOAL>#↑Set.univ < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<GOAL>#↑Set.univ < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<GOAL>#↑(Iio a ∪ {a} ∪ Ioi a) < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<GOAL>#↑(Iio a ∪ {a}) + #↑(Ioi a) < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<GOAL>#↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<VAR>h2 : (fun x => a + a - x) '' Ioi a = Iio a<GOAL>#↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<VAR>h2 : (fun x => a + a - x) '' Ioi a = Iio a<GOAL>#↑((fun x => a + a - x) '' Ioi a) + #↑{a} + #↑(Ioi a) < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<VAR>h2 : (fun x => a + a - x) '' Ioi a = Iio a<GOAL>#↑((fun x => a + a - x) '' Ioi a) + #↑{a} < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<VAR>h2 : (fun x => a + a - x) '' Ioi a = Iio a<GOAL>#↑{a} < 𝔠
<VAR>c : ℝ<VAR>f g : ℕ → Bool<VAR>n : ℕ<VAR>a : ℝ<VAR>h : #↑(Ioi a) < 𝔠<VAR>hu : Iio a ∪ {a} ∪ Ioi a = Set.univ<VAR>h2 : (fun x => a + a - x) '' Ioi a = Iio a<GOAL>1 < 𝔠
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedAddCommGroup E'<VAR>inst✝¹² : NormedAddCommGroup E''<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>inst✝⁷ : NormedSpace 𝕜 E''<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : μ.IsAddLeftInvariant<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : μ.IsNegInvariant<VAR>h : ConvolutionExistsAt f g x L μ<GOAL>Integrable (fun t => (L (f (x - t))) (g t)) μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedAddCommGroup E'<VAR>inst✝¹² : NormedAddCommGroup E''<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>inst✝⁷ : NormedSpace 𝕜 E''<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁵ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : μ.IsAddLeftInvariant<VAR>inst✝¹ : MeasurableAdd G<VAR>inst✝ : μ.IsNegInvariant<VAR>h : ConvolutionExistsAt f g x L μ<VAR>x✝ : G<GOAL>x✝ = x - (x - x✝)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>x : ZMod m<VAR>hψ : ψ (-1) = 1<GOAL>ψ (-x) = ψ x
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>S : Type<VAR>inst✝ : CommRing S<VAR>m : ℕ<VAR>ψ : DirichletCharacter S m<VAR>x : ZMod m<VAR>hψ : ψ (-1) = 1<GOAL>ψ (-1) * ψ x = ψ x
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx : x ∈ M.accepts<VAR>hlen : Fintype.card σ ≤ x.length<GOAL>∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>a b c : List α<VAR>hx : x = a ++ b ++ c<VAR>hlen : a.length + b.length ≤ Fintype.card σ<VAR>hnil : b ≠ []<VAR>hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a<VAR>hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x<GOAL>∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>a b c : List α<VAR>hx : x = a ++ b ++ c<VAR>hlen : a.length + b.length ≤ Fintype.card σ<VAR>hnil : b ≠ []<VAR>hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a<VAR>hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x<GOAL>{a} * {b}∗ * {c} ≤ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>a b c : List α<VAR>hx : x = a ++ b ++ c<VAR>hlen : a.length + b.length ≤ Fintype.card σ<VAR>hnil : b ≠ []<VAR>hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a<VAR>hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x<VAR>y : List α<VAR>hy : y ∈ {a} * {b}∗ * {c}<GOAL>y ∈ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>a b c : List α<VAR>hx : x = a ++ b ++ c<VAR>hlen : a.length + b.length ≤ Fintype.card σ<VAR>hnil : b ≠ []<VAR>hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a<VAR>hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x<VAR>y : List α<VAR>hy : ∃ a_1 ∈ {a} * {b}∗, ∃ b ∈ {c}, a_1 ++ b = y<GOAL>y ∈ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>a b c : List α<VAR>hx : x = a ++ b ++ c<VAR>hlen : a.length + b.length ≤ Fintype.card σ<VAR>hnil : b ≠ []<VAR>hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a<VAR>hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x<VAR>ab : List α<VAR>hab : ab ∈ {a} * {b}∗<VAR>c' : List α<VAR>hc' : c' ∈ {c}<GOAL>ab ++ c' ∈ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>a b c : List α<VAR>hx : x = a ++ b ++ c<VAR>hlen : a.length + b.length ≤ Fintype.card σ<VAR>hnil : b ≠ []<VAR>hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a<VAR>hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x<VAR>ab : List α<VAR>hab : ∃ a_1 ∈ {a}, ∃ b_1 ∈ {b}∗, a_1 ++ b_1 = ab<VAR>c' : List α<VAR>hc' : c' ∈ {c}<GOAL>ab ++ c' ∈ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>a b c : List α<VAR>hx : x = a ++ b ++ c<VAR>hlen : a.length + b.length ≤ Fintype.card σ<VAR>hnil : b ≠ []<VAR>hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a<VAR>hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x<VAR>c' : List α<VAR>hc' : c' ∈ {c}<VAR>a' : List α<VAR>ha' : a' ∈ {a}<VAR>b' : List α<VAR>hb' : b' ∈ {b}∗<GOAL>a' ++ b' ++ c' ∈ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>a b c : List α<VAR>hx : x = a ++ b ++ c<VAR>hlen : a.length + b.length ≤ Fintype.card σ<VAR>hnil : b ≠ []<VAR>hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a<VAR>hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x<VAR>c' : List α<VAR>hc' : c' = c<VAR>a' : List α<VAR>ha' : a' = a<VAR>b' : List α<VAR>hb' : b' ∈ {b}∗<GOAL>a' ++ b' ++ c' ∈ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>b : List α<VAR>hnil : b ≠ []<VAR>c' a' b' : List α<VAR>hb' : b' ∈ {b}∗<VAR>hlen : a'.length + b.length ≤ Fintype.card σ<VAR>hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'<VAR>hx : x = a' ++ b ++ c'<VAR>hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x<GOAL>a' ++ b' ++ c' ∈ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>hx✝ : x ∈ M.accepts<VAR>hlen✝ : Fintype.card σ ≤ x.length<VAR>b : List α<VAR>hnil : b ≠ []<VAR>c' a' b' : List α<VAR>hb' : b' ∈ {b}∗<VAR>hlen : a'.length + b.length ≤ Fintype.card σ<VAR>hb : M.evalFrom (M.evalFrom M.start a') b = M.evalFrom M.start a'<VAR>hx : x = a' ++ b ++ c'<VAR>hc : M.evalFrom (M.evalFrom M.start a') c' = M.evalFrom M.start x<VAR>h : M.evalFrom (M.evalFrom M.start a') b' = M.evalFrom M.start a'<GOAL>a' ++ b' ++ c' ∈ M.accepts
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing A'<VAR>inst✝⁷ : CommRing A''<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R A'<VAR>inst✝⁴ : Algebra R A''<VAR>a b : R<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra K A<VAR>inst✝¹ : IsEmpty ι<VAR>inst✝ : Nontrivial A<GOAL>AlgebraicIndependent K x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing A'<VAR>inst✝⁷ : CommRing A''<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R A'<VAR>inst✝⁴ : Algebra R A''<VAR>a b : R<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra K A<VAR>inst✝¹ : IsEmpty ι<VAR>inst✝ : Nontrivial A<GOAL>Injective ⇑(algebraMap K A)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<VAR>b : Finset M<VAR>h : LinearIndependent R fun x => ↑x<GOAL>b.card ≤ finrank R M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<VAR>b : Finset M<VAR>h : LinearIndependent R fun x => ↑x<GOAL>Fintype.card { x // x ∈ b } ≤ finrank R M
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' Ioc ↑x ↑y = Ioc x y
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' (Ioi ↑x ∩ Iic ↑y) = Ioi x ∩ Iic y
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>hl : l ≠ []<VAR>hl2 : l.getLast hl ≠ 0<GOAL>(b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>hl : l ≠ []<VAR>hl2 : l.getLast hl ≠ 0<GOAL>(b + 2) ^ (l.dropLast ++ [l.getLast hl]).length ≤ (b + 2) * ofDigits (b + 2) (l.dropLast ++ [l.getLast hl])
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>hl : l ≠ []<VAR>hl2 : l.getLast hl ≠ 0<GOAL>(b + 2) * (b + 2) ^ (l.length - 1) ≤ (b + 2) * (ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl)
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>hl : l ≠ []<VAR>hl2 : l.getLast hl ≠ 0<GOAL>(b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>hl : l ≠ []<VAR>hl2 : l.getLast hl ≠ 0<GOAL>(b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>hl : l ≠ []<VAR>hl2 : l.getLast hl ≠ 0<VAR>this : 0 < l.getLast hl<GOAL>(b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl
<VAR>n b : ℕ<VAR>l : List ℕ<VAR>hl : l ≠ []<VAR>hl2 : l.getLast hl ≠ 0<VAR>this : 0 < l.getLast hl<GOAL>(b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a : α<VAR>b : Associates α<GOAL>∀ (a_1 : α), Associates.out ⟦a_1⟧ ∣ a ↔ ⟦a_1⟧ ≤ Associates.mk a
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>n : ℕ<VAR>f : Fin n → E<VAR>h : ∀ (i : Fin n), ‖f i‖ ≤ 2<VAR>h' : Pairwise fun i j => 1 - goodδ E ≤ ‖f i - f j‖<GOAL>n ≤ multiplicity E
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y : (i : ι) → β i<GOAL>0 < hammingDist x y ↔ x ≠ y
<VAR>X : TopCat<VAR>ι : Type u_1<VAR>inst✝ : Category.{u_2, u_1} ι<VAR>B : ι ⥤ Opens ↑X<GOAL>B.IsCoverDense (Opens.grothendieckTopology ↑X) ↔ Opens.IsBasis (Set.range B.obj)
<VAR>X : TopCat<VAR>ι : Type u_1<VAR>inst✝ : Category.{u_2, u_1} ι<VAR>B : ι ⥤ Opens ↑X<GOAL>B.IsCoverDense (Opens.grothendieckTopology ↑X) ↔ ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>e : L ≃ₗ⁅R⁆ L'<VAR>x : L<VAR>y' : L'<GOAL>(e.toLinearEquiv.conj ((ad R L) x)) y' = ((ad R L') (e x)) y'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivInvMonoid G<VAR>a b c x y : G<GOAL>x * (1 / y) = x / y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq (α × β)<VAR>s : Finset α<VAR>t : Finset β<GOAL>Prod.swap '' ↑t ×ˢ ↑s = ↑s ×ˢ ↑t
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>M : Type u_2<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>a : A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module A M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsScalarTower R A M<VAR>m : AEval R M a<GOAL>(of R M a).symm (X • m) = a • (of R M a).symm m
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>e : A →ₐ[R] B<VAR>x : A<GOAL>Subalgebra.map e (adjoin R {x}) = adjoin R {e x}
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A : Matrix m n α<VAR>B : Matrix n m α<GOAL>(A * B + 1).det = (B * A + 1).det
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>p : k[X]<VAR>hsep : p.Separable<GOAL>p.roots = 0 ↔ p = C (p.coeff 0)
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>h : p.roots = 0<GOAL>p = C (p.coeff 0)
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>h : p.roots = 0<VAR>hd : p.degree ≤ 0<GOAL>p = C (p.coeff 0)
<VAR>k : Type u<VAR>inst✝² : Field k<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : IsSepClosed k<VAR>p : k[X]<VAR>hsep : p.Separable<VAR>h : p.roots = 0<VAR>hd : 0 < p.degree<GOAL>p = C (p.coeff 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>a : α<GOAL>stieltjesFunctionAux (fun p => f p.2) ((), a) = stieltjesFunctionAux f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α<VAR>ι : Type u_6<VAR>R : Type u_7<VAR>F : Filter ι<VAR>inst✝ : CompleteLattice R<VAR>a : ι → R<GOAL>limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α<VAR>ι : Type u_6<VAR>R : Type u_7<VAR>F : Filter ι<VAR>inst✝ : CompleteLattice R<VAR>a : ι → R<GOAL>limsup a F ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteLattice α<VAR>ι : Type u_6<VAR>R : Type u_7<VAR>F : Filter ι<VAR>inst✝ : CompleteLattice R<VAR>a : ι → R<GOAL>sInf ((fun I => sSup (a '' I)) '' F.sets) ≤ limsup a F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<GOAL>Primrec₂ fun x x_1 => x / x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<GOAL>PrimrecRel fun a b => (fun x x_1 => x / x_1) a.1 a.2 = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2<GOAL>PrimrecRel fun a b => (fun x x_1 => x / x_1) a.1 a.2 = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2<GOAL>∀ (a : ℕ × ℕ) (b : ℕ), a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2 ↔ (fun x x_1 => x / x_1) a.1 a.2 = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2<VAR>a k q : ℕ<GOAL>(a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔ (fun x x_1 => x / x_1) (a, k).1 (a, k).2 = q
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<GOAL>mixedEmbedding.norm ((mixedEmbedding K) x) = ↑|(Algebra.norm ℚ) x|
<VAR>α : Type u_1<VAR>inst✝ : OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<VAR>u : Set α<VAR>hu : u.IsPWO<VAR>x : α × α<GOAL>x ∈ mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>k : Type u_2<VAR>inst✝² : Field k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this : Algebra K ℂ := φ.toAlgebra<GOAL>∃ σ, φ.comp ↑σ.symm = ψ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>k : Type u_2<VAR>inst✝² : Field k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<GOAL>∃ σ, φ.comp ↑σ.symm = ψ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>k : Type u_2<VAR>inst✝² : Field k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<VAR>ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }<GOAL>∃ σ, φ.comp ↑σ.symm = ψ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>k : Type u_2<VAR>inst✝² : Field k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<VAR>ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }<GOAL>φ.comp ↑(ψ'.restrictNormal' K).symm.symm = ψ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>k : Type u_2<VAR>inst✝² : Field k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<VAR>ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }<VAR>x : K<GOAL>(φ.comp ↑(ψ'.restrictNormal' K).symm.symm) x = ψ x
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>[s.head] ++ₛ s.tail = s
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>s : Set A<VAR>z : A<GOAL>(∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g