ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<VAR>hC₀ : 0 < C<VAR>this : 0 < (rexp 1 * C)⁻¹<GOAL>∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<VAR>hC₀ : 0 < C<VAR>this : 0 < (rexp 1 * C)⁻¹<VAR>N : ℕ<VAR>hN : ∀ k ≥ N, ↑k ^ n / rexp 1 ^ k < (rexp 1 * C)⁻¹<GOAL>∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<VAR>hC₀ : 0 < C<VAR>this : 0 < (rexp 1 * C)⁻¹<VAR>N : ℕ<VAR>hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)<GOAL>∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
<VAR>α : Type u_1<VAR>x✝ y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<VAR>hC₀ : 0 < C<VAR>this : 0 < (rexp 1 * C)⁻¹<VAR>N : ℕ<VAR>hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)<VAR>x : ℝ<VAR>hx : x ∈ Set.Ioi ↑N<GOAL>rexp x / x ^ n ∈ Set.Ici C
<VAR>α : Type u_1<VAR>x✝ y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<VAR>hC₀ : 0 < C<VAR>this : 0 < (rexp 1 * C)⁻¹<VAR>N : ℕ<VAR>hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)<VAR>x : ℝ<VAR>hx : ↑N < x<GOAL>rexp x / x ^ n ∈ Set.Ici C
<VAR>α : Type u_1<VAR>x✝ y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<VAR>hC₀ : 0 < C<VAR>this : 0 < (rexp 1 * C)⁻¹<VAR>N : ℕ<VAR>hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)<VAR>x : ℝ<VAR>hx : ↑N < x<VAR>hx₀ : 0 < x<GOAL>rexp x / x ^ n ∈ Set.Ici C
<VAR>α : Type u_1<VAR>x✝ y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<VAR>hC₀ : 0 < C<VAR>this : 0 < (rexp 1 * C)⁻¹<VAR>N : ℕ<VAR>hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)<VAR>x : ℝ<VAR>hx : ↑N < x<VAR>hx₀ : 0 < x<GOAL>x ^ n ≤ rexp x / C
<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>asympBound g a b =O[atTop] T
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' = K.d₂ c₁₂ i₁ i₂ i₁₂'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>p ∉ support R M ↔ ∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>(∀ (m : M), ∃ r ∈ p.asIdeal.primeCompl, r • m = 0) ↔ ∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j k : ι<VAR>inst✝ : K.HasHomology i<GOAL>K.fromOpcycles i j ≫ K.d j k = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>b c d : WithTop α<VAR>x y : α<VAR>inst✝ : IsRightCancelAdd α<VAR>a : α<GOAL>b + ↑a = c + ↑a ↔ b = c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>c d : WithTop α<VAR>x y : α<VAR>inst✝ : IsRightCancelAdd α<VAR>a : α<GOAL>⊤ + ↑a = c + ↑a ↔ ⊤ = c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>b c d : WithTop α<VAR>x y : α<VAR>inst✝ : IsRightCancelAdd α<VAR>a : α<VAR>hb : b ≠ ⊤<GOAL>b + ↑a = c + ↑a ↔ b = c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>c d : WithTop α<VAR>x y : α<VAR>inst✝ : IsRightCancelAdd α<VAR>a b : α<GOAL>↑b + ↑a = c + ↑a ↔ ↑b = c
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪o.rightAngleRotation x, y⟫_ℝ = (o.areaForm x) y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪(LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) x, y⟫_ℝ = (o.areaForm x) y
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>cd : Fin 2 → R<VAR>b₀ a : R<VAR>gcd_eqn : b₀ * cd 0 + a * cd 1 = 1<VAR>A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]<GOAL>cd ∈ (fun g => ↑g 1) '' Set.univ
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>cd : Fin 2 → R<VAR>b₀ a : R<VAR>gcd_eqn : b₀ * cd 0 + a * cd 1 = 1<VAR>A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]<VAR>det_A_1 : A.det = 1<GOAL>cd ∈ (fun g => ↑g 1) '' Set.univ
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>cd : Fin 2 → R<VAR>b₀ a : R<VAR>gcd_eqn : b₀ * cd 0 + a * cd 1 = 1<VAR>A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]<VAR>det_A_1 : A.det = 1<GOAL>(fun g => ↑g 1) ⟨A, det_A_1⟩ = cd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : ℕ → ℕ →. α<VAR>h : Partrec (Nat.unpaired f)<GOAL>Partrec₂ f
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<GOAL>op a ∈ s.op ↔ a ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>ι' : Type u_8<VAR>φ : ι' → ι<GOAL>induced (fun f j => f (φ j)) topologicalSpace = ⨅ i', induced (eval (φ i')) (T (φ i'))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a b c : α<GOAL>Codisjoint a (￢￢b) ↔ Codisjoint a b
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x y L : R<GOAL>(map W f).toAffine.addPolynomial (f x) (f y) (f L) = Polynomial.map f (W.addPolynomial x y L)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x y L : R<GOAL>eval₂ (mapRingHom f) (C (f L) * (X - C (f x)) + C (f y)) W.polynomial = eval₂ (mapRingHom f) ((mapRingHom f) (C L * (X - C x) + C y)) W.polynomial
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ : Filter α<VAR>s : Set α<VAR>a : α<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Tendsto f (↑g) l₂
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedSemiring α<VAR>inst✝³ : FloorSemiring α<VAR>a✝ : α<VAR>n✝ : ℕ<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ExistsAddOfLE α<VAR>a : α<VAR>n : ℕ<GOAL>⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedSemiring α<VAR>inst✝³ : FloorSemiring α<VAR>a✝ : α<VAR>n✝ : ℕ<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ExistsAddOfLE α<VAR>a : α<VAR>n : ℕ<VAR>ha : a ≤ 0<GOAL>⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedSemiring α<VAR>inst✝³ : FloorSemiring α<VAR>a✝ : α<VAR>n✝ : ℕ<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ExistsAddOfLE α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedSemiring α<VAR>inst✝³ : FloorSemiring α<VAR>a✝ : α<VAR>n✝ : ℕ<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ExistsAddOfLE α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>h : a ≤ ↑n<GOAL>⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedSemiring α<VAR>inst✝³ : FloorSemiring α<VAR>a✝ : α<VAR>n✝ : ℕ<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ExistsAddOfLE α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>h : ↑n ≤ a<GOAL>⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>h : ¬IsUnit A.det<GOAL>A⁻¹ = 0
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x p : ℝ<VAR>hp : 1 < p<GOAL>HasDerivAt (fun x => |x| ^ p) (p * |x| ^ (p - 2) * x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>hs : DirSupInacc s<VAR>ht : DirSupInacc t<GOAL>DirSupInacc (s ∪ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>s t : Set α<VAR>hs : DirSupInacc s<VAR>ht : DirSupInacc t<GOAL>DirSupClosed (sᶜ ∩ tᶜ)
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>hT : FinMeasAdditive μ T<VAR>hT' : FinMeasAdditive μ T'<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<GOAL>(T + T') (s ∪ t) = (T + T') s + (T + T') t
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T T' : Set α → β<VAR>hT : FinMeasAdditive μ T<VAR>hT' : FinMeasAdditive μ T'<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<GOAL>T s + T t + (T' s + T' t) = T s + T' s + (T t + T' t)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝¹ : Subsingleton ι<VAR>i : ι<VAR>f : M₂ →ₗ[R] M₃<VAR>inst✝ : DecidableEq ι<VAR>m✝ : ι → M₂<VAR>i✝ : ι<VAR>x✝ y✝ : M₂<GOAL>(fun x => f (x i)) (update m✝ i✝ (x✝ + y✝)) = (fun x => f (x i)) (update m✝ i✝ x✝) + (fun x => f (x i)) (update m✝ i✝ y✝)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>inst✝⁷ : AddCommMonoid M'<VAR>inst✝⁶ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁵ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝¹ : Subsingleton ι<VAR>i : ι<VAR>f : M₂ →ₗ[R] M₃<VAR>inst✝ : DecidableEq ι<VAR>m✝ : ι → M₂<VAR>i✝ : ι<VAR>c✝ : R<VAR>x✝ : M₂<GOAL>(fun x => f (x i)) (update m✝ i✝ (c✝ • x✝)) = c✝ • (fun x => f (x i)) (update m✝ i✝ x✝)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>f : MultilinearMap R (fun x => M₂) M₃<VAR>x y : M₂<GOAL>(fun x => f fun x_1 => x) (x + y) = (fun x => f fun x_1 => x) x + (fun x => f fun x_1 => x) y
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>f : MultilinearMap R (fun x => M₂) M₃<VAR>c : R<VAR>x : M₂<GOAL>{ toFun := fun x => f fun x_1 => x, map_add' := ⋯ }.toFun (c • x) = (RingHom.id R) c • { toFun := fun x => f fun x_1 => x, map_add' := ⋯ }.toFun x
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>f : MultilinearMap R (fun x => M₂) M₃<VAR>x : ι → M₂<GOAL>((fun f => { toFun := fun x => f (x i), map_add' := ⋯, map_smul' := ⋯ }) ((fun f => { toFun := fun x => f fun x_1 => x, map_add' := ⋯, map_smul' := ⋯ }) f)) x = f x
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Subsingleton ι<VAR>i : ι<VAR>f : MultilinearMap R (fun x => M₂) M₃<VAR>x : ι → M₂<GOAL>(fun x_1 => x i) = x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>x : P<VAR>x✝ : x ∈ 0<VAR>x' : R<VAR>x'_mem_zero : x' ∈ ↑0<VAR>x'_eq_x : (Algebra.linearMap R P) x' = x<VAR>x'_eq_zero : x' = 0<GOAL>x = 0
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>C : ℝ<VAR>hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C<VAR>θ : Fin n → ℝ<VAR>x✝ : θ ∈ Icc 0 fun x => 2 * π<GOAL>‖(∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ)‖ = (∏ i : Fin n, |R i|) * ‖f (torusMap c R θ)‖
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>C : ℝ<VAR>hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C<GOAL>(∏ i : Fin n, |R i|) * C * (volume (Icc 0 fun x => 2 * π)).toReal = ((2 * π) ^ n * ∏ i : Fin n, |R i|) * C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set β<GOAL>(e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr (e.source ∩ ↑e ⁻¹' s)).source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set β<GOAL>e.source ∩ ↑e ⁻¹' s = e.source ∩ (e.source ∩ ↑e ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<GOAL>Ici a \ Ioi a = {a}
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>μ ≪ μ[|univ]
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>μ ≪ (μ univ)⁻¹ • μ
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>(μ univ)⁻¹ ≠ 0
<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>A : E →L[𝕜] F<VAR>x : E<VAR>y : F<GOAL>⟪(adjointAux A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M✝ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁷ : Semiring R✝<VAR>inst✝⁶ : AddCommGroup M✝<VAR>inst✝⁵ : Module R✝ M✝<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : CharZero R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>v : M<GOAL>v = -v ↔ v = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f✝ : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>hg : OpenEmbedding g<GOAL>OpenEmbedding (g ∘ f) ↔ OpenEmbedding f
<VAR>𝕜✝ : Type u_1<VAR>𝕜' : Type u_2<VAR>E✝ : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>𝕜 : Type u_7<VAR>E : Type u_8<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>S : Set E<GOAL>IsVonNBounded 𝕜 S ↔ Tendsto (fun x => x • S) (𝓝 0) (𝓝 0).smallSets
<VAR>𝕜✝ : Type u_1<VAR>𝕜' : Type u_2<VAR>E✝ : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>𝕜 : Type u_7<VAR>E : Type u_8<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>S : Set E<GOAL>IsVonNBounded 𝕜 S ↔ ∀ t ∈ 𝓝 0, ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t
<VAR>𝕜✝ : Type u_1<VAR>𝕜' : Type u_2<VAR>E✝ : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>𝕜 : Type u_7<VAR>E : Type u_8<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>S V : Set E<VAR>hV : V ∈ 𝓝 0<GOAL>Absorbs 𝕜 V S ↔ ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ V
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Ring B<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>f✝ f : R →+* S<VAR>n : Type u_5<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n A<VAR>h : ∀ (i j : n), IsIntegral R (M i j)<GOAL>IsIntegral R M.det
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Ring B<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>f✝ f : R →+* S<VAR>n : Type u_5<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>M : Matrix n n A<VAR>h : ∀ (i j : n), IsIntegral R (M i j)<GOAL>IsIntegral R (∑ σ : Equiv.Perm n, Equiv.Perm.sign σ • ∏ i : n, M (σ i) i)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w u : W<VAR>i : B<GOAL>cs.IsReflection (w * (u * cs.simple i * u⁻¹) * w⁻¹)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w u : W<VAR>i : B<GOAL>w * (u * cs.simple i * u⁻¹) * w⁻¹ = w * u * cs.simple i * (w * u)⁻¹
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<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 F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hp : Fact (1 ≤ p)<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>‖lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<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 F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hp : Fact (1 ≤ p)<VAR>hm : m ≤ m0<VAR>f : ↥(lpMeasSubgroup F m p μ)<GOAL>‖↑f‖ = ‖f‖
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h : t.dual.Bounded o₂ o₁<GOAL>t.Bounded o₁ o₂
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>t : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>h : t.dual.Bounded o₂ o₁<VAR>this : t.dual.dual.Bounded o₁ o₂<GOAL>t.Bounded o₁ o₂
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<GOAL>finrank ℝ ({ w // w ≠ w₀ } → ℝ) = rank K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>f g : α →₀ ℕ<VAR>a✝ : α<GOAL>Multiset.count a✝ (toMultiset (f ⊓ g)) = Multiset.count a✝ (toMultiset f ∩ toMultiset g)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>M : Matrix n n R<VAR>e : m ≃ n<VAR>h : (M.submatrix ⇑e ⇑e).PosSemidef<GOAL>M.PosSemidef
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Integrable f (μ + ν)<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Memℒp f 1 (μ + ν)<GOAL>Memℒp f 1 μ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>(logEmbedding K) x = 0 ↔ x ∈ torsion K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>(logEmbedding K) x = 0 ↔ ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1
<VAR>b✝ x y a b c : ℝ<VAR>h₁ : b ≠ 0<VAR>h₂ : b ≠ 1<VAR>h₃ : b ≠ -1<GOAL>log b / log a * (log c / log b) = log c / log a
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f✝ : X → Y<VAR>s✝ t : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>f : X → Y<VAR>s : Set X<VAR>hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t<GOAL>dimH (f '' s) ≤ dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f✝ : X → Y<VAR>s✝ t : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>f : X → Y<VAR>s : Set X<VAR>hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t<VAR>this : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t<GOAL>dimH (f '' s) ≤ dimH s
<VAR>n m : ℕ<GOAL>n ≤ m + n.dist m
<VAR>n m : ℕ<GOAL>n ≤ m + m.dist n