ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableEq R<VAR>x✝² : (p : R[X]) ×' p ≠ 0<VAR>a✝¹ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y x✝² → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>p✝ : R[X]<VAR>x✝¹ : p✝ ≠ 0<VAR>a✝ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y ⟨p✝, x✝¹⟩ → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>x✝ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y ⟨p, hp⟩ → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<GOAL>(p /ₘ (X - C x)).natDegree < p.natDegree
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableEq R<VAR>x✝² : (p : R[X]) ×' p ≠ 0<VAR>a✝¹ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y x✝² → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>p✝ : R[X]<VAR>x✝¹ : p✝ ≠ 0<VAR>a✝ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y ⟨p✝, x✝¹⟩ → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>x✝ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y ⟨p, hp⟩ → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<GOAL>↑(p /ₘ (X - C x)).natDegree < ↑p.natDegree
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableEq R<VAR>x✝² : (p : R[X]) ×' p ≠ 0<VAR>a✝¹ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y x✝² → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>p✝ : R[X]<VAR>x✝¹ : p✝ ≠ 0<VAR>a✝ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y ⟨p✝, x✝¹⟩ → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>x✝ : ∀ (y : (p : R[X]) ×' p ≠ 0), (invImage (fun x => PSigma.casesOn x fun p x => p.natDegree) instWellFoundedRelationOfSizeOf).1 y ⟨p, hp⟩ → ∃ s, ↑(Multiset.card s) ≤ y.1.degree ∧ ∀ (a : R), count a s = rootMultiplicity a y.1<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : ↑(p /ₘ (X - C x)).natDegree < ↑p.natDegree<GOAL>↑(p /ₘ (X - C x)).natDegree < ↑p.natDegree
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n : ℕ<GOAL>Option.map (Pair.map Rat.cast) ((of q).s.get? n) = (of v).s.get? n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n : ℕ<GOAL>Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.Seq.get? ⟨IntFractPair.stream q, ⋯⟩ (n + 1))) = Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.Seq.get? ⟨IntFractPair.stream v, ⋯⟩ (n + 1))
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n : ℕ<GOAL>Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) = Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream v (n + 1))
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n : ℕ<GOAL>Option.map (Pair.map Rat.cast) (Option.map (fun p => { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) = Option.map (fun p => { a := 1, b := ↑p.b }) (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<GOAL>cycleFactorsFinset 1 = ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>hc : ∀ (i : ι), Continuous (f i)<VAR>hf : LocallyFinite fun i => mulSupport (f i)<GOAL>Continuous fun x => ∏ᶠ (i : ι), f i x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>hc : ∀ (i : ι), Continuous (f i)<VAR>hf : LocallyFinite fun i => mulSupport (f i)<VAR>x : X<GOAL>ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>hc : ∀ (i : ι), Continuous (f i)<VAR>hf : LocallyFinite fun i => mulSupport (f i)<VAR>x : X<VAR>s : Finset ι<VAR>hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y<GOAL>ContinuousAt (fun x => ∏ᶠ (i : ι), f i x) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>hc : ∀ (i : ι), Continuous (f i)<VAR>hf : LocallyFinite fun i => mulSupport (f i)<VAR>x : X<VAR>s : Finset ι<VAR>hs : ∀ᶠ (y : X) in 𝓝 x, ∏ᶠ (i : ι), f i y = ∏ i ∈ s, f i y<GOAL>ContinuousAt (fun x => ∏ i ∈ s, f i x) x
<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>hf : ∀ b ∈ t, Injective fun a => f a b<VAR>ht : ((fun b => image (fun a => f a b) s) '' ↑t).PairwiseDisjoint id<GOAL>s.card ∣ (image₂ f s t).card
<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>hf : ∀ b ∈ t, Injective fun a => f a b<VAR>ht : ((fun b => image (fun a => f a b) s) '' ↑t).PairwiseDisjoint id<GOAL>s.card ∣ (image₂ (fun b a => f a b) t s).card
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<GOAL>1 ≤ ↑w.mult
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<GOAL>1 ≤ w.mult
<VAR>μ : YoungDiagram<VAR>i : ℕ<GOAL>∃ j, (i, j) ∉ μ
<VAR>μ : YoungDiagram<VAR>i j : ℕ<VAR>hj : j ∉ μ.cells.preimage (Prod.mk i) ⋯<GOAL>∃ j, (i, j) ∉ μ
<VAR>μ : YoungDiagram<VAR>i j : ℕ<VAR>hj : (i, j) ∉ μ.cells<GOAL>∃ j, (i, j) ∉ μ
<VAR>x y : ℤ<GOAL>x.gcd y = x.natAbs.gcd y.natAbs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Finset ι<VAR>f : ι → Set α<VAR>hd : (↑s).Pairwise (AEDisjoint μ on f)<VAR>hm : ∀ b ∈ s, NullMeasurableSet (f b) μ<GOAL>μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>s : Finset ι<VAR>f : ι → Set α<VAR>hd : (↑s).Pairwise (AEDisjoint μ on f)<VAR>hm : ∀ b ∈ s, NullMeasurableSet (f b) μ<GOAL>μ (⋃ b ∈ s, f b) = ∑' (b : { x // x ∈ s }), μ (f ↑b)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommRing R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<GOAL>(p - q).vars ⊆ p.vars ∪ q.vars
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonAssocSemiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j✝ : n<GOAL>(M * 1) i✝ j✝ = M i✝ j✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : s.ncard ≠ 0<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : s.ncard ≠ 0<GOAL>s ≠ ∅
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>ι : Type u_3<VAR>hs : IsZlattice K L<VAR>b : Basis ι ℤ ↥L<VAR>x : ↥L<VAR>i : ι<GOAL>((ofZlatticeBasis K L b).repr ↑x) i = ↑((b.repr x) i)
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>ι : Type u_3<VAR>hs : IsZlattice K L<VAR>b : Basis ι ℤ ↥L<VAR>x : ↥L<VAR>i : ι<GOAL>↑ℤ ↑(ofZlatticeBasis K L b).repr ∘ₗ L.subtype.toIntLinearMap = Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr
<VAR>K : Type u_1<VAR>inst✝⁷ : NormedLinearOrderedField K<VAR>inst✝⁶ : HasSolidNorm K<VAR>inst✝⁵ : FloorRing K<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>inst✝² : FiniteDimensional K E<VAR>inst✝¹ : ProperSpace E<VAR>L : AddSubgroup E<VAR>inst✝ : DiscreteTopology ↥L<VAR>ι : Type u_3<VAR>hs : IsZlattice K L<VAR>b : Basis ι ℤ ↥L<VAR>x : ↥L<VAR>i✝ i : ι<GOAL>(↑ℤ ↑(ofZlatticeBasis K L b).repr ∘ₗ L.subtype.toIntLinearMap) (b i) = (Finsupp.mapRange.linearMap (Algebra.linearMap ℤ K) ∘ₗ ↑b.repr) (b i)
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>n : ℕ<GOAL>s.sum ^ (Multiset.card s * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<GOAL>Multiset.sum 0 ^ (Multiset.card 0 * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) 0).toFinset
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<VAR>a : α<VAR>s : Multiset α<VAR>hs : s.sum ^ (Multiset.card s * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset<GOAL>(a ::ₘ s).sum ^ (Multiset.card (a ::ₘ s) * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) (a ::ₘ s)).toFinset
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<VAR>a : α<VAR>s : Multiset α<VAR>hs : s.sum ^ (Multiset.card s * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset<GOAL>∑ m ∈ Finset.range ((Multiset.card s + 1) * n + 1 + 1), a ^ m * s.sum ^ ((Multiset.card s + 1) * n + 1 - m) * ↑(((Multiset.card s + 1) * n + 1).choose m) ∈ span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset)
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<VAR>a : α<VAR>s : Multiset α<VAR>hs : s.sum ^ (Multiset.card s * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset<GOAL>∀ c ∈ Finset.range ((Multiset.card s + 1) * n + 1 + 1), a ^ c * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) * ↑(((Multiset.card s + 1) * n + 1).choose c) ∈ span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset)
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<VAR>a : α<VAR>s : Multiset α<VAR>hs : s.sum ^ (Multiset.card s * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset<VAR>c : ℕ<VAR>_hc : c ∈ Finset.range ((Multiset.card s + 1) * n + 1 + 1)<GOAL>a ^ c * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) * ↑(((Multiset.card s + 1) * n + 1).choose c) ∈ span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset)
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b : α<VAR>inst✝¹ : CommSemiring α<VAR>I : Ideal α<VAR>inst✝ : DecidableEq α<VAR>n : ℕ<VAR>a : α<VAR>s : Multiset α<VAR>hs : s.sum ^ (Multiset.card s * n + 1) ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset<VAR>c : ℕ<VAR>_hc : c ∈ Finset.range ((Multiset.card s + 1) * n + 1 + 1)<GOAL>∃ a_1, ∃ z ∈ span ↑(Multiset.map (fun x => x ^ (n + 1)) s).toFinset, a ^ c * s.sum ^ ((Multiset.card s + 1) * n + 1 - c) * ↑(((Multiset.card s + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : TendstoUniformlyOn F f φ (cthickening δ K)<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<GOAL>TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hδ : 0 < δ<VAR>hF : TendstoUniformlyOn F f ⊥ (cthickening δ K)<VAR>hFn : ∀ᶠ (n : ι) in ⊥, ContinuousOn (F n) (cthickening δ K)<GOAL>TendstoUniformlyOn (cderiv δ ∘ F) (cderiv δ f) ⊥ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : TendstoUniformlyOn F f φ (cthickening δ K)<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<GOAL>TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : TendstoUniformlyOn F f φ (cthickening δ K)<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<VAR>e1 : ContinuousOn f (cthickening δ K)<GOAL>TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<VAR>e1 : ContinuousOn f (cthickening δ K)<GOAL>∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<VAR>e1 : ContinuousOn f (cthickening δ K)<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ᶠ (n : ι) in φ, ∀ x ∈ K, dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z✝ : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<VAR>e1 : ContinuousOn f (cthickening δ K)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ι<VAR>h : ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε * δ<VAR>h' : ContinuousOn (F n) (cthickening δ K)<VAR>z : ℂ<VAR>hz : z ∈ K<GOAL>dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z✝ : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<VAR>e1 : ContinuousOn f (cthickening δ K)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ι<VAR>h' : ContinuousOn (F n) (cthickening δ K)<VAR>z : ℂ<VAR>hz : z ∈ K<VAR>h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ<GOAL>‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z✝ : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<VAR>e1 : ContinuousOn f (cthickening δ K)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ι<VAR>h' : ContinuousOn (F n) (cthickening δ K)<VAR>z : ℂ<VAR>hz : z ∈ K<VAR>h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ<VAR>e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ<GOAL>‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z✝ : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<VAR>e1 : ContinuousOn f (cthickening δ K)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ι<VAR>h' : ContinuousOn (F n) (cthickening δ K)<VAR>z : ℂ<VAR>hz : z ∈ K<VAR>h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ<VAR>e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ<VAR>e3 : sphere z δ ⊆ cthickening δ K<GOAL>‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z✝ : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hF : ∀ ε > 0, ∀ᶠ (n : ι) in φ, ∀ x ∈ cthickening δ K, dist (f x) (F n x) < ε<VAR>hδ : 0 < δ<VAR>hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)<VAR>hne : φ.NeBot<VAR>e1 : ContinuousOn f (cthickening δ K)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>n : ι<VAR>h' : ContinuousOn (F n) (cthickening δ K)<VAR>z : ℂ<VAR>hz : z ∈ K<VAR>h : ∀ x ∈ cthickening δ K, ‖f x - F n x‖ < ε * δ<VAR>e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ<VAR>e3 : sphere z δ ⊆ cthickening δ K<VAR>hf : ContinuousOn f (sphere z δ)<GOAL>‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : BijOn f ∅ t<GOAL>t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<GOAL>BijOn f ∅ ∅
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsInt e (Int.negOfNat n)<GOAL>0 ≤ Real.log e
<VAR>e : ℝ<VAR>d n : ℕ<VAR>h : NormNum.IsInt e (Int.negOfNat n)<GOAL>0 ≤ Real.log (-↑n)
<VAR>R : Type u<VAR>inst✝³ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝² : CommSemiring S<VAR>f : R →* S<VAR>g : R →+* S<VAR>p m n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : ExpChar S p<VAR>x y : R<GOAL>(iterateFrobenius R p 1) x = x ^ p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformEmbedding g<VAR>f : α → β<GOAL>UniformEmbedding (g ∘ f) ↔ UniformEmbedding f
<VAR>R : Type u_1<VAR>m n : ℕ<VAR>hmn : m.Coprime n<GOAL>∑ d ∈ (m * n).divisors, d = (∑ d ∈ m.divisors, d) * ∑ d ∈ n.divisors, d
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>k m n : ℕ<VAR>hm : m ≠ 0<VAR>hkmn : m * k ≤ n<GOAL>MapsTo val (Iic ↑k) (Iic k)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>k m n : ℕ<VAR>hm : m ≠ 0<VAR>hkmn : m * k ≤ n<VAR>x : ℕ<VAR>hx : x ≤ k<GOAL>↑x ∈ Iic ↑k ∧ ↑↑x = x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>k m n : ℕ<VAR>hm : m ≠ 0<VAR>hkmn : m * k ≤ n<VAR>s t : Multiset (Fin (n + 1))<VAR>hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k<VAR>htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k<VAR>hs : card s = m<VAR>ht : card t = m<VAR>this : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum<GOAL>(map val s).sum = (map val t).sum ↔ (Nat.castRingHom (Fin (n + 1))) (map val s).sum = (Nat.castRingHom (Fin (n + 1))) (map val t).sum
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>k m n : ℕ<VAR>hm : m ≠ 0<VAR>hkmn : m * k ≤ n<VAR>s t : Multiset (Fin (n + 1))<VAR>hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k<VAR>htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k<VAR>hs : card s = m<VAR>ht : card t = m<VAR>this✝ : ∀ (u : Multiset (Fin (n + 1))), (Nat.castRingHom (Fin (n + 1))) (map val u).sum = u.sum<VAR>this : ∀ {u : Multiset (Fin (n + 1))}, (∀ x ∈ u, x ≤ ↑k) → card u = m → (map val u).sum < n + 1<GOAL>(map val s).sum = (map val t).sum ↔ (Nat.castRingHom (Fin (n + 1))) (map val s).sum = (Nat.castRingHom (Fin (n + 1))) (map val t).sum
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : DifferentiableWithinAt 𝕜 (dslope f a) s b<GOAL>DifferentiableWithinAt 𝕜 f s b
<VAR>R✝ : Type u_1<VAR>inst✝² : AddMonoidWithOne R✝<VAR>p✝ a✝ b✝ : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : AddMonoidWithOne R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>a b : ℕ<VAR>h : a ≡ b [MOD p]<VAR>hle : a ≤ b<GOAL>↑a = ↑b
<VAR>R✝ : Type u_1<VAR>inst✝² : AddMonoidWithOne R✝<VAR>p✝ a✝ b✝ : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : AddMonoidWithOne R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>a b : ℕ<VAR>h : p ∣ b - a<VAR>hle : a ≤ b<GOAL>↑a = ↑b
<VAR>x y : ℝ<VAR>n : ℤ<GOAL>0 ≤ log ↑n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>hf : LeftOrdContinuous f<VAR>g : ι → α<VAR>hg : BddAbove (range g)<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)