ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<GOAL>comap (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : InnerProductSpace 𝕜 F<VAR>inst✝⁴ : InnerProductSpace 𝕜 G<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : CompleteSpace G<VAR>inst✝¹ : CompleteSpace F<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<GOAL>adjoint (orthogonalProjection U) = U.subtypeL
<VAR>ι : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : ConditionallyCompleteLattice G<VAR>inst✝¹ : CovariantClass G G (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : Nonempty ι<VAR>f : ι → G<VAR>hf : BddBelow (range f)<VAR>a : G<GOAL>(⨅ i, f i) / a = ⨅ i, f i / a
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_4<VAR>M : Type u_5<VAR>ι : Type u_6<VAR>inst✝³ : Semiring R<VAR>inst✝² : Subsingleton R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : M<GOAL>(fun x => 0) ({ toFun := fun x => 0, map_add' := ⋯, map_smul' := ⋯ }.toFun m) = m
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_4<VAR>M : Type u_5<VAR>ι : Type u_6<VAR>inst✝³ : Semiring R<VAR>inst✝² : Subsingleton R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : M<VAR>this : Subsingleton M := Module.subsingleton R M<GOAL>(fun x => 0) ({ toFun := fun x => 0, map_add' := ⋯, map_smul' := ⋯ }.toFun m) = m
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>inst✝⁸ : Semiring R✝<VAR>inst✝⁷ : AddCommMonoid M✝<VAR>inst✝⁶ : Module R✝ M✝<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R✝ N<VAR>R : Type u_4<VAR>M : Type u_5<VAR>ι : Type u_6<VAR>inst✝³ : Semiring R<VAR>inst✝² : Subsingleton R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : ι →₀ R<GOAL>{ toFun := fun x => 0, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun x => 0) f) = f
<VAR>p : ℕ<VAR>w : 1 < p<GOAL>sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0
<VAR>p : ℕ<VAR>w : 1 < p<GOAL>↑(sMod p (p - 2)) = 0 ↔ sMod p (p - 2) = 0
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : M →* N<VAR>hf : ∀ (x : M), f x = 1 → x = 1<VAR>g : α → M<VAR>hg : ¬(mulSupport (g ∘ PLift.down)).Finite<GOAL>f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : M →* N<VAR>hf : ∀ (x : M), f x = 1 → x = 1<VAR>g : α → M<VAR>hg : ¬(mulSupport (g ∘ PLift.down)).Finite<GOAL>¬(mulSupport ((fun i => f (g i)) ∘ PLift.down)).Finite
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : M →* N<VAR>hf : ∀ (x : M), f x = 1 → x = 1<VAR>g : α → M<VAR>hg : ¬(mulSupport (g ∘ PLift.down)).Finite<GOAL>¬(mulSupport ((fun i => g i) ∘ PLift.down)).Finite
<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<GOAL>(optionEquivLeft R S₁) (X none) = Polynomial.X
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<GOAL>Module.rank (↥⊥) E = Module.rank F E
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b c : α<GOAL>∃! x, b + (Equiv.addRight 1) x • a ∈ Ioc c (c + a)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>(↑(quotKerTotalEquiv R S).symm).compDer (D R S) = derivationQuotKerTotal R S
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>s t : Multiset α<GOAL>map f s ≤ map f t ↔ s ≤ t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑((orthogonalProjection s) ↑((orthogonalProjection s) p)) = ↑((orthogonalProjection s) p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑((orthogonalProjection s) p) ∈ s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>hf : f ∈ maximalAtlas M' G'<VAR>h : LiftPropOn P g s<VAR>y : H<VAR>hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)<GOAL>P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) y
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>hf : f ∈ maximalAtlas M' G'<VAR>h : LiftPropOn P g s<VAR>y : H<VAR>hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)<GOAL>y = ↑e (↑e.symm y)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>W.Equation 0 0 ↔ W.a₆ = 0
<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>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq κ<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : Finset κ<VAR>i : ι<VAR>x : κ<VAR>hx : x ∈ s<GOAL>∏ j ∈ univ.erase i, s.card = s.card ^ (card ι - 1)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, p i<VAR>hp : ∀ (i : ι), ∀ x ∈ p i, C x<VAR>h0 : C 0<VAR>hadd : ∀ (x y : M), C x → C y → C (x + y)<GOAL>C x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, (p i).toAddSubmonoid<VAR>hp : ∀ (i : ι), ∀ x ∈ p i, C x<VAR>h0 : C 0<VAR>hadd : ∀ (x y : M), C x → C y → C (x + y)<GOAL>C x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2<GOAL>∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2<VAR>i : α<GOAL>b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2<VAR>i : α<VAR>h₁ : 0 ≤ b i<GOAL>b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>n : ℕ<VAR>hn : ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2<VAR>i : α<VAR>h₁ : 0 ≤ b i<GOAL>b i * ↑n - ↑(r i n) ≤ ↑n / log ↑n ^ 2
<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>inst✝³ : DecidableEq ι<VAR>inst✝² : DecidableEq κ<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>s : (i : ι) → Finset (α i)<VAR>i : ι<VAR>a : α i<VAR>ha : a ∈ s i<GOAL>(filter (fun f => f i = a) (piFinset s)).card = ∏ j ∈ univ.erase i, (s j).card
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.1345, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction₂ X Y<GOAL>φ.f' + φ.f = φ.f + φ.f'
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : Semiring C<VAR>inst✝² : Algebra R C<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : Algebra S A<VAR>r : R<GOAL>(algebraMap R (A ⊗[R] B)) r = 1 ⊗ₜ[R] (algebraMap R B) r
<VAR>k : ℕ<VAR>IH : multichoose 1 k = 1<GOAL>multichoose 1 (k + 1) = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Module S M<VAR>r : R<VAR>s : S<VAR>x : M<GOAL>(addEquiv R S M).symm ((r • s) • x) = r • (addEquiv R S M).symm (s • x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Module S M<VAR>r : R<VAR>s : S<VAR>x : M<GOAL>(addEquiv R S M).symm ((algebraMap R S) r • s • x) = r • (addEquiv R S M).symm (s • x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m : ℕ<VAR>h₀ : 0 ≤ a<VAR>h₁ : a < 1<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>a ^ (n + 1) < 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m : ℕ<VAR>h₀ : 0 ≤ a<VAR>h₁ : a < 1<VAR>n : ℕ<VAR>x✝ : n + 1 ≠ 0<GOAL>a * a ^ n < 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R →₀ ℤ<GOAL>count K v (exps.prod fun x x_1 => ↑x.asIdeal ^ x_1) = exps v
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R →₀ ℤ<GOAL>∑ i ∈ exps.support, count K v (↑i.asIdeal ^ exps i) = exps v
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R →₀ ℤ<GOAL>∀ i ∈ exps.support, ↑i.asIdeal ^ exps i ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : (comap m g).NeBot<GOAL>g.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : comap m g ≠ ⊥<GOAL>g ≠ ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : g = ⊥<GOAL>comap m g = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : g = ⊥<GOAL>comap m ⊥ = ⊥
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<VAR>hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n<GOAL>∫ (x : ℝ) in a..b, sin x ^ m * cos x ^ (2 * n + 1) = ∫ (x : ℝ) in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<VAR>hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n<GOAL>∫ (x : ℝ) in a..b, sin x ^ m * ((cos x * cos x) ^ n * cos x) = ∫ (x : ℝ) in a..b, sin x ^ m * ((1 - sin x * sin x) ^ n * cos x)
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<VAR>hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n<VAR>x✝ : ℝ<GOAL>cos x✝ * cos x✝ = 1 - sin x✝ * sin x✝
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<VAR>hc : Continuous fun u => u ^ m * (1 - u ^ 2) ^ n<GOAL>∫ (x : ℝ) in a..b, sin x ^ m * (1 - sin x ^ 2) ^ n * cos x = ∫ (u : ℝ) in sin a..sin b, u ^ m * (1 - u ^ 2) ^ n
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>a : M<VAR>b c : ↥S<GOAL>a * ↑(b * c) = a * ↑c * ↑b
<VAR>m : ℕ<VAR>a : Fin m → ℕ<VAR>i : Fin m<GOAL>a i < Nat.coprimes a i
<VAR>m : ℕ<VAR>a : Fin m → ℕ<VAR>i : Fin m<VAR>h₁ : a i < Nat.supOfSeq a<GOAL>a i < Nat.coprimes a i
<VAR>m : ℕ<VAR>a : Fin m → ℕ<VAR>i : Fin m<VAR>h₁ : a i < Nat.supOfSeq a<VAR>h₂ : Nat.supOfSeq a ≤ (↑i + 1) * (Nat.supOfSeq a)! + 1<GOAL>a i < Nat.coprimes a i
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : ℕ → Set X<VAR>hs : ∀ (n : ℕ), IsMeagre (s n)<GOAL>IsMeagre (⋃ n, s n)
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>s : ℕ → Set X<VAR>hs : ∀ (n : ℕ), IsMeagre (s n)<GOAL>⋂ i, (s i)ᶜ ∈ residual X
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<GOAL>Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑n = ↑↑n.pred' + 1
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑(↑n.pred' + 1) = ↑↑n.pred' + 1
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝¹ : PartialOrder ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<GOAL>Memℒp (stoppedValue u τ) p μ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝¹ : PartialOrder ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<GOAL>Memℒp (∑ i ∈ s, {ω | τ ω = i}.indicator (u i)) p μ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝¹ : PartialOrder ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>i : ι<VAR>x✝ : i ∈ s<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝¹ : PartialOrder ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>i : ι<VAR>x✝ : i ∈ s<GOAL>(Set.range τ).Countable
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝¹ : PartialOrder ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Memℒp (u n) p μ<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>i : ι<VAR>x✝ : i ∈ s<VAR>ω : ι<VAR>hω : ω ∈ Set.range τ<GOAL>ω ∈ ↑s
<VAR>α✝ : Type u<VAR>a : α✝<VAR>inst✝² : Group α✝<VAR>α : Type u<VAR>inst✝¹ : Group α<VAR>inst✝ : Fintype α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card α = p<GOAL>IsCyclic α
<VAR>α✝ : Type u<VAR>a : α✝<VAR>inst✝² : Group α✝<VAR>α : Type u<VAR>inst✝¹ : Group α<VAR>inst✝ : Fintype α<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card α = p<VAR>g : α<VAR>hg : g ≠ 1<GOAL>IsCyclic α
<VAR>a b c d n k : ℕ<VAR>p q : ℕ → Prop<VAR>w✝ : ℕ<VAR>hm : n * w✝ ≠ 0<GOAL>n * w✝ / (n * w✝ / n) = n
<VAR>a b c d n k : ℕ<VAR>p q : ℕ → Prop<VAR>w✝ : ℕ<VAR>hm : n ≠ 0 ∧ w✝ ≠ 0<GOAL>n * w✝ / (n * w✝ / n) = n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T T' : Set α → F →L[ℝ] F'<VAR>f : α →ₛ F<GOAL>setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T T' : Set α → F →L[ℝ] F'<VAR>f : α →ₛ F<GOAL>∑ x ∈ f.range, (T (↑f ⁻¹' {x}) + T' (↑f ⁻¹' {x})) x = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) x + ∑ x ∈ f.range, (T' (↑f ⁻¹' {x})) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T T' : Set α → F →L[ℝ] F'<VAR>f : α →ₛ F<GOAL>∑ x ∈ f.range, (⇑(T (↑f ⁻¹' {x})) + ⇑(T' (↑f ⁻¹' {x}))) x = ∑ x ∈ f.range, (T (↑f ⁻¹' {x})) x + ∑ x ∈ f.range, (T' (↑f ⁻¹' {x})) x
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>h : ∀ (x : α), (connectedComponent x).Subsingleton<VAR>s : Set α<VAR>s_sub : s ⊆ univ<VAR>hs : IsPreconnected s<GOAL>s.Subsingleton
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>h : ∀ (x : α), (connectedComponent x).Subsingleton<VAR>s_sub : ∅ ⊆ univ<VAR>hs : IsPreconnected ∅<GOAL>∅.Subsingleton
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>h : ∀ (x : α), (connectedComponent x).Subsingleton<VAR>s : Set α<VAR>s_sub : s ⊆ univ<VAR>hs : IsPreconnected s<VAR>x : α<VAR>x_in : x ∈ s<GOAL>s.Subsingleton
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>b : ℕ → ℝ<VAR>hb : ∀ (n : ℕ), 0 < b n<GOAL>∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε<VAR>b : ℕ → ℝ<VAR>hb : ∀ (n : ℕ), 0 < b n<GOAL>∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : ℕ → α<VAR>hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε<VAR>b : ℕ → ℝ<VAR>hb : ∀ (n : ℕ), 0 < b n<VAR>hu' : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k<GOAL>∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>inst✝ : IsReduced X<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<GOAL>X.basicOpen s = ⊥ ↔ s = 0
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>inst✝ : IsReduced X<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<GOAL>s = 0 → X.basicOpen s = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hus : u ⊆ s<VAR>hut : u ⊆ t<GOAL>{ ofColex := s \ u } ≤ { ofColex := t \ u } ↔ { ofColex := s } ≤ { ofColex := t }
<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>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι → 𝕜<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>⟪∑ i ∈ s, l i • v i, v i⟫_𝕜 = (starRingEnd 𝕜) (l i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<GOAL>‖↑((condexpL2 E 𝕜 hm) f)‖ ≤ ‖f‖