ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>x : α<GOAL>x ∈ insert a (insert a s) ↔ x ∈ insert a s
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.Basis I X ↔ I ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I ∧ I ⊆ X}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : Filter α<VAR>g : Filter β<VAR>hf : Cauchy f<VAR>hg : Cauchy g<GOAL>Cauchy (f ×ˢ g)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : Filter α<VAR>g : Filter β<VAR>hf : Cauchy f<VAR>hg : Cauchy g<VAR>this : f.NeBot<GOAL>Cauchy (f ×ˢ g)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : Filter α<VAR>g : Filter β<VAR>hf : Cauchy f<VAR>hg : Cauchy g<VAR>this✝ : f.NeBot<VAR>this : g.NeBot<GOAL>Cauchy (f ×ˢ g)
<VAR>α : Sort u_1<VAR>x y z : α<VAR>h : x = y<GOAL>x = z ↔ y = z
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝¹ : Zero R<VAR>inst✝ : Pow R ℕ<VAR>s : Set ℕ := {k | x ^ k = 0}<VAR>hx : 0 < sInf s<GOAL>s.Nonempty
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝¹ : Zero R<VAR>inst✝ : Pow R ℕ<VAR>s : Set ℕ := {k | x ^ k = 0}<VAR>hx : 0 < sInf s<VAR>contra : ¬s.Nonempty<GOAL>False
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring S<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid N₁<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module S M₃<VAR>σ✝ : R →+* S<VAR>fₗ gₗ : M →ₗ[R] M₂<VAR>f✝ g✝ : M →ₛₗ[σ✝] M₃<VAR>σ : Rᵐᵒᵖ →+* S<VAR>f g : R →ₛₗ[σ] M₃<VAR>h : f 1 = g 1<VAR>x : R<GOAL>f x = g x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring S<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid N₁<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module S M₃<VAR>σ✝ : R →+* S<VAR>fₗ gₗ : M →ₗ[R] M₂<VAR>f✝ g✝ : M →ₛₗ[σ✝] M₃<VAR>σ : Rᵐᵒᵖ →+* S<VAR>f g : R →ₛₗ[σ] M₃<VAR>h : f 1 = g 1<VAR>x : R<GOAL>f (MulOpposite.op x • 1) = g (MulOpposite.op x • 1)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring S<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid N₁<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module S M₃<VAR>σ✝ : R →+* S<VAR>fₗ gₗ : M →ₗ[R] M₂<VAR>f✝ g✝ : M →ₛₗ[σ✝] M₃<VAR>σ : Rᵐᵒᵖ →+* S<VAR>f g : R →ₛₗ[σ] M₃<VAR>h : f 1 = g 1<VAR>x : R<GOAL>σ (MulOpposite.op x) • f 1 = g (MulOpposite.op x • 1)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring S<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid N₁<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module S M₃<VAR>σ✝ : R →+* S<VAR>fₗ gₗ : M →ₗ[R] M₂<VAR>f✝ g✝ : M →ₛₗ[σ✝] M₃<VAR>σ : Rᵐᵒᵖ →+* S<VAR>f g : R →ₛₗ[σ] M₃<VAR>h : f 1 = g 1<VAR>x : R<GOAL>σ (MulOpposite.op x) • g 1 = g (MulOpposite.op x • 1)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>le : map f p ≤ P<GOAL>ramificationIdx f p P ≠ 0
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>le : map f p ≤ P<VAR>hP0 : P ≠ ⊥<GOAL>ramificationIdx f p P ≠ 0
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>le : map f p ≤ P<VAR>hP0 : P ≠ ⊥<VAR>hPirr : Irreducible P<GOAL>ramificationIdx f p P ≠ 0
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>le : map f p ≤ P<VAR>hP0 : P ≠ ⊥<VAR>hPirr : Irreducible P<GOAL>Multiset.count P (normalizedFactors (map f p)) ≠ 0
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>le : map f p ≤ P<VAR>hP0 : P ≠ ⊥<VAR>hPirr : Irreducible P<VAR>P' : Ideal S<VAR>hP' : P' ∈ normalizedFactors (map f p)<VAR>P'_eq : Associated P P'<GOAL>Multiset.count P (normalizedFactors (map f p)) ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²³ : Semifield R<VAR>inst✝²² : StarRing R<VAR>inst✝²¹ : MetricSpace R<VAR>inst✝²⁰ : TopologicalSemiring R<VAR>inst✝¹⁹ : ContinuousStar R<VAR>inst✝¹⁸ : Semifield S<VAR>inst✝¹⁷ : StarRing S<VAR>inst✝¹⁶ : MetricSpace S<VAR>inst✝¹⁵ : TopologicalSemiring S<VAR>inst✝¹⁴ : ContinuousStar S<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : Ring A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : Algebra S A<VAR>inst✝⁹ : ContinuousFunctionalCalculus S q<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : IsScalarTower R S A<VAR>inst✝⁵ : StarModule R S<VAR>inst✝⁴ : ContinuousSMul R S<VAR>inst✝³ : CompleteSpace R<VAR>inst✝² : ContinuousFunctionalCalculus R p<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : SpectrumRestricts a ⇑f<VAR>inst✝ : CompactSpace ↑(spectrum S a)<GOAL>cfcHom hpa = starAlgHom (cfcHom hqa) h
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²³ : Semifield R<VAR>inst✝²² : StarRing R<VAR>inst✝²¹ : MetricSpace R<VAR>inst✝²⁰ : TopologicalSemiring R<VAR>inst✝¹⁹ : ContinuousStar R<VAR>inst✝¹⁸ : Semifield S<VAR>inst✝¹⁷ : StarRing S<VAR>inst✝¹⁶ : MetricSpace S<VAR>inst✝¹⁵ : TopologicalSemiring S<VAR>inst✝¹⁴ : ContinuousStar S<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : Ring A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : Algebra S A<VAR>inst✝⁹ : ContinuousFunctionalCalculus S q<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : IsScalarTower R S A<VAR>inst✝⁵ : StarModule R S<VAR>inst✝⁴ : ContinuousSMul R S<VAR>inst✝³ : CompleteSpace R<VAR>inst✝² : ContinuousFunctionalCalculus R p<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : SpectrumRestricts a ⇑f<VAR>inst✝ : CompactSpace ↑(spectrum S a)<GOAL>Continuous ⇑(starAlgHom (cfcHom hqa) h)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²³ : Semifield R<VAR>inst✝²² : StarRing R<VAR>inst✝²¹ : MetricSpace R<VAR>inst✝²⁰ : TopologicalSemiring R<VAR>inst✝¹⁹ : ContinuousStar R<VAR>inst✝¹⁸ : Semifield S<VAR>inst✝¹⁷ : StarRing S<VAR>inst✝¹⁶ : MetricSpace S<VAR>inst✝¹⁵ : TopologicalSemiring S<VAR>inst✝¹⁴ : ContinuousStar S<VAR>inst✝¹³ : TopologicalSpace A<VAR>inst✝¹² : Ring A<VAR>inst✝¹¹ : StarRing A<VAR>inst✝¹⁰ : Algebra S A<VAR>inst✝⁹ : ContinuousFunctionalCalculus S q<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : IsScalarTower R S A<VAR>inst✝⁵ : StarModule R S<VAR>inst✝⁴ : ContinuousSMul R S<VAR>inst✝³ : CompleteSpace R<VAR>inst✝² : ContinuousFunctionalCalculus R p<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus R A<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>a : A<VAR>hpa : p a<VAR>hqa : q a<VAR>h : SpectrumRestricts a ⇑f<VAR>inst✝ : CompactSpace ↑(spectrum S a)<GOAL>(starAlgHom (cfcHom hqa) h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝² : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>u : α → Set α<VAR>hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x<VAR>hu₀ : ∀ x ∈ s, μ (u x) = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝² : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t✝ : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>u : α → Set α<VAR>hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x<VAR>hu₀ : ∀ x ∈ s, μ (u x) = 0<VAR>t : Set α<VAR>ht : t ⊆ s ∧ t.Countable ∧ s ⊆ ⋃ x ∈ t, u x<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝² : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t✝ : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>u : α → Set α<VAR>hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x<VAR>hu₀ : ∀ x ∈ s, μ (u x) = 0<VAR>t : Set α<VAR>ts : t ⊆ s<VAR>t_count : t.Countable<VAR>ht : s ⊆ ⋃ x ∈ t, u x<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝² : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t✝ : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>u : α → Set α<VAR>hxu : ∀ x ∈ s, u x ∈ 𝓝[s] x<VAR>hu₀ : ∀ x ∈ s, μ (u x) = 0<VAR>t : Set α<VAR>ts : t ⊆ s<VAR>t_count : t.Countable<VAR>ht : s ⊆ ⋃ x ∈ t, u x<GOAL>μ (⋃ x ∈ t, u x) = 0
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>W : Projective R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>P : Fin 3 → R<VAR>u : Rˣ<GOAL>u • P = ![↑u * P 0, ↑u * P 1, ↑u * P 2]
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>W : Projective R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>P : Fin 3 → R<VAR>u : Rˣ<GOAL>u • ![P 0, P 1, P 2] = ![↑u * ![P 0, P 1, P 2] 0, ↑u * ![P 0, P 1, P 2] 1, ↑u * ![P 0, P 1, P 2] 2]
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>W : Projective R✝<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>P : Fin 3 → R<VAR>u : Rˣ<GOAL>![u • P 0, u • P 1, u • P 2] = ![↑u * P 0, ↑u * P 1, ↑u * P 2]
<VAR>α β : Type u<VAR>c : Cardinal.{?u.230017}<VAR>f : α → β<VAR>s : Set β<VAR>h : s ⊆ range f<GOAL>#↑s ≤ #↑(f ⁻¹' s)
<VAR>α β : Type u<VAR>c : Cardinal.{?u.230017}<VAR>f : α → β<VAR>s : Set β<VAR>h : s ⊆ range f<GOAL>lift.{u, u} #↑s ≤ lift.{u, u} #↑(f ⁻¹' s)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e✝ : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>inst✝¹ : CommSemiring S₂<VAR>inst✝ : CommSemiring S₃<VAR>e : S₁ ≃+* S₂<VAR>f : S₂ ≃+* S₃<VAR>p : MvPolynomial σ S₁<GOAL>((mapEquiv σ e).trans (mapEquiv σ f)) p = (mapEquiv σ (e.trans f)) p
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<VAR>ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)<GOAL>∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<VAR>ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)<VAR>this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)<GOAL>∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<VAR>ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)<VAR>this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)<GOAL>(u (n + 1) - u n) • f (u n) = ∑ i ∈ Ico (u n) (u (n + 1)), f (u n)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIciTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a✝ b✝ c✝ : α<VAR>f : α → β<VAR>a b c : α<VAR>H : b ∈ Ico a c<GOAL>Iio c ∩ Ioi b ⊆ Ioo a c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIciTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a✝ b✝ c✝ : α<VAR>f : α → β<VAR>a b c : α<VAR>H : b ∈ Ico a c<GOAL>Ioo b c ⊆ Ioo a c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : SemilatticeInf α<VAR>a b c : α<GOAL>Ioc a b ∩ Iic c = Ioc a (b ⊓ c)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2) (hurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>(↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2 = ↑(SignType.sign (↑↑n + a)) / ↑|↑↑n + a| ^ s / 2 + ↑(SignType.sign (↑(-(↑n + 1)) + a)) / ↑|↑(-(↑n + 1)) + a| ^ s / 2
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) = ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑n + 1) + a)) / ↑|-(↑n + 1) + a| ^ s / 2
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>this : -(↑n + 1) + a = -(↑n + 1 - a)<GOAL>↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) = ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑n + 1) + a)) / ↑|-(↑n + 1) + a| ^ s / 2
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<GOAL>Function.HasTemperateGrowth fun x => 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>n : ℕ<VAR>x : E<GOAL>‖iteratedFDeriv ℝ n (fun x => 0) x‖ ≤ 0 * (1 + ‖x‖) ^ 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>n : ℕ<VAR>x : E<GOAL>0 ≤ 0 * (1 + ‖x‖) ^ 0
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a a' : α<VAR>b : β a<VAR>b' : β a'<VAR>s✝ : Finmap β<VAR>h : a ≠ a'<VAR>s : AList β<GOAL>insert a' b' (insert a b ⟦s⟧) = insert a b (insert a' b' ⟦s⟧)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>i : Fin (n + 1)<VAR>x : β<VAR>p : Fin n → β<GOAL>∀ (x_1 : Fin n), i.insertNth x p (i.succAbove x_1) = p x_1
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>inst✝ : IsReflexive K V₂<GOAL>(ker B).dualAnnihilator = range (B.dualMap ∘ₗ ↑(evalEquiv K V₂))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f✝ (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>f : R → R<GOAL>cfc f 0 = (algebraMap R A) (f 0)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsCountablySpanning (C i)<GOAL>MeasurableSpace.pi = generateFrom (univ.pi '' univ.pi C)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsCountablySpanning (C i)<VAR>val✝ : Encodable ι<GOAL>MeasurableSpace.pi = generateFrom (univ.pi '' univ.pi C)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsCountablySpanning (C i)<VAR>val✝ : Encodable ι<GOAL>MeasurableSpace.pi ≤ generateFrom (univ.pi '' univ.pi C)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝¹ : Finite ι<VAR>inst✝ : Finite ι'<VAR>C : (i : ι) → Set (Set (α i))<VAR>hC : ∀ (i : ι), IsCountablySpanning (C i)<VAR>val✝ : Encodable ι<GOAL>generateFrom (univ.pi '' univ.pi C) ≤ MeasurableSpace.pi
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : α → ℝ≥0<GOAL>∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable fun a => ↑(f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : α → ℝ≥0<GOAL>∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable f
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>TendstoInMeasure μ f atTop g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hg : AEStronglyMeasurable g μ<GOAL>TendstoInMeasure μ f atTop g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hg : AEStronglyMeasurable g μ<GOAL>TendstoInMeasure μ (fun i => AEStronglyMeasurable.mk (f i) ⋯) atTop (AEStronglyMeasurable.mk g hg)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hg : AEStronglyMeasurable g μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hg : AEStronglyMeasurable g μ<VAR>hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hg : AEStronglyMeasurable g μ<VAR>hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x<VAR>x : α<VAR>hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x<VAR>hxg : g x = AEStronglyMeasurable.mk g hg x<VAR>hxfg : Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g hg x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>hg : AEStronglyMeasurable g μ<VAR>hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x<VAR>x : α<VAR>hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) ⋯ x = f n x<VAR>hxg : g x = AEStronglyMeasurable.mk g hg x<VAR>hxfg : Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>Tendsto (fun n => f n x) atTop (𝓝 (g x))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Set ℝ<VAR>x : ℝ<GOAL>x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n p k : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hk : ¬IsPeriodicPt f (p ^ k) x<VAR>hk1 : IsPeriodicPt f (p ^ (k + 1)) x<GOAL>minimalPeriod f x = p ^ (k + 1)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : Type w<VAR>f : J → C<VAR>inst✝⁶ : HasProduct f<VAR>D : Type t<VAR>inst✝⁵ : Category.{r, t} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>F : C ⥤ D<VAR>inst✝³ : PreservesLimit (Discrete.functor f) F<VAR>inst✝² : HasProduct fun j => F.obj (f j)<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)<VAR>inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)<VAR>x y : (forget D).obj (F.obj (∏ᶜ f))<VAR>h : ∀ (i : J), (F.map (Pi.π f i)) x = (F.map (Pi.π f i)) y<GOAL>x = y
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : Type w<VAR>f : J → C<VAR>inst✝⁶ : HasProduct f<VAR>D : Type t<VAR>inst✝⁵ : Category.{r, t} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>F : C ⥤ D<VAR>inst✝³ : PreservesLimit (Discrete.functor f) F<VAR>inst✝² : HasProduct fun j => F.obj (f j)<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)<VAR>inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)<VAR>x y : (forget D).obj (F.obj (∏ᶜ f))<VAR>h : ∀ (i : J), (F.map (Pi.π f i)) x = (F.map (Pi.π f i)) y<GOAL>(PreservesProduct.iso F f).hom x = (PreservesProduct.iso F f).hom y
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : Type w<VAR>f : J → C<VAR>inst✝⁶ : HasProduct f<VAR>D : Type t<VAR>inst✝⁵ : Category.{r, t} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>F : C ⥤ D<VAR>inst✝³ : PreservesLimit (Discrete.functor f) F<VAR>inst✝² : HasProduct fun j => F.obj (f j)<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)<VAR>inst✝ : PreservesLimit (Discrete.functor fun b => F.obj (f b)) (forget D)<VAR>x y : (forget D).obj (F.obj (∏ᶜ f))<VAR>h : ∀ (i : J), (F.map (Pi.π f i)) x = (F.map (Pi.π f i)) y<GOAL>∀ (j : Discrete J), (limit.π (Discrete.functor fun b => F.obj (f b)) j) ((piComparison F f) x) = (limit.π (Discrete.functor fun b => F.obj (f b)) j) ((piComparison F f) y)