ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : TopologicalSpace Y<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T2Space X<VAR>hf : LocallyIntegrable f μ<VAR>g : X → ℝ<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>K : Set X := tsupport g<VAR>hK : IsCompact K<VAR>this : (K.indicator fun x => g x • f x) = fun x => g x • f x<GOAL>Memℒp g ⊤ μ
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : SMulCommClass S R M<VAR>inst✝¹ : SMul R S<VAR>inst✝ : IsScalarTower R S M<VAR>x : R<VAR>h : IsUnit ((algebraMap R (End S M)) x)<VAR>m m' : M<VAR>H : m = x • m'<GOAL>↑h.unit⁻¹ (x • m') = m'
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : SMulCommClass S R M<VAR>inst✝¹ : SMul R S<VAR>inst✝ : IsScalarTower R S M<VAR>x : R<VAR>h : IsUnit ((algebraMap R (End S M)) x)<VAR>m m' : M<VAR>H : m = x • m'<GOAL>↑h.unit (↑h.unit⁻¹ (x • m')) = ↑h.unit m'
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : SMulCommClass S R M<VAR>inst✝¹ : SMul R S<VAR>inst✝ : IsScalarTower R S M<VAR>x : R<VAR>h : IsUnit ((algebraMap R (End S M)) x)<VAR>m m' : M<VAR>H : m = x • m'<GOAL>x • m' = ↑h.unit m'
<VAR>m n✝ : ℕ<VAR>inst✝ : NeZero (n✝ + 1 + 1)<VAR>k : Fin (n✝ + 1 + 1)<GOAL>k * 1 = k
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<GOAL>∑ m ∈ range (j - n), 1 / ↑(m + n).factorial ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<GOAL>∑ x ∈ range (j - n), (↑(x + n).factorial)⁻¹ ≤ ∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<VAR>i✝ : ℕ<VAR>a✝ : i✝ ∈ range (j - n)<GOAL>↑n.factorial * ↑n.succ ^ i✝ ≤ ↑(i✝ + n).factorial
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<VAR>i✝ : ℕ<VAR>a✝ : i✝ ∈ range (j - n)<GOAL>n.factorial * n.succ ^ i✝ ≤ (n + i✝).factorial
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<GOAL>∑ m ∈ range (j - n), (↑n.factorial * ↑n.succ ^ m)⁻¹ = (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<GOAL>(↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m = (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<VAR>h₁ : ↑n.succ ≠ 1<GOAL>(↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m = (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>n j : ℕ<VAR>hn : 0 < n<VAR>h₁ : ↑n.succ ≠ 1<VAR>h₂ : ↑n.succ ≠ 0<VAR>h₃ : ↑n.factorial * ↑n ≠ 0<VAR>h₄ : ↑n.succ - 1 = ↑n<GOAL>(↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m = (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>X Y : Type u<VAR>x₀ : X<VAR>f : X → Y<VAR>g : Y → F (α ::: X)<GOAL>Cofix.corec (g ∘ f) x₀ = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x₀)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>X Y : Type u<VAR>x₀ : X<VAR>f : X → Y<VAR>g : Y → F (α ::: X)<VAR>R : Cofix F α → Cofix F α → Prop := fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)<VAR>a b : Cofix F α<VAR>x : X<VAR>Ha : a = Cofix.corec (g ∘ f) x<VAR>Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)<GOAL>LiftR' (α.RelLast' R) a.dest b.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>X Y : Type u<VAR>x₀ : X<VAR>f : X → Y<VAR>g : Y → F (α ::: X)<VAR>R : Cofix F α → Cofix F α → Prop := fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)<VAR>a b : Cofix F α<VAR>x : X<VAR>Ha : a = Cofix.corec (g ∘ f) x<VAR>Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)<GOAL>LiftR' (α.RelLast' R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x)) ((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g)) <$$> (TypeVec.id ::: f) <$$> g (f x))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>X Y : Type u<VAR>x₀ : X<VAR>f : X → Y<VAR>g : Y → F (α ::: X)<VAR>R : Cofix F α → Cofix F α → Prop := fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)<VAR>a b : Cofix F α<VAR>x : X<VAR>Ha : a = Cofix.corec (g ∘ f) x<VAR>Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)<GOAL>LiftR' (α.RelLast' R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x)) ((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) ∘ f) <$$> g (f x))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>X Y : Type u<VAR>x₀ : X<VAR>f : X → Y<VAR>g : Y → F (α ::: X)<VAR>R : Cofix F α → Cofix F α → Prop := fun a b => ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)<VAR>a b : Cofix F α<VAR>x : X<VAR>Ha : a = Cofix.corec (g ∘ f) x<VAR>Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)<GOAL>∀ (x : X), R (Cofix.corec (g ∘ f) x) ((Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) ∘ f) x)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e✝ : Basis ι R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : N →ₗ[R] M<VAR>e e' : M ≃ₗ[R] N<GOAL>Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e✝ : Basis ι R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : N →ₗ[R] M<VAR>e e' : M ≃ₗ[R] N<GOAL>∀ (x : M), (f ∘ₗ ↑e) x = (f ∘ₗ ↑e') ((e ≪≫ₗ e'.symm) x)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e✝ : Basis ι R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : N →ₗ[R] M<VAR>e e' : M ≃ₗ[R] N<VAR>x : M<GOAL>(f ∘ₗ ↑e) x = (f ∘ₗ ↑e') ((e ≪≫ₗ e'.symm) x)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : 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<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : ↥(span R (range ⇑b))<VAR>i : ι<GOAL>(algebraMap R S) (((restrictScalars R b).repr m) i) = (b.repr ↑m) i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : 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<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : ↥(span R (range ⇑b))<VAR>i : ι<GOAL>Finsupp.mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr = (↑R ↑b.repr).domRestrict (span R (range ⇑b))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : 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<VAR>V' : Type u_9<VAR>S : Type u_10<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Nontrivial S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsScalarTower R S M<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>b : Basis ι S M<VAR>m : ↥(span R (range ⇑b))<VAR>i x✝ : ι<GOAL>(Finsupp.mapRange.linearMap (Algebra.linearMap R S) ∘ₗ ↑(restrictScalars R b).repr) ((restrictScalars R b) x✝) = ((↑R ↑b.repr).domRestrict (span R (range ⇑b))) ((restrictScalars R b) x✝)
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>√x = √y ↔ x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>s : Set X<VAR>f : ↥(Lp E p μ)<GOAL>‖Memℒp.toLp ↑↑f ⋯‖ ≤ ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>s : Set X<VAR>f : ↥(Lp E p μ)<GOAL>eLpNorm (↑↑(Memℒp.toLp ↑↑f ⋯)) p (μ.restrict s) ≤ eLpNorm (↑↑f) p μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>s : Set X<VAR>f : ↥(Lp E p μ)<GOAL>eLpNorm (↑↑(Memℒp.toLp ↑↑f ⋯)) p (μ.restrict s) = eLpNorm (↑↑f) p (μ.restrict s)
<VAR>α : Type u<VAR>l✝ l' l : List α<GOAL>l.cyclicPermutations.head ⋯ = l
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>h : 0 < l.cyclicPermutations.length<GOAL>l.cyclicPermutations.head ⋯ = l
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>x : A<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((algebraMap A S) x) = (algebraMap A S') x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>ht : t ∈ 𝓝 x<GOAL>MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x
<VAR>y : ℝ<GOAL>Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
<VAR>y : ℝ<VAR>this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))<GOAL>Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
<VAR>y : ℝ<VAR>this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))<GOAL>Tendsto (rexp ∘ fun x => log (x + y) - log x) atTop (𝓝 (1 + 0))
<VAR>y : ℝ<VAR>this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))<GOAL>(fun x => 1 + y / x) =ᶠ[atTop] rexp ∘ fun x => log (x + y) - log x
<VAR>y : ℝ<VAR>this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))<VAR>x : ℝ<VAR>hx₀ : 0 < x<VAR>hxy : -y < x<GOAL>1 + y / x = (rexp ∘ fun x => log (x + y) - log x) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>c : 𝕜<VAR>f : ↥(Lp F p μ)<VAR>s : Set X<GOAL>↑↑(Memℒp.toLp ↑↑(c • f) ⋯) =ᶠ[ae (μ.restrict s)] ↑↑(c • Memℒp.toLp ↑↑f ⋯)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>c : 𝕜<VAR>f : ↥(Lp F p μ)<VAR>s : Set X<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(Memℒp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • Memℒp.toLp ↑↑f ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>c : 𝕜<VAR>f : ↥(Lp F p μ)<VAR>s : Set X<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ↑↑(Memℒp.toLp ↑↑f ⋯) x = ↑↑f x → ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(Memℒp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • Memℒp.toLp ↑↑f ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>c : 𝕜<VAR>f : ↥(Lp F p μ)<VAR>s : Set X<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ↑↑(Memℒp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • f) x → ↑↑(Memℒp.toLp ↑↑f ⋯) x = ↑↑f x → ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(Memℒp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • Memℒp.toLp ↑↑f ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>c : 𝕜<VAR>f : ↥(Lp F p μ)<VAR>s : Set X<VAR>x : X<VAR>hx1 : ↑↑(c • Memℒp.toLp ↑↑f ⋯) x = (c • ↑↑(Memℒp.toLp ↑↑f ⋯)) x<VAR>hx2 : ↑↑(Memℒp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • f) x<VAR>hx3 : ↑↑(Memℒp.toLp ↑↑f ⋯) x = ↑↑f x<VAR>hx4 : ↑↑(c • f) x = (c • ↑↑f) x<GOAL>↑↑(Memℒp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • Memℒp.toLp ↑↑f ⋯) x
<VAR>k n m : ℕ<GOAL>(k * n).dist (k * m) = k * n.dist m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>inst✝ : DenselyOrdered α<GOAL>Iio a ⊆ Iic b ↔ a ≤ b
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Ico ↑a ⊤ = Ici a
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ 𝒰.gluedCoverT' y z x ≫ 𝒰.gluedCoverT' z x y = 𝟙 (pullback (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)))
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ 𝒰.gluedCoverT' y z x ≫ 𝒰.gluedCoverT' z x y ≫ pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) = pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z))
<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 F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : AddCommGroup P<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : Module R Q<VAR>inst✝⁴ : Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Free R N<VAR>inst✝¹ : Module.Finite R N<VAR>inst✝ : Nontrivial R<GOAL>↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor R M P Q
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>↑(legendreSym p a) = ↑a ^ (p / 2)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hc : ringChar (ZMod p) = 2<GOAL>↑(legendreSym p a) = ↑a ^ (p / 2)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>hc : ringChar (ZMod p) ≠ 2<GOAL>↑(legendreSym p a) = ↑a ^ (p / 2)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝⁴ : CommSemiring R<VAR>A : Type v<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>S✝ T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>p : Submodule R S<VAR>y : S<VAR>hx : x ∈ nonZeroDivisors S<GOAL>(∃ a ∈ ↑p, (DistribMulAction.toLinearMap R S x) a = x * y) ↔ y ∈ p
<VAR>t : ℝ<VAR>ht : |t| ≤ 1<VAR>x : ℝ<GOAL>rexp (t * x) ≤ cosh x + t * sinh x
<VAR>t : ℝ<VAR>ht : -1 ≤ t ∧ t ≤ 1<VAR>x : ℝ<GOAL>rexp (t * x) ≤ cosh x + t * sinh x
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : DivisionSemiring R<VAR>q : ℚ≥0<VAR>f : R[X]<GOAL>q • f = C ↑q * f
<VAR>z w : ℂ<GOAL>cos z = w ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0
<VAR>z w : ℂ<GOAL>cos z - w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0
<VAR>z w : ℂ<GOAL>cexp (z * I) * cexp (z * I) + 1 - cexp (z * I) * 2 * w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0
<VAR>z w : ℂ<GOAL>cexp (z * I) * cexp (z * I) + 1 - cexp (z * I) * 2 * w = cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1
<VAR>N : ℕ<VAR>x✝ : SL(2, ℤ)<GOAL>x✝ ∈ Gamma 0 ↔ x✝ ∈ ⊥
<VAR>N : ℕ<VAR>x✝ : SL(2, ℤ)<GOAL>↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 ↔ x✝ = 1
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>P : ℕ → ℕ → Prop<VAR>ha : ∀ (a : ℕ), P (a + 1) (a + 1)<VAR>hb : ∀ (b : ℕ), P 0 (b + 1)<VAR>hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)<VAR>a b : ℕ<VAR>h : a + 1 < b + 1<GOAL>P (a + 1) (b + 1)
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>P : ℕ → ℕ → Prop<VAR>ha : ∀ (a : ℕ), P (a + 1) (a + 1)<VAR>hb : ∀ (b : ℕ), P 0 (b + 1)<VAR>hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)<VAR>a b : ℕ<VAR>h : a + 1 < b + 1<GOAL>P (a + 1) b
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>P : ℕ → ℕ → Prop<VAR>ha : ∀ (a : ℕ), P (a + 1) (a + 1)<VAR>hb : ∀ (b : ℕ), P 0 (b + 1)<VAR>hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)<VAR>a b : ℕ<VAR>h : a + 1 < b + 1<GOAL>P a (b + 1)
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>P : ℕ → ℕ → Prop<VAR>ha : ∀ (a : ℕ), P (a + 1) (a + 1)<VAR>hb : ∀ (b : ℕ), P 0 (b + 1)<VAR>hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)<VAR>a b : ℕ<VAR>h : a + 1 < b + 1<VAR>x✝ : a + (b + 1) < a + 1 + (b + 1)<GOAL>a < b + 1
<VAR>R✝ : Type u_1<VAR>inst✝² : Mul R✝<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>inst✝ : ExistsAddOfLE R<VAR>S : R<VAR>pS : isSumSq S<GOAL>0 ≤ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝⁴ : NonUnitalSemiring α<VAR>inst✝³ : StarRing α<VAR>inst✝² : NonUnitalSemiring β<VAR>inst✝¹ : StarRing β<VAR>inst✝ : Fintype m<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>hA : A.IsHermitian<GOAL>(Bᴴ * A * B).IsHermitian
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.222391, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : S.f ≫ k = 0<VAR>inst✝¹ : S.HasRightHomology<VAR>φ : S₁ ⟶ S<VAR>inst✝ : S₁.HasRightHomology<GOAL>S₁.f ≫ φ.τ₂ ≫ k = 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : S.f ≫ k = 0<VAR>inst✝¹ : S.HasRightHomology<VAR>φ : S₁ ⟶ S<VAR>inst✝ : S₁.HasRightHomology<GOAL>opcyclesMap φ ≫ S.descOpcycles k hk = S₁.descOpcycles (φ.τ₂ ≫ k) ⋯
<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>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>a : α<GOAL>ContinuousWithinAt f {a}ᶜ a ↔ ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>c d : β<VAR>h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d<VAR>this : Decidable (Finite a b) := Classical.dec (Finite a b)<VAR>hab : Finite a b<GOAL>multiplicity a b ≤ multiplicity c d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>c d : β<VAR>h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d<VAR>this : Decidable (Finite a b) := Classical.dec (Finite a b)<VAR>hab : Finite a b<GOAL>↑((multiplicity a b).get ⋯) ≤ multiplicity c d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>c d : β<VAR>h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d<VAR>this : Decidable (Finite a b) := Classical.dec (Finite a b)<VAR>hab : ¬Finite a b<GOAL>multiplicity a b ≤ multiplicity c d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>c d : β<VAR>h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d<VAR>this✝ : Decidable (Finite a b) := Classical.dec (Finite a b)<VAR>hab : ¬Finite a b<VAR>this : ∀ (n : ℕ), c ^ n ∣ d<GOAL>multiplicity a b ≤ multiplicity c d
<VAR>α β : Type u<VAR>c : Cardinal.{?u.255346}<VAR>a : Cardinal.{u_1}<VAR>h : a ≠ 0<GOAL>0 ^< a = 1
<VAR>α β : Type u<VAR>c : Cardinal.{?u.255346}<VAR>a : Cardinal.{u_1}<VAR>h : a ≠ 0<GOAL>1 ≤ 0 ^< a
<VAR>α β : Type u<VAR>c : Cardinal.{?u.255346}<VAR>a : Cardinal.{u_1}<VAR>h : a ≠ 0<GOAL>?m.255561 ^ 0 ≤ 0 ^< a
<VAR>α β : Type u<VAR>c : Cardinal.{?u.255346}<VAR>a : Cardinal.{u_1}<VAR>h : a ≠ 0<GOAL>Cardinal.{u_1}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>Tendsto (fun x => (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔ Tendsto (fun x => (s.restrict f x.1, s.restrict f x.2)) (𝓤 ↑s) (𝓤 β)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>Tendsto ((fun x => (f x.1, f x.2)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔ Tendsto (fun x => (s.restrict f x.1, s.restrict f x.2)) (𝓤 ↑s) (𝓤 β)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E✝<VAR>inst✝⁷ : NormedSpace 𝕜 E✝<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>x✝ y : E✝<VAR>s✝ t : Set E✝<VAR>ι : Type u_5<VAR>inst✝² : Finite ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)<GOAL>UniqueDiffWithinAt 𝕜 (univ.pi s) x