ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : F<VAR>p : Submodule R₂ M₂<GOAL>range f ≤ p ↔ comap f p = ⊤
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>X : C<GOAL>F.δ (𝟙_ C) X ≫ F.η ▷ F.obj X ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom
<VAR>m n a b c d : ℤ<GOAL>a ≡ 0 [ZMOD n] ↔ n ∣ a
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p : ℕ<VAR>f : σ → MvPolynomial τ R<GOAL>(expand p).comp (bind₁ f) = bind₁ fun i => (expand p) (f i)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p : ℕ<VAR>f : σ → MvPolynomial τ R<GOAL>∀ (i : σ), ((expand p).comp (bind₁ f)) (X i) = (bind₁ fun i => (expand p) (f i)) (X i)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p : ℕ<VAR>f : σ → MvPolynomial τ R<VAR>i : σ<GOAL>((expand p).comp (bind₁ f)) (X i) = (bind₁ fun i => (expand p) (f i)) (X i)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<VAR>h : e.toBasis.orientation = f.toBasis.orientation<GOAL>e.toBasis.det ⇑f = 1
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<VAR>h : e.toBasis.orientation = f.toBasis.orientation<GOAL>¬e.toBasis.det ⇑f = -1
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<VAR>h : e.toBasis.orientation = f.toBasis.orientation<VAR>this : 0 < e.toBasis.det ⇑f<GOAL>¬e.toBasis.det ⇑f = -1
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<GOAL>N = H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<GOAL>H.normalizer ≤ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<GOAL>N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<VAR>aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H<GOAL>N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<VAR>aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H<VAR>aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N<GOAL>N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<VAR>aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H<VAR>aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N<VAR>dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂<GOAL>N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<VAR>aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H<VAR>aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N<VAR>dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂<VAR>k : ℕ<VAR>hk : ∀ b ≥ k, Codisjoint (LinearMap.ker (dx ^ b)) (LinearMap.range (dx ^ b))<GOAL>N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<VAR>aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H<VAR>aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N<VAR>dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂<VAR>k : ℕ<VAR>hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))<GOAL>N.toSubmodule ≤ (engel R x).toSubmodule ⊔ H.toSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>x : L<VAR>h : engel R x ≤ H<VAR>N : LieSubalgebra R L := H.normalizer<VAR>aux₁ : ∀ n ∈ N, ⁅x, n⁆ ∈ H<VAR>aux₂ : ∀ n ∈ N, ⁅x, n⁆ ∈ N<VAR>dx : ↥N →ₗ[R] ↥N := LinearMap.restrict ((ad R L) x) aux₂<VAR>k : ℕ<VAR>hk : Codisjoint (LinearMap.ker (dx ^ (k + 1))) (LinearMap.range (dx ^ (k + 1)))<GOAL>⊤ ≤ Submodule.comap N.subtype ((engel R x).toSubmodule ⊔ H.toSubmodule)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : CommRing K<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : Fintype Kˣ<GOAL>∏ x : Kˣ, x = -1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommSemiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R A B<VAR>x : σ → B<VAR>p : MvPolynomial σ R<GOAL>(aeval x) ((map (algebraMap R A)) p) = (aeval x) p
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝¹ : CountableInterFilter l<VAR>inst✝ : Countable ι<VAR>p : α → ι → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ : Set (α → M)<VAR>ι : Type u_2<VAR>f : ι → Set (α → M)<VAR>hf : ∀ (i : ι), A.Definable L (f i)<VAR>s : Finset ι<GOAL>A.Definable L (⋂ i ∈ s, f i)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝ : Category.{?u.5749, u_3} E<VAR>J : GrothendieckTopology C<VAR>K✝ : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>G : C ⥤ D<VAR>K : GrothendieckTopology D<VAR>h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K.sieves B<VAR>B : D<VAR>X : C<VAR>f : G.obj X ⟶ B<VAR>h : Sieve.generate (Presieve.singleton f) ∈ K.sieves B<GOAL>Sieve.coverByImage G B ∈ K.sieves B
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝ : Category.{?u.5749, u_3} E<VAR>J : GrothendieckTopology C<VAR>K✝ : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>G : C ⥤ D<VAR>K : GrothendieckTopology D<VAR>h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K.sieves B<VAR>B : D<VAR>X : C<VAR>f : G.obj X ⟶ B<VAR>h : Sieve.generate (Presieve.singleton f) ∈ K.sieves B<GOAL>Sieve.generate (Presieve.singleton f) ≤ Sieve.coverByImage G B
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>x✝ : ↥(adjoin R s)<VAR>x : A<VAR>hx : x ∈ adjoin R s<GOAL>p ⟨x, hx⟩
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<VAR>p : ↥(adjoin R s) → Prop<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)<VAR>add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)<VAR>x✝ : ↥(adjoin R s)<VAR>x : A<VAR>hx : x ∈ adjoin R s<GOAL>∃ (x_1 : x ∈ adjoin R s), p ⟨x, x_1⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>p q : α → Prop<VAR>h : MeasurableSet {a | p a}<GOAL>MeasurableSet (p ⁻¹' {True})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>p q : α → Prop<VAR>h : Measurable p<GOAL>MeasurableSet {a | p a}
<VAR>c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<VAR>a b : Ordinal.{u_1}<VAR>ha : a < c.ord<VAR>hb : b < c.ord<GOAL>(fun x x_1 => x + x_1) a b < c.ord
<VAR>c : Cardinal.{u_1}<VAR>hc : ℵ₀ ≤ c<VAR>a b : Ordinal.{u_1}<VAR>ha : a.card < c<VAR>hb : b.card < c<GOAL>a.card + b.card < c
<VAR>p : ℕ<GOAL>Nat.rec 0 (fun y IH => (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>f : α → E<GOAL>(Summable fun x => ‖f x‖) ↔ Summable f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>f : α → E<VAR>hf : Summable f<GOAL>Summable fun x => ‖f x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>f : α → E<VAR>hf : Summable f<GOAL>∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖
<VAR>α : Type u_1<VAR>N : ℕ<VAR>g : α → Fin N → ℝ<VAR>hg : Summable g<GOAL>Summable fun x => ‖g x‖
<VAR>α : Type u_1<VAR>N : ℕ<VAR>g : α → Fin N → ℝ<VAR>hg : Summable g<VAR>this : ∀ (i : Fin N), Summable fun x => ‖g x i‖<GOAL>Summable fun x => ‖g x‖
<VAR>α : Type u_1<VAR>N : ℕ<VAR>g : α → Fin N → ℝ<VAR>hg : Summable g<VAR>this : ∀ (i : Fin N), Summable fun x => ‖g x i‖<VAR>x : α<GOAL>‖‖g x‖‖ ≤ ∑ i : Fin N, ‖g x i‖
<VAR>α : Type u_1<VAR>N : ℕ<VAR>g : α → Fin N → ℝ<VAR>hg : Summable g<VAR>this : ∀ (i : Fin N), Summable fun x => ‖g x i‖<VAR>x : α<GOAL>∀ (i : Fin N), ‖g x i‖ ≤ ∑ i : Fin N, ‖g x i‖
<VAR>α : Type u_1<VAR>N : ℕ<VAR>g : α → Fin N → ℝ<VAR>hg : Summable g<VAR>this : ∀ (i : Fin N), Summable fun x => ‖g x i‖<VAR>x : α<GOAL>0 ≤ ∑ i : Fin N, ‖g x i‖
<VAR>s : ℂ<GOAL>(1 - s).Gammaℝ * (1 + s).Gammaℝ = ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2))
<VAR>s : ℂ<GOAL>↑π ^ (-(1 - s) / 2) * Gamma ((1 - s) / 2) * (↑π ^ (-(1 + s) / 2) * Gamma ((1 + s) / 2)) = ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2))
<VAR>s : ℂ<GOAL>↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2)) = ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2)
<VAR>s : ℂ<GOAL>↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (↑π / sin (↑π * ((1 - s) / 2))) = ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π / sin (↑π / 2 - ↑π * s / 2)
<VAR>s : ℂ<GOAL>↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2) = (cos (↑π * s / 2))⁻¹
<VAR>s : ℂ<GOAL>↑π ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos (↑π * s / 2) = (cos (↑π * s / 2))⁻¹
<VAR>s : ℂ<GOAL>↑π ^ 0 * (cos (s * ↑π * (1 / 2)))⁻¹ = (cos (s * ↑π * (1 / 2)))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : ℕ → ℝ<VAR>R : ℝ<GOAL>[∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x, ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n, ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : ℕ → ℝ<VAR>R : ℝ<VAR>A : Set.Ico 0 R ⊆ Set.Ioo (-R) R<GOAL>[∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x, ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n, ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : ℕ → ℝ<VAR>R : ℝ<VAR>A : Set.Ico 0 R ⊆ Set.Ioo (-R) R<VAR>B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R<GOAL>[∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x, ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n, ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>f : β → α<VAR>a : α<VAR>s : Set α<VAR>l : Filter β<VAR>h : Tendsto f l (𝓝[s] a)<GOAL>∀ᶠ (i : β) in l, f i ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>f : β → α<VAR>a : α<VAR>s : Set α<VAR>l : Filter β<VAR>h : ∀ (i : Set α), a ∈ i ∧ IsOpen i → (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s<GOAL>∀ᶠ (i : β) in l, f i ∈ s
<VAR>a b c : Ordinal.{u_1}<VAR>b0 : ¬b = 0<VAR>a0 : ¬a = 0<GOAL>a ^ (b * c) = (a ^ b) ^ c
<VAR>a b c : Ordinal.{u_1}<VAR>b0 : ¬b = 0<VAR>a0 : ¬a = 0<VAR>a1 : 1 = a<GOAL>a ^ (b * c) = (a ^ b) ^ c
<VAR>a b c : Ordinal.{u_1}<VAR>b0 : ¬b = 0<VAR>a0 : ¬a = 0<VAR>a1 : 1 < a<GOAL>a ^ (b * c) = (a ^ b) ^ c
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>castNum <$> ofZNum' (ZNum.pos p) = (↑p).toNat'
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>castNum <$> ofZNum' (ZNum.pos p) = (↑↑p).toNat'
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>↑(↑p.pred' + 1) = ↑p
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>↑↑p.pred'.succ' = ↑p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s t : Set α<GOAL>s.encard - t.encard ≤ (s \ t).encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s t : Set α<GOAL>s.encard ≤ (s \ t).encard + t.encard
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s t : Set α<VAR>Hs : IsConnected s<VAR>Ht : IsConnected t<VAR>x : α<VAR>hx : x ∈ s ∩ t<GOAL>IsConnected (s ∪ t)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s t : Set α<VAR>Hs : IsConnected s<VAR>Ht : IsConnected t<VAR>x : α<VAR>hx : x ∈ s ∩ t<GOAL>IsPreconnected (s ∪ t)
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o : Ordinal.{u_1}<GOAL>enumOrd (range f) o = f o
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o : Ordinal.{u_1}<GOAL>∀ (j : Ordinal.{u_1}), (∀ k < j, enumOrd (range f) k = f k) → enumOrd (range f) j = f j
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o a : Ordinal.{u_1}<VAR>H : ∀ k < a, enumOrd (range f) k = f k<GOAL>enumOrd (range f) a = f a
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o a : Ordinal.{u_1}<VAR>H : ∀ k < a, enumOrd (range f) k = f k<GOAL>sInf (range f ∩ {b | ∀ c < a, enumOrd (range f) c < b}) = f a
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o a : Ordinal.{u_1}<VAR>H : ∀ k < a, enumOrd (range f) k = f k<VAR>Hfa : f a ∈ range f ∩ {b | ∀ c < a, enumOrd (range f) c < b}<GOAL>sInf (range f ∩ {b | ∀ c < a, enumOrd (range f) c < b}) = f a
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o a : Ordinal.{u_1}<VAR>H : ∀ k < a, enumOrd (range f) k = f k<VAR>Hfa : f a ∈ range f ∩ {b | ∀ c < a, enumOrd (range f) c < b}<GOAL>∀ b ∈ range f ∩ {b | ∀ c < a, enumOrd (range f) c < b}, f a ≤ b
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o a : Ordinal.{u_1}<VAR>H : ∀ k < a, enumOrd (range f) k = f k<VAR>Hfa : f a ∈ range f ∩ {b | ∀ c < a, enumOrd (range f) c < b}<VAR>c : Ordinal.{u_1}<VAR>hc : ∀ b < a, enumOrd (range f) b < f c<GOAL>f a ≤ f c
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o a : Ordinal.{u_1}<VAR>H : ∀ k < a, enumOrd (range f) k = f k<VAR>Hfa : f a ∈ range f ∩ {b | ∀ c < a, enumOrd (range f) c < b}<VAR>c : Ordinal.{u_1}<VAR>hc : ∀ b < a, enumOrd (range f) b < f c<GOAL>a ≤ c
<VAR>S : Set Ordinal.{u}<VAR>f : Ordinal.{u_1} → Ordinal.{u_1}<VAR>hf : StrictMono f<VAR>o a : Ordinal.{u_1}<VAR>H : ∀ k < a, enumOrd (range f) k = f k<VAR>Hfa : f a ∈ range f ∩ {b | ∀ c < a, enumOrd (range f) c < b}<VAR>c : Ordinal.{u_1}<VAR>hc : c < a<GOAL>∃ b < a, f c ≤ enumOrd (range f) b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V✝ : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV✝ : OrthogonalFamily 𝕜 G V✝<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>V : ι → Submodule 𝕜 E<VAR>hV : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ<GOAL>CompleteLattice.Independent V
<VAR>f : C(ℝ, ℂ)<VAR>hf : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>m : ℤ<GOAL>fourierCoeff ⋯.lift m = 𝓕 ⇑f ↑m
<VAR>f : C(ℝ, ℂ)<VAR>hf : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>m : ℤ<VAR>e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }<GOAL>fourierCoeff ⋯.lift m = 𝓕 ⇑f ↑m
<VAR>f : C(ℝ, ℂ)<VAR>hf : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>m : ℤ<VAR>e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }<VAR>neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖<GOAL>fourierCoeff ⋯.lift m = 𝓕 ⇑f ↑m
<VAR>f : C(ℝ, ℂ)<VAR>hf : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>m : ℤ<VAR>e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }<VAR>neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖<VAR>eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e<GOAL>fourierCoeff ⋯.lift m = 𝓕 ⇑f ↑m
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<GOAL>J(a | b) ≠ 0
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<VAR>hb : b = 0<GOAL>J(a | b) ≠ 0
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<VAR>h✝ : NeZero b<GOAL>J(a | b) ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : Associates α<GOAL>a.factors.prod = a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<GOAL>(Associates.mk a).factors.prod = Associates.mk a
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<GOAL>(Associates.mk 0).factors.prod = Associates.mk 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>(Associates.mk a).factors.prod = Associates.mk a
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F₁ : A ⥤ C<VAR>U₁ : C ⥤ A<VAR>F₂ : B ⥤ D<VAR>U₂ : D ⥤ B<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : F₁ ⊣ U₁<VAR>adj₄ : F₂ ⊣ U₂<VAR>α : U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁<GOAL>(mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) = (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm α
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} A<VAR>inst✝² : Category.{v₂, u₂} B<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F₁ : A ⥤ C<VAR>U₁ : C ⥤ A<VAR>F₂ : B ⥤ D<VAR>U₂ : D ⥤ B<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : F₁ ⊣ U₁<VAR>adj₄ : F₂ ⊣ U₂<VAR>α : U₂ ⋙ R₁ ⟶ R₂ ⋙ U₁<GOAL>(mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α))) = α
<VAR>x : ↑I<GOAL>0 ≤ 1 - ↑x
<VAR>F : Type u → Type u<VAR>inst✝¹ : Applicative F<VAR>inst✝ : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>α β : Type u_1<VAR>h : α → β<GOAL>Functor.map h ∘ Coe.coe = Coe.coe ∘ Functor.map h
<VAR>F : Type u → Type u<VAR>inst✝¹ : Applicative F<VAR>inst✝ : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>α β : Type u_1<VAR>h : α → β<VAR>x✝ : List α<GOAL>(Functor.map h ∘ Coe.coe) x✝ = (Coe.coe ∘ Functor.map h) x✝
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>x : M ∗ N<GOAL>(toProd x).2 = snd x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>x : M ∗ N<GOAL>(toProd x).2 = ((MonoidHom.snd M N).comp toProd) x