ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : Group γ<VAR>inst✝² : DistribMulAction γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hf : ¬Summable f<VAR>mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g<GOAL>¬Summable (⇑mul_g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : Group γ<VAR>inst✝² : DistribMulAction γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hf : ¬Summable f<VAR>mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g<GOAL>Continuous ⇑mul_g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁸ : Monoid γ✝<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : AddCommMonoid α<VAR>inst✝⁵ : DistribMulAction γ✝ α<VAR>inst✝⁴ : ContinuousConstSMul γ✝ α<VAR>f : β → α<VAR>γ : Type u_5<VAR>inst✝³ : Group γ<VAR>inst✝² : DistribMulAction γ α<VAR>inst✝¹ : ContinuousConstSMul γ α<VAR>inst✝ : T2Space α<VAR>g : γ<VAR>hf : ¬Summable f<VAR>mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g<GOAL>Continuous (EquivLike.inv mul_g)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : EDist α<VAR>inst✝ : EDist β<VAR>x y : WithLp p (α × β)<VAR>x' : α × β<VAR>f g : WithLp 0 (α × β)<GOAL>edist f g = (if edist f.1 g.1 = 0 then 0 else 1) + if edist f.2 g.2 = 0 then 0 else 1
<VAR>b x : Bool<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)<VAR>h2 : Even (x :: l).length<GOAL>count (!b) (x :: l) = count b (x :: l)
<VAR>b x : Bool<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)<VAR>h2 : l.length % 2 = 1<GOAL>count (!b) (x :: l) = count b (x :: l)
<VAR>b x : Bool<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)<VAR>h2 : l.length % 2 = 1<GOAL>count (!x) (x :: l) = count x (x :: l)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)<GOAL>∀ (x : CliffordAlgebra Q), P x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)<GOAL>∀ (x : CliffordAlgebra Q), P (reverse x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)<VAR>x : CliffordAlgebra Q<GOAL>P (reverse x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)<VAR>r : R<GOAL>P (reverse ((_root_.algebraMap R (CliffordAlgebra Q)) r))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)<VAR>x y : CliffordAlgebra Q<VAR>hx : P (reverse x)<VAR>hy : P (reverse y)<GOAL>P (reverse (x + y))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticForm R M<VAR>P : CliffordAlgebra Q → Prop<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R (CliffordAlgebra Q)) r)<VAR>add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)<VAR>ι_mul : ∀ (x : CliffordAlgebra Q) (m : M), P x → P ((ι Q) m * x)<VAR>m : M<VAR>x : CliffordAlgebra Q<VAR>hx : P (reverse x)<GOAL>P (reverse (x * (ι Q) m))
<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>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v✝ : E<VAR>L : E →L[𝕜] F<VAR>hf : HasFDerivAt f L x<VAR>v : E<GOAL>HasLineDerivAt 𝕜 f (L v) x v
<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>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v✝ : E<VAR>L : E →L[𝕜] F<VAR>hf : HasFDerivAt f L x<VAR>v : E<GOAL>HasLineDerivWithinAt 𝕜 f (L v) univ x v
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a h : M<VAR>t : List M<VAR>n : ℕ<VAR>p : n + 1 < (h :: t).length<GOAL>(h :: take (n + 1) t).prod = (h :: take n t).prod * t[n]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin (n + 1) → M<GOAL>(liftAt 1 n φ).Realize v xs ↔ φ.Realize v (xs ∘ castSucc)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin (n + 1) → M<GOAL>φ.Realize v (xs ∘ fun i => if ↑i < n then i.castSucc else i.succ) = φ.Realize v (xs ∘ castSucc)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin (n + 1) → M<VAR>i : Fin n<GOAL>(if ↑i < n then i.castSucc else i.succ) = i.castSucc
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>ρ : Measure (α × β)<GOAL>ρ.fst univ = ρ univ
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Fintype R<VAR>p : R[X]<VAR>hp : 0 < p.degree<VAR>a : R<VAR>x✝ : a ∈ image (fun x => eval x p) univ<GOAL>filter (fun x => eval x p = a) univ = (p - C a).roots.toFinset
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → α → β<VAR>s t : Finset α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>image2 f (↑s ∩ ↑t) (↑s ∪ ↑t) ⊆ image2 f ↑s ↑t
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R✝ : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S R : Sieve X<VAR>hS : J.Covers S f<VAR>hR : J.Covers R f<GOAL>J.Covers (S ⊓ R) f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : Filter α<VAR>s : Set α<VAR>a : α<VAR>H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g<VAR>hf : s ∉ f<VAR>g : Filter ↑sᶜ := comap Subtype.val f<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : Filter α<VAR>s : Set α<VAR>a : α<VAR>H : ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g<VAR>hf : s ∉ f<VAR>g : Filter ↑sᶜ := comap Subtype.val f<VAR>this : g.NeBot<GOAL>False
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsOpen (s i)<VAR>B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}<GOAL>∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsOpen (s i)<VAR>B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}<VAR>f : ↑B → ι<VAR>hf : ∀ (b : ↑B), ↑b ⊆ s (f b)<GOAL>∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsOpen (s i)<VAR>B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}<VAR>f : ↑B → ι<VAR>hf : ∀ (b : ↑B), ↑b ⊆ s (f b)<VAR>this : Countable ↑B<GOAL>∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsOpen (s i)<VAR>B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}<VAR>f : ↑B → ι<VAR>hf : ∀ (b : ↑B), ↑b ⊆ s (f b)<VAR>this : Countable ↑B<GOAL>∀ t' ∈ range fun i => s i, t' ⊆ ⋃ i ∈ range f, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsOpen (s i)<VAR>B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}<VAR>f : ↑B → ι<VAR>hf : ∀ (b : ↑B), ↑b ⊆ s (f b)<VAR>this : Countable ↑B<VAR>i : ι<VAR>x : α<VAR>xs : x ∈ (fun i => s i) i<GOAL>x ∈ ⋃ i ∈ range f, s i
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_1<VAR>s : ι → Set α<VAR>H : ∀ (i : ι), IsOpen (s i)<VAR>B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}<VAR>f : ↑B → ι<VAR>hf : ∀ (b : ↑B), ↑b ⊆ s (f b)<VAR>this : Countable ↑B<VAR>i : ι<VAR>x : α<VAR>xs : x ∈ (fun i => s i) i<VAR>b : Set α<VAR>hb : b ∈ countableBasis α<VAR>xb : x ∈ b<VAR>bs : b ⊆ (fun i => s i) i<GOAL>x ∈ ⋃ i ∈ range f, s i
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s t : Multiset α<GOAL>s.Disjoint t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f g : R[X]<VAR>h : (f * g).Separable<GOAL>IsCoprime f g
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f g : R[X]<VAR>h : (f * g).Separable<VAR>this : IsCoprime f (derivative (f * g))<GOAL>IsCoprime f g
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f g : R[X]<VAR>h : (f * g).Separable<VAR>this : IsCoprime f (derivative f * g + f * derivative g)<GOAL>IsCoprime f g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>1 / a < b ↔ 1 / b < a
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasDerivedCategory C<GOAL>HasExt C
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasDerivedCategory C<GOAL>∀ (X Y : C) (n : ℤ), Small.{w, w} ((DerivedCategory.singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((DerivedCategory.singleFunctor C 0).obj Y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>a : α<VAR>s : List α<VAR>p : α → Bool<VAR>a✝ : α<GOAL>a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter (fun x => p x = true) s.toFinset
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Continuous f<VAR>c : Set α<VAR>c_count : c.Countable<VAR>hc : s ⊆ closure c<GOAL>IsSeparable (f '' s)
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Continuous f<VAR>c : Set α<VAR>c_count : c.Countable<VAR>hc : s ⊆ closure c<GOAL>f '' s ⊆ closure (f '' c)
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hf : Continuous f<VAR>c : Set α<VAR>c_count : c.Countable<VAR>hc : s ⊆ closure c<GOAL>s ⊆ f ⁻¹' closure (f '' c)
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<GOAL>(X ^ n + C a).degree = ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>a : R<VAR>this : (C a).degree < (X ^ n).degree<GOAL>(X ^ n + C a).degree = ↑n
<VAR>k✝ : Type u<VAR>inst✝⁵ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : Ring K<VAR>inst✝² : IsDomain K<VAR>hk : IsAlgClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsIntegral k K<VAR>x : K<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k✝ : Type u<VAR>inst✝⁵ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : Ring K<VAR>inst✝² : IsDomain K<VAR>hk : IsAlgClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsIntegral k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k✝ : Type u<VAR>inst✝⁵ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : Ring K<VAR>inst✝² : IsDomain K<VAR>hk : IsAlgClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsIntegral k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<VAR>h : (minpoly k x).degree = 1<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k✝ : Type u<VAR>inst✝⁵ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : Ring K<VAR>inst✝² : IsDomain K<VAR>hk : IsAlgClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsIntegral k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<VAR>h : (minpoly k x).degree = 1<VAR>this : (aeval x) (minpoly k x) = 0<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>k✝ : Type u<VAR>inst✝⁵ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : Ring K<VAR>inst✝² : IsDomain K<VAR>hk : IsAlgClosed k<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : Algebra.IsIntegral k K<VAR>x : K<VAR>hq : (minpoly k x).leadingCoeff = 1<VAR>h : (minpoly k x).degree = 1<VAR>this : x = -(algebraMap k K) ((minpoly k x).coeff 0)<GOAL>(algebraMap k K) (-(minpoly k x).coeff 0) = x
<VAR>x : PartENat<VAR>n : ℕ<GOAL>x < ↑n ↔ ∃ (h : x.Dom), x.get h < n
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>inst✝ : Finite ↥H<VAR>h : H = ⊤<GOAL>Nat.card ↥H = Nat.card G
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>U : Set 𝕜<VAR>hf : AnalyticOn 𝕜 f U<VAR>hg : AnalyticOn 𝕜 g U<VAR>hU : IsPreconnected U<VAR>h₀ : z₀ ∈ U<VAR>hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z<GOAL>EqOn f g U
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>U : Set 𝕜<VAR>hf : AnalyticOn 𝕜 f U<VAR>hg : AnalyticOn 𝕜 g U<VAR>hU : IsPreconnected U<VAR>h₀ : z₀ ∈ U<VAR>hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z<VAR>hfg' : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, (f - g) z = 0<GOAL>EqOn f g U
<VAR>a b : ℤ<VAR>h : a ≤ b<GOAL>↑(Fintype.card ↑(Set.Ico a b)) = b - a
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>n + 1 ≤ (n + 1) * (n + 1)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>(N₁Γ₀.app K).hom = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<GOAL>((Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫ (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ≫ (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>hg : G ≠ ⊥<GOAL>∑ x : ↥G, ↑↑x = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>hg : ∃ a, a ≠ 1<GOAL>∑ x : ↥G, ↑↑x = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>a : ↥G<VAR>ha : a ≠ 1<VAR>a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a<VAR>h_unchanged : map a_mul_emb univ = univ<GOAL>∑ x : ↥G, ↑↑x = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>a : ↥G<VAR>ha : a ≠ 1<VAR>a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a<VAR>h_unchanged : map a_mul_emb univ = univ<VAR>h_sum_map : ∑ x ∈ map a_mul_emb univ, ↑↑x = ∑ x : ↥G, ↑↑(a_mul_emb x)<GOAL>∑ x : ↥G, ↑↑x = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>a : ↥G<VAR>ha : a ≠ 1<VAR>a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a<VAR>h_unchanged : map a_mul_emb univ = univ<VAR>h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x<GOAL>∑ x : ↥G, ↑↑x = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>a : ↥G<VAR>ha : a ≠ 1<VAR>a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a<VAR>h_unchanged : map a_mul_emb univ = univ<VAR>h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x<VAR>hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0<GOAL>∑ x : ↥G, ↑↑x = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>a : ↥G<VAR>ha : a ≠ 1<VAR>a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a<VAR>h_unchanged : map a_mul_emb univ = univ<VAR>h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x<VAR>hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0<GOAL>¬↑↑a - 1 = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>a : ↥G<VAR>a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a<VAR>h_unchanged : map a_mul_emb univ = univ<VAR>h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x<VAR>hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0<VAR>ha : ↑↑a - 1 = 0<GOAL>a = 1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Ring K<VAR>inst✝¹ : NoZeroDivisors K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>a : ↥G<VAR>a_mul_emb : ↥G ↪ ↥G := mulLeftEmbedding a<VAR>h_unchanged : map a_mul_emb univ = univ<VAR>h_sum_map : ∑ x : ↥G, ↑↑x = ↑↑a * ∑ x : ↥G, ↑↑x<VAR>hzero : ↑↑a - 1 = 0 ∨ ∑ x : ↥G, ↑↑x = 0<VAR>ha : ↑↑a - 1 = 0<GOAL>↑↑a = ↑↑1
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : AEStronglyMeasurable X ℙ<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<GOAL>ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ evariance X ℙ / ↑c ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : AEStronglyMeasurable X ℙ<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>A : ↑c ≠ 0<GOAL>ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ evariance X ℙ / ↑c ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : AEStronglyMeasurable X ℙ<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>A : ↑c ≠ 0<VAR>B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ<GOAL>ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} ≤ evariance X ℙ / ↑c ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : AEStronglyMeasurable X ℙ<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>A : ↑c ≠ 0<VAR>B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ<GOAL>ℙ {ω | ↑c ≤ |X ω - ∫ (a : Ω), X a|} = ℙ {x | ↑c ≤ ↑‖(X - fun x => ∫ (a : Ω), X a) x‖₊}
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : AEStronglyMeasurable X ℙ<VAR>c : ℝ≥0<VAR>hc : c ≠ 0<VAR>A : ↑c ≠ 0<VAR>B : AEStronglyMeasurable (fun x => ∫ (a : Ω), X a) ℙ<GOAL>evariance X ℙ / ↑c ^ 2 = (↑c)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun x => ∫ (a : Ω), X a) 2 ℙ ^ ENNReal.toReal 2
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>n.sqrt * n.sqrt + n.sqrt ≤ n.sqrt.succ.succ.mul (n.sqrt + 1)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s✝ : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → Y → α<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>x : X<VAR>y : Y<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<VAR>l : Filter α<GOAL>Tendsto (uncurry (lift₂ f hf)) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s✝ : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → Y → α<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>x : X<VAR>y : Y<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<VAR>l : Filter α<GOAL>Tendsto (uncurry (lift₂ f hf)) (Filter.map (Prod.map mk mk) (𝓝 (x, y) ⊓ 𝓟 (Prod.map mk mk ⁻¹' s))) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>0 < Gamma s
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0<GOAL>0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0<GOAL>0 < volume ((Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0)