ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p > 0<VAR>hf : ¬f = 0<VAR>hf1 : (expand R p) f ≠ 0<GOAL>↑(f.natDegree * p) = ((expand R p) f).degree
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p > 0<VAR>hf : ¬f = 0<VAR>hf1 : (expand R p) f ≠ 0<GOAL>((expand R p) f).degree = ↑(f.natDegree * p)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p > 0<VAR>hf : ¬f = 0<VAR>hf1 : (expand R p) f ≠ 0<VAR>n : ℕ<VAR>hn : ↑(f.natDegree * p) < ↑n<GOAL>((expand R p) f).coeff n = 0
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q p : ℕ<VAR>f : R[X]<VAR>hp : p > 0<VAR>hf : ¬f = 0<VAR>hf1 : (expand R p) f ≠ 0<GOAL>↑(f.natDegree * p) ≤ ((expand R p) f).degree
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h0 : p.comp q = 0<GOAL>(p.comp q).natDegree ≤ p.natDegree * q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h0 : p.comp q = 0<GOAL>0 ≤ p.natDegree * q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h0 : ¬p.comp q = 0<VAR>n : ℕ<VAR>hn : n ∈ p.support<GOAL>↑(C (p.coeff n)).natDegree + n • ↑q.natDegree = ↑(n * q.natDegree)
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h0 : ¬p.comp q = 0<VAR>n : ℕ<VAR>hn : n ∈ p.support<GOAL>↑n * ↑q.natDegree = ↑(n * q.natDegree)
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J<VAR>π' : Prepartition I<GOAL>π' ≤ π.biUnion πi ↔ π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J<VAR>π' : Prepartition I<VAR>H : π' ≤ π.biUnion πi<VAR>J : Box ι<VAR>hJ : J ∈ π<GOAL>π'.restrict J ≤ πi J
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi✝ πi₁ πi₂ πi : (J : Box ι) → Prepartition J<VAR>π' : Prepartition I<GOAL>(π' ≤ π ∧ ∀ J ∈ π, π'.restrict J ≤ πi J) → π' ≤ π.biUnion πi
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>h : f.HasGenEigenvalue μ 0<GOAL>False
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<GOAL>Fintype.card G.ConnectedComponent = FiniteDimensional.finrank ℝ ↥(LinearMap.ker (toLin' (lapMatrix ℝ G)))
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<GOAL>(c.embedding (c.index j)) (c.invEmbedding j) = j
<VAR>n : ℕ<VAR>c : Composition n<VAR>j : Fin n<GOAL>↑((c.embedding (c.index j)) (c.invEmbedding j)) = ↑j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.Finite<GOAL>s.encard < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.Finite<GOAL>∀ {a : α} {s : Set α}, a ∉ s → s.Finite → s.encard < ⊤ → (insert a s).encard < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>h : s.Finite<VAR>a : α<VAR>t : Set α<VAR>hat : a ∉ t<VAR>a✝ : t.Finite<VAR>ht' : t.encard < ⊤<GOAL>(insert a t).encard < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t✝ : Set α<VAR>h : s.Finite<VAR>a : α<VAR>t : Set α<VAR>hat : a ∉ t<VAR>a✝ : t.Finite<VAR>ht' : t.encard < ⊤<GOAL>t.encard + 1 < ⊤
<GOAL>RespectsIso fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
<GOAL>∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsIntegral
<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>e : R ≃+* S<VAR>x : S<GOAL>e.toRingHom.IsIntegralElem x
<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>e : R ≃+* S<VAR>x : S<GOAL>e.toRingHom.IsIntegralElem (e (e.symm x))
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p q : R[X]<VAR>inst✝³ : CommRing T<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<GOAL>aroots 0 S = 0
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>h : ∀ (i : 𝒰.J), (Hom.app (𝒰.map i) U) s = 0<VAR>i : 𝒰.J<GOAL>(Hom.app (𝒰.map i) U) s = (Hom.app (𝒰.map i) U) 0
<VAR>X✝ Y Z : Scheme<VAR>𝒰✝ : X✝.OpenCover<VAR>f : X✝ ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (x : 𝒰✝.J), HasPullback (𝒰✝.map x ≫ f) g<VAR>X : Scheme<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>𝒰 : X.OpenCover<VAR>h : ∀ (i : 𝒰.J), (Hom.app (𝒰.map i) U) s = 0<VAR>i : 𝒰.J<GOAL>(Hom.app (𝒰.map i) U) s = 0
<VAR>m : ℕ<GOAL>schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹
<GOAL>schnirelmannDensity {n | n ≡ 1 [MOD 1]} = (↑1)⁻¹
<VAR>m : ℕ<VAR>hm : m ≠ 1<GOAL>schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹
<VAR>m : ℕ<VAR>hm : m ≠ 1<GOAL>schnirelmannDensity {n | n ≡ 1 [MOD m]} = schnirelmannDensity {n | n % m = 1}
<VAR>m : ℕ<VAR>hm : m ≠ 1<GOAL>{n | n ≡ 1 [MOD m]} = {n | n % m = 1}
<VAR>m : ℕ<VAR>hm : m ≠ 1<VAR>n : ℕ<GOAL>n ∈ {n | n ≡ 1 [MOD m]} ↔ n ∈ {n | n % m = 1}
<VAR>S : Type u<VAR>inst✝¹ : Semiring S<VAR>T : Type v<VAR>inst✝ : Semiring T<VAR>f : S →+* T<VAR>n : ℕ<VAR>t : T<GOAL>eval t (ascPochhammer T n) = eval₂ f t (ascPochhammer S n)
<VAR>S : Type u<VAR>inst✝¹ : Semiring S<VAR>T : Type v<VAR>inst✝ : Semiring T<VAR>f : S →+* T<VAR>n : ℕ<VAR>t : T<GOAL>eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)
<VAR>α✝ : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝¹ : NonUnitalNonAssocSemiring α✝<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<VAR>A : m' → Fin n.succ → α<VAR>x : α<VAR>v : Fin n → α<VAR>i : m'<GOAL>(of A *ᵥ vecCons x v) i = (x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v) i
<VAR>α β : Type u<VAR>inst✝ : Finite α<VAR>s : Set α<VAR>t : Set β<VAR>h1 : #α = #β<VAR>h : #↑s = #↑t<GOAL>#↑sᶜ = #↑tᶜ
<VAR>α β : Type u<VAR>inst✝ : Finite α<VAR>s : Set α<VAR>t : Set β<VAR>h1 : #α = #β<VAR>h : #↑s = #↑t<GOAL>lift.{u, u} #↑sᶜ = lift.{u, u} #↑tᶜ
<VAR>θ ψ : Angle<VAR>hs : θ.sign = ψ.sign<VAR>hr : |θ.toReal| = |ψ.toReal|<GOAL>θ = ψ
<VAR>θ ψ : Angle<VAR>hs : θ.sign = ψ.sign<VAR>hr : θ.toReal = ψ.toReal ∨ θ.toReal = -ψ.toReal<GOAL>θ = ψ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>s : Set α<VAR>inst✝ : NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<GOAL>↑↑(indicatorConstLp 2 hs hμs x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>s : Set α<VAR>inst✝ : NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<GOAL>(s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>s : Set α<VAR>inst✝ : NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<VAR>h_compLp : ∀ᵐ (a : α) ∂μ, ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) a = (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)<GOAL>(s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>s : Set α<VAR>inst✝ : NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<VAR>h_compLp : ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)<GOAL>(s.indicator fun x_1 => x) =ᶠ[ae μ] ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>s : Set α<VAR>inst✝ : NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<VAR>h_compLp : ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)<GOAL>(s.indicator fun x_1 => x) =ᶠ[ae μ] fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>s : Set α<VAR>inst✝ : NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<VAR>h_compLp : ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)<VAR>y : α<VAR>hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y<GOAL>s.indicator (fun x_1 => x) y = (fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)) y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>s : Set α<VAR>inst✝ : NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<VAR>h_compLp : ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)<VAR>y : α<VAR>hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y<GOAL>s.indicator (fun x_1 => x) y = (ContinuousLinearMap.toSpanSingleton ℝ x) (s.indicator (fun x => 1) y)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>s : Set α<VAR>inst✝ : NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<VAR>h_compLp : ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᶠ[ae μ] fun a => (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)<VAR>y : α<VAR>hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x => 1) y<GOAL>s.indicator (fun x_1 => x) y = s.indicator (fun x => 1) y • x
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>x : α<VAR>xs : x ∈ s<GOAL>hausdorffEdist s ∅ = ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>x : α<VAR>xs : x ∈ s<VAR>this : infEdist x ∅ ≤ hausdorffEdist s ∅<GOAL>hausdorffEdist s ∅ = ⊤
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>s : Set G<VAR>inst✝ : Group G<VAR>t : Set G<VAR>ht : IsNormalSubgroup t<VAR>a : G<VAR>h : a ∈ t<VAR>x : G<VAR>hc : x ∈ conjugatesOf a<GOAL>x ∈ t
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c✝ : G<VAR>s : Set G<VAR>inst✝ : Group G<VAR>t : Set G<VAR>ht : IsNormalSubgroup t<VAR>a : G<VAR>h : a ∈ t<VAR>x : G<VAR>hc : x ∈ conjugatesOf a<VAR>c : G<VAR>w : c * a * c⁻¹ = x<GOAL>x ∈ t
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c✝ : G<VAR>s : Set G<VAR>inst✝ : Group G<VAR>t : Set G<VAR>ht : IsNormalSubgroup t<VAR>a : G<VAR>h : a ∈ t<VAR>x : G<VAR>hc : x ∈ conjugatesOf a<VAR>c : G<VAR>w : c * a * c⁻¹ = x<VAR>H : c * a * c⁻¹ ∈ t<GOAL>x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>f✝ g : α → β<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>f : α → β<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>f✝ g : α → β<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>f : α → β<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>h✝ : SecondCountableTopology α<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>f✝ g : α → β<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>h : SecondCountableTopologyEither α β<VAR>f : α → β<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>h✝ : SecondCountableTopology β<GOAL>StronglyMeasurable f
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : y ≠ 0<GOAL>‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : UpperSet α<VAR>a : α<VAR>f : ι → UpperSet α<GOAL>↑(⨅ i, f i).compl = ↑(⨅ i, (f i).compl)
<VAR>x : ℂ<GOAL>HasStrictDerivAt sinh (cosh x) x
<VAR>x : ℂ<GOAL>HasStrictDerivAt sinh ((cexp x + cexp (-x)) * 2⁻¹) x
<VAR>x : ℂ<GOAL>(cexp x + cexp (-x)) * 2⁻¹ = (cexp x - cexp (-id x) * -1) * 2⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : TendstoInMeasure μ f atTop g<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>ns : ℕ → ℕ<VAR>hns : Tendsto ns atTop atTop<GOAL>∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hut : UnifTight f p μ<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>ns : ℕ → ℕ<VAR>hns : Tendsto ns atTop atTop<VAR>ms : ℕ → ℕ<VAR>left✝ : StrictMono ms<VAR>hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns (ms i)) x) atTop (𝓝 (g x))<GOAL>∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
<VAR>xl xr : Type u<VAR>x x' : PGame<GOAL>(-x).insertLeft (-x') = -x.insertRight x'
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>v : n → R<VAR>A : Matrix n n R<VAR>i✝ j✝ : n<GOAL>of (fun i j => v j * A i j) i✝ j✝ = (A * diagonal v) i✝ j✝
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>v : n → R<VAR>A : Matrix n n R<GOAL>(A * diagonal v).det = (∏ i : n, v i) * A.det
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>hπ : IsStoppingTime f π<VAR>s : Set Ω<GOAL>MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ ⊥<GOAL>(algebraMap R₁ K) ↑I.den ∈ I⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ ⊥<GOAL>∀ y ∈ I, (algebraMap R₁ K) ↑I.den * y ∈ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ ⊥<VAR>i : K<VAR>hi : i ∈ I<GOAL>(algebraMap R₁ K) ↑I.den * i ∈ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ ⊥<VAR>i : K<VAR>hi : i ∈ I<GOAL>↑I.den • i ∈ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ ⊥<VAR>i : K<VAR>hi : i ∈ I<GOAL>Submodule.map (Algebra.linearMap R₁ K) I.num ≤ 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>hI : I ≠ ⊥<VAR>i : K<VAR>hi : i ∈ I<GOAL>Submodule.map (Algebra.linearMap R₁ K) 1 ≤ 1
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ {p | p.2 = x → p.1 ∈ s} ∈ 𝓤 α
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>{p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α ↔ {p | p.2 = x → p.1 ∈ s} ∈ Prod.swap <$> 𝓤 α
<VAR>a b : ℝ<GOAL>frontier {z | a ≤ z.re ∧ z.im ≤ b} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ z.im ≤ b}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<GOAL>∀ (a : List (Set α)), ⇑f '' Multiset.prod ⟦a⟧ = (Multiset.map (fun s => ⇑f '' s) ⟦a⟧).prod
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>m : α → β<VAR>f : Filter α<VAR>s : Set β<GOAL>sᶜ ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>hr : r ≠ 0<VAR>hv : v.asIdeal = Ideal.span {r}<GOAL>v.intValuation r = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>r : R<VAR>hr : r ≠ 0<VAR>hv : v.asIdeal = Ideal.span {r}<GOAL>Irreducible (Associates.mk v.asIdeal)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>x : ℝ<VAR>hw : ∀ i ∈ s, 0 ≤ w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 ≤ z i<VAR>hx : ∀ i ∈ s, w i ≠ 0 → z i = x<GOAL>∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<GOAL>(⋂₀ S)ᶜ = ⋃₀ (compl '' S)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<GOAL>StrictConvexOn ℝ s f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>0 < a * b * φ ‖x - y‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : 0 < ‖x - y‖<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>0 < a * b * φ ‖x - y‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : 0 < ‖x - y‖<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>this : 0 < φ ‖x - y‖<GOAL>0 < a * b * φ ‖x - y‖
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig α N τ<VAR>i : Fin N.succ<VAR>h : 1 ≤ τ<GOAL>a.r (last N) ≤ τ * a.r i
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : SatelliteConfig α N τ<VAR>i : Fin N.succ<VAR>h : 1 ≤ τ<VAR>H : i < last N<GOAL>a.r (last N) ≤ τ * a.r i