ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : Measurable g<VAR>hf : AEMeasurable f μ<GOAL>essSup g (Measure.map f μ) ≤ essSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : Measurable g<VAR>hf : AEMeasurable f μ<VAR>c : β<VAR>h_le : ∀ᶠ (n : β) in map (g ∘ f) (ae μ), n ≤ c<GOAL>∀ᶠ (n : β) in map g (ae (Measure.map f μ)), n ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : Measurable g<VAR>hf : AEMeasurable f μ<VAR>c : β<VAR>h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c<GOAL>∀ᵐ (a : γ) ∂Measure.map f μ, g a ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : CompleteLattice β<VAR>γ : Type u_3<VAR>mγ : MeasurableSpace γ<VAR>f : α → γ<VAR>g : γ → β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : OpensMeasurableSpace β<VAR>hg : Measurable g<VAR>hf : AEMeasurable f μ<VAR>c : β<VAR>h_le : ∀ᵐ (a : α) ∂μ, (g ∘ f) a ≤ c<GOAL>∀ᵐ (x : α) ∂μ, g (f x) ≤ c
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁵ : Field 𝕂<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : Algebra 𝕂 𝔸<VAR>inst✝² : TopologicalSpace 𝔸<VAR>inst✝¹ : TopologicalRing 𝔸<VAR>inst✝ : T2Space 𝔸<VAR>x : 𝔸<GOAL>exp 𝕂 (MulOpposite.op x) = MulOpposite.op (exp 𝕂 x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace γ<VAR>h : TendstoLocallyUniformly F f p<VAR>g : γ → α<VAR>cg : Continuous g<GOAL>TendstoLocallyUniformly (fun n => F n ∘ g) (f ∘ g) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace γ<VAR>h : TendstoLocallyUniformlyOn F f p univ<VAR>g : γ → α<VAR>cg : Continuous g<GOAL>TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g✝ : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace γ<VAR>h : TendstoLocallyUniformlyOn F f p univ<VAR>g : γ → α<VAR>cg : ContinuousOn g univ<GOAL>TendstoLocallyUniformlyOn (fun n => F n ∘ g) (f ∘ g) p univ
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ℵ₀<VAR>hb : ↑n < ℵ₀<GOAL>↑m ^ ↑n < ℵ₀
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ℵ₀<VAR>hb : ↑n < ℵ₀<GOAL>↑(m ^ n) < ℵ₀
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I✝ : Ideal A<VAR>I J : HomogeneousIdeal 𝒜<VAR>h : ∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J<VAR>x✝ : A<GOAL>x✝ ∈ I.toIdeal ↔ x✝ ∈ J.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I✝ : Ideal A<VAR>I J : HomogeneousIdeal 𝒜<VAR>h : ∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J<VAR>x✝ : A<GOAL>(∀ (i : ι), ↑(((decompose 𝒜) x✝) i) ∈ I.toIdeal) ↔ ∀ (i : ι), ↑(((decompose 𝒜) x✝) i) ∈ J.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I✝ : Ideal A<VAR>I J : HomogeneousIdeal 𝒜<VAR>h : ∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J<VAR>x✝ : A<GOAL>∀ (a : ι), ↑(((decompose 𝒜) x✝) a) ∈ I.toIdeal ↔ ↑(((decompose 𝒜) x✝) a) ∈ J.toIdeal
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : b < a<VAR>hc : c < 0<GOAL>c * a < c * b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d✝ : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : b < a<VAR>hc : c < 0<VAR>d : α<VAR>hcd : 0 = c + d<GOAL>c * a < c * b
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d✝ : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : b < a<VAR>hc : c < 0<VAR>d : α<VAR>hcd : 0 = c + d<GOAL>c * a + (d * b + d * a) < c * b + (d * b + d * a)
<VAR>l m r : List Char<VAR>p : Char → Bool<GOAL>ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r ({ str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len m } }.dropWhile p)
<VAR>l m r : List Char<VAR>p : Char → Bool<GOAL>ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) }, stopPos := { byteIdx := utf8Len l + utf8Len m } }
<VAR>l m r : List Char<VAR>p : Char → Bool<GOAL>utf8Len l + utf8Len m = utf8Len l + utf8Len (List.takeWhile p m) + utf8Len (List.dropWhile p m)
<VAR>R : Type u_1<VAR>inst✝³ : Monoid R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddMonoid X<VAR>inst✝ : DistribMulAction R X<VAR>r r' : X<VAR>s : ↥S<GOAL>r /ₒ s + r' /ₒ s = (r + r') /ₒ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hμ : IsFiniteMeasure μ<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>Summable fun x => (μ (f x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hμ : IsFiniteMeasure μ<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>∑' (x : ℕ), μ (f x) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hμ : IsFiniteMeasure μ<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>μ (⋃ i, f i) ≠ ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : TopologicalSpace α<VAR>f : ℝ → α<VAR>c : ℝ<VAR>hp : Periodic f c<VAR>hc : c ≠ 0<VAR>hf : Continuous f<GOAL>IsCompact (range f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : TopologicalSpace α<VAR>f : ℝ → α<VAR>c : ℝ<VAR>hp : Periodic f c<VAR>hc : c ≠ 0<VAR>hf : Continuous f<GOAL>IsCompact (f '' [[0, 0 + c]])
<VAR>α✝ β α : Type u<VAR>h : Fintype α<GOAL>∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
<VAR>α✝ β α : Type u<VAR>h : Fintype α<GOAL>∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) → ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i : β, f i)
<VAR>α✝ β α : Type u<VAR>h : Fintype α<GOAL>∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
<VAR>α✝ β α : Type u<VAR>h : Fintype α<GOAL>∀ (α : Type u) [inst : Fintype α], (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) → ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : Option α, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>y : Set β<GOAL>x ∩ f ⁻¹' maximals s (f '' x ∩ y) = maximals r (x ∩ f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>y : Set β<GOAL>∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (f a') (f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>n : ℤ<GOAL>a * a ^ n = a ^ (n + 1)
<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 : b ≠ a<GOAL>ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b
<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 : b ≠ a<VAR>hc : ContinuousWithinAt f s b<GOAL>ContinuousWithinAt (dslope f a) s b
<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 : b ≠ a<VAR>hc : ContinuousWithinAt f s b<GOAL>ContinuousWithinAt (slope f a) s b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>s : Set α<VAR>f : α →ᵤ[{s}] E<GOAL>LowerSemicontinuousAt (fun f => eVariationOn f s) f
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>s : Set α<VAR>f : α →ᵤ[{s}] E<GOAL>∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>s : Set α<VAR>f : α →ᵤ[{s}] E<VAR>this : Tendsto id (𝓝 f) (𝓝 f)<GOAL>∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>s : Set α<VAR>f : α →ᵤ[{s}] E<VAR>this : ∀ s_1 ∈ {s}, TendstoUniformlyOn (⇑(UniformOnFun.toFun {s}) ∘ id) ((UniformOnFun.toFun {s}) f) (𝓝 f) s_1<GOAL>∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>s : Set α<VAR>f : α →ᵤ[{s}] E<VAR>this : ∀ s_1 ∈ {s}, TendstoUniformlyOn (⇑(UniformOnFun.toFun {s}) ∘ id) ((UniformOnFun.toFun {s}) f) (𝓝 f) s_1<GOAL>∀ x ∈ s, TendstoUniformlyOn id f (𝓝 f) {x}
<VAR>ι : Type u_1<VAR>m : Multiset ℕ<VAR>k : ℕ<GOAL>m.prod.Coprime k ↔ ∀ n ∈ m, n.Coprime k
<VAR>ι : Type u_1<VAR>k : ℕ<VAR>a✝ : List ℕ<GOAL>(Multiset.prod ⟦a✝⟧).Coprime k ↔ ∀ n ∈ ⟦a✝⟧, n.Coprime k
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>f : E → F<GOAL>ContDiff 𝕜 (↑(n + 1)) f ↔ Differentiable 𝕜 f ∧ ∀ (y : E), ContDiff 𝕜 ↑n fun x => (fderiv 𝕜 f x) y
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β✝<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : Filter α<VAR>hf : f.HasBasis p s<VAR>β : ι → Type u_5<VAR>pg : (i : ι) → β i → Prop<VAR>sg : (i : ι) → β i → Set γ<VAR>g : Set α → Filter γ<VAR>hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)<VAR>gm : Monotone g<GOAL>(f.lift g).HasBasis (fun i => p i.fst ∧ pg i.fst i.snd) fun i => sg i.fst i.snd
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β✝<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>f : Filter α<VAR>hf : f.HasBasis p s<VAR>β : ι → Type u_5<VAR>pg : (i : ι) → β i → Prop<VAR>sg : (i : ι) → β i → Set γ<VAR>g : Set α → Filter γ<VAR>hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)<VAR>gm : Monotone g<VAR>t : Set γ<GOAL>(∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ t) ↔ ∃ i, (p i.fst ∧ pg i.fst i.snd) ∧ sg i.fst i.snd ⊆ t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : OrderedAddCommGroup α<VAR>s✝ t : Interval α<VAR>a : α<VAR>f : ι → Interval α<VAR>s : Finset ι<GOAL>(∑ i ∈ s, f i).length ≤ ∑ i ∈ s, (f i).length
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : OrderedAddCommGroup α<VAR>s✝ t : Interval α<VAR>a : α<VAR>f : ι → Interval α<VAR>s : Finset ι<GOAL>length 0 = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : OrderedAddCommGroup α<VAR>s✝ t : Interval α<VAR>a : α<VAR>f : ι → Interval α<VAR>s : Finset ι<GOAL>∀ (x y : Interval α), (x + y).length ≤ x.length + y.length
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε✝ δ✝ : 𝕜<VAR>u v : Finset α<VAR>ε δ : 𝕜<VAR>a b : α<VAR>ab : G.Adj a b<VAR>U : Finset α<VAR>UP : U ∈ P.parts<VAR>V : Finset α<VAR>VP : V ∈ P.parts<VAR>xU : a ∈ U<VAR>yV : b ∈ V<VAR>UV : U ≠ V<VAR>GUV : G.IsUniform ε U V<VAR>εUV : δ ≤ ↑(G.edgeDensity U V)<GOAL>G.Adj b a ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, b ∈ U ∧ a ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ ↑(G.edgeDensity U V)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε✝ δ✝ : 𝕜<VAR>u v : Finset α<VAR>ε δ : 𝕜<VAR>a b : α<VAR>ab : G.Adj a b<VAR>U : Finset α<VAR>UP : U ∈ P.parts<VAR>V : Finset α<VAR>VP : V ∈ P.parts<VAR>xU : a ∈ U<VAR>yV : b ∈ V<VAR>UV : U ≠ V<VAR>GUV : G.IsUniform ε U V<VAR>εUV : δ ≤ ↑(G.edgeDensity U V)<GOAL>δ ≤ ↑(G.edgeDensity V U)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : PartialOrder α<VAR>a b : α<VAR>hab : a < b<GOAL>minimals (fun x x_1 => x ≤ x_1) (Ico a b) = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>inst✝ : PartialOrder α<VAR>a b : α<VAR>hab : a < b<GOAL>minimals (fun x x_1 => x ≤ x_1) {x | x < b ∧ a ≤ x} = {a}
<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>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 hT) (c • f) = c • (setToL1 hT) 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>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1' 𝕜 hT h_smul) (c • f) = c • (setToL1' 𝕜 hT h_smul) f
<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>φ : K →+* ℂ<VAR>h : (mk φ).IsReal<GOAL>ComplexEmbedding.IsReal φ
<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>φ : K →+* ℂ<VAR>h : ¬ComplexEmbedding.IsReal φ<GOAL>¬(mk φ).IsReal
<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>φ : K →+* ℂ<VAR>h : ¬ComplexEmbedding.IsReal φ<GOAL>(mk φ).IsComplex
<VAR>α : Type u<VAR>β : Type v<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a b c d : R<VAR>h1 : a - b ∈ I<VAR>h2 : c - d ∈ I<GOAL>(a - b) * c + b * (c - d) ∈ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>a : α<VAR>b : β<VAR>s : Finset α<VAR>t : Finset β<GOAL>s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>i : ι × ι<VAR>a : ℬ i.1<VAR>b : 𝒜 i.2<GOAL>(gradedCommAux R 𝒜 ℬ) ((gradedCommAux R ℬ 𝒜) ((lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b))) = (lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) i) (a ⊗ₜ[R] b)
<VAR>α : Type u_1<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a * ↑u ∣ b ↔ a ∣ 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>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι →₀ 𝕜<VAR>i : ι<GOAL>⟪v i, (Finsupp.total ι E 𝕜 v) l⟫_𝕜 = l i
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>f : (j : ι) → i = j → α<GOAL>(∏ j : ι, if h : i = j then f j h else 1) = f i ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ l l' : List α<VAR>x✝ : α<VAR>h : x✝ ∈ {x | (zipWith swap l l').prod x ≠ x}<GOAL>x✝ ∈ ↑(l.toFinset ⊔ l'.toFinset)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) = (rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>∑ i ∈ range (n + 1), ↑p ^ i * wittMul p i ^ p ^ (n - i) = (bind₁ (wittStructureInt p (X 0 * X 1))) (wittPolynomial p ℤ n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>(rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (wittPolynomial p ℤ n)) (X 0 * X 1)
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a * b<GOAL>a * b = max a b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a * b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>ha' : ℵ₀ ≤ a<GOAL>a * b = max a b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a * b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hb' : ℵ₀ ≤ b<GOAL>a * b = max a b
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>V : (↑U).Opens<VAR>W : (↑(f ⁻¹ᵁ U)).Opens<VAR>e : W ≤ (f ∣_ U) ⁻¹ᵁ V<GOAL>Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a<GOAL>map (g ∘ f) ⟨s, al⟩ = map g (map f ⟨s, al⟩)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a<GOAL>↑(map (g ∘ f) ⟨s, al⟩) = ↑(map g (map f ⟨s, al⟩))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : Stream' (Option α)<VAR>al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a<GOAL>(fun o => Option.rec none (fun val => some (g (f val))) o) = (fun o => Option.rec none (fun val => some (g val)) o) ∘ fun o => Option.rec none (fun val => some (f val)) o
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.135729, u_1} C<VAR>inst✝ : HasShift C ℤ<VAR>T : (Triangle C)ᵒᵖ<GOAL>((Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫ (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).mor₃ ≫ (shiftFunctor C 1).map (Iso.refl (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫ (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₁).hom).op = ((Iso.refl (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫ (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₃).hom ≫ (Opposite.unop T).mor₃).op
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s✝ t : Set P<VAR>x : P<VAR>s : Set P<GOAL>intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>hp : p ≠ 0<GOAL>p.trailingDegree = ↑n ↔ p.natTrailingDegree = n
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.Ψ (2 * (↑m + 3)) * W.ψ₂ = W.Ψ (↑m + 2) ^ 2 * W.Ψ (↑m + 3) * W.Ψ (↑m + 5) - W.Ψ (↑m + 1) * W.Ψ (↑m + 3) * W.Ψ (↑m + 4) ^ 2
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>(C (W.preΨ' (2 * (m + 3))) * if Even (2 * (m + 3)) then W.ψ₂ else 1) * W.ψ₂ = (C (W.preΨ' (m + 2)) * if Even (m + 2) then W.ψ₂ else 1) ^ 2 * (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) * (C (W.preΨ' (m + 5)) * if Even (m + 5) then W.ψ₂ else 1) - (C (W.preΨ' (m + 1)) * if Even (m + 1) then W.ψ₂ else 1) * (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) * (C (W.preΨ' (m + 4)) * if Even (m + 4) then W.ψ₂ else 1) ^ 2